Grace/Cumulus/Algebra/Polynomial/TranscendenceLocalization.g17

Open in Workbench Download source

Imports

AlgebraicDependence · Field.FiniteAlgebraicLocalization · IntegralFinite

Declarations

Source

1-- Finite generators become integral over one localization of an independent family.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.TranscendenceLocalization8import AlgebraicDependence9import Field.FiniteAlgebraicLocalization10import IntegralFinite1112section Families13variable (I M A add z neg mul one B plus o minus times unit f v : Set)14notation ring R := (A, add, z, neg, mul, one)15notation ring S := (B, plus, o, minus, times, unit)16notation ring Q := R[M]17hypothesis source : IsCommRing(R)18hypothesis field : IsField(S)19hypothesis hom : IsRingHom(f, R, S)20hypothesis assignment : v : I → S21hypothesis subset : M ⊆ I22hypothesis independent : AlgebraicallyIndependent(M, R, S, f, restrict(v, M))23hypothesis maximal : ∀ T, T ⊆ I → M ⊆ T → AlgebraicallyIndependent(T, R, S, f, restrict(v, T)) → T = M2425theorem AlgebraicallyIndependent.maximal_generators_algebraic26  shows ∀ x ∈ functionImage(v, I, S), AlgebraicOver(polynomialAtOver(M, R, S, f, restrict(v, M)), Q, S, x)27proof28  have target := IsField.comm_ring with field29  have sourceQ : IsCommRing(Q)30    exact polynomials.comm_ring with *31  have data := independent32  have restricted := data.right.left33  have injective := data.right.right34  have evaluation : IsRingHom(polynomialAtOver(M, R, S, f, restrict(v, M)), Q,35    S)36    exact polynomialAtOver.hom with *37  have domain : IsIntegralDomain(Q)38    exact IsRingHom.domain_of_field_embedding with *39  have nontrivial := IsIntegralDomain.nontrivial with domain40  have zeroIn : R[0] ∈ R by typecheck41  have oneIn : R[1] ∈ R by typecheck42  have closed : ∀ i ∈ M, v(i) ∈ S43    intros i member44    have included := subset45    have inI := included with i, member46    exact FunctionBetween.apply_closed with assignment, inI47  intros x inImage48  obtain ⟨element, j, index, value⟩ := functionImage.membership.forward with inImage49  have alternatives : j ∈ M ∨ ¬(j ∈ M) by tauto50  cases alternatives with included | outside51  . have coefficient := polynomialVariable.member at M, A, z, one, j with *52    have integral := IntegralOver.coefficient with coefficient53    have evaluated := polynomialAtOver.variable at M, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, restrict(v, M), j with *54    have original := restrict.apply with *55    have equal : polynomialAtOver(M, R, S, f, restrict(v, M))(polynomialVariable(M, R, j)) = x by cc56    rw equal at integral57    exact IntegralOver.algebraic_of_nontrivial with *58  . have algebraic := AlgebraicallyIndependent.maximal_algebraic with *59    rwa value6061theorem AlgebraicallyIndependent.maximal_common_localization62  requires finite : Finite(I)63  shows ∃ s ∈ Q, s ≠ Q[0] ∧ (∀ x ∈ functionImage(v, I, S),64    IntegralOver(identity(localizationWithin(S, functionImage(polynomialAtOver(M, R, S, f, restrict(v, M)), Q, S), denominatorPowers(S, polynomialAtOver(M, R, S, f, restrict(v, M))(s)))), localizationWithin(S, functionImage(polynomialAtOver(M, R, S, f, restrict(v, M)), Q, S), denominatorPowers(S, polynomialAtOver(M, R, S, f, restrict(v, M))(s))), S, x))65proof66  have target := IsField.comm_ring with field67  have sourceQ : IsCommRing(Q)68    exact polynomials.comm_ring with *69  have data := independent70  have restricted := data.right.left71  have injective := data.right.right72  have evaluation : IsRingHom(polynomialAtOver(M, R, S, f, restrict(v, M)), Q,73    S)74    exact polynomialAtOver.hom with *75  have reflexive := Subset.reflexive at I76  have finiteImage := Finite.function_image with assignment, finite, reflexive77  have algebraic := AlgebraicallyIndependent.maximal_generators_algebraic with *78  exact AlgebraicOver.finite_principal_integral with *7980theorem AlgebraicallyIndependent.maximal_finite_module81  requires finite : Finite(I)82  requires generates : algebraAdjoin(f, R, S, functionImage(v, I, S)) = S83  shows ∃ s ∈ Q, s ≠ Q[0] ∧ (∃ T,84    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))) ∧85    FiniteAlgebraModule(identity(T), T, S))86proof87  have target := IsField.comm_ring with field88  have sourceQ : IsCommRing(Q)89    exact polynomials.comm_ring with *90  have data := independent91  have restricted := data.right.left92  have injective := data.right.right93  have evaluation : IsRingHom(polynomialAtOver(M, R, S, f, restrict(v, M)), Q,94    S)95    exact polynomialAtOver.hom with *96  obtain ⟨s, polynomial, nonzero, integral⟩ := AlgebraicallyIndependent.maximal_common_localization at I, M, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, v with *97  have localized := IsRingHom.principal_localization_subring with *98  have powers := IsRingHom.denominator_powers with *99  rw powers at localized100  have imageRing : IsSubring(S, functionImage(polynomialAtOver(M, R, S, f, restrict(v, M)), Q, S))101    exact IsRingHom.image_subring with *102  have function := IsRingHom.function with evaluation103  have image := functionImage.value with *104  have zeroQ : Q[0] ∈ Q by typecheck105  have zero := IsRingHom.zero with evaluation106  have imageNonzero : polynomialAtOver(M, R, S, f, restrict(v, M))(s) ≠ S[0]107    intro vanishes108    have equal : polynomialAtOver(M, R, S, f, restrict(v, M))(s) = polynomialAtOver(M, R, S, f, restrict(v, M))(Q[0])109      cc110    have original := Injective.apply_cancel with injective, polynomial, equal111    exact nonzero with original112  have denominators := denominatorPowers.denominators with *113  have contains := localizationWithin.contains with target, imageRing, denominators114  have coefficientImage := polynomialAtOver.coefficient_image at M, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, restrict(v, M) with *115  have coefficients := Subset.transitive with coefficientImage, contains116  have reflexive := Subset.reflexive at I117  have finiteImage := Finite.function_image with assignment, finite, reflexive118  have bounded := functionImage.subset at v, I, S119  have finiteModule := integralGenerators.finite_module_enlarged with *120  refine ⟨s, polynomial, nonzero, localizationWithin(S, functionImage(polynomialAtOver(M, R, S, f, restrict(v, M)), Q, S), denominatorPowers(S, polynomialAtOver(M, R, S, f, restrict(v, M))(s))), rfl, finiteModule⟩121122end Families123