-- Recovering a common zero from an isomorphism of the coefficient and residue fields.
-- 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.Polynomial.Residue
import Universal
import FiniteGeneration
import Field.Embedding

def polynomialResidueCoefficients (I A add zero neg mul one J : Set) : Set :=
  compose(quotientProjection(polynomials(I, A, zero), idealRelation(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), polynomialNeg(I, A, add, zero, neg, mul, one), J)), polynomialCoefficients(I, A, zero), A, polynomials(I, A, zero), (polynomials(I, A, zero) ⧸ idealRelation(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), polynomialNeg(I, A, add, zero, neg, mul, one), J)))

notation scoped polynomialResidueCoefficients(I, R, J) => polynomialResidueCoefficients(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, J)

def polynomialResidueRetraction (I A add zero neg mul one J : Set) : Set :=
  compose(converse(polynomialResidueCoefficients(I, A, add, zero, neg, mul, one, J), A, (polynomials(I, A, zero) ⧸ idealRelation(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), polynomialNeg(I, A, add, zero, neg, mul, one), J))), quotientProjection(polynomials(I, A, zero), idealRelation(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), polynomialNeg(I, A, add, zero, neg, mul, one), J)), polynomials(I, A, zero), (polynomials(I, A, zero) ⧸ idealRelation(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), polynomialNeg(I, A, add, zero, neg, mul, one), J)), A)

notation scoped polynomialResidueRetraction(I, R, J) => polynomialResidueRetraction(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, J)

section Residues
variable (I A add zero neg mul one J : Set)
notation ring R := (A, add, zero, neg, mul, one)
notation ring P := R[I]
notation ring Q := P ⧸ J
hypothesis ring : IsCommRing(R)
hypothesis ideal : IsIdeal(P, J)

theorem polynomialResidueCoefficients.hom
  shows IsRingHom(polynomialResidueCoefficients(I, R, J), R, Q)
proof
  have polynomialRing := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *
  have coefficients := polynomialCoefficients.hom at I, A, add, zero, neg, mul, one with *
  have projection := idealQuotient.projection_hom with polynomialRing, ideal
  unfold polynomialResidueCoefficients
  exact IsRingHom.compose with ring, coefficients, projection

theorem polynomialResidueCoefficients.value (a : Set)
  requires coefficient : a ∈ R
  shows polynomialResidueCoefficients(I, R, J)(a) = quotientProjection(P, idealRelation(P, J))(polynomialConstant(I, R, a))
proof
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have polynomialRing := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *
  have coefficients := polynomialCoefficients.hom at I, A, add, zero, neg, mul, one with *
  have projection := idealQuotient.projection_hom with polynomialRing, ideal
  have coefficientFunction := IsRingHom.function with coefficients
  have projectionFunction := IsRingHom.function with projection
  have value := compose.apply at quotientProjection(P, idealRelation(P, J)), polynomialCoefficients(I, R), R, P, Q, a with *
  have constant := polynomialCoefficients.value at I, A, zero, a with *
  unfold polynomialResidueCoefficients
  cc

theorem polynomialResidueCoefficients.finitely_generated
  requires finite : Finite(I)
  shows FinitelyGeneratedAlgebra(polynomialResidueCoefficients(I, R, J), R, Q)
proof
  unfold polynomialResidueCoefficients
  exact polynomialQuotient.finitely_generated with *

section Isomorphisms
hypothesis iso : IsRingIso(polynomialResidueCoefficients(I, R, J), R, Q)

theorem polynomialResidueRetraction.hom
  shows IsRingHom(polynomialResidueRetraction(I, R, J), P, R)
proof
  have polynomialRing := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *
  have quotientRing := idealQuotient.comm_ring with polynomialRing, ideal
  have projection := idealQuotient.projection_hom with polynomialRing, ideal
  have inverse := IsRingIso.inverse with ring, quotientRing, iso
  have inverseHom := IsRingIso.hom with inverse
  unfold polynomialResidueRetraction
  exact IsRingHom.compose with polynomialRing, projection, inverseHom

theorem polynomialResidueRetraction.constant (a : Set)
  requires coefficient : a ∈ R
  shows polynomialResidueRetraction(I, R, J)(polynomialConstant(I, R, a)) = a
proof
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have member := polynomialConstant.member at I, A, zero, a with *
  have polynomialRing := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *
  have projection := idealQuotient.projection_hom with polynomialRing, ideal
  have function := IsRingHom.function with projection
  have bijective := IsRingIso.bijective with iso
  have inverse := converse.function_of_bijective with bijective
  have value := compose.apply at converse(polynomialResidueCoefficients(I, R, J), R, Q), quotientProjection(P, idealRelation(P, J)), P, Q, R, polynomialConstant(I, R, a) with *
  have residue := polynomialResidueCoefficients.value at I, A, add, zero, neg, mul, one, J, a with *
  have recovered := Bijective.inverse_apply with bijective, coefficient
  unfold polynomialResidueRetraction
  cc

theorem polynomialResidueRetraction.vanishes (p : Set)
  requires member : p ∈ J
  shows polynomialResidueRetraction(I, R, J)(p) = R[0]
proof
  have bounded := IsIdeal.subset_carrier with ideal
  have polynomial := bounded with p, member
  have polynomialRing := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *
  have quotientRing := idealQuotient.comm_ring with polynomialRing, ideal
  have equivalence := idealRelation.equivalence with polynomialRing, ideal
  have projection := idealQuotient.projection_hom with polynomialRing, ideal
  have projectionFunction := IsRingHom.function with projection
  have inverse := IsRingIso.inverse with ring, quotientRing, iso
  have inverseHom := IsRingIso.hom with inverse
  have inverseFunction := IsRingHom.function with inverseHom
  have inverseZero := IsRingHom.zero with inverseHom
  have projectionValue := quotientProjection.value at P, idealRelation(P, J), p with *
  have classZero := idealClass.eq_zero.backward with polynomialRing, ideal, polynomial, member
  have value := compose.apply at converse(polynomialResidueCoefficients(I, R, J), R, Q), quotientProjection(P, idealRelation(P, J)), P, Q, R, p with *
  unfold polynomialResidueRetraction
  cc

theorem polynomialResidueCoefficients.common_zero_of_iso
  shows ∃ v, PolynomialCommonZero(I, R, J, v)
proof
  have hom := polynomialResidueRetraction.hom with *
  have constants : ∀ a ∈ R, polynomialResidueRetraction(I, R, J)(polynomialConstant(I, R, a)) = a
    intros a ha
    exact polynomialResidueRetraction.constant with *
  have assignment := polynomialValues.function at I, A, add, zero, neg, mul, one, polynomialResidueRetraction(I, R, J) with *
  have evaluation := IsRingHom.eq_polynomialAt with ring, hom, constants
  witness polynomialValues(I, R, polynomialResidueRetraction(I, R, J))
  constructor
  . exact assignment
  . intros p hp
    have vanishes := polynomialResidueRetraction.vanishes with *
    rwa evaluation at vanishes

end Isomorphisms
end Residues

section Fields
variable (I A add zero neg mul one J : Set)
notation ring R := (A, add, zero, neg, mul, one)
notation ring P := R[I]
notation ring Q := P ⧸ J
hypothesis field : IsField(R)
hypothesis maximal : IsMaximalIdeal(P, J)

theorem polynomialResidueCoefficients.iso_of_surjective
  requires onto : SurjectiveBetween(polynomialResidueCoefficients(I, R, J), R, Q)
  shows IsRingIso(polynomialResidueCoefficients(I, R, J), R, Q)
proof
  have ring := IsField.comm_ring with field
  have polynomialRing := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *
  have ideal := IsMaximalIdeal.ideal with maximal
  have quotientField := idealQuotient.is_field_of_maximal with polynomialRing, maximal
  have quotientRing := IsField.comm_ring with quotientField
  have nontrivial := IsField.nontrivial with quotientField
  have hom := polynomialResidueCoefficients.hom with *
  exact IsRingHom.field_iso_of_surjective with field, quotientRing, nontrivial, hom, onto

theorem polynomialResidueCoefficients.common_zero_of_surjective
  requires onto : SurjectiveBetween(polynomialResidueCoefficients(I, R, J), R, Q)
  shows ∃ v, PolynomialCommonZero(I, R, J, v)
proof
  have ring := IsField.comm_ring with field
  have ideal := IsMaximalIdeal.ideal with maximal
  have iso := polynomialResidueCoefficients.iso_of_surjective with *
  exact polynomialResidueCoefficients.common_zero_of_iso with *

end Fields