Grace/Cumulus/Algebra/Polynomial/Universal.g17

Open in Workbench Download source

Imports

Generation · Assignment · Ring.Equalizer

Declarations

Source

1-- Polynomial homomorphisms are determined by coefficients and variable values.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.Universal8import Generation9import Assignment10import Ring.Equalizer1112section Homomorphisms13variable (I A add zero neg mul one B plus z minus times unit f g : Set)14notation ring R := (A, add, zero, neg, mul, one)15notation ring P := R[I]16notation ring S := (B, plus, z, minus, times, unit)17hypothesis ring : IsCommRing(R)18hypothesis first : IsRingHom(f, P, S)19hypothesis second : IsRingHom(g, P, S)2021theorem IsRingHom.polynomial_ext22  requires constants : ∀ a ∈ R, f(polynomialConstant(I, R, a)) = g(polynomialConstant(I, R, a))23  requires variables : ∀ j ∈ I, f(polynomialVariable(I, R, j)) = g(polynomialVariable(I, R, j))24  shows f = g25proof26  have source := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *27  have subring := ringEqualizer.subring with source, first, second28  have ordinary := IsCommRing.ring with ring29  have zeroIn := IsRing.zero_in_carrier with ordinary30  have multiplicative := IsRing.multiplicative with ordinary31  have oneIn := IsMonoid.unit_in_carrier with multiplicative32  have coefficients : functionImage(polynomialCoefficients(I, R), R, P) ⊆ ringEqualizer(f, g, P)33    intros p hp34    obtain ⟨member, a, ha, shape⟩ := functionImage.membership.forward with hp35    have value := polynomialCoefficients.value at I, A, zero, a with *36    have equal := constants with a, ha37    apply ringEqualizer.membership.backward38    constructor39    . exact member40    . cc41  have subalgebra : Subalgebra(polynomialCoefficients(I, R), R, P, ringEqualizer(f, g, P))42    unfold Subalgebra43    refine ⟨subring, coefficients⟩44  have generators : ∀ j ∈ I, polynomialVariable(I, R, j) ∈ ringEqualizer(f, g, P)45    intros j hj46    have member := polynomialVariable.member at I, A, zero, one, j with *47    have equal := variables with j, hj48    exact ringEqualizer.membership.backward with ⟨member, equal⟩49  have all := polynomialSubalgebra.eq_carrier with ring, subalgebra, generators50  have functionF := IsRingHom.function with first51  have functionG := IsRingHom.function with second52  apply FunctionBetween.ext with functionF, functionG53  intros p hp54  have member : p ∈ ringEqualizer(f, g, P) by rwa all55  have data := ringEqualizer.membership.forward with member56  exact data.right5758end Homomorphisms5960-- The assignment induced by any homomorphism back to the coefficient ring.61defgraph polynomialValues (I A add zero neg mul one h : Set) (j ∈ I) : A := h(polynomialVariable(I, A, zero, one, j))62requires ring : IsCommRing(A, add, zero, neg, mul, one)63requires hom : IsRingHom(h, polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), constantFunction(monomials(I), A, zero), polynomialNeg(I, A, add, zero, neg, mul, one), polynomialMul(I, A, add, zero, neg, mul, one), polynomialConstant(I, A, zero, one), A, add, zero, neg, mul, one)64proof65  have ordinary := IsCommRing.ring with ring66  have zeroIn := IsRing.zero_in_carrier with ordinary67  have multiplicative := IsRing.multiplicative with ordinary68  have oneIn := IsMonoid.unit_in_carrier with multiplicative69  have variableMember := polynomialVariable.member at I, A, zero, one, j with *70  exact IsRingHom.closed with hom, variableMember7172notation scoped polynomialValues(I, R, h) => polynomialValues(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, h)7374section Evaluation75variable (I A add zero neg mul one h : Set)76notation ring R := (A, add, zero, neg, mul, one)77notation ring P := R[I]78hypothesis ring : IsCommRing(R)79hypothesis hom : IsRingHom(h, P, R)80hypothesis constants : ∀ a ∈ R, h(polynomialConstant(I, R, a)) = a8182theorem IsRingHom.eq_polynomialAt83  shows h = polynomialAt(I, R, polynomialValues(I, A, add, zero, neg, mul, one, h))84proof85  have assignment := polynomialValues.function at I, A, add, zero, neg, mul, one, h with *86  have evaluation := polynomialAt.hom with *87  have sameConstants : ∀ a ∈ R, h(polynomialConstant(I, R, a)) = polynomialAt(I, R, polynomialValues(I, A, add, zero, neg, mul, one, h))(polynomialConstant(I, R, a))88    intros a ha89    have first := constants with a, ha90    have second := polynomialAt.constant with *91    cc92  have sameVariables : ∀ j ∈ I, h(polynomialVariable(I, R, j)) = polynomialAt(I, R, polynomialValues(I, A, add, zero, neg, mul, one, h))(polynomialVariable(I, R, j))93    intros j hj94    have first := polynomialValues.value at I, A, add, zero, neg, mul, one, h, j with *95    have second := polynomialAt.variable with *96    cc97  exact IsRingHom.polynomial_ext with ring, hom, evaluation, sameConstants, sameVariables9899end Evaluation100