Grace/Cumulus/Algebra/Polynomial/PointIdeal.g17

Open in Workbench Download source

Imports

Assignment · Field.Homomorphism

Declarations

Source

1-- Point ideals, coordinate separation, and residue rings (ZF).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.PointIdeal8import Assignment9import Field.Homomorphism1011def pointIdeal (I A add zero neg mul one v : Set) : Set :=12  ringKernel(polynomialAt(I, A, add, zero, neg, mul, one, v), polynomials(I, A, zero), zero)1314notation scoped pointIdeal(I, R, v) => pointIdeal(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, v)1516def polynomialCoordinateDifference (I A add zero neg mul one j a : Set) : Set :=17  (polynomialAdd(I, A, add, zero, neg, mul, one))(polynomialVariable(I, A, zero, one, j), (polynomialNeg(I, A, add, zero, neg, mul, one))(polynomialConstant(I, A, zero, a)))1819notation scoped polynomialCoordinateDifference(I, R, j, a) => polynomialCoordinateDifference(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, j, a)2021section Coordinates22variable (I A add zero neg mul one : Set)23hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)24notation ring R := (A, add, zero, neg, mul, one)25notation ring P := R[I]2627theorem polynomialCoordinateDifference.member (j a : Set)28  requires coefficient : a ∈ R29  shows polynomialCoordinateDifference(I, A, add, zero, neg, mul, one, j, a) ∈ P30proof31  have ordinary := IsCommRing.ring with ring32  have zeroIn := IsRing.zero_in_carrier with ordinary33  have multiplicative := IsRing.multiplicative with ordinary34  have oneIn := IsMonoid.unit_in_carrier with multiplicative35  have variable := polynomialVariable.member at I, A, zero, one, j with *36  have constant := polynomialConstant.member at I, A, zero, a with *37  have source := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *38  have polynomialRing := IsCommRing.ring with source39  have negative := IsRing.neg_closed with polynomialRing, constant40  unfold polynomialCoordinateDifference41  exact IsRing.add_closed with polynomialRing, variable, negative4243theorem polynomialAt.coordinate_difference (v j a : Set)44  requires assignment : v : I → A45  requires index : j ∈ I46  requires coefficient : a ∈ R47  shows polynomialAt(I, A, add, zero, neg, mul, one, v)(polynomialCoordinateDifference(I, A, add, zero, neg, mul, one, j, a)) = R[v(j) - a]48proof49  have ordinary := IsCommRing.ring with ring50  have zeroIn := IsRing.zero_in_carrier with ordinary51  have multiplicative := IsRing.multiplicative with ordinary52  have oneIn := IsMonoid.unit_in_carrier with multiplicative53  have variable := polynomialVariable.member at I, A, zero, one, j with *54  have constant := polynomialConstant.member at I, A, zero, a with *55  have hom := polynomialAt.hom with *56  have source := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *57  have subtraction := IsRingHom.sub with source, hom, variable, constant58  have valueVariable := polynomialAt.variable with *59  have valueConstant := polynomialAt.constant at I, A, add, zero, neg, mul, one, v, a with *60  unfold polynomialCoordinateDifference61  cc6263-- Evaluate at the constant point a + 1 to distinguish X_j - a from zero.64theorem polynomialCoordinateDifference.nonzero (j a : Set)65  requires distinct : R[0] ≠ R[1]66  requires index : j ∈ I67  requires coefficient : a ∈ R68  shows polynomialCoordinateDifference(I, A, add, zero, neg, mul, one, j, a) ≠ P[0]69proof70  have ordinary := IsCommRing.ring with ring71  have monoid := IsRing.multiplicative with ordinary72  have oneIn := IsMonoid.unit_in_carrier with monoid73  have shifted := IsRing.add_closed with ordinary, coefficient, oneIn74  have assignment := constantFunction.function at I, A, R[a + 1] with shifted75  have value := constantFunction.apply with index, shifted76  have evaluated := polynomialAt.coordinate_difference with assignment, index, coefficient77  have hom := polynomialAt.hom with *78  have zeroValue := IsRingHom.zero with hom79  have difference : R[(a + 1) - a] = R[1] by ring80  intro equal81  have impossible : R[0] = R[1] by cc82  exact distinct with impossible8384end Coordinates8586section Points87variable (I A add zero neg mul one v : Set)88hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)89hypothesis assignment : v : I → A90notation ring R := (A, add, zero, neg, mul, one)91notation ring P := R[I]9293theorem pointIdeal.membership (p : Set)94  shows p ∈ pointIdeal(I, A, add, zero, neg, mul, one, v) ↔ p ∈ P ∧ polynomialAt(I, A, add, zero, neg, mul, one, v)(p) = R[0]95proof96  simp [pointIdeal, ringKernel.membership]9798theorem pointIdeal.ideal99  shows IsIdeal(P, polynomialAdd(I, A, add, zero, neg, mul, one), P[0], polynomialNeg(I, A, add, zero, neg, mul, one), polynomialMul(I, A, add, zero, neg, mul, one), pointIdeal(I, A, add, zero, neg, mul, one, v))100proof101  unfold pointIdeal102  exact polynomialAt.kernel_ideal with *103104theorem pointIdeal.coordinate_difference (j a : Set)105  requires index : j ∈ I106  requires coefficient : a ∈ R107  shows polynomialCoordinateDifference(I, A, add, zero, neg, mul, one, j, a) ∈ pointIdeal(I, A, add, zero, neg, mul, one, v) ↔ v(j) = a108proof109  have member := polynomialCoordinateDifference.member at I, A, add, zero, neg, mul, one, j, a with *110  have image := FunctionBetween.apply_closed with *111  have value := polynomialAt.coordinate_difference at I, A, add, zero, neg, mul, one, v, j, a with *112  constructor113  . intro vanishes114    have data := pointIdeal.membership.forward with *115    have equation : R[v(j) - a] = R[0] by cc116    linear_combination equation117  . intro equal118    have equation : R[v(j) - a] = R[0]119      rw equal120      ring121    apply pointIdeal.membership.backward with ring, assignment122    refine ⟨member, ?_⟩123    cc124125theorem pointIdeal.contains_centered_variable (j : Set)126  requires index : j ∈ I127  shows polynomialCoordinateDifference(I, A, add, zero, neg, mul, one, j, v(j)) ∈ pointIdeal(I, A, add, zero, neg, mul, one, v)128proof129  have coefficient := FunctionBetween.apply_closed with *130  apply pointIdeal.coordinate_difference.backward with ring, assignment, index, coefficient131  rfl132133theorem pointIdeal.subset_iff (w : Set)134  requires other : w : I → A135  shows pointIdeal(I, A, add, zero, neg, mul, one, v) ⊆ pointIdeal(I, A, add, zero, neg, mul, one, w) ↔ v = w136proof137  constructor138  . intro included139    apply FunctionBetween.ext with assignment, other140    intros j hj141    have coefficient := FunctionBetween.apply_closed at v, I, A, j with *142    have centered := pointIdeal.contains_centered_variable at I, A, add, zero, neg, mul, one, v, j with *143    have member := included with polynomialCoordinateDifference(I, A, add, zero, neg, mul, one, j, v(j)), centered144    have equal := pointIdeal.coordinate_difference.forward with ring, other, hj, coefficient, member145    symm146    exact equal147  . intro equal148    rw equal149    simp150151theorem pointIdeal.eq_iff (w : Set)152  requires other : w : I → A153  shows pointIdeal(I, A, add, zero, neg, mul, one, v) = pointIdeal(I, A, add, zero, neg, mul, one, w) ↔ v = w154proof155  constructor156  . intro equal157    have included : pointIdeal(I, A, add, zero, neg, mul, one, v) ⊆ pointIdeal(I, A, add, zero, neg, mul, one, w)158      rw equal159      simp160    exact pointIdeal.subset_iff.forward with *161  . intro equal162    rw equal163    rfl164165theorem PolynomialCommonZero.iff_subset_pointIdeal (G : Set)166  requires generators : G ⊆ P167  shows PolynomialCommonZero(I, R, G, v) ↔ G ⊆ pointIdeal(I, A, add, zero, neg, mul, one, v)168proof169  constructor170  . intros common p hp171    have member := generators with p, hp172    have value := common.right with p, hp173    apply pointIdeal.membership.backward with ring, assignment174    refine ⟨member, value⟩175  . intro included176    unfold PolynomialCommonZero177    refine ⟨assignment, ?_⟩178    intros p hp179    have member := included with p, hp180    have data := pointIdeal.membership.forward with *181    exact data.right182183theorem pointIdeal.quotient_iso184  shows IsRingIso(quotientMap(polynomialAt(I, A, add, zero, neg, mul, one, v), polynomials(I, A, zero), A, idealRelation(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), polynomialNeg(I, A, add, zero, neg, mul, one), pointIdeal(I, A, add, zero, neg, mul, one, v))),185    (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), pointIdeal(I, A, add, zero, neg, mul, one, v))),186    quotientBinary(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), pointIdeal(I, A, add, zero, neg, mul, one, v)), polynomialAdd(I, A, add, zero, neg, mul, one)), ⟦constantFunction(monomials(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), pointIdeal(I, A, add, zero, neg, mul, one, v))],187    quotientUnary(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), pointIdeal(I, A, add, zero, neg, mul, one, v)), polynomialNeg(I, A, add, zero, neg, mul, one)), quotientBinary(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), pointIdeal(I, A, add, zero, neg, mul, one, v)), polynomialMul(I, A, add, zero, neg, mul, one)), ⟦polynomialConstant(I, A, zero, one)⟧[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), pointIdeal(I, A, add, zero, neg, mul, one, v))],188    A, add, zero, neg, mul, one)189proof190  have source := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *191  have hom := polynomialAt.hom with *192  have onto := polynomialAt.surjective with *193  have iso := idealQuotient.first_isomorphism with source, ring, hom, onto194  simpa [pointIdeal] using iso195196end Points197198section Fields199variable (I A add zero neg mul one v : Set)200hypothesis field : IsField(A, add, zero, neg, mul, one)201hypothesis assignment : v : I → A202notation ring R := (A, add, zero, neg, mul, one)203notation ring P := R[I]204205theorem pointIdeal.maximal206  shows IsMaximalIdeal(P, polynomialAdd(I, A, add, zero, neg, mul, one), P[0], polynomialNeg(I, A, add, zero, neg, mul, one), polynomialMul(I, A, add, zero, neg, mul, one), P[1], pointIdeal(I, A, add, zero, neg, mul, one, v))207proof208  have ring := IsField.comm_ring with field209  have source := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *210  have hom := polynomialAt.hom with *211  have onto := polynomialAt.surjective with *212  unfold pointIdeal213  exact IsRingHom.kernel_maximal with source, field, hom, onto214215theorem IsMaximalIdeal.common_zero_iff_point (M : Set)216  requires maximal : IsMaximalIdeal(P, polynomialAdd(I, A, add, zero, neg, mul, one), P[0], polynomialNeg(I, A, add, zero, neg, mul, one), polynomialMul(I, A, add, zero, neg, mul, one), P[1], M)217  shows PolynomialCommonZero(I, R, M, v) ↔ M = pointIdeal(I, A, add, zero, neg, mul, one, v)218proof219  have ring := IsField.comm_ring with field220  have ideal := IsMaximalIdeal.ideal with maximal221  have bounded := IsIdeal.subset_carrier with ideal222  have pointMaximal := pointIdeal.maximal with *223  have pointProper := IsMaximalIdeal.proper with pointMaximal224  constructor225  . intro common226    have included := PolynomialCommonZero.iff_subset_pointIdeal.forward with ring, assignment, bounded, common227    have data := maximal228    have equal := data.right with pointIdeal(I, A, add, zero, neg, mul, one, v), pointProper, included229    symm230    exact equal231  . intro equal232    have included : M ⊆ pointIdeal(I, A, add, zero, neg, mul, one, v)233      rw equal234      simp235    exact PolynomialCommonZero.iff_subset_pointIdeal.backward with *236237theorem IsMaximalIdeal.common_zero_unique (M w : Set)238  requires maximal : IsMaximalIdeal(P, polynomialAdd(I, A, add, zero, neg, mul, one), P[0], polynomialNeg(I, A, add, zero, neg, mul, one), polynomialMul(I, A, add, zero, neg, mul, one), P[1], M)239  requires other : w : I → A240  requires first : PolynomialCommonZero(I, R, M, v)241  requires second : PolynomialCommonZero(I, R, M, w)242  shows v = w243proof244  have ring := IsField.comm_ring with field245  have left := IsMaximalIdeal.common_zero_iff_point.forward with field, assignment, maximal, first246  have right := IsMaximalIdeal.common_zero_iff_point.forward with field, other, maximal, second247  have equal : pointIdeal(I, A, add, zero, neg, mul, one, v) = pointIdeal(I, A, add, zero, neg, mul, one, w) by cc248  exact pointIdeal.eq_iff.forward with *249250end Fields251