Grace/Cumulus/Algebra/Polynomial/ResidueCriterion.g17

Open in Workbench Download source

Imports

Residue · PointIdeal

Declarations

Source

1-- A maximal polynomial ideal has a common zero exactly when its coefficient map is onto.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.ResidueCriterion8import Residue9import PointIdeal1011section Residues12variable (I A add zero neg mul one J : Set)13notation ring R := (A, add, zero, neg, mul, one)14notation ring P := R[I]15notation ring Q := P ⧸ J16hypothesis field : IsField(R)17hypothesis maximal : IsMaximalIdeal(P, J)1819theorem polynomialResidueCoefficients.surjective_of_common_zero (v : Set)20  requires common : PolynomialCommonZero(I, R, J, v)21  shows SurjectiveBetween(polynomialResidueCoefficients(I, R, J), R, Q)22proof23  have ring := IsField.comm_ring with field24  have polynomialRing := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *25  have ordinary := IsCommRing.ring with ring26  have zeroIn := IsRing.zero_in_carrier with ordinary27  have ideal := IsMaximalIdeal.ideal with maximal28  have equivalence := idealRelation.equivalence with polynomialRing, ideal29  have data := common30  have assignment := data.left31  have evaluation := polynomialAt.hom with *32  have equalIdeal := IsMaximalIdeal.common_zero_iff_point.forward with *33  have hom := polynomialResidueCoefficients.hom with *34  have function := IsRingHom.function with hom35  constructor36  . exact function37  . intros X hX38    obtain ⟨p, hp, shape⟩ := quotient.representative with hX39    have value := IsRingHom.closed with evaluation, hp40    have constant := polynomialConstant.member at I, A, zero, polynomialAt(I, R, v)(p) with *41    have constantValue := polynomialAt.constant at I, A, add, zero, neg, mul, one, v, polynomialAt(I, R, v)(p) with *42    have congruent := IsRingHom.kernel_congruent.backward with polynomialRing, ring, evaluation, constant, hp, constantValue43    unfold pointIdeal at equalIdeal44    rw ← equalIdeal at congruent45    have equalClass := idealClass.eq_iff_congruent.backward with *46    have residueValue := polynomialResidueCoefficients.value at I, A, add, zero, neg, mul, one, J, polynomialAt(I, R, v)(p) with *47    have projectionValue := quotientProjection.value at P, idealRelation(P, J), polynomialConstant(I, R, polynomialAt(I, R, v)(p)) with *48    have output : polynomialResidueCoefficients(I, R, J)(polynomialAt(I, R, v)(p)) = X by cc49    have edge := FunctionBetween.relates_apply with function, value50    witness polynomialAt(I, R, v)(p)51    constructor52    . exact value53    . rw output at edge54      exact edge5556theorem polynomialResidueCoefficients.surjective_iff_common_zero57  shows SurjectiveBetween(polynomialResidueCoefficients(I, R, J), R, Q) ↔ ∃ v, PolynomialCommonZero(I, R, J, v)58proof59  constructor60  . intro onto61    exact polynomialResidueCoefficients.common_zero_of_surjective with *62  . intro exists63    obtain ⟨v, common⟩ := exists64    exact polynomialResidueCoefficients.surjective_of_common_zero with *6566end Residues67