-- Coefficient witnesses for adjoining a generator to a linear span (ZF).
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Algebra.SpanInsert
import LinearSpan

def scalarExtension (f A B plus times M x : Set) : Set :=
  {y ∈ B | ∃ a ∈ A, ∃ u ∈ M, y = plus(times(f(a), x), u)}

section Algebras
variable (A add zero neg mul one B plus z minus times unit f M x : Set)
notation ring R := (A, add, zero, neg, mul, one)
notation ring S := (B, plus, z, minus, times, unit)
hypothesis source : IsCommRing(R)
hypothesis target : IsCommRing(S)
hypothesis hom : IsRingHom(f, R, S)
hypothesis submodule : Submodule(f, R, S, M)
hypothesis element : x ∈ S

theorem scalarExtension.submodule
  shows Submodule(f, R, S, scalarExtension(f, A, B, plus, times, M, x))
proof
  have r := IsCommRing.ring with source
  have s := IsCommRing.ring with target
  have sourceZero := IsRing.zero_in_carrier with r
  have targetZero := IsRing.zero_in_carrier with s
  have zeroMem := Submodule.zero_mem with source, target, hom, submodule
  have boundedM := Submodule.subset with source, target, hom, submodule
  have negM := Submodule.neg_closed with source, target, hom, submodule
  have addM := Submodule.add_closed with source, target, hom, submodule
  have bounded : scalarExtension(f, A, B, plus, times, M, x) ⊆ S by simp [Subset, scalarExtension]
  have zeroMember : S[0] ∈ scalarExtension(f, A, B, plus, times, M, x)
    apply scalarExtension.membership.backward
    refine ⟨targetZero, zero, sourceZero, z, zeroMem, ?_⟩
    have mapped := IsRingHom.zero with hom
    rw mapped
    ring
  have negative : ClosedUnary(scalarExtension(f, A, B, plus, times, M, x), minus)
    intros y hy
    obtain ⟨member, a, ha, u, hu, equation⟩ := scalarExtension.membership.forward with hy
    have negativeY := IsRing.neg_closed with s, member
    have negativeA := IsRing.neg_closed with r, ha
    have negativeU := ClosedUnary.mem with negM, hu
    have inB : u ∈ S by exact boundedM with u, hu
    have image := IsRingHom.closed with hom, ha
    apply scalarExtension.membership.backward
    refine ⟨negativeY, R[-a], negativeA, S[-u], negativeU, ?_⟩
    have mapped := IsRingHom.neg with hom, ha
    rw [mapped, equation]
    ring
  have addition : ClosedBinary(scalarExtension(f, A, B, plus, times, M, x), plus)
    intros y hy w hw
    obtain ⟨memberY, a, ha, u, hu, equationY⟩ := scalarExtension.membership.forward with hy
    obtain ⟨memberW, b, hb, v, hv, equationW⟩ := scalarExtension.membership.forward with hw
    have sum := IsRing.add_closed with s, memberY, memberW
    have coefficient := IsRing.add_closed with r, ha, hb
    have remainder := ClosedBinary.mem with addM, hu, hv
    have inB : u ∈ S ∧ v ∈ S
      have first := boundedM with u, hu
      have second := boundedM with v, hv
      refine ⟨first, second⟩
    have memberU := inB.left
    have memberV := inB.right
    have imageA := IsRingHom.closed with hom, ha
    have imageB := IsRingHom.closed with hom, hb
    apply scalarExtension.membership.backward
    refine ⟨sum, R[a + b], coefficient, S[u + v], remainder, ?_⟩
    have mapped := IsRingHom.add with hom, ha, hb
    rw [mapped, equationY, equationW]
    ring
  have scalars : ∀ c ∈ R, ∀ y ∈ scalarExtension(f, A, B, plus, times, M, x), S[f(c) * y] ∈ scalarExtension(f, A, B, plus, times, M, x)
    intros c hc y hy
    obtain ⟨member, a, ha, u, hu, equation⟩ := scalarExtension.membership.forward with hy
    have imageC := IsRingHom.closed with hom, hc
    have imageA := IsRingHom.closed with hom, ha
    have product := IsRing.mul_closed with s, imageC, member
    have coefficient := IsRing.mul_closed with r, hc, ha
    have remainder := Submodule.scalar_mul_mem with source, target, hom, submodule, hc, hu
    have inB : u ∈ S by exact boundedM with u, hu
    apply scalarExtension.membership.backward
    refine ⟨product, R[c * a], coefficient, S[f(c) * u], remainder, ?_⟩
    have mapped := IsRingHom.mul with hom, hc, ha
    rw [mapped, equation]
    ring
  unfold Submodule
  refine ⟨bounded, zeroMember, negative, addition, scalars⟩

theorem scalarExtension.contains
  shows insert(x, M) ⊆ scalarExtension(f, A, B, plus, times, M, x)
proof
  have r := IsCommRing.ring with source
  have s := IsCommRing.ring with target
  have zeroIn := IsRing.zero_in_carrier with r
  have oneIn : R[1] ∈ R by typecheck
  have zeroMem := Submodule.zero_mem with source, target, hom, submodule
  have bound := Submodule.subset with source, target, hom, submodule
  intros y hy
  have alternatives := insert.membership.forward with hy
  cases alternatives with equal | old
  . rw equal
    apply scalarExtension.membership.backward
    refine ⟨element, one, oneIn, z, zeroMem, ?_⟩
    have mapped := IsRingHom.one with hom
    rw mapped
    ring
  . have member : y ∈ S
      exact bound with y, old
    apply scalarExtension.membership.backward
    refine ⟨member, zero, zeroIn, y, old, ?_⟩
    have mapped := IsRingHom.zero with hom
    rw mapped
    ring

end Algebras

section Spans
variable (A add zero neg mul one B plus z minus times unit f G x : Set)
notation ring R := (A, add, zero, neg, mul, one)
notation ring S := (B, plus, z, minus, times, unit)
hypothesis source : IsCommRing(R)
hypothesis target : IsCommRing(S)
hypothesis hom : IsRingHom(f, R, S)
hypothesis bounded : G ⊆ S
hypothesis element : x ∈ S

theorem linearSpan.insert
  shows linearSpan(f, R, S, insert(x, G)) = scalarExtension(f, A, B, plus, times, linearSpan(f, R, S, G), x)
proof
  have span := linearSpan.submodule at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, G with *
  have extension := scalarExtension.submodule with source, target, hom, span, element
  have contains := scalarExtension.contains with source, target, hom, span, element
  have oldContains := linearSpan.contains with source, target, hom, bounded
  have generators : insert(x, G) ⊆ scalarExtension(f, A, B, plus, times, linearSpan(f, R, S, G), x)
    simp
  have first := linearSpan.least with source, target, hom, extension, generators
  have enlarged := linearSpan.submodule at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, insert(x, G) with *
  have bound : insert(x, G) ⊆ S by simp [Subset, insert.membership]
  have included := linearSpan.contains with source, target, hom, bound
  have xIn : x ∈ linearSpan(f, R, S, insert(x, G)) by settle with Subset, insert.membership
  have old : G ⊆ insert(x, G) by simp [Subset, insert.membership]
  have oldSpan := linearSpan.mono with source, target, hom, bound, old
  have addClosed := Submodule.add_closed with source, target, hom, enlarged
  have second : scalarExtension(f, A, B, plus, times, linearSpan(f, R, S, G), x) ⊆ linearSpan(f, R, S, insert(x, G))
    intros y hy
    obtain ⟨member, a, ha, u, hu, equation⟩ := scalarExtension.membership.forward with hy
    have scalar := Submodule.scalar_mul_mem with source, target, hom, enlarged, ha, xIn
    have rest : u ∈ linearSpan(f, R, S, insert(x, G)) by exact oldSpan with u, hu
    rw equation
    exact ClosedBinary.mem with addClosed, scalar, rest
  exact Subset.antisymmetric with first, second

theorem linearSpan.insert_membership (y : Set)
  shows y ∈ linearSpan(f, R, S, insert(x, G)) ↔
    y ∈ S ∧ (∃ a ∈ R, ∃ u ∈ linearSpan(f, R, S, G), y = S[f(a) * x + u])
proof
  have equation := linearSpan.insert with source, target, hom, bounded, element
  rw equation
  exact scalarExtension.membership

end Spans
section EmptySpan
variable (A add zero neg mul one B plus z minus times unit f : Set)
notation ring R := (A, add, zero, neg, mul, one)
notation ring S := (B, plus, z, minus, times, unit)
hypothesis source : IsCommRing(R)
hypothesis target : IsCommRing(S)
hypothesis hom : IsRingHom(f, R, S)

theorem Submodule.zero
  shows Submodule(f, R, S, {S[0]})
proof
  have ordinary := IsCommRing.ring with target
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have bounded : {S[0]} ⊆ S by simp [Subset, singleton.membership]
  have zeroMember : S[0] ∈ {S[0]} by simp [singleton.membership]
  have negative : ClosedUnary({S[0]}, minus)
    intros u hu
    have equal := singleton.membership.forward with hu
    rw equal
    have value : S[-0] = S[0] by ring
    rwa value
  have addition : ClosedBinary({S[0]}, plus)
    intros u hu v hv
    have first := singleton.membership.forward with hu
    have second := singleton.membership.forward with hv
    rw [first, second]
    have value : S[0 + 0] = S[0] by ring
    rwa value
  have scalars : ∀ a ∈ R, ∀ u ∈ {S[0]}, S[f(a) * u] ∈ {S[0]}
    intros a ha u hu
    have image := IsRingHom.closed with hom, ha
    have equal := singleton.membership.forward with hu
    rw equal
    have value : S[f(a) * 0] = S[0] by ring
    rwa value
  unfold Submodule
  refine ⟨bounded, zeroMember, negative, addition, scalars⟩

theorem linearSpan.empty
  shows linearSpan(f, R, S, ∅) = {S[0]}
proof
  have zeroModule := Submodule.zero with *
  have empty := empty.subset at {S[0]}
  have first := linearSpan.least with source, target, hom, zeroModule, empty
  have span := linearSpan.submodule at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, ∅ with *
  have zeroMember := Submodule.zero_mem with source, target, hom, span
  have second : {S[0]} ⊆ linearSpan(f, R, S, ∅)
    intros y hy
    have equal := singleton.membership.forward with hy
    rwa equal
  exact Subset.antisymmetric with first, second

end EmptySpan