-- Quotient factorization and the surjective first isomorphism theorem in 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.Ring.FirstIsomorphism
import Homomorphism

theorem idealQuotient.projection_hom (A add zero neg mul one I : Set)
  requires source : IsCommRing(A, add, zero, neg, mul, one)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  shows IsRingHom(quotientProjection(A, idealRelation(A, add, neg, I)), A, add, zero, neg, mul, one, (A ⧸ idealRelation(A, add, neg, I)),
    quotientBinary(A, idealRelation(A, add, neg, I), add), ⟦zero⟧[A, idealRelation(A, add, neg, I)],
    quotientUnary(A, idealRelation(A, add, neg, I), neg), quotientBinary(A, idealRelation(A, add, neg, I), mul), ⟦one⟧[A, idealRelation(A, add, neg, I)])
proof
  have equivalence := idealRelation.equivalence with *
  have function := quotientProjection.function at A, idealRelation(A, add, neg, I) with *
  have ring := IsCommRing.ring with *
  have addClosed : IsMagma(A, add) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]
  have mulClosed : IsMagma(A, mul) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]
  have negClosed : neg : A → A by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, Inverse]
  have zeroIn := IsRing.zero_in_carrier with *
  have oneIn : one ∈ A by simp [IsCommRing, IsRing, IsMonoid, Identity]
  have addCompatible := idealRelation.add_compatible with *
  have mulCompatible := idealRelation.mul_compatible with *
  have negCompatible := idealRelation.neg_compatible with *
  have zeroValue := quotientProjection.value at A, idealRelation(A, add, neg, I), zero with *
  have oneValue := quotientProjection.value at A, idealRelation(A, add, neg, I), one with *
  unfold IsRingHom
  refine ⟨function, ⟨zeroValue, ⟨oneValue, ⟨?_, ⟨?_, ?_⟩⟩⟩⟩⟩
  . intros x hx
    have closed := IsRing.neg_closed with hx
    have vx := quotientProjection.value at A, idealRelation(A, add, neg, I), x with *
    have output := quotientProjection.value at A, idealRelation(A, add, neg, I), neg(x) with *
    have lifted := quotientUnary.classes with hx
    cc
  . intros x hx y hy
    have closed := IsRing.add_closed with hx, hy
    have vx := quotientProjection.value at A, idealRelation(A, add, neg, I), x with *
    have vy := quotientProjection.value at A, idealRelation(A, add, neg, I), y with *
    have output := quotientProjection.value at A, idealRelation(A, add, neg, I), call2(add, x, y) with *
    have lifted := quotientBinary.classes at A, idealRelation(A, add, neg, I), add, x, y with *
    cc
  . intros x hx y hy
    have closed := IsRing.mul_closed with hx, hy
    have vx := quotientProjection.value at A, idealRelation(A, add, neg, I), x with *
    have vy := quotientProjection.value at A, idealRelation(A, add, neg, I), y with *
    have output := quotientProjection.value at A, idealRelation(A, add, neg, I), call2(mul, x, y) with *
    have lifted := quotientBinary.classes at A, idealRelation(A, add, neg, I), mul, x, y with *
    cc

theorem IsRingHom.quotient (f A add zero neg mul one B plus z minus times unit I : Set)
  requires source : IsCommRing(A, add, zero, neg, mul, one)
  requires target : IsCommRing(B, plus, z, minus, times, unit)
  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  requires killed : I ⊆ ringKernel(f, A, z)
  shows IsRingHom(quotientMap(f, A, B, idealRelation(A, add, neg, I)), (A ⧸ idealRelation(A, add, neg, I)),
    quotientBinary(A, idealRelation(A, add, neg, I), add), ⟦zero⟧[A, idealRelation(A, add, neg, I)],
    quotientUnary(A, idealRelation(A, add, neg, I), neg), quotientBinary(A, idealRelation(A, add, neg, I), mul), ⟦one⟧[A, idealRelation(A, add, neg, I)], B, plus, z, minus, times, unit)
proof
  have function := IsRingHom.function with hom
  have equivalence := idealRelation.equivalence with *
  have respects := IsRingHom.respects_ideal with *
  have mapped := quotientMap.function at f, A, B, idealRelation(A, add, neg, I) with *
  have addClosed : IsMagma(A, add) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]
  have mulClosed : IsMagma(A, mul) by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, IsSemigroup]
  have negClosed : neg : A → A by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, Inverse]
  have zeroIn : zero ∈ A by simp [IsCommRing, IsRing, IsAbelianGroup, IsGroup, IsMonoid, Identity]
  have oneIn : one ∈ A by simp [IsCommRing, IsRing, IsMonoid, Identity]
  have addCompatible := idealRelation.add_compatible with *
  have mulCompatible := idealRelation.mul_compatible with *
  have negCompatible := idealRelation.neg_compatible with *
  have zeroClass := quotientMap.class at f, A, B, idealRelation(A, add, neg, I), zero with *
  have oneClass := quotientMap.class at f, A, B, idealRelation(A, add, neg, I), one with *
  have zeroValue := IsRingHom.zero with hom
  have oneValue := IsRingHom.one with hom
  unfold IsRingHom
  refine ⟨mapped, ⟨?_, ⟨?_, ⟨?_, ⟨?_, ?_⟩⟩⟩⟩⟩
  . cc
  . cc
  . intros X hX
    exact quotientMap.unary with function, equivalence, respects, negClosed, negCompatible, hom.right.right.right.left, hX
  . intros X hX Y hY
    exact quotientMap.binary with function, equivalence, respects, addClosed, addCompatible, hom.right.right.right.right.left, hX, hY
  . intros X hX Y hY
    exact quotientMap.binary with function, equivalence, respects, mulClosed, mulCompatible, hom.right.right.right.right.right, hX, hY

theorem IsRingHom.factorization (f A add zero neg mul one B plus z minus times unit I : Set)
  requires source : IsCommRing(A, add, zero, neg, mul, one)
  requires target : IsCommRing(B, plus, z, minus, times, unit)
  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  requires killed : I ⊆ ringKernel(f, A, z)
  shows compose(quotientMap(f, A, B, idealRelation(A, add, neg, I)), quotientProjection(A, idealRelation(A, add, neg, I)), A, (A ⧸ idealRelation(A, add, neg, I)), B) = f
proof
  have function := IsRingHom.function with hom
  have equivalence := idealRelation.equivalence with *
  have respects := IsRingHom.respects_ideal with *
  exact quotientMap.factorization with *

theorem IsRingHom.factor_unique (f A add zero neg mul one B plus z minus times unit I g : Set)
  requires source : IsCommRing(A, add, zero, neg, mul, one)
  requires target : IsCommRing(B, plus, z, minus, times, unit)
  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  requires killed : I ⊆ ringKernel(f, A, z)
  requires candidate : g : (A ⧸ idealRelation(A, add, neg, I)) → B
  requires factors : ∀ x ∈ A, g(⟦x⟧[A, idealRelation(A, add, neg, I)]) = f(x)
  shows g = quotientMap(f, A, B, idealRelation(A, add, neg, I))
proof
  have function := IsRingHom.function with hom
  have equivalence := idealRelation.equivalence with *
  have respects := IsRingHom.respects_ideal with *
  exact quotientMap.unique with *

-- For a surjective unital homomorphism, R/ker(f) is isomorphic to the target.
-- The quotient ring structure is supplied separately by idealQuotient.comm_ring.
theorem idealQuotient.first_isomorphism (f A add zero neg mul one B plus z minus times unit : Set)
  requires source : IsCommRing(A, add, zero, neg, mul, one)
  requires target : IsCommRing(B, plus, z, minus, times, unit)
  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)
  requires onto : SurjectiveBetween(f, A, B)
  shows IsRingIso(quotientMap(f, A, B, idealRelation(A, add, neg, ringKernel(f, A, z))), (A ⧸ idealRelation(A, add, neg, ringKernel(f, A, z))),
    quotientBinary(A, idealRelation(A, add, neg, ringKernel(f, A, z)), add), ⟦zero⟧[A, idealRelation(A, add, neg, ringKernel(f, A, z))],
    quotientUnary(A, idealRelation(A, add, neg, ringKernel(f, A, z)), neg), quotientBinary(A, idealRelation(A, add, neg, ringKernel(f, A, z)), mul), ⟦one⟧[A, idealRelation(A, add, neg, ringKernel(f, A, z))], B, plus, z, minus, times, unit)
proof
  have ideal := IsRingHom.kernel_ideal with *
  have killed : ringKernel(f, A, z) ⊆ ringKernel(f, A, z) by simp [Subset]
  have quotientHom := IsRingHom.quotient with *
  have function := IsRingHom.function at f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit with *
  have equivalence := idealRelation.equivalence with *
  have respects := IsRingHom.respects_ideal with *
  have reflects : ∀ x ∈ A, ∀ y ∈ A, f(x) = f(y) → relates(idealRelation(A, add, neg, ringKernel(f, A, z)), x, y)
    intros x hx y hy equal
    have congruent := IsRingHom.kernel_congruent.backward with *
    exact idealRelation.relates.backward with *
  have injective := quotientMap.injective with *
  have surjective := quotientMap.surjective with *
  unfold IsRingIso
  refine ⟨quotientHom, ?_⟩
  unfold BijectiveBetween
  refine ⟨injective, surjective⟩

-- The same results for bundled rings: the projection onto a quotient ring,
-- descent of a homomorphism to a quotient by an ideal inside its kernel,
-- and the first isomorphism theorem.
section BundledQuotients
variable (R I : Set)
hypothesis comm : CommRing(R)
hypothesis ideal : Ideal(R, I)

theorem quotientRing.projection_hom
  shows quotientProjection(R.carrier, quotientRelation(R, I)) : R →+* R ⧸ I
proof
  have parts := CommRing.parts with comm
  have idealParts := Ideal.parts with ideal
  have engine := idealQuotient.projection_hom with parts, idealParts
  have target := quotientRing.comm_ring with comm, ideal
  have shifted : IsRingHom(quotientProjection(R.carrier, quotientRelation(R, I)),
      R.carrier, R.add, R.zero, R.neg, R.mul, R.one,
      Ring.carrier(R ⧸ I), Ring.add(R ⧸ I),
      Ring.zero(R ⧸ I), Ring.neg(R ⧸ I),
      Ring.mul(R ⧸ I), Ring.one(R ⧸ I))
    rw [quotientRing.carrierOf, quotientRing.addOf, quotientRing.zeroOf,
      quotientRing.negOf, quotientRing.mulOf, quotientRing.oneOf,
      quotientRelation.value]
    exact engine
  exact RingHom.of_projections with (CommRing.to_ring with comm),
    (CommRing.to_ring with target), shifted

theorem quotientRing.projection_surjective
  shows SurjectiveBetween(quotientProjection(R.carrier, quotientRelation(R, I)),
    R.carrier, Ring.carrier(R ⧸ I))
proof
  have equivalence := quotientRelation.equivalence with comm, ideal
  rw quotientRing.carrierOf
  exact quotientProjection.surjective with equivalence

end BundledQuotients

-- The map a homomorphism induces on the quotient by its kernel is written
-- inducedMap(f) under f : R →+* S: the descent of f along the projection,
-- quotientMap(f, R.carrier, S.carrier, quotientRelation(R, ker(f))).
notation function "inducedMap(f)" => quotientMap(f, R.carrier, S.carrier, quotientRelation(R, ker(f))) via hypothesis RingHom(f, R, S)

section Descent
variable (f R S : Set)
hypothesis source : CommRing(R)
hypothesis target : CommRing(S)
hypothesis hom : f : R →+* S

theorem RingHom.quotient_hom (I : Set)
  requires ideal : Ideal(R, I)
  requires killed : I ⊆ ker(f)
  shows quotientMap(f, R.carrier, S.carrier, quotientRelation(R, I)) :
    R ⧸ I →+* S
proof
  have sourceParts := CommRing.parts with source
  have targetParts := CommRing.parts with target
  have parts := RingHom.parts with hom
  have idealParts := Ideal.parts with ideal
  have engine := IsRingHom.quotient with sourceParts, targetParts, parts,
    idealParts, killed
  have quotientComm := quotientRing.comm_ring with source, ideal
  have shifted : IsRingHom(quotientMap(f, R.carrier, S.carrier, quotientRelation(R, I)),
      Ring.carrier(R ⧸ I), Ring.add(R ⧸ I),
      Ring.zero(R ⧸ I), Ring.neg(R ⧸ I),
      Ring.mul(R ⧸ I), Ring.one(R ⧸ I),
      S.carrier, S.add, S.zero, S.neg, S.mul, S.one)
    rw [quotientRing.carrierOf, quotientRing.addOf, quotientRing.zeroOf,
      quotientRing.negOf, quotientRing.mulOf, quotientRing.oneOf,
      quotientRelation.value]
    exact engine
  exact RingHom.of_projections with (CommRing.to_ring with quotientComm),
    (CommRing.to_ring with target), shifted

theorem RingHom.quotient_factorization (I : Set)
  requires ideal : Ideal(R, I)
  requires killed : I ⊆ ker(f)
  shows compose(quotientMap(f, R.carrier, S.carrier, quotientRelation(R, I)),
    quotientProjection(R.carrier, quotientRelation(R, I)), R.carrier,
    (R.carrier ⧸ quotientRelation(R, I)), S.carrier) = f
proof
  have sourceParts := CommRing.parts with source
  have targetParts := CommRing.parts with target
  have parts := RingHom.parts with hom
  have idealParts := Ideal.parts with ideal
  have engine := IsRingHom.factorization with sourceParts, targetParts, parts,
    idealParts, killed
  rw quotientRelation.value
  exact engine

theorem RingHom.quotient_unique (I g : Set)
  requires ideal : Ideal(R, I)
  requires killed : I ⊆ ker(f)
  requires candidate : g : (R.carrier ⧸ quotientRelation(R, I)) → S.carrier
  requires factors : ∀ x ∈ R, g(⟦x⟧[R.carrier, quotientRelation(R, I)]) = f(x)
  shows g = quotientMap(f, R.carrier, S.carrier, quotientRelation(R, I))
proof
  have sourceParts := CommRing.parts with source
  have targetParts := CommRing.parts with target
  have parts := RingHom.parts with hom
  have idealParts := Ideal.parts with ideal
  rw quotientRelation.value at candidate
  rw under quotientRelation.value at factors
  rw quotientRelation.value
  exact IsRingHom.factor_unique with sourceParts, targetParts, parts,
    idealParts, killed, candidate, factors

-- The first isomorphism theorem: a surjective homomorphism identifies the
-- quotient by its kernel with the target.
theorem RingHom.first_isomorphism
  requires onto : SurjectiveBetween(f, R.carrier, S.carrier)
  shows inducedMap(f) : R ⧸ ker(f) ≃+* S
proof
  have sourceParts := CommRing.parts with source
  have targetParts := CommRing.parts with target
  have parts := RingHom.parts with hom
  have engine := idealQuotient.first_isomorphism with sourceParts, targetParts,
    parts, onto
  have kernelIdeal := ringKernel.ideal with source, target, hom
  have quotientComm := quotientRing.comm_ring with source, kernelIdeal
  have shifted : IsRingIso(inducedMap(f),
      Ring.carrier(R ⧸ ker(f)), Ring.add(R ⧸ ker(f)),
      Ring.zero(R ⧸ ker(f)), Ring.neg(R ⧸ ker(f)),
      Ring.mul(R ⧸ ker(f)), Ring.one(R ⧸ ker(f)),
      S.carrier, S.add, S.zero, S.neg, S.mul, S.one)
    rw [quotientRing.carrierOf, quotientRing.addOf, quotientRing.zeroOf,
      quotientRing.negOf, quotientRing.mulOf, quotientRing.oneOf,
      quotientRelation.value]
    exact engine
  exact RingIso.of_projections with (CommRing.to_ring with quotientComm),
    (CommRing.to_ring with target), shifted

end Descent