Grace/Cumulus/Algebra/Adjoin.g17

Open in Workbench Download source

Imports

Ring.GeneratedSubring · Ring.Image · Cardinal.Finite

Declarations

Source

1-- Coefficient-relative subalgebras and adjoining generators (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.Adjoin8import Ring.GeneratedSubring9import Ring.Image10import Cardinal.Finite1112-- Relative to a specified coefficient map; algebra theorems assume it is a homomorphism.13predicate Subalgebra (f A B plus z minus times unit T : Set) :=14  IsSubring(B, plus, z, minus, times, unit, T) ∧ functionImage(f, A, B) ⊆ T1516notation scoped Subalgebra(f, R, S, T) => Subalgebra(f, R.carrier, S.carrier, S.add, S.zero, S.neg, S.mul, S.one, T)1718def algebraAdjoin (f A B plus z minus times unit G : Set) : Set :=19  generatedSubring(B, plus, z, minus, times, unit, functionImage(f, A, B) ∪ G)2021notation scoped algebraAdjoin(f, R, S, G) => algebraAdjoin(f, R.carrier, S.carrier, S.add, S.zero, S.neg, S.mul, S.one, G)2223predicate FinitelyGeneratedAlgebra (f A B plus z minus times unit : Set) :=24  ∃ G, Finite(G) ∧ G ⊆ B ∧ algebraAdjoin(f, A, B, plus, z, minus, times, unit, G) = B2526notation scoped FinitelyGeneratedAlgebra(f, R, S) => FinitelyGeneratedAlgebra(f, R.carrier, S.carrier, S.add, S.zero, S.neg, S.mul, S.one)2728section Algebras29variable (A add zero neg mul one B plus z minus times unit f : Set)30notation ring R := (A, add, zero, neg, mul, one)31notation ring S := (B, plus, z, minus, times, unit)32hypothesis source : IsCommRing(R)33hypothesis target : IsCommRing(S)34hypothesis hom : IsRingHom(f, R, S)3536theorem Subalgebra.subring (T : Set)37  requires subalgebra : Subalgebra(f, R, S, T)38  shows IsSubring(S, T)39proof40  exact subalgebra.left4142theorem Subalgebra.coefficients (T : Set)43  requires subalgebra : Subalgebra(f, R, S, T)44  shows functionImage(f, A, B) ⊆ T45proof46  exact subalgebra.right4748theorem algebraAdjoin.subset (G : Set)49  shows algebraAdjoin(f, R, S, G) ⊆ S50proof51  unfold algebraAdjoin52  exact generatedSubring.subset with target5354theorem algebraAdjoin.subalgebra (G : Set)55  requires bounded : G ⊆ S56  shows Subalgebra(f, R, S, algebraAdjoin(f, R, S, G))57proof58  have imageBound := functionImage.subset at f, A, B59  have allBound : functionImage(f, A, B) ∪ G ⊆ S60    settle with Subset, union2.membership61  have subring := generatedSubring.subring at B, plus, z, minus, times, unit, functionImage(f, A, B) ∪ G with target62  have contains := generatedSubring.contains with target, allBound63  have coefficients : functionImage(f, A, B) ⊆ generatedSubring(S, functionImage(f, A, B) ∪ G)64    intros x hx65    have member := union2.left at x, functionImage(f, A, B), G with hx66    exact contains with x, member67  unfold algebraAdjoin68  unfold Subalgebra69  refine ⟨subring, coefficients⟩7071theorem algebraAdjoin.contains (G : Set)72  requires bounded : G ⊆ S73  shows G ⊆ algebraAdjoin(f, R, S, G)74proof75  have imageBound := functionImage.subset at f, A, B76  have allBound : functionImage(f, A, B) ∪ G ⊆ S77    settle with Subset, union2.membership78  have contains := generatedSubring.contains with target, allBound79  unfold algebraAdjoin80  intros x hx81  have member := union2.right at x, functionImage(f, A, B), G with hx82  exact contains with x, member8384theorem algebraAdjoin.least (G T : Set)85  requires subalgebra : Subalgebra(f, R, S, T)86  requires generators : G ⊆ T87  shows algebraAdjoin(f, R, S, G) ⊆ T88proof89  have subring := Subalgebra.subring with *90  have coefficients := Subalgebra.coefficients with *91  have included : functionImage(f, A, B) ∪ G ⊆ T by simp [Subset, union2.membership]92  unfold algebraAdjoin93  exact generatedSubring.least with *9495theorem algebraAdjoin.mono (G H : Set)96  requires included : G ⊆ H97  shows algebraAdjoin(f, R, S, G) ⊆ algebraAdjoin(f, R, S, H)98proof99  have larger : functionImage(f, A, B) ∪ G ⊆ functionImage(f, A, B) ∪ H by simp [Subset, union2.membership]100  have monotone := generatedSubring.mono at B, plus, z, minus, times, unit, functionImage(f, A, B) ∪ G, functionImage(f, A, B) ∪ H with *101  simpa [algebraAdjoin] using monotone102103theorem algebraAdjoin.eq_of_subalgebra (T : Set)104  requires subalgebra : Subalgebra(f, R, S, T)105  shows algebraAdjoin(f, R, S, T) = T106proof107  have subring := Subalgebra.subring with *108  have bounded := IsSubring.subset_carrier with subring109  have contains := algebraAdjoin.contains with *110  have reflexive : T ⊆ T by simp [Subset]111  have least := algebraAdjoin.least with *112  exact Subset.antisymmetric with least, contains113114theorem algebraAdjoin.idempotent (G : Set)115  requires bounded : G ⊆ S116  shows algebraAdjoin(f, R, S, algebraAdjoin(f, R, S, G)) = algebraAdjoin(f, R, S, G)117proof118  have subalgebra := algebraAdjoin.subalgebra with *119  exact algebraAdjoin.eq_of_subalgebra with *120121theorem algebraAdjoin.empty122  shows algebraAdjoin(f, R, S, ∅) = functionImage(f, A, B)123proof124  have image := IsRingHom.image_subring with source, target, hom125  have same : functionImage(f, A, B) ∪ ∅ = functionImage(f, A, B)126    ext x127    simp128  simp [algebraAdjoin]129  exact generatedSubring.eq_of_subring with *130131theorem Subalgebra.scalar_mul_mem (T a x : Set)132  requires subalgebra : Subalgebra(f, R, S, T)133  requires coefficient : a ∈ R134  requires member : x ∈ T135  shows S[f(a) * x] ∈ T136proof137  have function := IsRingHom.function with hom138  have image := functionImage.value with *139  have included := Subalgebra.coefficients with *140  have scalar := included with f(a), image141  have subring := Subalgebra.subring with *142  have closed := IsSubring.mul_closed with subring143  exact ClosedBinary.mem with closed, scalar, member144145theorem algebraAdjoin.coefficient (G a : Set)146  requires bounded : G ⊆ S147  requires coefficient : a ∈ R148  shows f(a) ∈ algebraAdjoin(f, R, S, G)149proof150  have subalgebra := algebraAdjoin.subalgebra with *151  have included := Subalgebra.coefficients with *152  have function := IsRingHom.function with hom153  have image := functionImage.value with *154  exact included with f(a), image155156theorem algebraAdjoin.union (G H : Set)157  requires boundedG : G ⊆ S158  requires boundedH : H ⊆ S159  shows algebraAdjoin(f, R, S, algebraAdjoin(f, R, S, G) ∪ H) = algebraAdjoin(f, R, S, G ∪ H)160proof161  have boundedUnion : G ∪ H ⊆ S162    settle with Subset, union2.membership163  have unionAlgebra := algebraAdjoin.subalgebra at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, G ∪ H with *164  have includesG := algebraAdjoin.contains at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, G with *165  have includesUnion := algebraAdjoin.contains at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, G ∪ H with *166  have subsetG : G ⊆ G ∪ H167    settle with Subset, union2.membership168  have generatedG := algebraAdjoin.mono at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, G, G ∪ H with *169  have generators : algebraAdjoin(f, R, S, G) ∪ H ⊆ algebraAdjoin(f, R, S, G ∪ H) by simp170  have left := algebraAdjoin.least at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, algebraAdjoin(f, R, S, G) ∪ H, algebraAdjoin(f, R, S, G ∪ H) with *171  have larger : G ∪ H ⊆ algebraAdjoin(f, R, S, G) ∪ H by simp [Subset, union2.membership]172  have right := algebraAdjoin.mono at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, G ∪ H, algebraAdjoin(f, R, S, G) ∪ H with *173  exact Subset.antisymmetric with left, right174175theorem algebraAdjoin.comm_ring (G : Set)176  requires bounded : G ⊆ S177  shows IsCommRing(algebraAdjoin(f, R, S, G), restrict(plus, algebraAdjoin(f, R, S, G) × algebraAdjoin(f, R, S, G)), z, restrict(minus, algebraAdjoin(f, R, S, G)), restrict(times, algebraAdjoin(f, R, S, G) × algebraAdjoin(f, R, S, G)), unit)178proof179  have subalgebra := algebraAdjoin.subalgebra with *180  have subring := Subalgebra.subring with *181  exact IsSubring.comm_ring with target, subring182183theorem algebraAdjoin.eq_target_of_surjective (G : Set)184  requires onto : SurjectiveBetween(f, A, B)185  requires bounded : G ⊆ S186  shows algebraAdjoin(f, R, S, G) = B187proof188  have subset := algebraAdjoin.subset at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, G with *189  have function := IsRingHom.function with hom190  apply Subset.antisymmetric191  . exact subset192    intros b hb193    have surjection := onto194    obtain ⟨a, ha, edge⟩ := surjection.right with b, hb195    have value := FunctionBetween.apply_value with *196    have member := algebraAdjoin.coefficient at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, G, a with *197    rwa value at member198199theorem FinitelyGeneratedAlgebra.of_surjective200  requires onto : SurjectiveBetween(f, A, B)201  shows FinitelyGeneratedAlgebra(f, R, S)202proof203  have finite := Finite.empty204  have bounded : ∅ ⊆ S by simp [Subset, set.empty]205  have generated := algebraAdjoin.eq_target_of_surjective with *206  unfold FinitelyGeneratedAlgebra207  refine ⟨∅, finite, bounded, generated⟩208209end Algebras210