PolynomialTranscendence
The finite algebraic-family and principal-localization steps toward Zariski's lemma
1-- The finite algebraic-family and principal-localization steps toward Zariski's lemma.2-- Part of the Grace17 examples.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module PolynomialTranscendence8import Grace.Cumulus.Algebra.Polynomial.TranscendenceLocalization910section Transfer11variable (I J A add z neg mul one : Set)12notation ring R := (A, add, z, neg, mul, one)13notation ring P := R[I]14notation ring Q := R[J]15hypothesis source : IsCommRing(R)1617theorem retain_used_variables (p : Set)18 requires polynomial : p ∈ P19 requires supported : polynomialVariablesUsed(I, R, p) ⊆ J20 shows polynomialTransfer(J, I, R)(polynomialTransfer(I, J, R)(p)) = p21proof22 exact polynomialTransfer.roundtrip with *2324theorem inclusion_is_injective25 requires subset : I ⊆ J26 shows InjectiveBetween(polynomialTransfer(I, J, R), P, Q)27proof28 exact polynomialTransfer.injective with *2930theorem retain_nonzero_coefficients (p : Set)31 requires polynomial : p ∈ P32 requires supported : polynomialVariablesUsed(I, R, p) ⊆ J33 requires nonzero : p ≠ P[0]34 shows polynomialTransfer(I, J, R)(p) ≠ Q[0]35proof36 exact polynomialTransfer.nonzero_supported with *3738theorem omitted_variable_is_one (i : Set)39 requires index : i ∈ I40 requires outside : ¬(i ∈ J)41 shows polynomialTransfer(I, J, R)(polynomialVariable(I, R, i)) = Q[1]42proof43 exact polynomialTransfer.outside_variable with *4445end Transfer46section Localization47variable (A add z neg mul one B plus o minus times unit f K : Set)48notation ring R := (A, add, z, neg, mul, one)49notation ring S := (B, plus, o, minus, times, unit)50hypothesis source : IsCommRing(R)51hypothesis field : IsField(S)52hypothesis hom : IsRingHom(f, R, S)53hypothesis injective : InjectiveBetween(f, R, S)5455theorem localize_an_algebraic_element (x : Set)56 requires algebraic : AlgebraicOver(f, R, S, x)57 shows ∃ a ∈ R, a ≠ R[0] ∧58 IntegralOver(identity(localizationWithin(S, functionImage(f, R, S), denominatorPowers(S, f(a)))), localizationWithin(S, functionImage(f, R, S), denominatorPowers(S, f(a))), S, x)59proof60 exact AlgebraicOver.exists_principal_integral with *6162theorem one_localization_for_a_finite_family63 requires finite : Finite(K)64 requires algebraic : ∀ x ∈ K, AlgebraicOver(f, R, S, x)65 shows ∃ s ∈ R, s ≠ R[0] ∧ (∀ x ∈ K,66 IntegralOver(identity(localizationWithin(S, functionImage(f, R, S), denominatorPowers(S, f(s)))), localizationWithin(S, functionImage(f, R, S), denominatorPowers(S, f(s))), S, x))67proof68 exact AlgebraicOver.finite_principal_integral with *6970end Localization71section Families72variable (I M A add z neg mul one B plus o minus times unit f v : Set)73notation ring R := (A, add, z, neg, mul, one)74notation ring S := (B, plus, o, minus, times, unit)75notation ring Q := R[M]76hypothesis source : IsCommRing(R)77hypothesis field : IsField(S)78hypothesis hom : IsRingHom(f, R, S)79hypothesis assignment : v : I → S80hypothesis subset : M ⊆ I81hypothesis independent : AlgebraicallyIndependent(M, R, S, f, restrict(v, M))82hypothesis maximal : ∀ T, T ⊆ I → M ⊆ T → AlgebraicallyIndependent(T, R, S, f, restrict(v, T)) → T = M8384theorem all_generators_are_algebraic85 shows ∀ x ∈ functionImage(v, I, S), AlgebraicOver(polynomialAtOver(M, R, S, f, restrict(v, M)), Q, S, x)86proof87 exact AlgebraicallyIndependent.maximal_generators_algebraic with *8889theorem finite_over_one_localization90 requires finite : Finite(I)91 requires generates : algebraAdjoin(f, R, S, functionImage(v, I, S)) = S92 shows ∃ s ∈ Q, s ≠ Q[0] ∧ (∃ T,93 T = localizationWithin(S, functionImage(polynomialAtOver(M, R, S, f, restrict(v, M)), Q, S), denominatorPowers(S, polynomialAtOver(M, R, S, f, restrict(v, M))(s))) ∧94 FiniteAlgebraModule(identity(T), T, S))95proof96 exact AlgebraicallyIndependent.maximal_finite_module with *9798end Families99