Grace/Cumulus/Algebra/Polynomial/Residue.g17

Open in Workbench Download source

Imports

Universal · FiniteGeneration · Field.Embedding

Declarations

Source

1-- Recovering a common zero from an isomorphism of the coefficient and residue fields.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Algebra.Polynomial.Residue8import Universal9import FiniteGeneration10import Field.Embedding1112def polynomialResidueCoefficients (I A add zero neg mul one J : Set) : Set :=13  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)))1415notation scoped polynomialResidueCoefficients(I, R, J) => polynomialResidueCoefficients(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, J)1617def polynomialResidueRetraction (I A add zero neg mul one J : Set) : Set :=18  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)1920notation scoped polynomialResidueRetraction(I, R, J) => polynomialResidueRetraction(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, J)2122section Residues23variable (I A add zero neg mul one J : Set)24notation ring R := (A, add, zero, neg, mul, one)25notation ring P := R[I]26notation ring Q := P ⧸ J27hypothesis ring : IsCommRing(R)28hypothesis ideal : IsIdeal(P, J)2930theorem polynomialResidueCoefficients.hom31  shows IsRingHom(polynomialResidueCoefficients(I, R, J), R, Q)32proof33  have polynomialRing := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *34  have coefficients := polynomialCoefficients.hom at I, A, add, zero, neg, mul, one with *35  have projection := idealQuotient.projection_hom with polynomialRing, ideal36  unfold polynomialResidueCoefficients37  exact IsRingHom.compose with ring, coefficients, projection3839theorem polynomialResidueCoefficients.value (a : Set)40  requires coefficient : a ∈ R41  shows polynomialResidueCoefficients(I, R, J)(a) = quotientProjection(P, idealRelation(P, J))(polynomialConstant(I, R, a))42proof43  have ordinary := IsCommRing.ring with ring44  have zeroIn := IsRing.zero_in_carrier with ordinary45  have polynomialRing := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *46  have coefficients := polynomialCoefficients.hom at I, A, add, zero, neg, mul, one with *47  have projection := idealQuotient.projection_hom with polynomialRing, ideal48  have coefficientFunction := IsRingHom.function with coefficients49  have projectionFunction := IsRingHom.function with projection50  have value := compose.apply at quotientProjection(P, idealRelation(P, J)), polynomialCoefficients(I, R), R, P, Q, a with *51  have constant := polynomialCoefficients.value at I, A, zero, a with *52  unfold polynomialResidueCoefficients53  cc5455theorem polynomialResidueCoefficients.finitely_generated56  requires finite : Finite(I)57  shows FinitelyGeneratedAlgebra(polynomialResidueCoefficients(I, R, J), R, Q)58proof59  unfold polynomialResidueCoefficients60  exact polynomialQuotient.finitely_generated with *6162section Isomorphisms63hypothesis iso : IsRingIso(polynomialResidueCoefficients(I, R, J), R, Q)6465theorem polynomialResidueRetraction.hom66  shows IsRingHom(polynomialResidueRetraction(I, R, J), P, R)67proof68  have polynomialRing := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *69  have quotientRing := idealQuotient.comm_ring with polynomialRing, ideal70  have projection := idealQuotient.projection_hom with polynomialRing, ideal71  have inverse := IsRingIso.inverse with ring, quotientRing, iso72  have inverseHom := IsRingIso.hom with inverse73  unfold polynomialResidueRetraction74  exact IsRingHom.compose with polynomialRing, projection, inverseHom7576theorem polynomialResidueRetraction.constant (a : Set)77  requires coefficient : a ∈ R78  shows polynomialResidueRetraction(I, R, J)(polynomialConstant(I, R, a)) = a79proof80  have ordinary := IsCommRing.ring with ring81  have zeroIn := IsRing.zero_in_carrier with ordinary82  have member := polynomialConstant.member at I, A, zero, a with *83  have polynomialRing := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *84  have projection := idealQuotient.projection_hom with polynomialRing, ideal85  have function := IsRingHom.function with projection86  have bijective := IsRingIso.bijective with iso87  have inverse := converse.function_of_bijective with bijective88  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 *89  have residue := polynomialResidueCoefficients.value at I, A, add, zero, neg, mul, one, J, a with *90  have recovered := Bijective.inverse_apply with bijective, coefficient91  unfold polynomialResidueRetraction92  cc9394theorem polynomialResidueRetraction.vanishes (p : Set)95  requires member : p ∈ J96  shows polynomialResidueRetraction(I, R, J)(p) = R[0]97proof98  have bounded := IsIdeal.subset_carrier with ideal99  have polynomial := bounded with p, member100  have polynomialRing := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *101  have quotientRing := idealQuotient.comm_ring with polynomialRing, ideal102  have equivalence := idealRelation.equivalence with polynomialRing, ideal103  have projection := idealQuotient.projection_hom with polynomialRing, ideal104  have projectionFunction := IsRingHom.function with projection105  have inverse := IsRingIso.inverse with ring, quotientRing, iso106  have inverseHom := IsRingIso.hom with inverse107  have inverseFunction := IsRingHom.function with inverseHom108  have inverseZero := IsRingHom.zero with inverseHom109  have projectionValue := quotientProjection.value at P, idealRelation(P, J), p with *110  have classZero := idealClass.eq_zero.backward with polynomialRing, ideal, polynomial, member111  have value := compose.apply at converse(polynomialResidueCoefficients(I, R, J), R, Q), quotientProjection(P, idealRelation(P, J)), P, Q, R, p with *112  unfold polynomialResidueRetraction113  cc114115theorem polynomialResidueCoefficients.common_zero_of_iso116  shows ∃ v, PolynomialCommonZero(I, R, J, v)117proof118  have hom := polynomialResidueRetraction.hom with *119  have constants : ∀ a ∈ R, polynomialResidueRetraction(I, R, J)(polynomialConstant(I, R, a)) = a120    intros a ha121    exact polynomialResidueRetraction.constant with *122  have assignment := polynomialValues.function at I, A, add, zero, neg, mul, one, polynomialResidueRetraction(I, R, J) with *123  have evaluation := IsRingHom.eq_polynomialAt with ring, hom, constants124  witness polynomialValues(I, R, polynomialResidueRetraction(I, R, J))125  constructor126  . exact assignment127  . intros p hp128    have vanishes := polynomialResidueRetraction.vanishes with *129    rwa evaluation at vanishes130131end Isomorphisms132end Residues133134section Fields135variable (I A add zero neg mul one J : Set)136notation ring R := (A, add, zero, neg, mul, one)137notation ring P := R[I]138notation ring Q := P ⧸ J139hypothesis field : IsField(R)140hypothesis maximal : IsMaximalIdeal(P, J)141142theorem polynomialResidueCoefficients.iso_of_surjective143  requires onto : SurjectiveBetween(polynomialResidueCoefficients(I, R, J), R, Q)144  shows IsRingIso(polynomialResidueCoefficients(I, R, J), R, Q)145proof146  have ring := IsField.comm_ring with field147  have polynomialRing := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *148  have ideal := IsMaximalIdeal.ideal with maximal149  have quotientField := idealQuotient.is_field_of_maximal with polynomialRing, maximal150  have quotientRing := IsField.comm_ring with quotientField151  have nontrivial := IsField.nontrivial with quotientField152  have hom := polynomialResidueCoefficients.hom with *153  exact IsRingHom.field_iso_of_surjective with field, quotientRing, nontrivial, hom, onto154155theorem polynomialResidueCoefficients.common_zero_of_surjective156  requires onto : SurjectiveBetween(polynomialResidueCoefficients(I, R, J), R, Q)157  shows ∃ v, PolynomialCommonZero(I, R, J, v)158proof159  have ring := IsField.comm_ring with field160  have ideal := IsMaximalIdeal.ideal with maximal161  have iso := polynomialResidueCoefficients.iso_of_surjective with *162  exact polynomialResidueCoefficients.common_zero_of_iso with *163164end Fields165