Grace/Cumulus/Algebra/LinearSpanMultiplication.g17

Open in Workbench Download source

Imports

LinearSpan

Declarations

Source

1-- Multiplication can be checked on generators of a relative linear span.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.LinearSpanMultiplication8import LinearSpan910def rightMultipliers (B times T y : Set) : Set := {u ∈ B | times(u, y) ∈ T}1112section Algebras13variable (A add zero neg mul one B plus z minus times unit f T y : Set)14notation ring R := (A, add, zero, neg, mul, one)15notation ring S := (B, plus, z, minus, times, unit)16hypothesis source : IsCommRing(R)17hypothesis target : IsCommRing(S)18hypothesis hom : IsRingHom(f, R, S)19hypothesis submodule : Submodule(f, R, S, T)20hypothesis element : y ∈ S2122theorem rightMultipliers.submodule23  shows Submodule(f, R, S, rightMultipliers(B, times, T, y))24proof25  have ordinary := IsCommRing.ring with target26  have zeroIn := IsRing.zero_in_carrier with ordinary27  have zeroMem := Submodule.zero_mem with source, target, hom, submodule28  have negClosed := Submodule.neg_closed with source, target, hom, submodule29  have addClosed := Submodule.add_closed with source, target, hom, submodule30  have bounded : rightMultipliers(B, times, T, y) ⊆ B by simp [Subset, rightMultipliers]31  have zeroMember : S[0] ∈ rightMultipliers(B, times, T, y)32    have value : S[0 * y] = S[0] by ring33    apply rightMultipliers.membership.backward34    rw value35    refine ⟨zeroIn, zeroMem⟩36  have negative : ClosedUnary(rightMultipliers(B, times, T, y), minus)37    intros u hu38    obtain ⟨member, product⟩ := rightMultipliers.membership.forward with hu39    have closed := IsRing.neg_closed with ordinary, member40    have included := ClosedUnary.mem with negClosed, product41    have equation : S[(-u) * y] = S[-(u * y)] by ring42    apply rightMultipliers.membership.backward43    rw equation44    refine ⟨closed, included⟩45  have addition : ClosedBinary(rightMultipliers(B, times, T, y), plus)46    intros u hu v hv47    obtain ⟨memberU, productU⟩ := rightMultipliers.membership.forward with hu48    obtain ⟨memberV, productV⟩ := rightMultipliers.membership.forward with hv49    have closed := IsRing.add_closed with ordinary, memberU, memberV50    have included := ClosedBinary.mem with addClosed, productU, productV51    have equation : S[(u + v) * y] = S[u * y + v * y] by ring52    apply rightMultipliers.membership.backward53    rw equation54    refine ⟨closed, included⟩55  have scalars : ∀ a ∈ R, ∀ u ∈ rightMultipliers(B, times, T, y), S[f(a) * u] ∈ rightMultipliers(B, times, T, y)56    intros a ha u hu57    obtain ⟨member, product⟩ := rightMultipliers.membership.forward with hu58    have image := IsRingHom.closed with hom, ha59    have closed := IsRing.mul_closed with ordinary, image, member60    have included := Submodule.scalar_mul_mem with source, target, hom, submodule, ha, product61    have equation : S[(f(a) * u) * y] = S[f(a) * (u * y)] by ring62    apply rightMultipliers.membership.backward63    rw equation64    refine ⟨closed, included⟩65  unfold Submodule66  refine ⟨bounded, zeroMember, negative, addition, scalars⟩6768theorem linearSpan.mul_mem (G x : Set)69  requires bounded : G ⊆ S70  requires generators : ∀ g ∈ G, S[g * y] ∈ T71  requires member : x ∈ linearSpan(f, R, S, G)72  shows S[x * y] ∈ T73proof74  have multipliers := rightMultipliers.submodule with *75  have included : G ⊆ rightMultipliers(B, times, T, y)76    intros g hg77    have inB := bounded with g, hg78    have product := generators with g, hg79    exact rightMultipliers.membership.backward with ⟨inB, product⟩80  have span := linearSpan.least with source, target, hom, multipliers, included81  have multiplier := span with x, member82  have data := rightMultipliers.membership.forward with multiplier83  exact data.right8485end Algebras86