-- Finite modules compose in a tower of commutative algebras (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.FiniteModuleTower
import LinearSpanMap

section Algebras
variable (A add zero neg mul one B plus z minus times unit C sum o inverse product e f g : Set)
notation ring R := (A, add, zero, neg, mul, one)
notation ring S := (B, plus, z, minus, times, unit)
notation ring U := (C, sum, o, inverse, product, e)
hypothesis coefficients : IsCommRing(R)
hypothesis source : IsCommRing(S)
hypothesis target : IsCommRing(U)
hypothesis coefficientMap : IsRingHom(f, R, S)
hypothesis hom : IsRingHom(g, S, U)

theorem linearSpan.tower_generators (G H : Set)
  requires boundedG : G ⊆ S
  requires boundedH : H ⊆ U
  requires spansG : linearSpan(f, R, S, G) = S
  requires spansH : linearSpan(g, S, U, H) = U
  shows linearSpan(compose(g, f, A, B, C), R, U, spanProducts(U, functionImage(g, G, C), H)) = U
proof
  have composite := IsRingHom.compose with coefficients, coefficientMap, hom
  have ordinaryS := IsCommRing.ring with source
  have ordinaryU := IsCommRing.ring with target
  have multiplicative := IsRing.multiplicative with ordinaryS
  have oneIn := IsMonoid.unit_in_carrier with multiplicative
  have oneValue := IsRingHom.one with hom
  have imageBound : functionImage(g, G, C) ⊆ U by exact functionImage.subset at g, G, C
  have productsBound := spanProducts.subset at C, product, functionImage(g, G, C), H
  have span := linearSpan.submodule at A, add, zero, neg, mul, one, C, sum, o, inverse, product, e, compose(g, f, A, B, C), spanProducts(U, functionImage(g, G, C), H) with *
  have spanBound := Submodule.subset with coefficients, target, composite, span
  have spanZero := Submodule.zero_mem with coefficients, target, composite, span
  have spanNeg := Submodule.neg_closed with coefficients, target, composite, span
  have spanAdd := Submodule.add_closed with coefficients, target, composite, span
  have containsH := linearSpan.contains at A, add, zero, neg, mul, one, C, sum, o, inverse, product, e, compose(g, f, A, B, C), H with *
  have mappedSpan : ∀ b ∈ S, g(b) ∈ linearSpan(compose(g, f, A, B, C), R, U, functionImage(g, G, C))
    intros b hb
    have member : b ∈ linearSpan(f, R, S, G) by rwa spansG
    exact linearSpan.map_mem with coefficients, source, target, coefficientMap, hom, boundedG, member
  have scalars : ∀ b ∈ S, ∀ x ∈ linearSpan(compose(g, f, A, B, C), R, U, spanProducts(U, functionImage(g, G, C), H)), U[g(b) * x] ∈ linearSpan(compose(g, f, A, B, C), R, U, spanProducts(U, functionImage(g, G, C), H))
    intros b hb x hx
    have imageB := IsRingHom.closed with hom, hb
    have generators : ∀ p ∈ spanProducts(U, functionImage(g, G, C), H), U[p * g(b)] ∈ linearSpan(compose(g, f, A, B, C), R, U, spanProducts(U, functionImage(g, G, C), H))
      intros p hp
      obtain ⟨inP, a, ha, v, hv, valueP⟩ := spanProducts.membership.forward with hp
      obtain ⟨inA, u, hu, valueA⟩ := functionImage.membership.forward with ha
      have inU : u ∈ S by simp [Subset]
      have inV : v ∈ U by simp [Subset]
      have inSpanV : v ∈ linearSpan(compose(g, f, A, B, C), R, U, H) by simp [Subset]
      have imageU := IsRingHom.closed with hom, inU
      have closed := IsRing.mul_closed with ordinaryS, hb, inU
      have first := mappedSpan with S[b * u], closed
      have member := linearSpan.product_mem with coefficients, target, composite, imageBound, boundedH, first, inSpanV
      have mapped := IsRingHom.mul with hom, hb, inU
      rw mapped at member
      have equation : U[(g(u) * v) * g(b)] = U[(g(b) * g(u)) * v] by ring
      rwa [valueP, valueA, equation]
    have multiplied := linearSpan.mul_mem with coefficients, target, composite, span, productsBound, generators, hx
    have inX : x ∈ U by simp [Subset]
    have commute : U[g(b) * x] = U[x * g(b)] by ring
    rwa commute
  have overS : Submodule(g, S, U, linearSpan(compose(g, f, A, B, C), R, U, spanProducts(U, functionImage(g, G, C), H)))
    unfold Submodule
    refine ⟨spanBound, spanZero, spanNeg, spanAdd, scalars⟩
  have generators : H ⊆ linearSpan(compose(g, f, A, B, C), R, U, spanProducts(U, functionImage(g, G, C), H))
    intros v hv
    have inV : v ∈ U by simp [Subset]
    have inSpanV : v ∈ linearSpan(compose(g, f, A, B, C), R, U, H) by simp [Subset]
    have first := mappedSpan with unit, oneIn
    have member := linearSpan.product_mem with coefficients, target, composite, imageBound, boundedH, first, inSpanV
    rw oneValue at member
    have equation : U[1 * v] = v by ring
    rwa equation at member
  have whole := linearSpan.least with source, target, hom, overS, generators
  rw spansH at whole
  exact Subset.antisymmetric with spanBound, whole

theorem FiniteAlgebraModule.tower
  requires finiteS : FiniteAlgebraModule(f, R, S)
  requires finiteU : FiniteAlgebraModule(g, S, U)
  shows FiniteAlgebraModule(compose(g, f, A, B, C), R, U)
proof
  obtain ⟨G, finiteG, boundedG, spansG⟩ := finiteS
  obtain ⟨H, finiteH, boundedH, spansH⟩ := finiteU
  have composite := IsRingHom.compose with coefficients, coefficientMap, hom
  have function := IsRingHom.function with hom
  have finiteImage := Finite.function_image with function, finiteG, boundedG
  have imageBound : functionImage(g, G, C) ⊆ U by exact functionImage.subset at g, G, C
  have finite := spanProducts.finite with coefficients, target, composite, finiteImage, finiteH, imageBound, boundedH
  have bounded := spanProducts.subset at C, product, functionImage(g, G, C), H
  have spans := linearSpan.tower_generators with coefficients, source, target, coefficientMap, hom, boundedG, boundedH, spansG, spansH
  unfold FiniteAlgebraModule
  refine ⟨spanProducts(U, functionImage(g, G, C), H), finite, bounded, spans⟩

end Algebras