Grace/Cumulus/Algebra/Field/FiniteAlgebraicLocalization.g17
Open in Workbench Download source
Imports
AlgebraicLocalization
Declarations
Source
1234567module Grace.Cumulus.Algebra.Field.FiniteAlgebraicLocalization8import AlgebraicLocalization910section Fields11variable (A add z neg mul one B plus o minus times unit f K : Set)12notation ring R := (A, add, z, neg, mul, one)13notation ring S := (B, plus, o, minus, times, unit)14hypothesis source : IsCommRing(R)15hypothesis field : IsField(S)16hypothesis hom : IsRingHom(f, R, S)17hypothesis injective : InjectiveBetween(f, R, S)18hypothesis algebraic : ∀ x ∈ K, AlgebraicOver(f, R, S, x)1920theorem algebraicList.common_leading_multiple (xs : List(K))21 shows ∃ s ∈ R, s ≠ R[0] ∧ (∀ x ∈ listSupport{K}(xs), ∃ a ∈ R, ∃ b ∈ R,22 R[a * b] = s ∧ (∃ cs, List(A, cs) ∧ polynomialHorner{A}(f, plus, times, x, a, cs) = o))23proof24 induction xs25 | List.nil =>26 have domain : IsIntegralDomain(R)27 exact IsRingHom.domain_of_field_embedding with *28 have nontrivial := IsIntegralDomain.nontrivial with domain29 have distinct := Nontrivial.distinct with nontrivial30 have oneIn : R[1] ∈ R by typecheck31 have oneNonzero : R[1] ≠ R[0]32 intro equal33 apply distinct34 cc35 refine ⟨R[1], oneIn, oneNonzero, ?_⟩36 intros x member37 rw listSupport at member38 exfalso39 exact set.empty with member40 | List.cons(x, tail) using ih =>41 have ordinary := IsCommRing.ring with source42 have domain : IsIntegralDomain(R)43 exact IsRingHom.domain_of_field_embedding with *44 have noZero := IsIntegralDomain.no_zero_divisors with domain45 have member : x ∈ K by assumption46 have root := algebraic with x, member47 obtain ⟨a, aIn, nonzeroA, cs, list, relation⟩ := root.right48 obtain ⟨s, sIn, nonzeroS, previous⟩ := ih49 have product := IsRing.mul_closed with ordinary, aIn, sIn50 have nonzero : R[a * s] ≠ R[0]51 intro vanishes52 have alternatives := noZero with a, aIn, s, sIn, vanishes53 tauto54 refine ⟨R[a * s], product, nonzero, ?_⟩55 intros y inList56 rw listSupport at inList57 have alternatives := insert.membership.forward with inList58 cases alternatives with same | inTail59 . have relationY : polynomialHorner{A}(f, plus, times, y, a, cs) = o60 rwa same61 refine ⟨a, aIn, s, sIn, rfl, cs, list, relationY⟩62 . obtain ⟨c, cIn, b, bIn, divides, ds, listD, relationD⟩ := previous with y, inTail63 have factor := IsRing.mul_closed with ordinary, aIn, bIn64 have equality : R[c * (a * b)] = R[a * s]65 have rearrange : R[c * (a * b)] = R[a * (c * b)] by ring66 rw [rearrange, divides]67 rfl68 refine ⟨c, cIn, R[a * b], factor, equality, ds, listD, relationD⟩6970theorem AlgebraicOver.finite_principal_integral71 requires finite : Finite(K)72 shows ∃ s ∈ R, s ≠ R[0] ∧ (∀ x ∈ K,73 IntegralOver(identity(localizationWithin(S, functionImage(f, R, S), denominatorPowers(S, f(s)))), localizationWithin(S, functionImage(f, R, S), denominatorPowers(S, f(s))), S, x))74proof75 have target := IsField.comm_ring with field76 have ordinary := IsCommRing.ring with target77 have function := IsRingHom.function with hom78 have imageRing : IsSubring(S, functionImage(f, R, S))79 exact IsRingHom.image_subring with *80 obtain ⟨xs, list, covers⟩ := Finite.list_cover with finite81 obtain ⟨s, sIn, nonzero, witnesses⟩ := algebraicList.common_leading_multiple at A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, K, xs with *82 have zeroIn : R[0] ∈ R by typecheck83 have zero := IsRingHom.zero with hom84 have image := IsRingHom.closed with hom, sIn85 have inImage := functionImage.value at f, R, S, s with *86 have imageNonzero : f(s) ≠ S[0]87 intro vanishes88 have equal : f(s) = f(R[0]) by cc89 have original := Injective.apply_cancel with injective, sIn, equal90 exact nonzero with original91 have denominators := denominatorPowers.denominators with *92 have localized := localizationWithin.subring with target, imageRing, denominators93 have contains := localizationWithin.contains with target, imageRing, denominators94 have coefficients : ∀ c ∈ R, f(c) ∈ localizationWithin(S, functionImage(f, R, S), denominatorPowers(S, f(s)))95 intros c member96 have value := functionImage.value at f, R, S, c with *97 exact contains with f(c), value98 obtain ⟨y, inverse⟩ := IsField.inverse_exists at B, plus, o, minus, times, unit, f(s) with *99 have power : monoidPow(S, f(s), (1:Nat)) = f(s)100 rw [monoidPow.succ, monoidPow.zero]101 ring102 have natural := Naturals.constructor.succ with Naturals.constructor.zero103 have denominator : f(s) ∈ denominatorPowers(S, f(s))104 apply denominatorPowers.membership.backward105 refine ⟨image, (1:Nat), natural, ?_⟩106 symm107 exact power108 have inverseIn := localizationWithin.inverse_mem with target, imageRing, denominators, denominator, inverse109 have data := inverse110 have yIn := data.right.left111 have cancels := data.right.right.right112 have multiplication := IsSubring.mul_closed with localized113 refine ⟨s, sIn, nonzero, ?_⟩114 intros x inK115 have inList : x ∈ listSupport{K}(xs) by exact covers with x, inK116 obtain ⟨a, aIn, b, bIn, divides, cs, listC, relation⟩ := witnesses with x, inList117 have algebraicX := algebraic with x, inK118 have element := algebraicX.left119 have imageA := IsRingHom.closed with hom, aIn120 have imageB := IsRingHom.closed with hom, bIn121 have coefficientB := coefficients with b, bIn122 have candidateIn := ClosedBinary.mem with multiplication, coefficientB, inverseIn123 have candidate := IsRing.mul_closed with ordinary, imageB, yIn124 have mapped := IsRingHom.mul with hom, aIn, bIn125 have leadingInverse : S[f(a) * (f(b) * y)] = S[1]126 have rearrange : S[f(a) * (f(b) * y)] = S[(f(a) * f(b)) * y] by ring127 rwa [rearrange, ← mapped, divides]128 have inverseLeading : IsInverse(B, times, unit, f(a), S[f(b) * y])129 unfold IsInverse130 refine ⟨imageA, candidate, ?_⟩131 constructor132 . have commute : S[(f(b) * y) * f(a)] = S[f(a) * (f(b) * y)]133 ring134 rwa commute135 . exact leadingInverse136 exact IntegralOver.of_invertible_leading with *137138end Fields139