AlgebraAdjoin

Adjoining generators over a specified coefficient map

Open in Workbench View on GitHub

1-- Adjoining generators over a specified coefficient map.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 AlgebraAdjoin8import Grace.Cumulus.Algebra.Adjoin910section Algebras11variable (A add zero neg mul one B plus z minus times unit f : Set)12notation ring R := (A, add, zero, neg, mul, one)13notation ring S := (B, plus, z, minus, times, unit)14hypothesis source : IsCommRing(R)15hypothesis target : IsCommRing(S)16hypothesis hom : IsRingHom(f, R, S)1718theorem adjoining_in_stages (G H : Set)19  requires generators : G ⊆ S20  requires more : H ⊆ S21  shows algebraAdjoin(f, R, S, algebraAdjoin(f, R, S, G) ∪ H) = algebraAdjoin(f, R, S, G ∪ H)22proof23  exact algebraAdjoin.union at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, G, H with *2425theorem no_generators_gives_coefficients26  shows algebraAdjoin(f, R, S, ∅) = functionImage(f, R, S)27proof28  exact algebraAdjoin.empty at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f with *2930theorem scalar_closure (T a x : Set)31  requires subalgebra : Subalgebra(f, R, S, T)32  requires scalar : a ∈ R33  requires element : x ∈ T34  shows S[f(a) * x] ∈ T35proof36  exact Subalgebra.scalar_mul_mem at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, T, a, x with *3738theorem surjective_coefficients_generate39  requires onto : SurjectiveBetween(f, R, S)40  shows FinitelyGeneratedAlgebra(f, R, S)41proof42  exact FinitelyGeneratedAlgebra.of_surjective at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f with *4344end Algebras45