-- Surjective images preserve finite generation of 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.Image
import Adjoin
import Cardinal.FiniteImage

def subringComap (g B T : Set) : Set := {x ∈ B | g(x) ∈ T}

section Maps
variable (B plus z minus times unit C sum o inverse product e g : Set)
notation ring S := (B, plus, z, minus, times, unit)
notation ring U := (C, sum, o, inverse, product, e)
hypothesis source : IsCommRing(S)
hypothesis target : IsCommRing(U)
hypothesis hom : IsRingHom(g, S, U)

theorem subringComap.subring (T : Set)
  requires subring : IsSubring(U, T)
  shows IsSubring(S, subringComap(g, B, T))
proof
  have ordinary := IsCommRing.ring with source
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have multiplicative := IsRing.multiplicative with ordinary
  have oneIn := IsMonoid.unit_in_carrier with multiplicative
  have zeroMem := IsSubring.zero_closed with subring
  have oneMem := IsSubring.one_closed with subring
  have negClosed := IsSubring.neg_closed with subring
  have addClosed := IsSubring.add_closed with subring
  have mulClosed := IsSubring.mul_closed with subring
  have zeroValue := IsRingHom.zero with hom
  have oneValue := IsRingHom.one with hom
  have subset : subringComap(g, B, T) ⊆ B
    intros x hx
    have data := subringComap.membership.forward with hx
    exact data.left
  unfold IsSubring
  refine ⟨subset, ⟨?_, ⟨?_, ⟨?_, ⟨?_, ?_⟩⟩⟩⟩⟩
  . apply subringComap.membership.backward at g, B, T, z
    rw zeroValue
    refine ⟨zeroIn, zeroMem⟩
  . apply subringComap.membership.backward at g, B, T, unit
    rw oneValue
    refine ⟨oneIn, oneMem⟩
    intros x hx
    obtain ⟨member, value⟩ := subringComap.membership.forward with hx
    have closed := IsRing.neg_closed with ordinary, member
    have mapped := IsRingHom.neg with hom, member
    have output := ClosedUnary.mem with negClosed, value
    apply subringComap.membership.backward
    rw mapped
    refine ⟨closed, output⟩
    intros x hx y hy
    obtain ⟨memberX, valueX⟩ := subringComap.membership.forward with hx
    obtain ⟨memberY, valueY⟩ := subringComap.membership.forward with hy
    have closed := IsRing.add_closed with ordinary, memberX, memberY
    have mapped := IsRingHom.add with hom, memberX, memberY
    have output := ClosedBinary.mem with addClosed, valueX, valueY
    apply subringComap.membership.backward
    rw mapped
    refine ⟨closed, output⟩
    intros x hx y hy
    obtain ⟨memberX, valueX⟩ := subringComap.membership.forward with hx
    obtain ⟨memberY, valueY⟩ := subringComap.membership.forward with hy
    have closed := IsRing.mul_closed with ordinary, memberX, memberY
    have mapped := IsRingHom.mul with hom, memberX, memberY
    have output := ClosedBinary.mem with mulClosed, valueX, valueY
    apply subringComap.membership.backward
    rw mapped
    refine ⟨closed, output⟩

end Maps

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 Subalgebra.comap (T : Set)
  requires subalgebra : Subalgebra(compose(g, f, A, B, C), R, U, T)
  shows Subalgebra(f, R, S, subringComap(g, B, T))
proof
  have functionF := IsRingHom.function with coefficientMap
  have functionG := IsRingHom.function with hom
  have composite := compose.function at g, f, A, B, C with *
  have structure := subalgebra
  have subring := subringComap.subring with source, target, hom, structure.left
  have included := structure.right
  have image : functionImage(f, A, B) ⊆ subringComap(g, B, T)
    intros b hb
    obtain ⟨memberB, a, ha, value⟩ := functionImage.membership.forward with hb
    have compositeValue := compose.apply at g, f, A, B, C, a with *
    have imageValue := functionImage.value at compose(g, f, A, B, C), A, C, a with *
    have member := included with compose(g, f, A, B, C)(a), imageValue
    apply subringComap.membership.backward
    constructor
    . exact memberB
    . rw [value, ← compositeValue]
      exact member
  unfold Subalgebra
  refine ⟨subring, image⟩

theorem algebraAdjoin.map_into (G : Set)
  requires bounded : G ⊆ S
  shows algebraAdjoin(f, R, S, G) ⊆ subringComap(g, B, algebraAdjoin(compose(g, f, A, B, C), R, U, functionImage(g, G, C)))
proof
  have composite := IsRingHom.compose with coefficients, coefficientMap, hom
  have function := IsRingHom.function with hom
  have imageBound := functionImage.subset at g, G, C
  have generated := algebraAdjoin.subalgebra with coefficients, target, composite, imageBound
  have contains := algebraAdjoin.contains with coefficients, target, composite, imageBound
  have preimage := Subalgebra.comap with coefficients, source, target, coefficientMap, hom, generated
  have generators : G ⊆ subringComap(g, B, algebraAdjoin(compose(g, f, A, B, C), R, U, functionImage(g, G, C)))
    intros x hx
    have member := bounded with x, hx
    have value := FunctionBetween.apply_closed with function, member
    have image : g(x) ∈ functionImage(g, G, C)
      apply functionImage.membership.backward
      refine ⟨value, x, hx, ?_⟩
      rfl
    have generatedValue := contains with g(x), image
    exact subringComap.membership.backward with ⟨member, generatedValue⟩
  exact algebraAdjoin.least with coefficients, source, coefficientMap, preimage, generators

theorem algebraAdjoin.surjective_image (G : Set)
  requires onto : SurjectiveBetween(g, B, C)
  requires bounded : G ⊆ S
  requires generates : algebraAdjoin(f, R, S, G) = S
  shows algebraAdjoin(compose(g, f, A, B, C), R, U, functionImage(g, G, C)) = U
proof
  have composite := IsRingHom.compose with coefficients, coefficientMap, hom
  have subset := algebraAdjoin.subset at A, add, zero, neg, mul, one, C, sum, o, inverse, product, e, compose(g, f, A, B, C), functionImage(g, G, C) with *
  have mapped := algebraAdjoin.map_into with coefficients, source, target, coefficientMap, hom, bounded
  rw generates at mapped
  have surjection := onto
  apply Subset.antisymmetric with subset
  intros y hy
  obtain ⟨x, hx, edge⟩ := surjection.right with y, hy
  have value := FunctionBetween.apply_value with surjection.left, hx, edge
  have member := mapped with x, hx
  have data := subringComap.membership.forward with member
  rw value at data
  exact data.right

theorem FinitelyGeneratedAlgebra.surjective_image
  requires finiteGeneration : FinitelyGeneratedAlgebra(f, R, S)
  requires onto : SurjectiveBetween(g, B, C)
  shows FinitelyGeneratedAlgebra(compose(g, f, A, B, C), R, U)
proof
  obtain ⟨G, finite, bounded, generates⟩ := finiteGeneration
  have function := IsRingHom.function with hom
  have imageFinite := Finite.function_image with function, finite, bounded
  have imageBound := functionImage.subset at g, G, C
  have imageGenerates := algebraAdjoin.surjective_image with coefficients, source, target, coefficientMap, hom, onto, bounded, generates
  unfold FinitelyGeneratedAlgebra
  refine ⟨functionImage(g, G, C), imageFinite, imageBound, imageGenerates⟩

end Algebras
section Quotients
variable (A add zero neg mul one B plus z minus times unit f J : Set)
notation ring R := (A, add, zero, neg, mul, one)
notation ring S := (B, plus, z, minus, times, unit)
notation ring Q := S ⧸ J
hypothesis coefficients : IsCommRing(R)
hypothesis source : IsCommRing(S)
hypothesis hom : IsRingHom(f, R, S)
hypothesis ideal : IsIdeal(S, J)

theorem FinitelyGeneratedAlgebra.quotient
  requires finiteGeneration : FinitelyGeneratedAlgebra(f, R, S)
  shows FinitelyGeneratedAlgebra(compose(quotientProjection(B, idealRelation(B, plus, minus, J)), f, A, B, Q), R, Q)
proof
  have target := idealQuotient.comm_ring with *
  have projection := idealQuotient.projection_hom with *
  have equivalence := idealRelation.equivalence with *
  have onto := quotientProjection.surjective with *
  exact FinitelyGeneratedAlgebra.surjective_image with coefficients, source, target, hom, projection, finiteGeneration, onto

end Quotients