Grace/Cumulus/Algebra/Polynomial/Nullstellensatz.g17

Open in Workbench Download source

Imports

MatrixAnnihilator · IntegralFinite · NullstellensatzReduction · InfiniteFieldLocalization · EmptyVariables · TranscendenceLocalization · Field.Rigidity · Field.Infinite

Declarations

Source

1-- Weak Nullstellensatz and Zariski's lemma over algebraically closed 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.Nullstellensatz8import MatrixAnnihilator9import IntegralFinite10import NullstellensatzReduction11import InfiniteFieldLocalization12import EmptyVariables13import TranscendenceLocalization14import Field.Rigidity15import Field.Infinite1617section ZariskiFamilies18variable (I M A add zero neg mul one B plus z minus times unit f v : Set)19notation ring R := (A, add, zero, neg, mul, one)20notation ring S := (B, plus, z, minus, times, unit)21notation ring Q := R[M]22hypothesis coefficients : IsField(R)23hypothesis infinite : ¬Finite(R)24hypothesis field : IsField(S)25hypothesis hom : IsRingHom(f, R, S)26hypothesis finite : Finite(I)27hypothesis assignment : v : I → S28hypothesis subset : M ⊆ I29hypothesis independent : AlgebraicallyIndependent(M, R, S, f, restrict(v, M))30hypothesis maximal : ∀ T, T ⊆ I → M ⊆ T → AlgebraicallyIndependent(T, R, S, f, restrict(v, T)) → T = M31hypothesis generates : algebraAdjoin(f, R, S, functionImage(v, I, S)) = S3233-- A nonempty independent family contradicts the existing localization obstruction.34-- Finite-module integrality supplies the constructive determinant trick.35theorem maximal_independent_empty36  shows M = ∅37proof38  have source := IsField.comm_ring with coefficients39  have target := IsField.comm_ring with field40  have sourceQ : IsCommRing(Q)41    exact polynomials.comm_ring with *42  have data := independent43  have restricted := data.right.left44  have injective := data.right.right45  have evaluation : IsRingHom(polynomialAtOver(M, R, S, f, restrict(v, M)), Q,46    S)47    exact polynomialAtOver.hom with *48  obtain ⟨s, polynomial, nonzero, T, carrier, finiteModule⟩ := AlgebraicallyIndependent.maximal_finite_module at I, M, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, v with *49  have localized := IsRingHom.principal_localization_subring with *50  have powers := IsRingHom.denominator_powers with *51  have mappedCarrier : T = localizationWithin(S, functionImage(polynomialAtOver(M, R, S, f, restrict(v, M)), Q, S), functionImage(polynomialAtOver(M, R, S, f, restrict(v, M)), denominatorPowers(Q, s), S))52    rwa powers53  have subring : IsSubring(S, T) by rwa mappedCarrier54  have smaller := IsSubring.comm_ring with target, subring55  have inclusion := IsSubring.inclusion_hom with target, subring56  have integral : ∀ x ∈ S, IntegralOver(identity(T), T, B, plus, z, times, unit, x)57    intros x member58    exact FiniteAlgebraModule.integral with *59  ext j60  constructor61  . intro index62    have obstruction := polynomialLocalization.not_integral with *63    exfalso64    exact obstruction with integral65  . intro impossible66    exfalso67    exact set.empty with impossible6869end ZariskiFamilies7071section EmptyCoefficients72variable (A add zero neg mul one B plus z minus times unit f v x : Set)73notation ring R := (A, add, zero, neg, mul, one)74notation ring S := (B, plus, z, minus, times, unit)75notation ring Q := R[∅]76hypothesis coefficients : IsField(R)77hypothesis field : IsField(S)78hypothesis hom : IsRingHom(f, R, S)79hypothesis assignment : v : ∅ → S8081-- Z1 DISCHARGED: extract constant coefficients and transport the finite relation.82theorem algebraic_over_empty_variables83  requires algebraic : AlgebraicOver(polynomialAtOver(∅, R, S, f, v), Q, S, x)84  shows AlgebraicOver(f, R, S, x)85proof86  have source := IsField.comm_ring with coefficients87  have target := IsField.comm_ring with field88  exact AlgebraicOver.empty_variables with *8990end EmptyCoefficients9192section Zariski93variable (A add zero neg mul one B plus z minus times unit f : Set)94notation ring R := (A, add, zero, neg, mul, one)95notation ring S := (B, plus, z, minus, times, unit)96hypothesis coefficients : IsField(R)97hypothesis infinite : ¬Finite(R)98hypothesis field : IsField(S)99hypothesis hom : IsRingHom(f, R, S)100hypothesis generated : FinitelyGeneratedAlgebra(f, R, S)101102theorem FinitelyGeneratedAlgebra.finite_module_of_field103  shows FiniteAlgebraModule(f, R, S)104proof105  have source := IsField.comm_ring with coefficients106  have target := IsField.comm_ring with field107  have nontrivial := IsField.nontrivial with field108  have injective : InjectiveBetween(f, R, S)109    exact IsRingHom.field_injective with *110  obtain ⟨G, finite, bounded, generates⟩ := generated111  have assignment := identity.inclusion with bounded112  have image := functionImage.identity with bounded113  have generation : algebraAdjoin(f, R, S, functionImage(identity(G), G, S)) = S by rwa image114  obtain ⟨M, subset, independent, maximal⟩ := AlgebraicallyIndependent.exists_maximal at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, G, identity(G) with *115  have empty := maximal_independent_empty at G, M, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, identity(G) with *116  have roots := AlgebraicallyIndependent.maximal_generators_algebraic with *117  have data := independent118  have restricted := data.right.left119  rw empty at restricted120  have algebraic : ∀ x ∈ G, AlgebraicOver(f, R, S, x)121    intros x member122    have inImage : x ∈ functionImage(identity(G), G, S) by rwa image123    have root := roots with x, inImage124    rw empty at root125    exact algebraic_over_empty_variables with *126  exact algebraicGenerators.finite_module with *127128theorem FinitelyGeneratedAlgebra.algebraic_of_field129  shows ∀ x ∈ S, AlgebraicOver(f, R, S, x)130proof131  have source := IsField.comm_ring with coefficients132  have target := IsField.comm_ring with field133  have finiteModule : FiniteAlgebraModule(f, R, S)134    exact FinitelyGeneratedAlgebra.finite_module_of_field with *135  intros x member136  have integral : IntegralOver(f, R, S, x)137    exact FiniteAlgebraModule.integral with *138  exact IntegralOver.algebraic with coefficients, target, hom, integral139140end Zariski141142section AlgebraicClosure143variable (A add zero neg mul one : Set)144notation ring R := (A, add, zero, neg, mul, one)145hypothesis closed : IsAlgebraicallyClosed(R)146147-- A1 discharged: an explicit positive-degree monic vanishing polynomial plus 1.148theorem algebraically_closed_infinite149  shows ¬Finite(R)150proof151  exact IsAlgebraicallyClosed.infinite with *152153-- A2 discharged: synthetic division and induction on the monic relation degree.154theorem algebraic_element_in_image (B plus z minus times unit f x : Set)155  requires field : IsField(B, plus, z, minus, times, unit)156  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)157  requires algebraic : AlgebraicOver(f, A, zero, B, plus, z, times, x)158  shows ∃ a ∈ R, f(a) = x159proof160  exact IsAlgebraicallyClosed.algebraic_in_image with *161162theorem IsAlgebraicallyClosed.field_algebra_surjective (B plus z minus times unit f : Set)163  requires field : IsField(B, plus, z, minus, times, unit)164  requires hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)165  requires generated : FinitelyGeneratedAlgebra(f, A, B, plus, z, minus, times, unit)166  shows SurjectiveBetween(f, A, B)167proof168  have coefficients := IsAlgebraicallyClosed.field with closed169  have infinite : ¬Finite(R)170    exact algebraically_closed_infinite with *171  have algebraic := FinitelyGeneratedAlgebra.algebraic_of_field with *172  exact IsAlgebraicallyClosed.algebraic_extension_surjective with *173174section Polynomials175variable (I G : Set)176notation ring P := R[I]177hypothesis finite : Finite(I)178hypothesis generators : G ⊆ P179180theorem polynomialIdeal.unit_iff_no_common_zero181  shows P[1] ∈ idealSpan(P, G) ↔ ¬(∃ v, PolynomialCommonZero(I, R, G, v))182proof183  have field := IsAlgebraicallyClosed.field with closed184  have rigidity : ∀ B, ∀ plus, ∀ z, ∀ minus, ∀ times, ∀ unit, ∀ f, IsField(B, plus, z, minus, times, unit) → IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit) → FinitelyGeneratedAlgebra(f, A, B, plus, z, minus, times, unit) → SurjectiveBetween(f, A, B)185    intros B plus z minus times unit f target hom generated186    exact IsAlgebraicallyClosed.field_algebra_surjective with *187  exact polynomialIdeal.unit_iff_no_common_zero_of_field_algebra_rigidity with *188189theorem polynomialIdeal.finite_certificate_iff_no_common_zero190  shows (∃ terms, List(idealProducts(P, G), terms) ∧ P[1] = ringSum{idealProducts(P, G)}(polynomialAdd(I, R), P[0], terms)) ↔ ¬(∃ v, PolynomialCommonZero(I, R, G, v))191proof192  have field := IsAlgebraicallyClosed.field with closed193  have coefficients := IsField.comm_ring with field194  have ring : IsCommRing(P)195    exact polynomials.comm_ring with *196  have certificate := idealSpan.unit_iff_finite_certificate with *197  have equivalence := polynomialIdeal.unit_iff_no_common_zero with *198  tauto199200end Polynomials201end AlgebraicClosure202