MoritaCartanTransport110.lean

1 import PaperXI.MoritaLattice110
2 import Mathlib.GroupTheory.Index
3 
4 /-! Actual lattice-index transport under normalizing outer Cartan factors.
5 The intersection is transported by the additive conjugation equivalence;
6 relative index is preserved by its proved injectivity. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.MoritaCartanTransport110
10 open PaperXI.MoritaLattice110
11 
12 section Conjugation
13 variable {D : Type*} [Ring D]
14 
15 /-- The literal additive-subgroup image under unit conjugation. -/
16 def conjugate (L : AddSubgroup D) (u : Dˣ) : AddSubgroup D :=
17   L.map (unitConjugation u).toAddMonoidHom
18 
19 /-- The order of the conjugations agrees with multiplication of the units. -/
20 theorem unitConjugation_mul (u v : Dˣ) :
21     (unitConjugation (u * v)).toAddMonoidHom =
22       (unitConjugation u).toAddMonoidHom.comp (unitConjugation v).toAddMonoidHom := by
23   ext x
24   simp [unitConjugation, mul_assoc]
25 
26 theorem unitConjugation_inv_apply_apply (u : Dˣ) (x : D) :
27     unitConjugation u⁻¹ (unitConjugation u x) = x := by
28   simp [unitConjugation, mul_assoc]
29 
30 theorem conjugate_mul (L : AddSubgroup D) (u v : Dˣ) :
31     conjugate L (u * v) = conjugate (conjugate L v) u := by
32   unfold conjugate
33   rw [unitConjugation_mul, AddSubgroup.map_map]
34 
35 /-- Normalization fixes the actual subgroup image, not merely its size. -/
36 theorem conjugate_eq_of_normalizing (L : AddSubgroup D) (u : Dˣ)
37     (hu : u ∈ normalizingUnits L) : conjugate L u = L := by
38   ext x
39   change x ∈ L.map (unitConjugation u).toAddMonoidHom ↔ x ∈ L
40   rw [mem_conjugate]
41   exact ((normalizingUnits L).inv_mem hu) x
42 
43 /-- The additive equivalence carries the actual intersection to the intersection of images. -/
44 theorem conjugate_inf (L M : AddSubgroup D) (u : Dˣ) :
45     conjugate (L ⊓ M) u = conjugate L u ⊓ conjugate M u :=
46   AddSubgroup.map_inf L M (unitConjugation u).toAddMonoidHom (unitConjugation u).injective
47 
48 /-- Removing the right factor and transporting by the left factor gives an
49 equality of the actual intersection subgroups. -/
50 theorem intersection_outer_factors (L : AddSubgroup D) (k₁ d k₂ : Dˣ)
51     (hk₁ : k₁ ∈ normalizingUnits L) (hk₂ : k₂ ∈ normalizingUnits L) :
52     L ⊓ conjugate L (k₁ * d * k₂) = conjugate (L ⊓ conjugate L d) k₁ := by
53   rw [conjugate_mul L (k₁ * d) k₂, conjugate_eq_of_normalizing L k₂ hk₂,
54     conjugate_mul L k₁ d, conjugate_inf, conjugate_eq_of_normalizing L k₁ hk₁]
55 
56 /-- The actual lattice-relative-index is invariant under normalizing outer factors.
57 No final-index or quotient-cardinality premise is supplied. -/
58 theorem intersection_relIndex_outer_factors (L : AddSubgroup D) (k₁ d k₂ : Dˣ)
59     (hk₁ : k₁ ∈ normalizingUnits L) (hk₂ : k₂ ∈ normalizingUnits L) :
60     (L ⊓ L.map (unitConjugation (k₁ * d * k₂)).toAddMonoidHom).relIndex L =
61       (L ⊓ L.map (unitConjugation d).toAddMonoidHom).relIndex L := by
62   change (L ⊓ conjugate L (k₁ * d * k₂)).relIndex L =
63     (L ⊓ conjugate L d).relIndex L
64   calc
65     _ = (conjugate (L ⊓ conjugate L d) k₁).relIndex (conjugate L k₁) := by
66       rw [intersection_outer_factors L k₁ d k₂ hk₁ hk₂,
67         conjugate_eq_of_normalizing L k₁ hk₁]
68     _ = _ := AddSubgroup.relIndex_map_map_of_injective
69       (L ⊓ conjugate L d) L (unitConjugation k₁).injective
70 
71 end Conjugation
72 
73 section IntegralMatrixUnits
74 variable {R D m : Type*} [Ring R] [Ring D] [Fintype m] [DecidableEq m]
75 
76 /-- A genuine coefficient-matrix unit mapped into the endomorphism matrix ring. -/
77 def mappedMatrixUnit (φ : R →+* D) (k : (Matrix m m R)ˣ) : (Matrix m m D)ˣ :=
78   Units.map φ.mapMatrix.toMonoidHom k
79 
80 @[simp] theorem mappedMatrixUnit_val (φ : R →+* D) (k : (Matrix m m R)ˣ) :
81     (mappedMatrixUnit φ k : Matrix m m D) = (k : Matrix m m R).map φ := rfl
82 
83 @[simp] theorem mappedMatrixUnit_inv (φ : R →+* D) (k : (Matrix m m R)ˣ) :
84     mappedMatrixUnit φ k⁻¹ = (mappedMatrixUnit φ k)⁻¹ := by
85   exact map_inv
86     (Units.map (φ.mapMatrix : Matrix m m R →+* Matrix m m D).toMonoidHom) k
87 
88 /-- Bimodule stability supplies actual integral-unit conjugation stability. -/
89 theorem mappedMatrixUnit_conjugation_mem (φ : R →+* D)
90     (L : AddSubgroup (Matrix m m D)) (hL : IsMatrixBimodule φ L)
91     (k : (Matrix m m R)ˣ) {x : Matrix m m D} (hx : x ∈ L) :
92     unitConjugation (mappedMatrixUnit φ k) x ∈ L := by
93   have h := hL.2 ((k⁻¹ : (Matrix m m R)ˣ) : Matrix m m R) _
94     (hL.1 (k : Matrix m m R) x hx)
95   simpa [unitConjugation, ← mappedMatrixUnit_inv] using h
96 
97 /-- Every actual mapped integral matrix unit normalizes the lattice. -/
98 theorem mappedMatrixUnit_mem_normalizingUnits (φ : R →+* D)
99     (L : AddSubgroup (Matrix m m D)) (hL : IsMatrixBimodule φ L)
100     (k : (Matrix m m R)ˣ) : mappedMatrixUnit φ k ∈ normalizingUnits L := by
101   intro x
102   constructor
103   · intro hx
104     have h := mappedMatrixUnit_conjugation_mem φ L hL k⁻¹ hx
105     rw [mappedMatrixUnit_inv, unitConjugation_inv_apply_apply] at h
106     exact h
107   · exact mappedMatrixUnit_conjugation_mem φ L hL k
108 
109 /-- The generic Cartan transport applies to actual mapped integral matrix factors. -/
110 theorem matrix_intersection_relIndex_outer_factors (φ : R →+* D)
111     (L : AddSubgroup (Matrix m m D)) (hL : IsMatrixBimodule φ L)
112     (k₁ k₂ : (Matrix m m R)ˣ) (d : (Matrix m m D)ˣ) :
113     (L ⊓ L.map (unitConjugation (mappedMatrixUnit φ k₁ * d *
114       mappedMatrixUnit φ k₂)).toAddMonoidHom).relIndex L =
115         (L ⊓ L.map (unitConjugation d).toAddMonoidHom).relIndex L :=
116   intersection_relIndex_outer_factors L (mappedMatrixUnit φ k₁) d
117     (mappedMatrixUnit φ k₂) (mappedMatrixUnit_mem_normalizingUnits φ L hL k₁)
118       (mappedMatrixUnit_mem_normalizingUnits φ L hL k₂)
119 
120 end IntegralMatrixUnits
121 end PaperXI.MoritaCartanTransport110

Back to source controls