Grace/Cumulus/Algebra/Polynomial/FiniteGeneration.g17

Open in Workbench Download source

Imports

Generation · Image · Field.Quotient

Declarations

• polynomialGenerators.finite theorem derivation
• polynomials.finitely_generated theorem derivation
• polynomialQuotient.finitely_generated theorem derivation
• polynomialQuotient.maximal_residue theorem derivation

Source

1-- Finite-variable polynomial algebras are finitely generated over their coefficients.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.FiniteGeneration8import Generation9import Image10import Field.Quotient1112section Polynomials13variable (I A add zero neg mul one : Set)14notation ring R := (A, add, zero, neg, mul, one)15notation ring P := R[I]16hypothesis ring : IsCommRing(R)17hypothesis finite : Finite(I)1819theorem polynomialGenerators.finite20  shows Finite(polynomialGenerators(I, R))21proof22  have ordinary := IsCommRing.ring with ring23  have zeroIn := IsRing.zero_in_carrier with ordinary24  have multiplicative := IsRing.multiplicative with ordinary25  have oneIn := IsMonoid.unit_in_carrier with multiplicative26  have function := polynomialVariables.function at I, A, zero, one with *27  have subset := Subset.reflexive at I28  unfold polynomialGenerators29  exact Finite.function_image with function, finite, subset3031theorem polynomials.finitely_generated32  shows FinitelyGeneratedAlgebra(polynomialCoefficients(I, R), R, P)33proof34  have generators := polynomialGenerators.finite with *35  have bounded := polynomialGenerators.subset at I, A, add, zero, neg, mul, one with *36  have generated := polynomialGenerators.adjoin at I, A, add, zero, neg, mul, one with *37  unfold FinitelyGeneratedAlgebra38  refine ⟨polynomialGenerators(I, R), generators, bounded, generated⟩3940section Quotients41variable (J : Set)42notation ring Q := P ⧸ J4344theorem polynomialQuotient.finitely_generated45  requires ideal : IsIdeal(P, J)46  shows FinitelyGeneratedAlgebra(compose(quotientProjection(P, idealRelation(P, J)), polynomialCoefficients(I, R), R, P, Q), R, Q)47proof48  have polynomialRing := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *49  have hom := polynomialCoefficients.hom at I, A, add, zero, neg, mul, one with *50  have generated := polynomials.finitely_generated at I, A, add, zero, neg, mul, one with *51  exact FinitelyGeneratedAlgebra.quotient with ring, polynomialRing, hom, ideal, generated5253theorem polynomialQuotient.maximal_residue54  requires maximal : IsMaximalIdeal(P, J)55  shows IsField(Q) ∧ FinitelyGeneratedAlgebra(compose(quotientProjection(P, idealRelation(P, J)), polynomialCoefficients(I, R), R, P, Q), R, Q)56proof57  have polynomialRing := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *58  have ideal : IsIdeal(P, J) by simp [IsMaximalIdeal, IsProperIdeal]59  have field := idealQuotient.is_field_of_maximal with polynomialRing, maximal60  have generated := polynomialQuotient.finitely_generated with *61  refine ⟨field, generated⟩6263end Quotients6465end Polynomials66