MoritaEndomorphismCoordinates111.lean

1 import PaperXI.MoritaActualCartan110
2 import PaperXI.ActualCuspidalCandidate105
3 import Mathlib.LinearAlgebra.Pi
4 import Mathlib.LinearAlgebra.Matrix.ToLin
5 
6 /-! Natural block-endomorphism coordinates for the literal Morita carrier.
7 No basis of E over F is chosen: the block decomposition uses the finite
8 product's coordinate inclusions and projections. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.MoritaEndomorphismCoordinates111
12 open Matrix Module
13 
14 section BlockEndomorphisms
15 variable (F E m : Type*) [Field F] [Field E] [Algebra F E]
16   [Fintype m] [DecidableEq m]
17 
18 /-- Assemble each row by the finite-product universal property, then assemble
19 the output coordinates. This is the natural block decomposition. -/
20 def blockLinearEquiv : Matrix m m (Module.End F E) ≃ₗ[F] Module.End F (m → E) :=
21   (LinearEquiv.piCongrRight fun _ : m =>
22     LinearMap.lsum F (fun _ : m => E) F).trans (LinearEquiv.linearMapPi F)
23 
24 @[simp] theorem blockLinearEquiv_apply (A : Matrix m m (Module.End F E))
25     (v : m → E) (i : m) :
26     blockLinearEquiv F E m A v i = ∑ j, A i j (v j) := by
27   change (∑ j, (A i j).comp (LinearMap.proj j)) v = _
28   simp only [LinearMap.sum_apply, LinearMap.comp_apply, LinearMap.proj_apply]
29 
30 /-- Matrix multiplication is composition of the actual block actions. -/
31 theorem blockLinearEquiv_mul (A B : Matrix m m (Module.End F E)) :
32     blockLinearEquiv F E m (A * B) = blockLinearEquiv F E m A * blockLinearEquiv F E m B := by
33   apply LinearMap.ext
34   intro v
35   funext i
36   simp only [blockLinearEquiv_apply, Module.End.mul_apply, Matrix.mul_apply,
37     LinearMap.sum_apply, map_sum]
38   exact Finset.sum_comm
39 
40 /-- The exact ring equivalence between Morita matrices and endomorphisms of E^m. -/
41 def blockRingEquiv : Matrix m m (Module.End F E) ≃+* Module.End F (m → E) where
42   __ := (blockLinearEquiv F E m).toAddEquiv
43   map_mul' := blockLinearEquiv_mul F E m
44 
45 @[simp] theorem blockRingEquiv_apply (A : Matrix m m (Module.End F E))
46     (v : m → E) (i : m) :
47     blockRingEquiv F E m A v i = ∑ j, A i j (v j) :=
48   blockLinearEquiv_apply F E m A v i
49 
50 end BlockEndomorphisms
51 
52 section ActualCoordinates
53 variable (F E m n : Type*) [Field F] [Field E] [Algebra F E]
54   [TopologicalSpace F] [TopologicalSpace E]
55   [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n]
56 
57 /-- Transport the actual block carrier through the supplied F-coordinates. -/
58 def coordinateRingEquiv (e : (m → E) ≃L[F] (n → F)) :
59     Matrix m m (Module.End F E) ≃+* Matrix n n F :=
60   (blockRingEquiv F E m).trans
61     ((e.toLinearEquiv.conjAlgEquiv F).toRingEquiv.trans
62       LinearMap.toMatrixAlgEquiv'.toRingEquiv)
63 
64 /-- The induced map on genuine units of the Morita carrier. -/
65 def coordinateUnitMap (e : (m → E) ≃L[F] (n → F)) :
66     (Matrix m m (Module.End F E))ˣ →* GL n F :=
67   Units.map (coordinateRingEquiv F E m n e).toMonoidHom
68 
69 omit [TopologicalSpace F] [TopologicalSpace E] in
70 /-- The block embedding acts exactly as the existing restricted-scalar E-matrix action. -/
71 theorem blockRingEquiv_centralizerEmbedding (y : GL m E) :
72     blockRingEquiv F E m (PaperXI.MoritaActualCartan110.centralizerEmbedding F E m y :
73       Matrix m m (Module.End F E)) =
74         (PaperXI.ActualELatticeResidue59.restrictScalarMatrix F E m y).toLinearMap := by
75   apply LinearMap.ext
76   intro v
77   funext i
78   rw [blockRingEquiv_apply]
79   rfl
80 
81 /-- The supplied-coordinate unit action agrees with the block endomorphism action. -/
82 theorem coordinateAut_coordinateUnitMap (e : (m → E) ≃L[F] (n → F))
83     (u : (Matrix m m (Module.End F E))ˣ) (v : m → E) :
84     PaperXI.LatticeCongruenceTopology60.coordinateAut e (coordinateUnitMap F E m n e u) v =
85       blockRingEquiv F E m (u : Matrix m m (Module.End F E)) v := by
86   rw [PaperXI.LatticeCongruenceTopology60.coordinateAut_apply]
87   change e.symm ((LinearMap.toMatrix'
88     ((e.toLinearEquiv.conjAlgEquiv F) (blockRingEquiv F E m (u : Matrix m m (Module.End F E)))))
89       *ᵥ e v) = _
90   rw [LinearMap.toMatrix'_mulVec]
91   change e.symm (e (blockRingEquiv F E m (u : Matrix m m (Module.End F E))
92     (e.symm (e v)))) = _
93   simp only [e.symm_apply_apply]
94 
95 /-- The Morita centralizer maps to the literal existing centralizer on the original F-carrier. -/
96 theorem coordinateUnitMap_centralizer (e : (m → E) ≃L[F] (n → F)) (y : GL m E) :
97     coordinateUnitMap F E m n e
98       (PaperXI.MoritaActualCartan110.centralizerEmbedding F E m y) =
99         PaperXI.ActualCuspidalCandidate105.centralizerMap F E m n e y := by
100   apply (PaperXI.LatticeCongruenceTopology60.coordinateAut e).injective
101   change PaperXI.LatticeCongruenceTopology60.coordinateAut e
102     (coordinateUnitMap F E m n e
103       (PaperXI.MoritaActualCartan110.centralizerEmbedding F E m y)) =
104         PaperXI.LatticeCongruenceTopology60.coordinateAut e
105           ((PaperXI.LatticeCongruenceTopology60.coordinateAut e).symm
106             (PaperXI.ActualELatticeResidue59.restrictScalarMatrix F E m y))
107   rw [MulEquiv.apply_symm_apply]
108   apply LinearEquiv.ext
109   intro v
110   rw [coordinateAut_coordinateUnitMap]
111   exact congrArg (fun f : Module.End F (m → E) => f v)
112     (blockRingEquiv_centralizerEmbedding F E m y)
113 
114 /-- Ring transport intertwines the actual unit-conjugation actions. -/
115 theorem coordinateRingEquiv_unitConjugation (e : (m → E) ≃L[F] (n → F))
116     (u : (Matrix m m (Module.End F E))ˣ) (x : Matrix m m (Module.End F E)) :
117     coordinateRingEquiv F E m n e (PaperXI.MoritaLattice110.unitConjugation u x) =
118       PaperXI.MoritaLattice110.unitConjugation (coordinateUnitMap F E m n e u)
119         (coordinateRingEquiv F E m n e x) := by
120   change coordinateRingEquiv F E m n e ((u : Matrix m m (Module.End F E)) * x *
121     ((u⁻¹ : (Matrix m m (Module.End F E))ˣ) : Matrix m m (Module.End F E))) = _
122   change _ = coordinateRingEquiv F E m n e (u : Matrix m m (Module.End F E)) *
123     coordinateRingEquiv F E m n e x * coordinateRingEquiv F E m n e
124       ((u⁻¹ : (Matrix m m (Module.End F E))ˣ) : Matrix m m (Module.End F E))
125   simp only [map_mul]
126 
127 /-- The literal image of a conjugated lattice is the conjugate of its image. -/
128 theorem coordinate_map_conjugate (e : (m → E) ≃L[F] (n → F))
129     (L : AddSubgroup (Matrix m m (Module.End F E)))
130     (u : (Matrix m m (Module.End F E))ˣ) :
131     (L.map (PaperXI.MoritaLattice110.unitConjugation u).toAddMonoidHom).map
132       (coordinateRingEquiv F E m n e).toAddMonoidHom =
133         (L.map (coordinateRingEquiv F E m n e).toAddMonoidHom).map
134           (PaperXI.MoritaLattice110.unitConjugation (coordinateUnitMap F E m n e u)).toAddMonoidHom := by
135   rw [AddSubgroup.map_map, AddSubgroup.map_map]
136   congr 1
137   apply AddMonoidHom.ext
138   intro x
139   exact coordinateRingEquiv_unitConjugation F E m n e u x
140 
141 /-- The relative index of the actual conjugate intersection is preserved in F-matrix coordinates. -/
142 theorem coordinate_intersection_relIndex (e : (m → E) ≃L[F] (n → F))
143     (L : AddSubgroup (Matrix m m (Module.End F E)))
144     (u : (Matrix m m (Module.End F E))ˣ) :
145     ((L.map (coordinateRingEquiv F E m n e).toAddMonoidHom) ⊓
146       (L.map (coordinateRingEquiv F E m n e).toAddMonoidHom).map
147         (PaperXI.MoritaLattice110.unitConjugation (coordinateUnitMap F E m n e u)).toAddMonoidHom).relIndex
148           (L.map (coordinateRingEquiv F E m n e).toAddMonoidHom) =
149             (L ⊓ L.map (PaperXI.MoritaLattice110.unitConjugation u).toAddMonoidHom).relIndex L := by
150   have h := AddSubgroup.map_inf L
151     (L.map (PaperXI.MoritaLattice110.unitConjugation u).toAddMonoidHom)
152     (coordinateRingEquiv F E m n e).toAddMonoidHom (coordinateRingEquiv F E m n e).injective
153   rw [coordinate_map_conjugate F E m n e L u] at h
154   rw [← h]
155   exact AddSubgroup.relIndex_map_map_of_injective
156     (L ⊓ L.map (PaperXI.MoritaLattice110.unitConjugation u).toAddMonoidHom) L
157       (coordinateRingEquiv F E m n e).injective
158 
159 section IntegralCoordinates
160 open ValuativeRel
161 variable [ValuativeRel E]
162 
163 /-- Integral centralizer units agree with the existing integral-matrix coordinate map. -/
164 theorem coordinateUnitMap_integral (e : (m → E) ≃L[F] (n → F)) (k : GL m 𝒪[E]) :
165     coordinateUnitMap F E m n e
166       (PaperXI.MoritaCartanTransport110.mappedMatrixUnit
167         (PaperXI.MoritaCornerRank110.coefficientMap F E) k) =
168           (PaperXI.LatticeCongruenceTopology60.coordinateAut e).symm
169             (PaperXI.ActualELatticeResidue59.integralMatrix F E m k) := by
170   rw [← PaperXI.MoritaActualCartan110.centralizerEmbedding_integral F E m k,
171     coordinateUnitMap_centralizer F E m n e]
172   rfl
173 
174 end IntegralCoordinates
175 end ActualCoordinates
176 end PaperXI.MoritaEndomorphismCoordinates111

Back to source controls