Grace/Cumulus/Algebra/Field/Algebraic.g17

Open in Workbench Download source

Imports

IntegralAdjoin · Construction · Ring.FiniteSum

Declarations

Source

1-- Algebraic elements over a field satisfy monic relations and generate finite modules.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.Algebraic8import IntegralAdjoin9import Construction10import Ring.FiniteSum1112-- Horner evaluation with explicit nonzero leading coefficient a. The list13-- contains the lower coefficients in ascending order, so trailing zeros pose14-- no ambiguity about which coefficient is asserted to be nonzero.15def polynomialHorner {A : Set} (f plus times x a : Set) (cs : List(A)) : Set :=16  monicValue{A}(f, plus, times, f(a), x, cs)1718predicate AlgebraicOver (f A zero B plus z times x : Set) :=19  x ∈ B ∧ ∃ a ∈ A, a ≠ zero ∧ ∃ cs, List(A, cs) ∧ polynomialHorner{A}(f, plus, times, x, a, cs) = z2021notation scoped AlgebraicOver(f, R, S, x) => AlgebraicOver(f, R.carrier, R.zero, S.carrier, S.add, S.zero, S.mul, x)2223section Evaluation24variable (A add zero neg mul one B plus z minus times unit f x : Set)25notation ring R := (A, add, zero, neg, mul, one)26notation ring S := (B, plus, z, minus, times, unit)27hypothesis source : IsCommRing(R)28hypothesis target : IsCommRing(S)29hypothesis hom : IsRingHom(f, R, S)30hypothesis element : x ∈ S3132theorem hornerValue.closed (leading : Set) (cs : List(A))33  requires coefficient : leading ∈ S34  shows monicValue{A}(f, plus, times, leading, x, cs) ∈ S35proof36  induction cs37  | List.nil =>38    rwa monicValue39  | List.cons(a, tail) using ih =>40    have aIn : a ∈ A by assumption41    have image := IsRingHom.closed with hom, aIn42    have ordinary := IsCommRing.ring with target43    have product := IsRing.mul_closed with ordinary, element, ih44    rw monicValue45    exact IsRing.add_closed with ordinary, product4647theorem hornerValue.scale (c leading : Set) (cs : List(A))48  requires coefficient : c ∈ R49  requires initial : leading ∈ S50  shows monicValue{A}(f, plus, times, S[f(c) * leading], x, ringScale{A}(mul, c, cs)) = S[f(c) * monicValue{A}(f, plus, times, leading, x, cs)]51proof52  induction cs53  | List.nil =>54    rw [ringScale, monicValue, monicValue]55    rfl56  | List.cons(a, tail) using ih =>57    have aIn : a ∈ R by assumption58    have ordinary := IsCommRing.ring with source59    have scaleClosed : ∀ u ∈ A, R[c * u] ∈ A60      intros u hu61      exact IsRing.mul_closed with ordinary, coefficient, hu62    have product := IsRing.mul_closed with ordinary, coefficient, aIn63    have imageC := IsRingHom.closed with hom, coefficient64    have imageA := IsRingHom.closed with hom, aIn65    have mapped := IsRingHom.mul with hom, coefficient, aIn66    have value := hornerValue.closed at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x, leading, tail with *67    rw [ringScale, monicValue, monicValue, ih, mapped]68    ring6970end Evaluation7172section Fields73variable (A add zero neg mul one B plus z minus times unit f x : Set)74notation ring R := (A, add, zero, neg, mul, one)75notation ring S := (B, plus, z, minus, times, unit)76hypothesis field : IsField(R)77hypothesis target : IsCommRing(S)78hypothesis hom : IsRingHom(f, R, S)7980theorem IntegralOver.algebraic81  requires integral : IntegralOver(f, R, S, x)82  shows AlgebraicOver(f, R, S, x)83proof84  have source := IsField.comm_ring with field85  have nontrivial := IsField.nontrivial with field86  have distinct := Nontrivial.distinct with nontrivial87  have ordinary := IsCommRing.ring with source88  have monoid := IsRing.multiplicative with ordinary89  have oneIn := IsMonoid.unit_in_carrier with monoid90  have nonzero : one ≠ zero91    intro equal92    have impossible : zero = one by cc93    exact distinct with impossible94  have oneValue := IsRingHom.one with hom95  obtain ⟨cs, list, relation⟩ := integral.right96  have equation : polynomialHorner{A}(f, plus, times, x, one, cs) = S[0]97    simp [polynomialHorner]98  unfold AlgebraicOver99  refine ⟨integral.left, one, oneIn, nonzero, cs, list, equation⟩100101theorem AlgebraicOver.integral102  requires algebraic : AlgebraicOver(f, R, S, x)103  shows IntegralOver(f, R, S, x)104proof105  have source := IsField.comm_ring with field106  have ordinary := IsCommRing.ring with source107  unfold AlgebraicOver at algebraic108  obtain ⟨a, aIn, nonzero, cs, list, relation⟩ := algebraic.right109  obtain ⟨b, inverse⟩ := IsField.inverse_exists at A, add, zero, neg, mul, one, a with *110  unfold IsInverse at inverse111  have bIn := inverse.right.left112  have cancels := inverse.right.right.right113  have mapped := IsRingHom.mul with hom, bIn, aIn114  have oneValue := IsRingHom.one with hom115  have normalizedLeading : S[f(b) * f(a)] = S[1] by cc116  have imageA := IsRingHom.closed with hom, aIn117  have imageB := IsRingHom.closed with hom, bIn118  have scaleClosed : ∀ u ∈ A, R[b * u] ∈ A119    intros u hu120    exact IsRing.mul_closed with ordinary, bIn, hu121  have scaled := ringScale.closed with *122  have identity := hornerValue.scale at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x, b, f(a), cs with *123  rw normalizedLeading at identity124  unfold polynomialHorner at relation125  rw relation at identity126  have annihilate : S[f(b) * 0] = S[0] by ring127  rw annihilate at identity128  unfold IntegralOver129  refine ⟨algebraic.left, ringScale{A}(mul, b, cs), scaled, identity⟩130131theorem AlgebraicOver.iff_integral132  shows AlgebraicOver(f, R, S, x) ↔ IntegralOver(f, R, S, x)133proof134  constructor135  . intro algebraic136    exact AlgebraicOver.integral with field, target, hom, algebraic137  . intro integral138    exact IntegralOver.algebraic with field, target, hom, integral139140theorem AlgebraicOver.finite_adjoin141  requires algebraic : AlgebraicOver(f, R, S, x)142  shows ∃ G, Finite(G) ∧ G ⊆ algebraAdjoin(f, R, S, {x}) ∧ linearSpan(f, R, S, G) = algebraAdjoin(f, R, S, {x})143proof144  have source := IsField.comm_ring with field145  have integral := AlgebraicOver.integral with field, target, hom, algebraic146  have data := integral147  unfold IntegralOver at data148  exact IntegralOver.finite_adjoin with *149150theorem AlgebraicOver.finite_module_of_generates151  requires algebraic : AlgebraicOver(f, R, S, x)152  requires generates : algebraAdjoin(f, R, S, {x}) = S153  shows FiniteAlgebraModule(f, R, S)154proof155  have source := IsField.comm_ring with field156  have integral := AlgebraicOver.integral with field, target, hom, algebraic157  have data := integral158  unfold IntegralOver at data159  exact IntegralOver.finite_module_of_generates with *160161end Fields162