Grace/Cumulus/Algebra/IntegralFinite.g17

Open in Workbench Download source

Imports

FiniteSpan · Field.Algebraic

Declarations

Source

1-- Finitely many integral generators give a finite module (ZF).2-- Part of Cumulus, the Grace17 mathematics library.3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Algebra.IntegralFinite9import FiniteSpan10import Field.Algebraic1112section Algebras13variable (A add zero neg mul one B plus z minus times unit f : 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)1920theorem IntegralOver.finite_span_adjoin (x : Set)21  requires integral : IntegralOver(f, R, S, x)22  shows FiniteSpan(f, R, S, algebraAdjoin(f, R, S, {x}))23proof24  have data := integral25  unfold IntegralOver at data26  exact IntegralOver.finite_adjoin at27    A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f, x with *2829theorem integralList.finite_adjoin (K : Set) (xs : List(K))30  requires bounded : K ⊆ S31  requires integral : ∀ x ∈ K, IntegralOver(f, R, S, x)32  shows FiniteSpan(f, R, S, algebraAdjoin(f, R, S, listSupport{K}(xs)))33proof34  induction xs35  | List.nil =>36    rw listSupport37    exact FiniteSpan.empty_adjoin at A, add, zero, neg, mul, one, B, plus, z, minus, times, unit, f with *38  | List.cons(x, tail) using ih =>39    have xIn : x ∈ S by simp [Subset]40    have singleBound : {x} ⊆ S41      intros u hu42      have equal := singleton.membership.forward with hu43      rwa equal44    have tailSubset := listSupport.subset at K, tail with *45    have tailBound := Subset.transitive with tailSubset, bounded46    have root := integral with x, assumption47    have single := IntegralOver.finite_span_adjoin with source, target, hom, root48    have joined := FiniteSpan.adjoin_union with source, target, hom, tailBound, singleBound, ih, single49    have equation : listSupport{K}(tail) ∪ {x} = insert(x, listSupport{K}(tail))50      ext u51      simp [union2.membership, singleton.membership, insert.membership]52    rw equation at joined53    rwa listSupport5455theorem integralGenerators.finite_adjoin (K : Set)56  requires finite : Finite(K)57  requires bounded : K ⊆ S58  requires integral : ∀ x ∈ K, IntegralOver(f, R, S, x)59  shows FiniteSpan(f, R, S, algebraAdjoin(f, R, S, K))60proof61  obtain ⟨xs, list, covers⟩ := Finite.list_cover with finite62  have subset := listSupport.subset with *63  have equal := Subset.antisymmetric with subset, covers64  have result := integralList.finite_adjoin with *65  rwa equal at result6667theorem integralGenerators.finite_module (K : Set)68  requires finite : Finite(K)69  requires bounded : K ⊆ S70  requires integral : ∀ x ∈ K, IntegralOver(f, R, S, x)71  requires generates : algebraAdjoin(f, R, S, K) = S72  shows FiniteAlgebraModule(f, R, S)73proof74  have result := integralGenerators.finite_adjoin with *75  rw generates at result76  exact FiniteSpan.target_iff.forward with source, target, hom, result7778theorem FinitelyGeneratedAlgebra.finite_module_of_integral79  requires generated : FinitelyGeneratedAlgebra(f, R, S)80  requires integral : ∀ x ∈ S, IntegralOver(f, R, S, x)81  shows FiniteAlgebraModule(f, R, S)82proof83  obtain ⟨K, finite, bounded, generates⟩ := generated84  have roots : ∀ x ∈ K, IntegralOver(f, R, S, x)85    intros x hx86    have member : x ∈ S by simp [Subset]87    exact integral with x, member88  exact integralGenerators.finite_module with source, target, hom, finite, bounded, roots, generates8990section BaseExtension91variable (T : Set)92notation ring L := S ↾ T9394theorem integralGenerators.finite_module_enlarged (K : Set)95  requires subring : IsSubring(S, T)96  requires coefficients : functionImage(f, R, S) ⊆ T97  requires finite : Finite(K)98  requires bounded : K ⊆ S99  requires integral : ∀ x ∈ K, IntegralOver(identity(T), L, S, x)100  requires generates : algebraAdjoin(f, R, S, K) = S101  shows FiniteAlgebraModule(identity(T), L, S)102proof103  have smaller : IsCommRing(L)104    exact IsSubring.comm_ring with *105  have inclusion : IsRingHom(identity(T), L, S)106    exact IsSubring.inclusion_hom with *107  have larger : Subalgebra(identity(T), L, S, algebraAdjoin(identity(T), L, S, K))108    exact algebraAdjoin.subalgebra with *109  have largerRing := Subalgebra.subring with smaller, target, inclusion, larger110  have includes : functionImage(f, R, S) ⊆ algebraAdjoin(identity(T), L, S, K)111    intros c member112    have inT : c ∈ T by exact coefficients with c, member113    have value := identity.apply at c, T with *114    have included := algebraAdjoin.coefficient at T, restrict(plus, T × T), z, restrict(minus, T), restrict(times, T × T), unit, B, plus, z, minus, times, unit, identity(T), K, c with *115    rwa value at included116  have oldAlgebra : Subalgebra(f, R, S, algebraAdjoin(identity(T), L, S, K))117    unfold Subalgebra118    refine ⟨largerRing, includes⟩119  have generators : K ⊆ algebraAdjoin(identity(T), L, S, K)120    exact algebraAdjoin.contains with *121  have first := algebraAdjoin.least with source, target, hom, oldAlgebra, generators122  rw generates at first123  have second : algebraAdjoin(identity(T), L, S, K) ⊆ S124    exact algebraAdjoin.subset with *125  have equality := Subset.antisymmetric with second, first126  exact integralGenerators.finite_module with *127128end BaseExtension129130end Algebras131132section Fields133variable (A add zero neg mul one B plus z minus times unit f : Set)134notation ring R := (A, add, zero, neg, mul, one)135notation ring S := (B, plus, z, minus, times, unit)136hypothesis field : IsField(R)137hypothesis target : IsCommRing(S)138hypothesis hom : IsRingHom(f, R, S)139140theorem algebraicGenerators.finite_adjoin (K : Set)141  requires finite : Finite(K)142  requires bounded : K ⊆ S143  requires algebraic : ∀ x ∈ K, AlgebraicOver(f, R, S, x)144  shows FiniteSpan(f, R, S, algebraAdjoin(f, R, S, K))145proof146  have source := IsField.comm_ring with field147  have integral : ∀ x ∈ K, IntegralOver(f, R, S, x)148    intros x hx149    have root := algebraic with x, hx150    exact AlgebraicOver.integral with field, target, hom, root151  exact integralGenerators.finite_adjoin with source, target, hom, finite, bounded, integral152153theorem algebraicGenerators.finite_module (K : Set)154  requires finite : Finite(K)155  requires bounded : K ⊆ S156  requires algebraic : ∀ x ∈ K, AlgebraicOver(f, R, S, x)157  requires generates : algebraAdjoin(f, R, S, K) = S158  shows FiniteAlgebraModule(f, R, S)159proof160  have source := IsField.comm_ring with field161  have result := algebraicGenerators.finite_adjoin with *162  rw generates at result163  exact FiniteSpan.target_iff.forward with source, target, hom, result164165theorem FinitelyGeneratedAlgebra.finite_module_of_algebraic166  requires generated : FinitelyGeneratedAlgebra(f, R, S)167  requires algebraic : ∀ x ∈ S, AlgebraicOver(f, R, S, x)168  shows FiniteAlgebraModule(f, R, S)169proof170  have source := IsField.comm_ring with field171  have integral : ∀ x ∈ S, IntegralOver(f, R, S, x)172    intros x hx173    have root := algebraic with x, hx174    exact AlgebraicOver.integral with field, target, hom, root175  exact FinitelyGeneratedAlgebra.finite_module_of_integral with source, target, hom, generated, integral176177end Fields178