Grace/Cumulus/Algebra/Polynomial/Generation.g17

Open in Workbench Download source

Imports

Constants · MonomialGeneration · Adjoin

Declarations

Source

1-- Polynomial algebras are generated by their variables over the coefficients (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.Polynomial.Generation8import Constants9import MonomialGeneration10import Adjoin1112defgraph polynomialVariables (I A zero one : Set) (j ∈ I) : polynomials(I, A, zero) := polynomialVariable(I, A, zero, one, j)13requires zeroIn : zero ∈ A14requires oneIn : one ∈ A15proof16  exact polynomialVariable.member at I, A, zero, one, j with *1718notation scoped polynomialVariables(I, R) => polynomialVariables(I, R.carrier, R.zero, R.one)1920def polynomialGenerators (I A zero one : Set) : Set :=21  functionImage(polynomialVariables(I, A, zero, one), I, polynomials(I, A, zero))2223notation scoped polynomialGenerators(I, R) => polynomialGenerators(I, R.carrier, R.zero, R.one)2425def subalgebraMonomials (I A zero one T : Set) : Set :=26  {m ∈ monomials(I) | polynomialTerm(I, A, zero, one, m) ∈ T}2728section Polynomials29variable (I A add zero neg mul one : Set)30notation ring R := (A, add, zero, neg, mul, one)31notation ring P := R[I]32hypothesis ring : IsCommRing(R)3334theorem polynomialGenerators.subset35  shows polynomialGenerators(I, R) ⊆ P36proof37  unfold polynomialGenerators38  exact functionImage.subset3940theorem polynomialGenerators.variable (j : Set)41  requires index : j ∈ I42  shows polynomialVariable(I, R, j) ∈ polynomialGenerators(I, R)43proof44  have ordinary := IsCommRing.ring with ring45  have zeroIn := IsRing.zero_in_carrier with ordinary46  have multiplicative := IsRing.multiplicative with ordinary47  have oneIn := IsMonoid.unit_in_carrier with multiplicative48  have function := polynomialVariables.function at I, A, zero, one with *49  have member := functionImage.value with *50  have value := polynomialVariables.value at I, A, zero, one, j with *51  rw value at member52  unfold polynomialGenerators53  exact member5455section Subalgebras56variable (T : Set)57hypothesis subalgebra : Subalgebra(polynomialCoefficients(I, R), R, P, T)5859theorem polynomialSubalgebra.constant (a : Set)60  requires coefficient : a ∈ R61  shows polynomialConstant(I, R, a) ∈ T62proof63  have ordinary := IsCommRing.ring with ring64  have zeroIn := IsRing.zero_in_carrier with ordinary65  have function := polynomialCoefficients.function at I, A, zero with *66  have value := polynomialCoefficients.value at I, A, zero, a with *67  have image := functionImage.value at polynomialCoefficients(I, R), A, P, a with *68  have contains := subalgebra.right69  have member := contains with polynomialCoefficients(I, R)(a), image70  rwa value at member7172hypothesis variables : ∀ j ∈ I, polynomialVariable(I, R, j) ∈ T7374theorem polynomialSubalgebra.monomial (m : Set)75  requires monomial : m ∈ monomials(I)76  shows polynomialTerm(I, A, zero, one, m) ∈ T77proof78  have ordinary := IsCommRing.ring with ring79  have zeroIn := IsRing.zero_in_carrier with ordinary80  have multiplicative := IsRing.multiplicative with ordinary81  have oneIn := IsMonoid.unit_in_carrier with multiplicative82  have structure := subalgebra83  have subring := structure.left84  have closed := IsSubring.mul_closed with subring85  have base : monomialOne(I) ∈ subalgebraMonomials(I, A, zero, one, T)86    have unit := monomialOne.member at I87    have constant := polynomialSubalgebra.constant at I, A, add, zero, neg, mul, one, T, one with *88    unfold polynomialConstant at constant89    exact subalgebraMonomials.membership.backward with ⟨unit, constant⟩90  have generators : ∀ j ∈ I, monomialVariable(I, j) ∈ subalgebraMonomials(I, A, zero, one, T)91    intros j hj92    have member := monomialVariable.member at I, j93    have variable := variables with j, hj94    unfold polynomialVariable at variable95    exact subalgebraMonomials.membership.backward with ⟨member, variable⟩96  have products : ∀ u ∈ subalgebraMonomials(I, A, zero, one, T), ∀ v ∈ subalgebraMonomials(I, A, zero, one, T), monomialProduct(I, u, v) ∈ subalgebraMonomials(I, A, zero, one, T)97    intros u hm v hn98    obtain ⟨memberM, termM⟩ := subalgebraMonomials.membership.forward with hm99    obtain ⟨memberN, termN⟩ := subalgebraMonomials.membership.forward with hn100    have product := monomialProduct.member at I, u, v with *101    have first := polynomialTerm.member at I, A, zero, one, u with *102    have second := polynomialTerm.member at I, A, zero, one, v with *103    have member := ClosedBinary.mem with closed, termM, termN104    have applied := polynomialMul.apply at I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, one, u), polynomialTerm(I, A, zero, one, v) with *105    have multiplied := polynomialProduct.terms at I, A, add, zero, neg, mul, one, one, one, u, v with *106    have unit : R[1 * 1] = R[1] by ring107    rw [applied, multiplied, unit] at member108    exact subalgebraMonomials.membership.backward with ⟨product, member⟩109  have generated := monomials.induction with *110  have result := subalgebraMonomials.membership.forward with generated111  exact result.right112113theorem polynomialSubalgebra.term (a m : Set)114  requires coefficient : a ∈ R115  requires monomial : m ∈ monomials(I)116  shows polynomialTerm(I, A, zero, a, m) ∈ T117proof118  have ordinary := IsCommRing.ring with ring119  have zeroIn := IsRing.zero_in_carrier with ordinary120  have multiplicative := IsRing.multiplicative with ordinary121  have oneIn := IsMonoid.unit_in_carrier with multiplicative122  have constant := polynomialSubalgebra.constant at I, A, add, zero, neg, mul, one, T, a with *123  have term := polynomialSubalgebra.monomial with *124  have structure := subalgebra125  have closed := IsSubring.mul_closed with structure.left126  have member := ClosedBinary.mem with closed, term, constant127  have first := polynomialTerm.member at I, A, zero, one, m with *128  have second := polynomialTerm.member at I, A, zero, a, monomialOne(I) with *129  have unitMonomial := monomialOne.member at I130  unfold polynomialConstant at member131  have applied := polynomialMul.apply at I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, one, m), polynomialTerm(I, A, zero, a, monomialOne(I)) with *132  have multiplied := polynomialProduct.terms at I, A, add, zero, neg, mul, one, one, a, m, monomialOne(I) with *133  have coefficientUnit : R[1 * a] = a by ring134  have monomialUnit := monomialProduct.one at I, m with *135  rwa [applied, multiplied, coefficientUnit, monomialUnit] at member136137theorem polynomialSubalgebra.eq_carrier138  shows T = P139proof140  have structure := subalgebra141  have subring := structure.left142  have subset := IsSubring.subset_carrier with subring143  have base := IsSubring.zero_closed with subring144  have closed := IsSubring.add_closed with subring145  have terms : ∀ a ∈ A, ∀ m ∈ monomials(I), polynomialTerm(I, A, zero, a, m) ∈ T146    intros a ha m hm147    exact polynomialSubalgebra.term with *148  have sums : ∀ p ∈ T, ∀ q ∈ T, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q) ∈ T149    intros p hp q hq150    have included := subset151    have first := included with p, hp152    have second := included with q, hq153    have member := ClosedBinary.mem with closed, hp, hq154    have applied := polynomialAdd.apply at I, A, add, zero, neg, mul, one, p, q with *155    rwa applied at member156  apply Subset.antisymmetric with subset157  intros p hp158  exact polynomials.induction with *159160end Subalgebras161162theorem polynomialGenerators.adjoin163  shows algebraAdjoin(polynomialCoefficients(I, R), R, P, polynomialGenerators(I, R)) = P164proof165  have target := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *166  have hom := polynomialCoefficients.hom at I, A, add, zero, neg, mul, one with *167  have bounded := polynomialGenerators.subset at I, A, add, zero, neg, mul, one with *168  have subalgebra := algebraAdjoin.subalgebra with ring, target, hom, bounded169  have included := algebraAdjoin.contains with ring, target, hom, bounded170  have variables : ∀ j ∈ I, polynomialVariable(I, R, j) ∈ algebraAdjoin(polynomialCoefficients(I, R), R, P, polynomialGenerators(I, R))171    intros j hj172    have generator := polynomialGenerators.variable at I, A, add, zero, neg, mul, one, j with *173    exact included with polynomialVariable(I, R, j), generator174  exact polynomialSubalgebra.eq_carrier with ring, subalgebra, variables175176end Polynomials177