Grace/Cumulus/Algebra/IntegralAdjoin.g17

Open in Workbench Download source

Imports

MonicRelations · LinearSpanMultiplication

Declarations

Source

1-- A monic relation gives an explicit finite spanning set for adjoining one element.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.IntegralAdjoin8import MonicRelations9import LinearSpanMultiplication1011section Algebras12variable (A add zero neg mul one B plus z minus times unit f x : Set)13notation ring R := (A, add, zero, neg, mul, one)14notation ring S := (B, plus, z, minus, times, unit)15hypothesis source : IsCommRing(R)16hypothesis target : IsCommRing(S)17hypothesis hom : IsRingHom(f, R, S)18hypothesis element : x ∈ S1920section Submodules21variable (M : Set)22hypothesis submodule : Submodule(f, R, S, M)23hypothesis unitIn : S[1] ∈ M2425theorem monicTailSet.stable (cs : List(A))26  shows monicTailSet(R, f, S, x, cs) ⊆ M → S[x * monicValue(R, f, S, x, cs)] ∈ M →27    ∀ u ∈ monicTailSet(R, f, S, x, cs), S[x * u] ∈ M28proof29  induction cs30  | List.nil =>31    intros covers initial u hu32    rw monicTailSet at hu33    have equal := singleton.membership.forward with hu34    rw monicValue at initial35    rwa equal36  | List.cons(a, tail) using ih =>37    intros covers initial u hu38    have ordinary := IsCommRing.ring with target39    have coefficient : a ∈ R by assumption40    have image := IsRingHom.closed with hom, coefficient41    have scalar := Submodule.scalar_mul_mem with source, target, hom, submodule, coefficient, unitIn42    have identity : S[f(a) * 1] = f(a) by ring43    rw identity at scalar44    have negative := Submodule.neg_closed with source, target, hom, submodule45    have negativeScalar := ClosedUnary.mem with negative, scalar46    have addition := Submodule.add_closed with source, target, hom, submodule47    have head := monicTailSet.head at A, f, plus, times, unit, x, a :: tail with *48    have included := covers49    have headIn := included with monicValue(R, f, S, x, a :: tail), head50    have difference := ClosedBinary.mem with addition, headIn, negativeScalar51    have tailValue := monicValue.closed at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x, tail with *52    have equation : S[monicValue(R, f, S, x, a :: tail) - f(a)] = S[x * monicValue(R, f, S, x, tail)]53      rw monicValue54      ring55    rw equation at difference56    have tailIncluded : monicTailSet(R, f, S, x, tail) ⊆ M57      rw monicTailSet at covers58      intros v hv59      have member := insert.contains at v, monicValue(R, f, S, x, a :: tail), monicTailSet(R, f, S, x, tail) with hv60      exact covers with v, member61    have rest := ih with tailIncluded, difference62    rw monicTailSet at hu63    have alternatives := insert.membership.forward with hu64    cases alternatives with equal | old65    . rw equal66      exact initial67    . exact rest with u, old6869hypothesis stable : ∀ y ∈ M, S[x * y] ∈ M7071theorem monicValue.mul_preserves (cs : List(A))72  shows ∀ y ∈ M, S[monicValue(R, f, S, x, cs) * y] ∈ M73proof74  induction cs75  | List.nil =>76    intros y hy77    have subset := Submodule.subset with source, target, hom, submodule78    have member := subset with y, hy79    have identity : S[1 * y] = y by ring80    rwa [monicValue, identity]81  | List.cons(a, tail) using ih =>82    intros y hy83    have coefficient : a ∈ R by assumption84    have subset := Submodule.subset with source, target, hom, submodule85    have member := subset with y, hy86    have image := IsRingHom.closed with hom, coefficient87    have tailValue := monicValue.closed at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x, tail with *88    have scalar := Submodule.scalar_mul_mem with source, target, hom, submodule, coefficient, hy89    have tailProduct := ih with y, hy90    have shifted := stable with S[monicValue(R, f, S, x, tail) * y], tailProduct91    have addition := Submodule.add_closed with source, target, hom, submodule92    have sum := ClosedBinary.mem with addition, scalar, shifted93    have equation : S[monicValue(R, f, S, x, a :: tail) * y] = S[f(a) * y + x * (monicValue(R, f, S, x, tail) * y)]94      rw monicValue95      ring96    rwa equation9798theorem monicTailSet.mul_preserves (cs : List(A))99  shows ∀ u ∈ monicTailSet(R, f, S, x, cs), ∀ y ∈ M, S[u * y] ∈ M100proof101  induction cs102  | List.nil =>103    intros u hu y hy104    rw monicTailSet at hu105    have equal := singleton.membership.forward with hu106    have preserved := monicValue.mul_preserves at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x, M, [] with *107    have result := preserved with y, hy108    rw monicValue at result109    rwa equal110  | List.cons(a, tail) using ih =>111    intros u hu y hy112    rw monicTailSet at hu113    have alternatives := insert.membership.forward with hu114    cases alternatives with equal | old115    . have preserved := monicValue.mul_preserves at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x, M, a :: tail with *116      have result := preserved with y, hy117      rwa equal118    . exact ih with u, old, y, hy119120end Submodules121122theorem monicTailSet.spans_adjoin (cs : List(A))123  requires relation : monicValue(R, f, S, x, cs) = S[0]124  shows linearSpan(f, R, S, monicTailSet(R, f, S, x, cs)) = algebraAdjoin(f, R, S, {x})125proof126  have ordinary := IsCommRing.ring with target127  have finite := monicTailSet.finite at A, f, plus, times, unit, x, cs with *128  have bounded := monicTailSet.subset with *129  have span := linearSpan.submodule at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, monicTailSet(R, f, S, x, cs) with *130  have contains := linearSpan.contains with source, target, hom, bounded131  have spanBound := linearSpan.subset at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, monicTailSet(R, f, S, x, cs) with *132  have spanZero := Submodule.zero_mem with source, target, hom, span133  have generatorUnit := monicTailSet.unit at A, f, plus, times, unit, x, cs with *134  have unitIn : S[1] ∈ linearSpan(f, R, S, monicTailSet(R, f, S, x, cs)) by exact contains with unit, generatorUnit135  have initial : S[x * monicValue(R, f, S, x, cs)] ∈ linearSpan(f, R, S, monicTailSet(R, f, S, x, cs))136    have vanishes : S[x * monicValue(R, f, S, x, cs)] = S[0]137      rw relation138      ring139    rwa vanishes140  have tailsStable := monicTailSet.stable with source, target, hom, element, span, unitIn, contains, initial141  have stable : ∀ y ∈ linearSpan(f, R, S, monicTailSet(R, f, S, x, cs)), S[x * y] ∈ linearSpan(f, R, S, monicTailSet(R, f, S, x, cs))142    intros y hy143    have included := spanBound144    have member := included with y, hy145    have generatorProducts : ∀ g ∈ monicTailSet(R, f, S, x, cs), S[g * x] ∈ linearSpan(f, R, S, monicTailSet(R, f, S, x, cs))146      intros g hg147      have bound := bounded148      have inB := bound with g, hg149      have product := tailsStable with g, hg150      have commute : S[g * x] = S[x * g] by ring151      rwa commute152    have multiplied := linearSpan.mul_mem with source, target, hom, span, element, bounded, generatorProducts, hy153    have commute : S[x * y] = S[y * x] by ring154    rwa commute155  have preserved := monicTailSet.mul_preserves with *156  have multiplication : ClosedBinary(linearSpan(f, R, S, monicTailSet(R, f, S, x, cs)), times)157    intros u hu v hv158    have included := spanBound159    have memberV := included with v, hv160    have generators : ∀ g ∈ monicTailSet(R, f, S, x, cs), S[g * v] ∈ linearSpan(f, R, S, monicTailSet(R, f, S, x, cs))161      intros g hg162      exact preserved with g, hg, v, hv163    exact linearSpan.mul_mem with source, target, hom, span, memberV, bounded, generators, hu164  have negative := Submodule.neg_closed with source, target, hom, span165  have addition := Submodule.add_closed with source, target, hom, span166  have subring : IsSubring(S, linearSpan(f, R, S, monicTailSet(R, f, S, x, cs)))167    unfold IsSubring168    refine ⟨spanBound, spanZero, unitIn, negative, addition, multiplication⟩169  have coefficients : functionImage(f, R, S) ⊆ linearSpan(f, R, S, monicTailSet(R, f, S, x, cs))170    intros b hb171    obtain ⟨memberB, a, ha, value⟩ := functionImage.membership.forward with hb172    have image := IsRingHom.closed with hom, ha173    have scalar := Submodule.scalar_mul_mem with source, target, hom, span, ha, unitIn174    have identity : S[f(a) * 1] = f(a) by ring175    rw identity at scalar176    rwa value177  have subalgebra : Subalgebra(f, R, S, linearSpan(f, R, S, monicTailSet(R, f, S, x, cs)))178    unfold Subalgebra179    refine ⟨subring, coefficients⟩180  have xIn : x ∈ linearSpan(f, R, S, monicTailSet(R, f, S, x, cs))181    have product := stable with unit, unitIn182    have identity : S[x * 1] = x by ring183    rwa identity at product184  have generatorIn : {x} ⊆ linearSpan(f, R, S, monicTailSet(R, f, S, x, cs))185    intros u hu186    have equal := singleton.membership.forward with hu187    rwa equal188  have first := algebraAdjoin.least with source, target, hom, subalgebra, generatorIn189  have singletonBound : {x} ⊆ S190    intros u hu191    have equal := singleton.membership.forward with hu192    rwa equal193  have adjoined := algebraAdjoin.subalgebra with source, target, hom, singletonBound194  have generatorContains := algebraAdjoin.contains with source, target, hom, singletonBound195  have generatorSelf : x ∈ {x} by simp [singleton.membership]196  have adjoinedX : x ∈ algebraAdjoin(f, R, S, {x}) by exact generatorContains with x, generatorSelf197  have tailsIncluded := monicTailSet.in_subalgebra at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x, algebraAdjoin(f, R, S, {x}), cs with *198  have adjoinedModule := Subalgebra.submodule with source, target, hom, adjoined199  have second := linearSpan.least with source, target, hom, adjoinedModule, tailsIncluded200  exact Subset.antisymmetric with second, first201202theorem IntegralOver.finite_adjoin203  requires integral : IntegralOver(f, R, S, x)204  shows ∃ G, Finite(G) ∧ G ⊆ algebraAdjoin(f, R, S, {x}) ∧ linearSpan(f, R, S, G) = algebraAdjoin(f, R, S, {x})205proof206  obtain ⟨cs, list, relation⟩ := integral.right207  have finite := monicTailSet.finite at A, f, plus, times, unit, x, cs with *208  have bounded := monicTailSet.subset with *209  have contains := linearSpan.contains with source, target, hom, bounded210  have spans := monicTailSet.spans_adjoin with *211  rw spans at contains212  refine ⟨monicTailSet(R, f, S, x, cs), finite, contains, spans⟩213214theorem IntegralOver.finite_module_of_generates215  requires integral : IntegralOver(f, R, S, x)216  requires generates : algebraAdjoin(f, R, S, {x}) = S217  shows FiniteAlgebraModule(f, R, S)218proof219  have finite := IntegralOver.finite_adjoin with *220  obtain ⟨G, finiteG, bounded, spans⟩ := finite221  rw generates at bounded222  rw generates at spans223  unfold FiniteAlgebraModule224  refine ⟨G, finiteG, bounded, spans⟩225226end Algebras227