Grace/Cumulus/Algebra/SpanAnnihilator.g17

Open in Workbench Download source

Imports

SpanCoefficients · LinearSpanMultiplication · MonicRelations

Declarations

Source

1-- Annihilating generators annihilates the span; a spanning algebra is faithful (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.SpanAnnihilator8import SpanCoefficients9import LinearSpanMultiplication10import MonicRelations1112section Algebras13variable (A add zero neg mul one B plus z minus times unit f G p : 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 bounded : G ⊆ S20hypothesis element : p ∈ S21hypothesis annihilates : ∀ g ∈ G, S[p * g] = S[0]2223theorem linearSpan.annihilates (y : Set)24  requires member : y ∈ linearSpan(f, R, S, G)25  shows S[p * y] = S[0]26proof27  have zeroModule := Submodule.zero with *28  have products : ∀ g ∈ G, S[g * p] ∈ {S[0]}29    intros g hg30    have inB : g ∈ S by exact bounded with g, hg31    have vanishes := annihilates with g, hg32    have equal : S[g * p] = S[p * g] by ring33    rw [equal, vanishes]34    simp35  have multiplied := linearSpan.mul_mem with *36  have vanishes := singleton.membership.forward with multiplied37  have spanBound := linearSpan.subset at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, G with *38  have inB : y ∈ S by exact spanBound with y, member39  have equal : S[p * y] = S[y * p] by ring40  rwa equal4142theorem linearSpan.annihilator_zero43  requires unitIn : S[1] ∈ linearSpan(f, R, S, G)44  shows p = S[0]45proof46  have vanishes := linearSpan.annihilates with *47  have equal : S[p * 1] = p by ring48  rwa equal at vanishes4950end Algebras5152section Relations53variable (A add zero neg mul one B plus z minus times unit f G x : Set)54notation ring R := (A, add, zero, neg, mul, one)55notation ring S := (B, plus, z, minus, times, unit)56hypothesis source : IsCommRing(R)57hypothesis target : IsCommRing(S)58hypothesis hom : IsRingHom(f, R, S)59hypothesis bounded : G ⊆ S60hypothesis element : x ∈ S61hypothesis unitIn : S[1] ∈ linearSpan(f, R, S, G)6263theorem IntegralOver.of_annihilates_generators (cs : List(A))64  requires annihilates : ∀ g ∈ G, S[monicValue(R, f, S, x, cs) * g] = S[0]65  shows IntegralOver(f, R, S, x)66proof67  have value := monicValue.closed with *68  have relation := linearSpan.annihilator_zero with *69  unfold IntegralOver70  refine ⟨element, cs, assumption, relation⟩7172end Relations73