Grace/Cumulus/Algebra/Field/Rigidity.g17

Open in Workbench Download source

Imports

AlgebraicClosure · Polynomial.HornerHom

Declarations

Source

1-- Algebraic elements over an algebraically closed field lie in its image.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.Rigidity8import AlgebraicClosure9import Polynomial.HornerHom1011section Fields12variable (A add zero neg mul one B plus z minus times unit f x : Set)13notation ring R := (A, add, zero, neg, mul, one)14notation ring S := (B, plus, z, minus, times, unit)15hypothesis closed : IsAlgebraicallyClosed(R)16hypothesis field : IsField(S)17hypothesis hom : IsRingHom(f, R, S)18hypothesis element : x ∈ S1920theorem monicValue.root_nonempty (cs : List(A))21  requires root : monicValue{A}(f, plus, times, unit, x, cs) = S[0]22  shows cs ≠ []23proof24  intro empty25  rw [empty, monicValue] at root26  have nontrivial := IsField.nontrivial with field27  have distinct := Nontrivial.distinct with nontrivial28  apply distinct29  symm30  exact root3132-- Dividing by a base-field root lowers the degree. A field has no zero divisors,33-- so either x is that root's image or the quotient still vanishes at x.34theorem monicValue.root_in_image_of_length (n : Nat) (cs : List(A))35  requires size : length{A}(cs) = n36  requires root : monicValue{A}(f, plus, times, unit, x, cs) = S[0]37  shows ∃ a ∈ R, f(a) = x38proof39  induction n generalizing cs40  | zero =>41    intros cs list size root42    have nonempty := monicValue.root_nonempty at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x, cs with *43    have alternatives := List.cases with list44    cases alternatives with empty | cons45    . exfalso46      exact nonempty with empty47    . obtain ⟨c, coefficient, tail, tailList, shape⟩ := cons48      rw shape at size49      rw length.cons at size50      exfalso51      apply Naturals.disjoint.zero.succ at length{A}(tail)52      symm53      exact size54  | succ(k) using ih =>55    intros cs list size root56    have nonempty := monicValue.root_nonempty at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x, cs with *57    have alternatives := List.cases with list58    cases alternatives with empty | cons59    . exfalso60      exact nonempty with empty61    . obtain ⟨c, coefficient, tail, tailList, shape⟩ := cons62      have tailSize : length{A}(tail) = k63        rw shape at size64        rw length.cons at size65        exact Naturals.injective.succ with size66      obtain ⟨a, center, baseRoot⟩ := IsAlgebraicallyClosed.root at A, add, zero, neg, mul, one, cs with *67      have baseField := IsAlgebraicallyClosed.field with closed68      have source := IsField.comm_ring with baseField69      have ordinary := IsCommRing.ring with source70      have multiplicative := IsRing.multiplicative with ordinary71      have initial := IsMonoid.unit_in_carrier with multiplicative72      have target := IsField.comm_ring with field73      have targetRing := IsCommRing.ring with target74      have imageA := IsRingHom.closed with hom, center75      have imageOne := IsRingHom.closed with hom, initial76      have oneValue := IsRingHom.one with hom77      have zeroValue := IsRingHom.zero with hom78      have quotient := hornerQuotient.closed at A, add, zero, neg, mul, one, one, a, tail with *79      have quotientLength := hornerQuotient.length at A, add, zero, neg, mul, one, one, a, tail with *80      have quotientSize : length{A}(hornerQuotient{A}(add, mul, one, a, tail)) = k by cc81      have division := hornerValue.synthetic_division at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, one, a, x, c, tail with *82      have baseValue : hornerAt{A}(add, mul, one, a, c :: tail) = R[0]83        rw shape at baseRoot84        simp [hornerAt]85      rw oneValue at division86      rw baseValue at division87      rw zeroValue at division88      rw shape at root89      rw root at division90      have value := hornerValue.closed at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x, f(one), hornerQuotient{A}(add, mul, one, a, tail) with *91      rw oneValue at value92      have negative := IsRing.neg_closed with targetRing, imageA93      have difference := IsRing.add_closed with targetRing, element, negative94      have productZero : S[(x - f(a)) * monicValue{A}(f, plus, times, unit, x, hornerQuotient{A}(add, mul, one, a, tail))] = S[0]95        linear_combination -division96      have noZero := IsField.no_zero_divisors with field97      have factors := noZero with S[x - f(a)], difference, monicValue{A}(f, plus, times, unit, x, hornerQuotient{A}(add, mul, one, a, tail)), value, productZero98      cases factors with same | remaining99      . have equal : f(a) = x100          linear_combination -same101        refine ⟨a, center, equal⟩102      . exact ih with hornerQuotient{A}(add, mul, one, a, tail), quotient, quotientSize, remaining103104theorem monicValue.root_in_image (cs : List(A))105  requires root : monicValue{A}(f, plus, times, unit, x, cs) = S[0]106  shows ∃ a ∈ R, f(a) = x107proof108  have size : length{A}(cs) = length{A}(cs) by rfl109  exact monicValue.root_in_image_of_length with *110111end Fields112113section Extensions114variable (A add zero neg mul one B plus z minus times unit f : Set)115notation ring R := (A, add, zero, neg, mul, one)116notation ring S := (B, plus, z, minus, times, unit)117118theorem IsAlgebraicallyClosed.algebraic_in_image (x : Set)119  requires closed : IsAlgebraicallyClosed(R)120  requires field : IsField(S)121  requires hom : IsRingHom(f, R, S)122  requires algebraic : AlgebraicOver(f, R, S, x)123  shows ∃ a ∈ R, f(a) = x124proof125  have baseField := IsAlgebraicallyClosed.field with closed126  have target := IsField.comm_ring with field127  have integral := AlgebraicOver.integral with baseField, target, hom, algebraic128  have element := integral.left129  obtain ⟨cs, list, root⟩ := integral.right130  exact monicValue.root_in_image with *131132-- There are no proper algebraic field extensions of an algebraically closed field.133theorem IsAlgebraicallyClosed.algebraic_extension_surjective134  requires closed : IsAlgebraicallyClosed(R)135  requires field : IsField(S)136  requires hom : IsRingHom(f, R, S)137  requires algebraic : ∀ y ∈ S, AlgebraicOver(f, R, S, y)138  shows SurjectiveBetween(f, R, S)139proof140  have function := IsRingHom.function with hom141  unfold SurjectiveBetween142  refine ⟨function, ?_⟩143  intros y member144  have relation := algebraic with y, member145  obtain ⟨a, inR, value⟩ := IsAlgebraicallyClosed.algebraic_in_image at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, y with *146  have graph := FunctionBetween.relates_apply with function, inR147  rw value at graph148  refine ⟨a, inR, graph⟩149150end Extensions151