MoritaScalarUpgrade110.lean

1 import PaperXI.MoritaLattice110
2 import Mathlib.RingTheory.Finiteness.Basic
3 import Mathlib.Algebra.Module.Submodule.RestrictScalars
4 
5 /-! Finite generation passes from a genuine base-integer lattice to the same
6 carrier with extension-integer scalars. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.MoritaScalarUpgrade110
10 open Matrix PaperXI.MoritaLattice110
11 
12 section StableSubmodule
13 variable {R S M : Type*} [Semiring R] [Semiring S] [AddCommGroup M]
14   [Module R M] [Module S M] [SMul R S] [IsScalarTower R S M]
15 
16 /-- The same actual additive lattice, with larger scalars proved to preserve it. -/
17 def upgrade (L : Submodule R M) (hstable : ∀ s : S, ∀ x ∈ L, s • x ∈ L) :
18     Submodule S M where
19   carrier := (L : Set M)
20   zero_mem' := L.zero_mem
21   add_mem' := L.add_mem
22   smul_mem' s {x} hx := hstable s x hx
23 
24 @[simp] theorem upgrade_restrictScalars (L : Submodule R M)
25     (hstable : ∀ s : S, ∀ x ∈ L, s • x ∈ L) :
26     (upgrade L hstable).restrictScalars R = L := by ext x; rfl
27 
28 /-- A finite generating set of the original lattice also generates it over the
29 larger ring; no free basis or rank is supplied as a premise. -/
30 theorem upgrade_fg (L : Submodule R M)
31     (hstable : ∀ s : S, ∀ x ∈ L, s • x ∈ L) (hfg : L.FG) :
32     (upgrade L hstable).FG := by
33   exact Submodule.FG.of_restrictScalars R (by simpa using hfg)
34 
35 end StableSubmodule
36 
37 section MatrixStability
38 variable {S D m : Type*} [Ring S] [Ring D] [Module S D]
39   [Fintype m] [DecidableEq m]
40 
41 /-- Extension-integer scalar stability follows from the actual maximal-order
42 matrix bimodule through its scalar matrices. -/
43 theorem scalar_stable_of_matrix_bimodule (φ : S →+* D)
44     (hsmul : ∀ (s : S) (x : D), s • x = φ s * x)
45     (L : AddSubgroup (Matrix m m D)) (hL : IsMatrixBimodule φ L) :
46     ∀ s : S, ∀ x ∈ L, s • x ∈ L := by
47   intro s x hx
48   have h := hL.1 (Matrix.scalar m s) x hx
49   have he : (Matrix.scalar m s).map φ * x = s • x := by
50     ext i j
51     simp [Matrix.scalar_apply, Matrix.diagonal_map, Matrix.diagonal_mul, hsmul]
52   rwa [he] at h
53 
54 end MatrixStability
55 end PaperXI.MoritaScalarUpgrade110

Back to source controls