MoritaPairIndex110.lean

1 import PaperXI.MoritaActualCartan110
2 
3 /-! The same actual Cartan witnesses compare two actual lattices. This is an
4 additive assertion; no canonical H1/J1 or multiplicative attachment is assumed. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.MoritaPairIndex110
8 open Matrix Module ValuativeRel
9 open PaperXI.MoritaLattice110 PaperXI.MoritaCornerRank110
10 open PaperXI.MoritaActualCartan110
11 
12 variable (F E : Type*) [Field F] [Field E] [Algebra F E]
13   [Module.Finite F E] [ValuativeRel E] [TopologicalSpace E]
14   [IsNonarchimedeanLocalField E]
15 variable (m : Type*) [Fintype m] [DecidableEq m] [Nonempty m]
16 
17 /-- The additive index is independent of the choice of finite full maximal-order
18 bimodule commuting with the scalar radical. Both sides use one factorization
19 of the same y, rather than independent existential exponent witnesses. -/
20 theorem actual_pair_index
21     (L₁ L₂ : Submodule 𝒪[E] (Matrix m m (Module.End F E)))
22     (hL₁ : IsMatrixBimodule (coefficientMap F E) L₁.toAddSubgroup)
23     (hL₂ : IsMatrixBimodule (coefficientMap F E) L₂.toAddSubgroup)
24     (hfg₁ : L₁.FG) (hfg₂ : L₂.FG)
25     (hfull₁ : Submodule.span F (L₁ : Set (Matrix m m (Module.End F E))) = ⊤)
26     (hfull₂ : Submodule.span F (L₂ : Set (Matrix m m (Module.End F E))) = ⊤)
27     (hcomm₁ : RadicalCommutes F E m L₁.toAddSubgroup)
28     (hcomm₂ : RadicalCommutes F E m L₂.toAddSubgroup) (y : GL m E) :
29     (L₁.toAddSubgroup ⊓ L₁.toAddSubgroup.map
30       (unitConjugation (centralizerEmbedding F E m y)).toAddMonoidHom).relIndex
31         L₁.toAddSubgroup =
32     (L₂.toAddSubgroup ⊓ L₂.toAddSubgroup.map
33       (unitConjugation (centralizerEmbedding F E m y)).toAddMonoidHom).relIndex
34         L₂.toAddSubgroup := by
35   obtain ⟨c, l, r, a, _, hy⟩ := PaperXI.ActualLocalCartan106.hasCartan E m y
36   rw [relIndex_of_actual_cartan F E m L₁ hL₁ hfg₁ hfull₁ hcomm₁ y c l r a hy,
37     relIndex_of_actual_cartan F E m L₂ hL₂ hfg₂ hfull₂ hcomm₂ y c l r a hy]
38 
39 end PaperXI.MoritaPairIndex110

Back to source controls