ActualELatticeFreeness59.lean

1 import PaperXI.ActualELatticeTypeGroup59
2 
3 /-!
4 # Uniformizer freeness for the actual lattice-product group
5 
6 Freeness is proved directly from the integral lattice and the strict valuation
7 of the actual extension-field uniformizer. It does not assume compactness of
8 the group or a matrix determinant identity.
9 -/
10 set_option autoImplicit false
11 noncomputable section
12 namespace PaperXI.ActualELatticeFreeness59
13 open Matrix ValuativeRel
14 open ActualELatticeNormalizer59 ActualELatticeResidue59 ActualELatticeTypeGroup59
15 
16 variable (K E : Type*) [Field K] [Field E] [Algebra K E]
17 variable (n : Type*) [Fintype n] [DecidableEq n]
18 variable [ValuativeRel E] [TopologicalSpace E] [IsNonarchimedeanLocalField E]
19 
20 /-- Literal extension-field scalar multiplication as a group homomorphism. -/
21 def scalarAction : Eˣ →* ((n → E) ≃ₗ[K] (n → E)) where
22   toFun u := (LinearEquiv.smulOfUnit u : (n → E) ≃ₗ[E] (n → E)).restrictScalars K
23   map_one' := by ext v i; simp [LinearEquiv.smulOfUnit]
24   map_mul' u v := by ext w i; simp [LinearEquiv.smulOfUnit, mul_smul]
25 
26 omit [Fintype n] [DecidableEq n] [ValuativeRel E]
27   [TopologicalSpace E] [IsNonarchimedeanLocalField E] in
28 @[simp] theorem scalarAction_apply (u : Eˣ) (v : n → E) :
29     scalarAction K E n u v = (u : E) • v := rfl
30 
31 omit [Fintype n] [DecidableEq n] in
32 /-- Every integer power acts by the corresponding actual field scalar. -/
33 theorem uniformizerAction_zpow_apply (r : ℤ) (v : n → E) :
34     (uniformizerAction K E n ^ r) v =
35       (ActualLocalUnitDecomposition.uniformizer E : E) ^ r • v := by
36   change ((scalarAction K E n (ActualLocalUnitDecomposition.uniformizerUnit E)) ^ r) v = _
37   rw [← map_zpow, scalarAction_apply, Units.val_zpow_eq_zpow_val]
38   rfl
39 
40 /-- The entire actual product group preserves each lattice level. -/
41 theorem typeGroup_le_stabilizer :
42     typeGroup K E n ≤ chainStabilizer (latticeChain K E n) := by
43   apply sup_le
44   · rintro g ⟨h, rfl⟩
45     exact integralMatrix_mem_stabilizer K E n h
46   · exact firstCongruence_le (latticeChain K E n)
47 
48 /-- A uniformizer power preserving the integral lattice has nonnegative exponent. -/
49 theorem uniformizerAction_exponent_nonneg [Nonempty n] (r : ℤ)
50     (hr : uniformizerAction K E n ^ r ∈ typeGroup K E n) : 0 ≤ r := by
51   classical
52   let i : n := Classical.choice inferInstance
53   have hv : (fun _ : n => (1 : E)) ∈ integralLattice E n :=
54     fun _ => (valuation E).integer.one_mem
55   have hg := typeGroup_le_stabilizer K E n hr
56   have h := (hg 0 (fun _ : n => (1 : E))).mpr (by rw [latticeChain_zero]; exact hv)
57   rw [latticeChain_zero, uniformizerAction_zpow_apply] at h
58   have hi := h i
59   change valuation E ((ActualLocalUnitDecomposition.uniformizer E : E) ^ r * 1) ≤ 1 at hi
60   simp only [mul_one, map_zpow₀] at hi
61   exact (zpow_le_one_iff_right_of_lt_one₀
62     (ActualLocalUnitDecomposition.uniformizer_value_pos E)
63     (ActualLocalUnitDecomposition.uniformizer_value_lt_one E)).mp hi
64 
65 /-- No nonzero uniformizer power belongs to the actual lattice-product group. -/
66 theorem uniformizerAction_free [Nonempty n] (r : ℤ)
67     (hr : uniformizerAction K E n ^ r ∈ typeGroup K E n) : r = 0 := by
68   have h₁ := uniformizerAction_exponent_nonneg K E n r hr
69   have h₂ := uniformizerAction_exponent_nonneg K E n (-r)
70     (by simpa using (typeGroup K E n).inv_mem hr)
71   omega
72 
73 end PaperXI.ActualELatticeFreeness59

Back to source controls