Grace/Cumulus/Algebra/Field/AlgebraicLocalization.g17

Open in Workbench Download source

Imports

HornerRelations · PrincipalLocalization · Set.OrderTransport

Declarations

Source

1-- Algebraic elements become integral after inverting a leading coefficient (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.Field.AlgebraicLocalization8import HornerRelations9import PrincipalLocalization10import Set.OrderTransport1112section Normalization13variable (A add z neg mul one B plus o minus times unit f T x a y : Set)14notation ring R := (A, add, z, neg, mul, one)15notation ring S := (B, plus, o, minus, times, unit)16notation ring L := S ↾ T17hypothesis source : IsCommRing(R)18hypothesis target : IsCommRing(S)19hypothesis hom : IsRingHom(f, R, S)20hypothesis subring : IsSubring(S, T)21hypothesis coefficients : ∀ c ∈ R, f(c) ∈ T22hypothesis element : x ∈ S23hypothesis leading : a ∈ R24hypothesis inverseIn : y ∈ T25hypothesis inverse : IsInverse(B, times, unit, f(a), y)2627theorem IntegralOver.of_invertible_leading (cs : List(A))28  requires relation : polynomialHorner{A}(f, plus, times, x, a, cs) = o29  shows IntegralOver(identity(T), L, S, x)30proof31  have smaller : IsCommRing(L)32    exact IsSubring.comm_ring with *33  have inclusion : IsRingHom(identity(T), L, S)34    exact IsSubring.inclusion_hom with *35  have function := IsRingHom.function with hom36  have corestricted := FunctionBetween.codomain_of_values with function, coefficients37  have agreement : ∀ c ∈ R, f(c) = identity(T)(f(c))38    intros c member39    have inT := coefficients with c, member40    symm41    exact identity.apply with *42  have changed := monicValue.change_coefficients at A, T, plus, times, f, identity(T), f, f(a), x, cs with *43  have identityY := identity.apply at y, T with *44  have data := inverse45  unfold IsInverse at data46  have leadingOne : S[identity(T)(y) * f(a)] = S[1] by cc47  have scaleClosed : ∀ c ∈ T, L[y * c] ∈ T48    intros c member49    have ordinary := IsCommRing.ring with smaller50    exact IsRing.mul_closed with ordinary, inverseIn, member51  have scaled := ringScale.closed at T, restrict(times, T × T), y, listMap{A}(f, cs) with *52  have scaledValue := hornerValue.scale at T, restrict(plus, T × T), o, restrict(minus, T), restrict(times, T × T), unit, B, plus, o, minus, times, unit, identity(T), x, y, f(a), listMap{A}(f, cs) with *53  rw leadingOne at scaledValue54  unfold polynomialHorner at relation55  have vanishes : monicValue{T}(identity(T), plus, times, f(a), x, listMap{A}(f, cs)) = o by cc56  rw vanishes at scaledValue57  have yIn := data.right.left58  have zeroProduct : S[identity(T)(y) * 0] = S[0]59    rw identityY60    ring61  rw zeroProduct at scaledValue62  unfold IntegralOver63  refine ⟨element, ringScale{T}(restrict(times, T × T), y, listMap{A}(f, cs)), scaled, scaledValue⟩6465end Normalization66section Fields67variable (A add z neg mul one B plus o minus times unit f : Set)68notation ring R := (A, add, z, neg, mul, one)69notation ring S := (B, plus, o, minus, times, unit)70hypothesis source : IsCommRing(R)71hypothesis field : IsField(S)72hypothesis hom : IsRingHom(f, R, S)73hypothesis injective : InjectiveBetween(f, R, S)7475theorem IsRingHom.domain_of_field_embedding76  shows IsIntegralDomain(R)77proof78  have zeroIn : R[0] ∈ R by typecheck79  have oneIn : R[1] ∈ R by typecheck80  have zero := IsRingHom.zero with hom81  have one := IsRingHom.one with hom82  have targetNontrivial := IsField.nontrivial with field83  have distinct := Nontrivial.distinct with targetNontrivial84  have sourceDistinct : R[0] ≠ R[1]85    intro equal86    apply distinct87    cc88  have nontrivial : Nontrivial(R)89    unfold Nontrivial90    refine ⟨zeroIn, oneIn, sourceDistinct⟩91  have targetDomain := IsField.no_zero_divisors with field92  have noZero : NoZeroDivisors(A, mul, z)93    intros a ha b hb vanishes94    have mapped := IsRingHom.mul with hom, ha, hb95    have imageA := IsRingHom.closed with hom, ha96    have imageB := IsRingHom.closed with hom, hb97    have productZero : S[f(a) * f(b)] = S[0] by cc98    have alternatives := targetDomain with f(a), f(b), productZero99    cases alternatives with leftZero | rightZero100    . have equal : f(a) = f(R[0])101        cc102      have original := Injective.apply_cancel with injective, ha, equal103      left104      exact original105    . have equal : f(b) = f(R[0])106        cc107      have original := Injective.apply_cancel with injective, hb, equal108      right109      exact original110  unfold IsIntegralDomain111  refine ⟨source, nontrivial, noZero⟩112113theorem AlgebraicOver.exists_principal_integral (x : Set)114  requires algebraic : AlgebraicOver(f, R, S, x)115  shows ∃ a ∈ R, a ≠ R[0] ∧116    IntegralOver(identity(localizationWithin(S, functionImage(f, R, S), denominatorPowers(S, f(a)))), localizationWithin(S, functionImage(f, R, S), denominatorPowers(S, f(a))), S, x)117proof118  have target := IsField.comm_ring with field119  have function := IsRingHom.function with hom120  have imageRing : IsSubring(S, functionImage(f, R, S))121    exact IsRingHom.image_subring with *122  have zeroIn : R[0] ∈ R by typecheck123  have zero := IsRingHom.zero with hom124  have element := algebraic.left125  obtain ⟨a, leading, nonzero, cs, list, relation⟩ := algebraic.right126  have inImage := functionImage.value at f, R, S, a with *127  have image := IsRingHom.closed with hom, leading128  have imageNonzero : f(a) ≠ S[0]129    intro vanishes130    have equal : f(a) = f(R[0]) by cc131    have original := Injective.apply_cancel with injective, leading, equal132    exact nonzero with original133  have denominators := denominatorPowers.denominators with *134  have localized := localizationWithin.subring with target, imageRing, denominators135  have contains := localizationWithin.contains with target, imageRing, denominators136  have coefficients : ∀ c ∈ R, f(c) ∈ localizationWithin(S, functionImage(f, R, S), denominatorPowers(S, f(a)))137    intros c member138    have value := functionImage.value at f, R, S, c with *139    exact contains with f(c), value140  obtain ⟨y, inverse⟩ := IsField.inverse_exists at B, plus, o, minus, times, unit, f(a) with *141  have ordinary := IsCommRing.ring with target142  have monoid := IsRing.multiplicative with ordinary143  have power : monoidPow(S, f(a), (1:Nat)) = f(a)144    rw [monoidPow.succ, monoidPow.zero]145    ring146  have natural := Naturals.constructor.succ with Naturals.constructor.zero147  have denominator : f(a) ∈ denominatorPowers(S, f(a))148    apply denominatorPowers.membership.backward149    refine ⟨image, (1:Nat), natural, ?_⟩150    symm151    exact power152  have inverseIn := localizationWithin.inverse_mem with target, imageRing, denominators, denominator, inverse153  have integral := IntegralOver.of_invertible_leading with *154  refine ⟨a, leading, nonzero, integral⟩155156end Fields157