Grace/Cumulus/Algebra/MonicRelations.g17

Open in Workbench Download source

Imports

LinearSpan · Cardinal.ListSupport

Declarations

Source

1-- Monic polynomial relations in an algebra, evaluated by Horner's rule (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.MonicRelations8import LinearSpan9import Cardinal.ListSupport1011-- [a0, ..., a(n-1)] represents a0 + a1 X + ... + X^n; [] represents 1.12def monicValue {A : Set} (f plus times unit x : Set) (cs : List(A)) → Set13  | f, plus, times, unit, x, List.nil => unit14  | f, plus, times, unit, x, List.cons(a, tail) => plus(f(a), times(x, monicValue(f, plus, times, unit, x, tail)))15  descends cs1617notation scoped monicValue(R, f, S, x, cs) => monicValue(R.carrier, f, S.add, S.mul, S.one, x, cs)1819-- All the successive Horner tails; this is a finite set, without choosing an enumeration.20def monicTailSet {A : Set} (f plus times unit x : Set) (cs : List(A)) → Set21  | f, plus, times, unit, x, List.nil => {unit}22  | f, plus, times, unit, x, List.cons(a, tail) => insert(monicValue(f, plus, times, unit, x, a :: tail), monicTailSet(f, plus, times, unit, x, tail))23  descends cs2425notation scoped monicTailSet(R, f, S, x, cs) => monicTailSet(R.carrier, f, S.add, S.mul, S.one, x, cs)2627predicate IntegralOver (f A B plus z times unit x : Set) :=28  x ∈ B ∧ ∃ cs, List(A, cs) ∧ monicValue{A}(f, plus, times, unit, x, cs) = z2930notation scoped IntegralOver(f, R, S, x) => IntegralOver(f, R.carrier, S.carrier, S.add, S.zero, S.mul, S.one, x)3132theorem monicTailSet.finite (A f plus times unit x : Set) (cs : List(A))33  shows Finite(monicTailSet{A}(f, plus, times, unit, x, cs))34proof35  induction cs36  | List.nil =>37    rw monicTailSet38    exact Finite.singleton39  | List.cons(a, tail) using ih =>40    rw monicTailSet41    exact Finite.insert with ih4243theorem monicTailSet.unit (A f plus times unit x : Set) (cs : List(A))44  shows unit ∈ monicTailSet{A}(f, plus, times, unit, x, cs)45proof46  induction cs47  | List.nil =>48    rw monicTailSet49    simp50  | List.cons(a, tail) using ih =>51    rw monicTailSet52    exact insert.contains with ih5354theorem monicTailSet.head (A f plus times unit x : Set) (cs : List(A))55  shows monicValue{A}(f, plus, times, unit, x, cs) ∈ monicTailSet{A}(f, plus, times, unit, x, cs)56proof57  induction cs58  | List.nil =>59    rw [monicTailSet, monicValue]60    simp61  | List.cons(a, tail) using ih =>62    rw monicTailSet63    exact insert.self6465section Algebras66variable (A add zero neg mul one B plus z minus times unit f x : Set)67notation ring R := (A, add, zero, neg, mul, one)68notation ring S := (B, plus, z, minus, times, unit)69hypothesis source : IsCommRing(R)70hypothesis target : IsCommRing(S)71hypothesis hom : IsRingHom(f, R, S)72hypothesis element : x ∈ S7374theorem monicValue.closed (cs : List(A))75  shows monicValue{A}(f, plus, times, unit, x, cs) ∈ S76proof77  induction cs78  | List.nil =>79    rw monicValue80    have ordinary := IsCommRing.ring with target81    have monoid := IsRing.multiplicative with ordinary82    exact IsMonoid.unit_in_carrier with monoid83  | List.cons(a, tail) using ih =>84    have ordinary := IsCommRing.ring with target85    have coefficient : a ∈ R by assumption86    have scalar := IsRingHom.closed with hom, coefficient87    have product := IsRing.mul_closed with ordinary, element, ih88    rw monicValue89    exact IsRing.add_closed with ordinary, product9091theorem monicTailSet.subset (cs : List(A))92  shows monicTailSet{A}(f, plus, times, unit, x, cs) ⊆ S93proof94  induction cs95  | List.nil =>96    have unitIn := monicValue.closed at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x, [] with *97    rw monicValue at unitIn98    rw monicTailSet99    intros u hu100    have equal := singleton.membership.forward with hu101    rwa equal102  | List.cons(a, tail) using ih =>103    have head := monicValue.closed at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x, a :: tail with *104    rw monicTailSet105    intros u hu106    have alternatives := insert.membership.forward with hu107    cases alternatives with equal | old108    . rw equal109      exact head110    . exact ih with u, old111112theorem monicValue.in_subalgebra (T : Set) (cs : List(A))113  requires subalgebra : Subalgebra(f, R, S, T)114  requires member : x ∈ T115  shows monicValue{A}(f, plus, times, unit, x, cs) ∈ T116proof117  induction cs118  | List.nil =>119    have subring := Subalgebra.subring with source, target, hom, subalgebra120    rw monicValue121    exact IsSubring.one_closed with subring122  | List.cons(a, tail) using ih =>123    have subring := Subalgebra.subring with source, target, hom, subalgebra124    have coefficients := Subalgebra.coefficients with source, target, hom, subalgebra125    have function := IsRingHom.function with hom126    have image := functionImage.value with *127    have scalar := coefficients with f(a), image128    have multiplication := IsSubring.mul_closed with subring129    have addition := IsSubring.add_closed with subring130    have product := ClosedBinary.mem with multiplication, member, ih131    rw monicValue132    exact ClosedBinary.mem with addition, scalar, product133134theorem monicTailSet.in_subalgebra (T : Set) (cs : List(A))135  requires subalgebra : Subalgebra(f, R, S, T)136  requires member : x ∈ T137  shows monicTailSet{A}(f, plus, times, unit, x, cs) ⊆ T138proof139  induction cs140  | List.nil =>141    have subring := Subalgebra.subring with source, target, hom, subalgebra142    have unitIn := IsSubring.one_closed with subring143    rw monicTailSet144    intros u hu145    have equal := singleton.membership.forward with hu146    rwa equal147  | List.cons(a, tail) using ih =>148    have head := monicValue.in_subalgebra at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x, T, a :: tail with *149    rw monicTailSet150    intros u hu151    have alternatives := insert.membership.forward with hu152    cases alternatives with equal | old153    . rw equal154      exact head155    . exact ih with u, old156157theorem IntegralOver.of_square (a : Set)158  requires coefficient : a ∈ R159  requires quadratic : S[x * x] = f(a)160  shows IntegralOver(f, R, S, x)161proof162  have ordinary := IsCommRing.ring with source163  have zeroIn := IsRing.zero_in_carrier with ordinary164  have negative := IsRing.neg_closed with ordinary, coefficient165  have mappedZero := IsRingHom.zero with hom166  have mappedNeg := IsRingHom.neg with hom, coefficient167  have image := IsRingHom.closed with hom, coefficient168  have list : List(A, [R[-a], R[0]]) by typecheck169  have relation : monicValue(R, f, S, x, [R[-a], R[0]]) = S[0]170    rw [monicValue, monicValue, monicValue, mappedNeg, mappedZero]171    have normalize : S[(-f(a)) + x * (0 + x * 1)] = S[x * x - f(a)] by ring172    rw [normalize, quadratic]173    ring174  unfold IntegralOver175  refine ⟨element, [R[-a], R[0]], list, relation⟩176177end Algebras178179section Coefficients180variable (A add zero neg mul one B plus z minus times unit f : Set)181notation ring R := (A, add, zero, neg, mul, one)182notation ring S := (B, plus, z, minus, times, unit)183hypothesis source : IsCommRing(R)184hypothesis target : IsCommRing(S)185hypothesis hom : IsRingHom(f, R, S)186187theorem IntegralOver.coefficient (a : Set)188  requires coefficient : a ∈ R189  shows IntegralOver(f, R, S, f(a))190proof191  have ordinary := IsCommRing.ring with source192  have negative := IsRing.neg_closed with ordinary, coefficient193  have element := IsRingHom.closed with hom, coefficient194  have mapped := IsRingHom.neg with hom, coefficient195  have list : List(A, [R[-a]]) by typecheck196  have relation : monicValue{A}(f, plus, times, unit, f(a), [R[-a]]) = S[0]197    rw [monicValue, monicValue, mapped]198    ring199  unfold IntegralOver200  refine ⟨element, [R[-a]], list, relation⟩201202end Coefficients203