MoritaIndex110.lean

1 import PaperXI.MoritaCornerRank110
2 import PaperXI.MoritaQuotient110
3 import PaperXI.FreeLatticeCard110
4 import PaperXI.MoritaUniformizer110
5 import Mathlib.Algebra.Module.Submodule.Pointwise
6 import Mathlib.GroupTheory.Index
7 
8 /-! Actual corner power quotients and the diagonal matrix-lattice index. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.MoritaIndex110
12 open scoped Pointwise
13 open PaperXI.MoritaLattice110 PaperXI.MoritaCornerRank110
14 
15 section PowerQuotient
16 variable {R D : Type*} [CommRing R] [Ring D] [Module R D]
17 
18 /-- An ambient left-power subgroup restricted to its actual corner module is
19 exactly the internally defined principal-ideal-power submodule. -/
20 theorem leftPower_addSubgroupOf_eq (φ : R →+* D)
21     (hsmul : ∀ (r : R) (x : D), r • x = φ r * x)
22     (Λ : Submodule R D) (π : R) (u : Dˣ) (hπ : (u : D) = φ π) (n : ℕ) :
23     (leftPower Λ.toAddSubgroup u (n : ℤ)).addSubgroupOf Λ.toAddSubgroup =
24       (((Ideal.span {π}) ^ n) • (⊤ : Submodule R Λ)).toAddSubgroup := by
25   ext x
26   change (x : D) ∈ leftPower Λ.toAddSubgroup u (n : ℤ) ↔
27     x ∈ ((Ideal.span {π}) ^ n) • (⊤ : Submodule R Λ)
28   rw [Submodule.mem_smul_top_iff, Ideal.span_singleton_pow,
29     Submodule.ideal_span_singleton_smul, Submodule.mem_smul_pointwise_iff_exists]
30   simp only [leftPower, AddSubgroup.mem_map]
31   have hp : ((u ^ (n : ℤ) : Dˣ) : D) = φ (π ^ n) := by
32     simp [hπ]
33   constructor
34   · rintro ⟨z, hz, hx⟩
35     change ((u ^ (n : ℤ) : Dˣ) : D) * z = (x : D) at hx
36     exact ⟨z, hz, by simpa only [hsmul, hp] using hx⟩
37   · rintro ⟨z, hz, hx⟩
38     refine ⟨z, hz, ?_⟩
39     change ((u ^ (n : ℤ) : Dˣ) : D) * z = (x : D)
40     simpa only [hsmul, hp] using hx
41 
42 /-- The literal ambient-power quotient obtains its cardinality from an actual
43 basis and an actual nonzero prime principal ideal. -/
44 theorem card_leftPower_quotient {ι : Type*} [Fintype ι] [DecidableEq ι]
45     [IsDedekindDomain R] (φ : R →+* D)
46     (hsmul : ∀ (r : R) (x : D), r • x = φ r * x)
47     (Λ : Submodule R D) (b : Module.Basis ι R Λ)
48     (π : R) [(Ideal.span {π} : Ideal R).IsPrime]
49     (hI : (Ideal.span {π} : Ideal R) ≠ ⊥)
50     (u : Dˣ) (hπ : (u : D) = φ π) (n : ℕ) :
51     Nat.card (Λ.toAddSubgroup ⧸
52       (leftPower Λ.toAddSubgroup u (n : ℤ)).addSubgroupOf Λ.toAddSubgroup) =
53       Nat.card (R ⧸ (Ideal.span {π} : Ideal R)) ^ (n * Fintype.card ι) := by
54   rw [leftPower_addSubgroupOf_eq φ hsmul Λ π u hπ n]
55   exact PaperXI.FreeLatticeCard110.card_quotient_prime_pow b
56     (Ideal.span {π}) hI n
57 
58 end PowerQuotient
59 
60 section ActualDiagonalIndex
61 open Module Matrix ValuativeRel
62 variable (F E : Type*) [Field F] [Field E] [Algebra F E]
63   [Module.Finite F E] [ValuativeRel E] [TopologicalSpace E]
64   [IsNonarchimedeanLocalField E]
65 variable {m : Type*} [Fintype m] [DecidableEq m]
66 
67 /-- Multiplication by an actual nonzero integer-ring element, as an invertible
68 F-linear endomorphism of E. -/
69 def coefficientUnit (π : 𝒪[E]) (hπ : (π : E) ≠ 0) : (Module.End F E)ˣ :=
70   Units.map (Algebra.lmul F E).toRingHom (Units.mk0 (π : E) hπ)
71 
72 omit [Module.Finite F E] [TopologicalSpace E] [IsNonarchimedeanLocalField E] in
73 @[simp] theorem coefficientUnit_coe (π : 𝒪[E]) (hπ : (π : E) ≠ 0) :
74     (coefficientUnit F E π hπ : Module.End F E) = coefficientMap F E π := rfl
75 
76 /-- The cardinality of the actual diagonal intersection is derived from matrix
77 units, radical normalization, a finite full corner, and its residue quotients. -/
78 theorem card_diagonal_intersection
79     (L : Submodule 𝒪[E] (Matrix m m (Module.End F E)))
80     (hL : IsMatrixBimodule (coefficientMap F E) L.toAddSubgroup) (p : m)
81     (hfg : L.FG)
82     (hfull : Submodule.span F (L : Set (Matrix m m (Module.End F E))) = ⊤)
83     (π : 𝒪[E]) (hπirr : Irreducible π) (u : (Module.End F E)ˣ)
84     (hπ : (u : Module.End F E) = coefficientMap F E π)
85     (hu : u ∈ normalizingUnits (corner L.toAddSubgroup p)) (a : m → ℤ) :
86     Nat.card (L.toAddSubgroup ⧸
87       (L.toAddSubgroup ⊓ L.toAddSubgroup.map
88         (unitConjugation (diagonalUnit (fun i => u ^ a i))).toAddMonoidHom).addSubgroupOf
89           L.toAddSubgroup) =
90       Nat.card 𝓀[E] ^ (Module.finrank F E * ∑ i, ∑ j, (a i - a j).toNat) := by
91   let Λ := cornerSubmodule F E L hL p
92   obtain ⟨n, b, hn⟩ := exists_corner_basis_degree F E L hL p hfg hfull
93   let I : Ideal 𝒪[E] := Ideal.span {π}
94   have hI : I ≠ ⊥ := PaperXI.MoritaUniformizer110.uniformizerIdeal_ne_bot π hπirr
95   let : I.IsPrime := PaperXI.MoritaUniformizer110.uniformizerIdeal_isPrime π hπirr
96   have hsmul : ∀ (r : 𝒪[E]) (x : Module.End F E),
97       r • x = coefficientMap F E r * x := by intro r x; ext v; rfl
98   have hcoordinate (k : ℕ) :
99       Nat.card (Λ.toAddSubgroup ⧸
100         (leftPower Λ.toAddSubgroup u (k : ℤ)).addSubgroupOf Λ.toAddSubgroup) =
101           Nat.card 𝓀[E] ^ (k * Module.finrank F E) := by
102     rw [card_leftPower_quotient (coefficientMap F E) hsmul Λ b π hI u hπ k]
103     have hq : Nat.card (𝒪[E] ⧸ (Ideal.span {π} : Ideal 𝒪[E])) = Nat.card 𝓀[E] :=
104       PaperXI.MoritaUniformizer110.card_uniformizer_quotient π hπirr
105     rw [hq]
106     simp [hn]
107   have hbase : L.toAddSubgroup = entrywise (fun _ _ => Λ.toAddSubgroup) := by
108     exact eq_matrix_corner (coefficientMap F E) L.toAddSubgroup hL p
109   rw [intersection_eq_nonnegative_entrywise (coefficientMap F E) L.toAddSubgroup
110     hL p π u hπ hu a]
111   change Nat.card (L.toAddSubgroup ⧸
112     (entrywise (fun i j => leftPower Λ.toAddSubgroup u ((a i - a j).toNat : ℤ))).addSubgroupOf
113       L.toAddSubgroup) = _
114   rw [hbase, PaperXI.MoritaQuotient110.card_matrix_quotient]
115   simp_rw [hcoordinate, Finset.prod_pow_eq_pow_sum]
116   congr 1
117   simp_rw [← Finset.sum_mul]
118   exact Nat.mul_comm _ _
119 
120 /-- The original scalar radical-commutation equality supplies the corner
121 normalization used above; it is not an additional index premise. -/
122 theorem diagonal_relIndex_of_radical_commutation
123     (L : Submodule 𝒪[E] (Matrix m m (Module.End F E)))
124     (hL : IsMatrixBimodule (coefficientMap F E) L.toAddSubgroup) (p : m)
125     (hfg : L.FG)
126     (hfull : Submodule.span F (L : Set (Matrix m m (Module.End F E))) = ⊤)
127     (π : 𝒪[E]) (hπirr : Irreducible π) (u : (Module.End F E)ˣ)
128     (hπ : (u : Module.End F E) = coefficientMap F E π)
129     (hcomm : L.toAddSubgroup.map
130         (AddMonoidHom.mulLeft ((diagonalUnit (fun _ : m => u) :
131           (Matrix m m (Module.End F E))ˣ) : Matrix m m (Module.End F E))) =
132       L.toAddSubgroup.map
133         (AddMonoidHom.mulRight ((diagonalUnit (fun _ : m => u) :
134           (Matrix m m (Module.End F E))ˣ) : Matrix m m (Module.End F E))))
135     (a : m → ℤ) :
136     (L.toAddSubgroup ⊓ L.toAddSubgroup.map
137       (unitConjugation (diagonalUnit (fun i => u ^ a i))).toAddMonoidHom).relIndex
138         L.toAddSubgroup =
139       Nat.card 𝓀[E] ^ (Module.finrank F E * ∑ i, ∑ j, (a i - a j).toNat) := by
140   exact card_diagonal_intersection F E L hL p hfg hfull π hπirr u hπ
141     (corner_normalizes_of_scalar_commutation L.toAddSubgroup u p hcomm) a
142 
143 end ActualDiagonalIndex
144 end PaperXI.MoritaIndex110

Back to source controls