Grace/Cumulus/Algebra/Polynomial/Unit.g17

Open in Workbench Download source

Imports

Distributivity

Declarations

Source

1-- The multiplicative identity for finite polynomial convolution (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.Unit8import Distributivity910theorem polynomialConstant.support (I A zero a : Set)11  requires zeroIn : zero ∈ A12  requires coefficient : a ∈ A13  shows functionSupport(polynomialConstant(I, A, zero, a), monomials(I), zero) ⊆ {monomialOne(I)}14proof15  unfold polynomialConstant16  unfold polynomialTerm17  exact coefficientSingle.support with *1819section Rings20variable (I A add zero neg mul one p : Set)21hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)22hypothesis member : p ∈ polynomials(I, A, zero)23notation ring R := (A, add, zero, neg, mul, one)2425theorem polynomialProduct.one_right26  shows polynomialProduct(I, A, add, zero, neg, mul, one, p, polynomialConstant(I, A, zero, one)) = p27proof28  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 unit := monomialOne.member at I33  have unitPolynomial := polynomialConstant.member at I, A, zero, one with *34  have unitValue := polynomialConstant.coefficient at I, A, zero, one with *35  have unitSupport := polynomialConstant.support at I, A, zero, one with *36  have support := functionSupport.subset at p, monomials(I), zero37  have singletonSubset : {monomialOne(I)} ⊆ monomials(I)38    settle with Subset, singleton.membership39  have finiteSupport := polynomials.finite_support with member40  have finiteSingleton := Finite.singleton at monomialOne(I)41  have finite := Finite.product with finiteSupport, finiteSingleton42  have domain := product.monotone with support, singletonSubset43  have reflexive : functionSupport(p, monomials(I), zero) ⊆ functionSupport(p, monomials(I), zero)44    settle with Subset45  have covers : convolutionPairs(I, zero, p, polynomialConstant(I, A, zero, one)) ⊆ functionSupport(p, monomials(I), zero) × {monomialOne(I)}46    unfold convolutionPairs47    exact product.monotone with reflexive, unitSupport48  have weights := boundedConvolutionWeights.function at I, functionSupport(p, monomials(I), zero) × {monomialOne(I)}, A, add, zero, neg, mul, one, p, polynomialConstant(I, A, zero, one) with *49  have target := polynomials.function with member50  have values : ∀ t ∈ functionSupport(p, monomials(I), zero) × {monomialOne(I)}, boundedConvolutionWeights(I, functionSupport(p, monomials(I), zero) × {monomialOne(I)}, A, add, zero, neg, mul, one, p, polynomialConstant(I, A, zero, one))(t) = p(monomialMul(I)(t))51    intros t ht52    obtain ⟨bound, u, hu, v, hv, shape⟩ := product.membership.forward at53      functionSupport(p, monomials(I), zero), {monomialOne(I)}, t with ht54    have equal := singleton.membership.forward at v, monomialOne(I) with hv55    have data := functionSupport.membership.forward at p, monomials(I), zero, u with hu56    have inD : (u, monomialOne(I)) ∈ functionSupport(p, monomials(I), zero) × {monomialOne(I)}57      have singleton := singleton.self at monomialOne(I)58      exact product.pair with hu, singleton59    have coefficient := polynomials.coefficient at I, A, zero, p, u with *60    have output := boundedConvolutionWeights.pair at I, functionSupport(p, monomials(I), zero) × {monomialOne(I)}, A, add, zero, neg, mul, one, p, polynomialConstant(I, A, zero, one), u, monomialOne(I) with *61    have index := monomialMul.apply at I, u, monomialOne(I) with *62    unfold call2 at index63    have unitLaw := monomialProduct.one at I, u with *64    have scalarUnit : p(u) * one = p(u)65      ring66    cc67  have injective : ∀ t ∈ functionSupport(p, monomials(I), zero) × {monomialOne(I)}, ∀ s ∈ functionSupport(p, monomials(I), zero) × {monomialOne(I)}, monomialMul(I)(t) = monomialMul(I)(s) → t = s68    intros t ht s hs equalImages69    obtain ⟨boundT, u, hu, v, hv, shapeT⟩ := product.membership.forward at70      functionSupport(p, monomials(I), zero), {monomialOne(I)}, t with ht71    obtain ⟨boundS, x, hx, y, hy, shapeS⟩ := product.membership.forward at72      functionSupport(p, monomials(I), zero), {monomialOne(I)}, s with hs73    have equalV := singleton.membership.forward at v, monomialOne(I) with hv74    have equalY := singleton.membership.forward at y, monomialOne(I) with hy75    have dataU := functionSupport.membership.forward at p, monomials(I), zero, u with hu76    have dataX := functionSupport.membership.forward at p, monomials(I), zero, x with hx77    have indexU := monomialMul.apply at I, u, monomialOne(I) with *78    have indexX := monomialMul.apply at I, x, monomialOne(I) with *79    unfold call2 at indexU80    unfold call2 at indexX81    have unitU := monomialProduct.one at I, u with *82    have unitX := monomialProduct.one at I, x with *83    cc84  have coverage : ∀ c ∈ monomials(I), p(c) ≠ zero → ∃ t ∈ functionSupport(p, monomials(I), zero) × {monomialOne(I)}, monomialMul(I)(t) = c85    intros c hc nonzero86    have supported : c ∈ functionSupport(p, monomials(I), zero)87      apply functionSupport.membership.backward at p, monomials(I), zero, c88      refine ⟨hc, nonzero⟩89    have singleton : monomialOne(I) ∈ {monomialOne(I)}90      settle with singleton.membership91    have pair := product.pair with supported, singleton92    have index := monomialMul.apply at I, c, monomialOne(I) with *93    unfold call2 at index94    have unitLaw := monomialProduct.one at I, c with *95    refine ⟨(c, monomialOne(I)), pair, _⟩96    cc97  have reconstructed := finitePushforward.reconstruct at functionSupport(p, monomials(I), zero) × {monomialOne(I)}, monomials(I), A, add, zero, neg, mul, one, monomialMul(I), boundedConvolutionWeights(I, functionSupport(p, monomials(I), zero) × {monomialOne(I)}, A, add, zero, neg, mul, one, p, polynomialConstant(I, A, zero, one)), p with *98  have bounded := polynomialProduct.on_domain with ring, member, unitPolynomial, domain, finite, covers99  cc100101theorem polynomialProduct.one_left102  shows polynomialProduct(I, A, add, zero, neg, mul, one, polynomialConstant(I, A, zero, one), p) = p103proof104  have ordinary := IsCommRing.ring with ring105  have zeroIn := IsRing.zero_in_carrier with ordinary106  have multiplicative := IsRing.multiplicative with ordinary107  have oneIn := IsMonoid.unit_in_carrier with multiplicative108  have unitPolynomial := polynomialConstant.member at I, A, zero, one with *109  have commutative := polynomialProduct.commutative at I, A, add, zero, neg, mul, one, polynomialConstant(I, A, zero, one), p with *110  have right := polynomialProduct.one_right with ring, member111  cc112113end Rings114