ActualELatticeScalarPeriod60.lean

1 import PaperXI.ActualELatticeFieldJoin59
2 import PaperXI.ActualEmbeddedUniformizer58
3 
4 /-!
5 # A base-field scalar period for the literal extension-field lattice chain
6 
7 The actual base-field uniformizer has nonzero extension-field degree. Otherwise
8 its image would be an integral extension-field unit, whose matrix determinant
9 degree vanishes, contradicting its known scalar-matrix degree. Choosing it or
10 its inverse supplies a positive period without assuming a ramification formula.
11 -/
12 set_option autoImplicit false
13 noncomputable section
14 namespace PaperXI.ActualELatticeScalarPeriod60
15 open Matrix ValuativeRel
16 open ActualLocalUnitTopology ActualLocalUnitDecomposition ActualDepthZeroExtension
17 open ActualEmbeddedUniformizer58 ActualELatticeResidue59 ActualELatticeNormalizer59
18 open ActualELatticeTypeGroup59 ActualELatticeFreeness59 ActualELatticeFieldJoin59
19 
20 variable (K E : Type*) [Field K] [ValuativeRel K] [TopologicalSpace K]
21   [IsNonarchimedeanLocalField K] [Field E] [ValuativeRel E] [TopologicalSpace E]
22   [IsNonarchimedeanLocalField E] [Algebra K E]
23 variable {d : Type*} [Fintype d] [DecidableEq d] [Nonempty d]
24 
25 /-- The actual base scalar cannot have zero extension-field degree. -/
26 theorem base_uniformizer_degree_ne_one (ι : E →ₐ[K] Matrix d d K)
27     (hι : Continuous ι) :
28     degree E (Units.map (algebraMap K E).toMonoidHom (uniformizerUnit K)) ≠ 1 := by
29   intro hz
30   have hu : Units.map (algebraMap K E).toMonoidHom (uniformizerUnit K) ∈ compactUnitSubgroup E := by
31     rw [← ker_degree]
32     exact hz
33   obtain ⟨u, hu⟩ := hu
34   have hd := determinantDegree_integral_unit K E d ι hι u
35   rw [hu, unitsEmbedding_baseScalar] at hd
36   change determinantDegree K d (scalarUniformizer K d) = 1 at hd
37   rw [determinantDegree_scalarUniformizer] at hd
38   have hn : (Fintype.card d : ℤ) = 0 := congrArg Multiplicative.toAdd hd
39   exact (Nat.ne_of_gt (Fintype.card_pos)).elim (Int.ofNat_eq_zero.mp hn)
40 
41 /-- The base uniformizer or its inverse has positive actual extension exponent. -/
42 theorem exists_positive_base_normalForm (ι : E →ₐ[K] Matrix d d K)
43     (hι : Continuous ι) :
44     ∃ c : Kˣ, ∃ u : 𝒪[E]ˣ, ∃ r : ℕ, 0 < r ∧
45       Units.map (algebraMap K E).toMonoidHom c = unitEmbedding E u * uniformizerUnit E ^ (r : ℤ) := by
46   obtain ⟨⟨u, z⟩, hz⟩ := (normalFormEquiv E).surjective
47     (Units.map (algebraMap K E).toMonoidHom (uniformizerUnit K))
48   have hn : z.toAdd ≠ 0 := by
49     intro hn
50     apply base_uniformizer_degree_ne_one K E ι hι
51     rw [← hz, normalFormEquiv_apply, degree_normalForm]
52     exact congrArg Multiplicative.ofAdd hn
53   have he : Units.map (algebraMap K E).toMonoidHom (uniformizerUnit K) =
54       unitEmbedding E u * uniformizerUnit E ^ z.toAdd := hz.symm
55   by_cases hp : 0 < z.toAdd
56   · refine ⟨uniformizerUnit K, u, z.toAdd.toNat, by omega, ?_⟩
57     simpa only [Int.toNat_of_nonneg hp.le] using he
58   · have hp' : 0 < -z.toAdd := by omega
59     refine ⟨(uniformizerUnit K)⁻¹, u⁻¹, (-z.toAdd).toNat, by omega, ?_⟩
60     rw [map_inv, he]
61     simp only [Int.toNat_of_nonneg hp'.le, map_inv, mul_inv, zpow_neg]
62 
63 variable (n : Type*) [Fintype n] [DecidableEq n]
64 
65 omit [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] in
66 /-- Any actual positive scalar normal form gives the literal chain period. -/
67 theorem chain_period_of_normalForm (c : Kˣ) (u : 𝒪[E]ˣ) (r : ℕ)
68     (he : Units.map (algebraMap K E).toMonoidHom c =
69       unitEmbedding E u * uniformizerUnit E ^ (r : ℤ)) :
70     ∀ i v, (c : K) • v ∈ latticeChain K E n (i + (r : ℤ)) ↔ v ∈ latticeChain K E n i := by
71   intro i v
72   have hu := integralMatrix_mem_stabilizer K E n (GeneralLinearGroup.scalar n u)
73   rw [integralMatrix_scalar] at hu
74   have hc : (c : K) • v = scalarAction K E n (Units.map (algebraMap K E).toMonoidHom c) v := by
75     ext j
76     simp [scalarAction_apply, Pi.smul_apply, Algebra.smul_def]
77   rw [hc, he, map_mul, map_zpow, LinearEquiv.mul_apply, hu]
78   exact periodicChain_shift (uniformizerAction K E n) (integralLattice E n) (r : ℤ) i v
79 
80 /-- A continuous finite matrix realization proves a positive period for all chain levels. -/
81 theorem exists_chain_period (ι : E →ₐ[K] Matrix d d K) (hι : Continuous ι) :
82     ∃ c : Kˣ, ∃ r : ℕ, 0 < r ∧
83       ∀ i v, (c : K) • v ∈ latticeChain K E n (i + (r : ℤ)) ↔ v ∈ latticeChain K E n i := by
84   obtain ⟨c, u, r, hr, he⟩ := exists_positive_base_normalForm K E ι hι
85   exact ⟨c, r, hr, chain_period_of_normalForm K E n c u r he⟩
86 
87 end PaperXI.ActualELatticeScalarPeriod60

Back to source controls