Grace/Cumulus/Algebra/FiniteSpan.g17

Open in Workbench Download source

Imports

SpanProduct

Declarations

Source

1-- Finite spans of subalgebras and their joint generation (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.FiniteSpan8import SpanProduct910predicate FiniteSpan (f A B plus z minus times T : Set) :=11  ∃ G, Finite(G) ∧ G ⊆ T ∧ linearSpan(f, A, B, plus, z, minus, times, G) = T1213notation scoped FiniteSpan(f, R, S, T) => FiniteSpan(f, R.carrier, S.carrier, S.add, S.zero, S.neg, S.mul, T)1415section Algebras16variable (A add zero neg mul one B plus z minus times unit f : Set)17notation ring R := (A, add, zero, neg, mul, one)18notation ring S := (B, plus, z, minus, times, unit)19hypothesis source : IsCommRing(R)20hypothesis target : IsCommRing(S)21hypothesis hom : IsRingHom(f, R, S)2223theorem FiniteSpan.target_iff24  shows FiniteSpan(f, R, S, S) ↔ FiniteAlgebraModule(f, R, S)25proof26  simp [FiniteSpan, FiniteAlgebraModule]2728theorem linearSpan.unit29  shows linearSpan(f, R, S, {S[1]}) = algebraAdjoin(f, R, S, ∅)30proof31  have ordinary := IsCommRing.ring with target32  have multiplicative := IsRing.multiplicative with ordinary33  have unitIn := IsMonoid.unit_in_carrier with multiplicative34  have singletonBound : {S[1]} ⊆ S35    settle with Subset, singleton.membership36  have emptyBound : ∅ ⊆ S37    settle with Subset, set.empty38  have adjoined := algebraAdjoin.subalgebra with source, target, hom, emptyBound39  have submodule := Subalgebra.submodule with source, target, hom, adjoined40  have subring := Subalgebra.subring with source, target, hom, adjoined41  have unitMember := IsSubring.one_closed with subring42  have generators : {S[1]} ⊆ algebraAdjoin(f, R, S, ∅)43    settle with Subset, singleton.membership44  have first := linearSpan.least with source, target, hom, submodule, generators45  have span := linearSpan.submodule at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, {S[1]} with *46  have contains := linearSpan.contains with source, target, hom, singletonBound47  have inSpan : S[1] ∈ linearSpan(f, R, S, {S[1]})48    settle with Subset, singleton.membership49  have image := algebraAdjoin.empty at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f with *50  have second : algebraAdjoin(f, R, S, ∅) ⊆ linearSpan(f, R, S, {S[1]})51    rw image52    intros b hb53    obtain ⟨inB, a, ha, value⟩ := functionImage.membership.forward at f, A, B, b with hb54    have mapped := IsRingHom.closed with hom, ha55    have scalar := Submodule.scalar_mul_mem with source, target, hom, span, ha, inSpan56    have equation : S[f(a) * 1] = f(a)57      ring58    rw equation at scalar59    rw value60    exact scalar61  exact Subset.antisymmetric with first, second6263theorem FiniteSpan.empty_adjoin64  shows FiniteSpan(f, R, S, algebraAdjoin(f, R, S, ∅))65proof66  have spans := linearSpan.unit with *67  have finite := Finite.singleton at unit68  have ordinary := IsCommRing.ring with target69  have multiplicative := IsRing.multiplicative with ordinary70  have unitIn := IsMonoid.unit_in_carrier with multiplicative71  have bound : {S[1]} ⊆ S by simp [Subset, singleton.membership]72  have contains := linearSpan.contains with source, target, hom, bound73  rw spans at contains74  unfold FiniteSpan75  refine ⟨{S[1]}, finite, contains, spans⟩7677theorem FiniteSpan.adjoin_union (U V : Set)78  requires boundedU : U ⊆ S79  requires boundedV : V ⊆ S80  requires finiteU : FiniteSpan(f, R, S, algebraAdjoin(f, R, S, U))81  requires finiteV : FiniteSpan(f, R, S, algebraAdjoin(f, R, S, V))82  shows FiniteSpan(f, R, S, algebraAdjoin(f, R, S, U ∪ V))83proof84  obtain ⟨G, finiteG, includedG, spansG⟩ := finiteU85  obtain ⟨H, finiteH, includedH, spansH⟩ := finiteV86  have subsetU := algebraAdjoin.subset at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, U with *87  have subsetV := algebraAdjoin.subset at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, V with *88  have boundedG := Subset.transitive with includedG, subsetU89  have boundedH := Subset.transitive with includedH, subsetV90  have finite := spanProducts.finite with source, target, hom, finiteG, finiteH, boundedG, boundedH91  have spans := linearSpan.product_adjoin with source, target, hom, boundedG, boundedH, boundedU, boundedV, spansG, spansH92  have bound := spanProducts.subset at B, times, G, H93  have contains := linearSpan.contains with source, target, hom, bound94  rw spans at contains95  unfold FiniteSpan96  refine ⟨spanProducts(B, times, G, H), finite, contains, spans⟩9798end Algebras99