English
For a K-basis B with i such that B i = 1 and IsNonarchimedean, there exists c > 0 with ∀ x,y ∈ L, B.norm(xy) ≤ c B.norm x B.norm y.
Русский
Для базиса K-L существует c > 0 такое, что для любых x,y ∈ L верно B.norm(xy) ≤ c B.norm x B.norm y.
LaTeX
$$$\exists c>0,\; \forall x,y\in L,\ B.norm(xy) \le c \cdot B.norm(x) \cdot B.norm(y)$$$
Lean4
/-- If `K` is a nonarchimedean normed field `L/K` is a finite extension, then there exists a
power-multiplicative nonarchimedean `K`-algebra norm on `L` extending the norm on `K`. -/
theorem exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional (hfd : FiniteDimensional K L)
(hna : IsNonarchimedean (norm : K → ℝ)) :
∃ f : AlgebraNorm K L, IsPowMul f ∧ (∀ (x : K), f ((algebraMap K L) x) = ‖x‖) ∧ IsNonarchimedean f := by
-- Choose a basis B = {1, e2,..., en} of the K-vector space L
set h1 : LinearIndepOn K id ({ 1 } : Set L) := LinearIndepOn.id_singleton _ one_ne_zero
set ι := { x // x ∈ LinearIndepOn.extend h1 (Set.subset_univ ({ 1 } : Set L)) }
set B : Basis ι K L := Basis.extend h1
letI hfin : Fintype ι := FiniteDimensional.fintypeBasisIndex B
haveI hem : Nonempty ι := B.index_nonempty
have h1L : (1 : L) ∈ LinearIndepOn.extend h1 _ := Basis.subset_extend _ (Set.mem_singleton (1 : L))
have hB1 : B ⟨1, h1L⟩ = (1 : L) := by
rw [Basis.coe_extend, Subtype.coe_mk]
-- Define a function g : L → ℝ by setting g (∑ki • ei) = maxᵢ ‖ ki ‖
set g : L → ℝ := B.norm
have hg0 : g 0 = 0 := B.norm_zero
have hg_nonneg : ∀ x : L, 0 ≤ g x := fun x ↦ by simp only [g, Basis.norm];
simp
-- g extends the norm on K
have hg_ext : ∀ (x : K), g ((algebraMap K L) x) = ‖x‖ := Basis.norm_extends hB1
have hg_na : IsNonarchimedean g := Basis.norm_isNonarchimedean hna
have hg_add : ∀ a b : L, g (a + b) ≤ g a + g b := fun _ _ ↦ IsNonarchimedean.add_le hg_nonneg hg_na
have hg_neg : ∀ a : L, g (-a) = g a := B.norm_neg
obtain ⟨_, _, hg_bdd⟩ := Basis.norm_mul_le_const_mul_norm hB1 hna
have hg_mul : ∀ (k : K) (y : L), g ((algebraMap K L) k * y) = g ((algebraMap K L) k) * g y := fun k y ↦
Basis.norm_smul hB1 k y
set f := seminormFromBounded hg0 hg_nonneg hg_bdd hg_add hg_neg
have hf_na : IsNonarchimedean f := seminormFromBounded_isNonarchimedean hg_nonneg hg_bdd hg_na
have hf_1 : f 1 ≤ 1 := seminormFromBounded_one_le hg_nonneg hg_bdd
have hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ‖x‖ := fun k ↦
hg_ext k ▸
seminormFromBounded_of_mul_apply hg_nonneg hg_bdd
(hg_mul k)
-- Using BGR Prop. 1.3.2/1, we obtain from f a power multiplicative K-algebra norm on L
-- extending the norm on K.
set F' := smoothingSeminorm f hf_1 hf_na with hF'
have hF'_ext : ∀ k : K, F' ((algebraMap K L) k) = ‖k‖ :=
by
intro k
rw [← hf_ext _]
exact
smoothingSeminorm_apply_of_map_mul_eq_mul f hf_1 hf_na
(seminormFromBounded_of_mul_is_mul hg_nonneg hg_bdd (hg_mul k))
have hF'_1 : F' 1 = 1 := by
have h1 : (1 : L) = (algebraMap K L) 1 := by rw [map_one]
simp only [h1, hF'_ext (1 : K), norm_one]
have hF'_0 : F' ≠ 0 := DFunLike.ne_iff.mpr ⟨(1 : L), by rw [hF'_1]; exact one_ne_zero⟩
set F : AlgebraNorm K L :=
{ RingSeminorm.toRingNorm F' hF'_0 with
smul' := fun k y ↦
by
have hk : ∀ y : L, f (algebraMap K L k * y) = f (algebraMap K L k) * f y :=
seminormFromBounded_of_mul_is_mul hg_nonneg hg_bdd (hg_mul k)
have hfk : ‖k‖ = (smoothingSeminorm f hf_1 hf_na) ((algebraMap K L) k) := by
rw [← hf_ext k, eq_comm, smoothingSeminorm_apply_of_map_mul_eq_mul f hf_1 hf_na hk]
simp only [hfk, hF']
-- TODO: There are missing `simp` lemmas here, that should be able to convert
-- `((smoothingSeminorm f hf_1 hf_na).toRingNorm ⋯).toRingSeminorm y` to
-- `(smoothingSeminorm f hf_1 hf_na y)`, after which the `erw` would work as a `rw`.
erw [← smoothingSeminorm_of_mul f hf_1 hf_na hk y]
rw [Algebra.smul_def]
rfl }
have hF_ext (k : K) : F ((algebraMap K L) k) = ‖k‖ :=
by
rw [← hf_ext]
exact
smoothingSeminorm_apply_of_map_mul_eq_mul f hf_1 hf_na
(seminormFromBounded_of_mul_is_mul hg_nonneg hg_bdd (hg_mul k))
exact ⟨F, isPowMul_smoothingFun f hf_1, hF_ext, isNonarchimedean_smoothingFun f hf_1 hf_na⟩
