ActualIntegerTower111.lean

1 import PaperXI.MoritaActualCartan110
2 import Mathlib.RingTheory.Valuation.Extension
3 import Mathlib.Topology.Order.Compact
4 import Mathlib.Topology.Algebra.Valued.WithZeroMulInt
5 
6 /-! Actual integer-ring compatibility from the original continuous local-field
7 embedding. Scalar towers are constructed; none is a supplied arithmetic input. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.ActualIntegerTower111
11 open Matrix Module ValuativeRel Filter
12 open scoped Topology
13 open scoped WithZeroTopology
14 variable (F E : Type*) [Field F] [ValuativeRel F] [TopologicalSpace F]
15   [IsNonarchimedeanLocalField F] [Field E] [ValuativeRel E] [TopologicalSpace E]
16   [IsNonarchimedeanLocalField E] [Algebra F E]
17 
18 /-- Powers of a base integer stay in a compact image, forcing their extension
19 valuations to be bounded and hence the image to be an extension integer. -/
20 theorem map_integer_of_continuous (hF : Continuous (algebraMap F E))
21     {x : F} (hx : x ∈ (valuation F).integer) :
22     algebraMap F E x ∈ (valuation E).integer := by
23   have hc : IsCompact ((algebraMap F E) '' ((valuation F).integer : Set F)) :=
24     (IsNonarchimedeanLocalField.isCompact_closedBall F 1).image hF
25   obtain ⟨C, hC⟩ := hc.bddAbove_image (IsValuativeTopology.continuous_valuation.continuousOn)
26   have hpow (n : ℕ) : valuation E (algebraMap F E x) ^ n ≤ C := by
27     have hm : algebraMap F E (x ^ n) ∈ (algebraMap F E) '' ((valuation F).integer : Set F) :=
28       ⟨x ^ n, (valuation F).integer.pow_mem hx n, rfl⟩
29     simpa only [map_pow] using hC ⟨_, hm, rfl⟩
30   rw [Valuation.mem_integer_iff]
31   by_contra hn
32   have hgt : 1 < valuation E (algebraMap F E x) := lt_of_not_ge hn
33   let : MulArchimedean (ValueGroupWithZero E) :=
34     MulArchimedean.comap (IsNonarchimedeanLocalField.valueGroupWithZeroIsoInt E).toMonoidHom
35       (IsNonarchimedeanLocalField.valueGroupWithZeroIsoInt E).strictMono
36   obtain ⟨n, hn⟩ := MulArchimedean.arch (C * valuation E (algebraMap F E x)) hgt
37   have hCpos : 0 < C := zero_lt_one.trans_le (by simpa using hpow 0)
38   have hClt : C < C * valuation E (algebraMap F E x) := by
39     simpa only [mul_one] using mul_lt_mul_of_pos_left hgt hCpos
40   exact (not_lt_of_ge (hpow n)) (hClt.trans_le hn)
41 
42 /-- The actual integer-ring homomorphism restricts the original algebra map. -/
43 def integerMap (hF : Continuous (algebraMap F E)) : 𝒪[F] →+* 𝒪[E] :=
44   (algebraMap F E).restrict (valuation F).integer (valuation E).integer
45     (fun _ hx => map_integer_of_continuous F E hF hx)
46 
47 @[simp] theorem integerMap_coe (hF : Continuous (algebraMap F E)) (a : 𝒪[F]) :
48     (integerMap F E hF a : E) = algebraMap F E (a : F) := rfl
49 
50 /-- Continuity detects base integrality by sending inverse powers to zero. -/
51 theorem integer_of_map_integer (hF : Continuous (algebraMap F E)) (x : F)
52     (hE : valuation E (algebraMap F E x) ≤ 1) : valuation F x ≤ 1 := by
53   by_contra hx
54   have hxgt : 1 < valuation F x := lt_of_not_ge hx
55   have hx0 : x ≠ 0 := by intro hz; simp [hz] at hxgt
56   have hxin : valuation F x⁻¹ < 1 := by
57     rw [map_inv₀]
58     exact (inv_lt_one₀ (zero_lt_one.trans hxgt)).2 hxgt
59   let := IsTopologicalAddGroup.rightUniformSpace F
60   let := isUniformAddGroup_of_addCommGroup (G := F)
61   have hp : Tendsto (fun n : ℕ => x⁻¹ ^ n) atTop (𝓝 (0 : F)) :=
62     Valued.tendsto_zero_pow_of_v_lt_one (Γ₀ := ValueGroupWithZero F) hxin
63   have hpE : Tendsto (fun n : ℕ => (algebraMap F E x)⁻¹ ^ n) atTop (𝓝 (0 : E)) := by
64     simpa only [Function.comp_def, map_pow, map_inv₀, map_zero] using (hF.tendsto 0).comp hp
65   have hb : {z : E | valuation E z < 1} ∈ 𝓝 (0 : E) :=
66     (IsValuativeTopology.hasBasis_nhds_zero E).mem_of_mem
67       (i := (1 : (ValueGroupWithZero E)ˣ)) trivial
68   obtain ⟨n, hn⟩ := (hpE.eventually hb).exists
69   have he0 : 0 < valuation E (algebraMap F E x) := by
70     apply zero_lt_iff.mpr
71     simpa using hx0
72   have hge : 1 ≤ (valuation E (algebraMap F E x))⁻¹ := (one_le_inv₀ he0).2 hE
73   have hpn : 1 ≤ (valuation E (algebraMap F E x))⁻¹ ^ n := one_le_pow₀ hge
74   have hlt : (valuation E (algebraMap F E x))⁻¹ ^ n < 1 := by
75     simpa only [map_pow, map_inv₀] using hn
76   exact (not_lt_of_ge hpn) hlt
77 
78 /-- The two actual integer rings match under the original field embedding. -/
79 theorem integer_comap_eq (hF : Continuous (algebraMap F E)) :
80     (valuation E).integer.comap (algebraMap F E) = (valuation F).integer := by
81   ext x
82   change valuation E (algebraMap F E x) ≤ 1 ↔ valuation F x ≤ 1
83   exact ⟨integer_of_map_integer F E hF x,
84     fun hx => map_integer_of_continuous F E hF hx⟩
85 
86 /-- Valuation extension, up to the correct normalization equivalence, follows
87 from the original continuity input rather than being a new hypothesis. -/
88 theorem valuationExtension (hF : Continuous (algebraMap F E)) :
89     (valuation F).HasExtension (valuation E) :=
90   Valuation.HasExtension.ofComapInteger (integer_comap_eq F E hF)
91 
92 /-- The native extension algebra on integer rings is built from the derived valuation extension. -/
93 @[instance_reducible] def integerAlgebra (hF : Continuous (algebraMap F E)) : Algebra 𝒪[F] 𝒪[E] := by
94   let : (valuation F).HasExtension (valuation E) := valuationExtension F E hF
95   infer_instance
96 
97 @[simp] theorem integerAlgebra_map_coe (hF : Continuous (algebraMap F E)) (a : 𝒪[F]) :
98     letI : Algebra 𝒪[F] 𝒪[E] := integerAlgebra F E hF
99     (algebraMap 𝒪[F] 𝒪[E] a : E) = algebraMap F E (a : F) := rfl
100 
101 /-- Compatibility on E itself is the native integer-ring scalar tower. -/
102 theorem integer_tower (hF : Continuous (algebraMap F E)) :
103     letI : Algebra 𝒪[F] 𝒪[E] := integerAlgebra F E hF
104     IsScalarTower 𝒪[F] 𝒪[E] E := by
105   let : (valuation F).HasExtension (valuation E) := valuationExtension F E hF
106   infer_instance
107 
108 /-- The induced integer algebra uses exactly the original restricted field map. -/
109 theorem integerAlgebra_map_eq (hF : Continuous (algebraMap F E)) :
110     letI : Algebra 𝒪[F] 𝒪[E] := integerAlgebra F E hF
111     algebraMap 𝒪[F] 𝒪[E] = integerMap F E hF := by
112   ext a
113   rfl
114 
115 /-- Valuation comparisons are preserved; equality of differently normalized
116 numeric valuations is not claimed. -/
117 theorem map_valuation_le_iff (hF : Continuous (algebraMap F E)) (x y : F) :
118     valuation E (algebraMap F E x) ≤ valuation E (algebraMap F E y) ↔
119       valuation F x ≤ valuation F y := by
120   let : (valuation F).HasExtension (valuation E) := valuationExtension F E hF
121   exact Valuation.HasExtension.val_map_le_iff (valuation F) (valuation E) x y
122 
123 omit [TopologicalSpace F] [IsNonarchimedeanLocalField F] [ValuativeRel E]
124   [TopologicalSpace E] [IsNonarchimedeanLocalField E] in
125 /-- The original base-integer action on the F-linear endomorphism carrier is unchanged. -/
126 theorem integer_end_smul_apply (r : 𝒪[F]) (f : Module.End F E) (v : E) :
127     (r • f) v = (r : F) • f v := rfl
128 
129 /-- Both integer-ring actions on the original F-linear endomorphism carrier
130 are compatible, via scalar multiplication on the codomain E. -/
131 theorem integer_end_tower (hF : Continuous (algebraMap F E)) :
132     letI : Algebra 𝒪[F] 𝒪[E] := integerAlgebra F E hF
133     IsScalarTower 𝒪[F] 𝒪[E] (Module.End F E) := by
134   let : Algebra 𝒪[F] 𝒪[E] := integerAlgebra F E hF
135   let : IsScalarTower 𝒪[F] 𝒪[E] E := integer_tower F E hF
136   infer_instance
137 
138 variable (m : Type*) [Fintype m] [DecidableEq m]
139 
140 omit [TopologicalSpace F] [IsNonarchimedeanLocalField F] [ValuativeRel E]
141   [TopologicalSpace E] [IsNonarchimedeanLocalField E] [Fintype m] [DecidableEq m] in
142 /-- The native base-integer action on matrices is entrywise on the same endomorphisms. -/
143 theorem integer_matrix_smul_apply (r : 𝒪[F])
144     (x : Matrix m m (Module.End F E)) (i j : m) (v : E) :
145     (r • x) i j v = (r : F) • (x i j) v := rfl
146 
147 omit [Fintype m] [DecidableEq m] in
148 /-- Entrywise matrix actions retain that proved integer-ring scalar tower. -/
149 theorem integer_matrix_tower (hF : Continuous (algebraMap F E)) :
150     letI : Algebra 𝒪[F] 𝒪[E] := integerAlgebra F E hF
151     IsScalarTower 𝒪[F] 𝒪[E] (Matrix m m (Module.End F E)) := by
152   let : Algebra 𝒪[F] 𝒪[E] := integerAlgebra F E hF
153   let : IsScalarTower 𝒪[F] 𝒪[E] (Module.End F E) := integer_end_tower F E hF
154   infer_instance
155 
156 variable [Module.Finite F E]
157 open PaperXI.MoritaLattice110 PaperXI.MoritaCornerRank110 PaperXI.MoritaCartanTransport110
158 open PaperXI.MoritaActualCartan110
159 
160 /-- The actual base-integer lattice now meets110's scalar-upgrade interface
161 without any scalar-tower premise, on its original additive carrier. -/
162 theorem exists_actual_cartan_index_of_integer_lattice [Nonempty m]
163     (hF : Continuous (algebraMap F E))
164     (L : Submodule 𝒪[F] (Matrix m m (Module.End F E)))
165     (hL : IsMatrixBimodule (coefficientMap F E) L.toAddSubgroup) (hfg : L.FG)
166     (hfull : Submodule.span F (L : Set (Matrix m m (Module.End F E))) = ⊤)
167     (hcomm : RadicalCommutes F E m L.toAddSubgroup) (y : GL m E) :
168     ∃ a : m → ℕ,
169       (L.toAddSubgroup ⊓ L.toAddSubgroup.map
170         (unitConjugation (centralizerEmbedding F E m y)).toAddMonoidHom).relIndex
171           L.toAddSubgroup =
172       Nat.card 𝓀[E] ^ (Module.finrank F E * ∑ i, ∑ j, ((a i : ℤ) - (a j : ℤ)).toNat) := by
173   let : Algebra 𝒪[F] 𝒪[E] := integerAlgebra F E hF
174   let : IsScalarTower 𝒪[F] 𝒪[E] (Matrix m m (Module.End F E)) :=
175     integer_matrix_tower F E m hF
176   exact exists_actual_cartan_index_of_base_lattice F E m L hL hfg hfull hcomm y
177 
178 end PaperXI.ActualIntegerTower111

Back to source controls