PolynomialGeneration

Polynomial generation over arbitrary coefficient rings, with finite generation for finite variables

Open in Workbench View on GitHub

1-- Polynomial generation over arbitrary coefficient rings, with finite generation for finite variables.2-- Part of the Grace17 examples.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module PolynomialGeneration8import Grace.Cumulus.Algebra.Polynomial.FiniteGeneration910section Polynomials11variable (I A add zero neg mul one : Set)12notation ring R := (A, add, zero, neg, mul, one)13notation ring P := R[I]14hypothesis coefficients : IsCommRing(R)1516theorem coefficients_and_variables_suffice (T : Set)17  requires subalgebra : Subalgebra(polynomialCoefficients(I, R), R, P, T)18  requires variables : ∀ j ∈ I, polynomialVariable(I, R, j) ∈ T19  shows T = P20proof21  exact polynomialSubalgebra.eq_carrier with coefficients, subalgebra, variables2223theorem adjoining_variables_gives_polynomials24  shows algebraAdjoin(polynomialCoefficients(I, R), R, P, polynomialGenerators(I, R)) = P25proof26  exact polynomialGenerators.adjoin at I, A, add, zero, neg, mul, one with *2728theorem finite_variables_give_finite_generation29  requires variables : Finite(I)30  shows FinitelyGeneratedAlgebra(polynomialCoefficients(I, R), R, P)31proof32  exact polynomials.finitely_generated at I, A, add, zero, neg, mul, one with *3334section ResidueFields35variable (J : Set)36notation ring Q := P ⧸ J3738theorem maximal_quotient_is_a_finitely_generated_field39  requires finite : Finite(I)40  requires maximal : IsMaximalIdeal(P, J)41  shows IsField(Q) ∧ FinitelyGeneratedAlgebra(compose(quotientProjection(P, idealRelation(P, J)), polynomialCoefficients(I, R), R, P, Q), R, Q)42proof43  exact polynomialQuotient.maximal_residue at I, A, add, zero, neg, mul, one, J with *4445end ResidueFields46end Polynomials47