feat(Analysis/Normed): Krasner's lemma (leanprover-community#26390)

This PR continues the work from leanprover-community#18444.

Original PR: leanprover-community#18444

Co-authored-by: Jiedong Jiang <emailboxofjjd@163.com>
Co-authored-by: jjdishere <emailboxofjjd@163.com>
Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Author: jjdishere

Mathlib.lean

@@ -1987,6 +1987,7 @@ public import Mathlib.Analysis.Normed.Algebra.Unitization
 public import Mathlib.Analysis.Normed.Algebra.UnitizationL1
 public import Mathlib.Analysis.Normed.Field.Basic
 public import Mathlib.Analysis.Normed.Field.Instances
+public import Mathlib.Analysis.Normed.Field.Krasner
 public import Mathlib.Analysis.Normed.Field.Lemmas
 public import Mathlib.Analysis.Normed.Field.ProperSpace
 public import Mathlib.Analysis.Normed.Field.TransferInstance

Mathlib/Algebra/Field/Subfield/Basic.lean

@@ -160,6 +160,13 @@ theorem mem_map {f : K →+* L} {s : Subfield K} {y : L} : y ∈ s.map f ↔ ∃
   unfold map
   simp only [mem_mk, Subring.mem_map, mem_toSubring]
 
+-- Higher priority to apply before `mem_map`.
+@[simp 1100]
+theorem map_mem_map (f : K →+* L) {s : Subfield K} {x : K} : f x ∈ s.map f ↔ x ∈ s :=
+  calc
+    _ ↔ f x ∈ (s.map f : Set L) := Iff.rfl
+    _ ↔ _ := by simp [Function.Injective.mem_set_image (f := f) f.injective]
+
 theorem map_map (g : L →+* M) (f : K →+* L) : (s.map f).map g = s.map (g.comp f) :=
   SetLike.ext' <| Set.image_image _ _ _
 

Mathlib/Analysis/Normed/Algebra/Basic.lean

@@ -30,6 +30,19 @@ normed algebra, character space, continuous functional calculus
 
 @[expose] public section
 
+namespace IntermediateField
+
+variable {K L : Type*} [NontriviallyNormedField K] [NormedField L] [NormedAlgebra K L]
+
+set_option backward.isDefEq.respectTransparency false in
+instance (F : IntermediateField K L) : NontriviallyNormedField F where
+  __ := SubfieldClass.toNormedField F
+  non_trivial := by
+    obtain ⟨k, hk⟩ :=  @NontriviallyNormedField.non_trivial K _
+    use algebraMap K F k
+    simp [hk]
+
+end IntermediateField
 
 variable {𝕜 : Type*} {A : Type*}
 

Mathlib/Analysis/Normed/Field/Krasner.lean

@@ -0,0 +1,148 @@
+/-
+Copyright (c) 2025 Jiedong Jiang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jiedong Jiang
+-/
+module
+
+public import Mathlib.Analysis.Normed.Algebra.Ultra
+public import Mathlib.Analysis.Normed.Unbundled.SpectralNorm
+public import Mathlib.FieldTheory.Minpoly.IsConjRoot
+public import Mathlib.FieldTheory.SeparableDegree
+public import Mathlib.Analysis.Normed.Algebra.Basic
+
+/-!
+# Krasner's Lemma
+
+In this file, we prove Krasner's lemma.
+
+## Main definitions
+
+* `IsKrasner K L` : Given a field extension `L / K` where `L` is a normed field,
+`IsKrasner K L` is the abstraction of the conclusion of Krasner's lemma. That is, `IsKrasner K L`
+means that given two elements `x y : L`, such that `x` is separable over `K`, all conjugate roots
+of `x` live in `L`, `y` is integral over `K`, and the distance between `x` and `y` is less than
+the distance between `x` and any other conjugate root of `x`, then `x` is in the field
+generated by `K` and `y`.
+
+## Main results
+
+* `IsKrasner.of_complete` : If `K` is a complete normed field, such that
+the norm of `L` extends the norm on `K`, then `IsKrasner K L` holds for every
+algebraic extension `L` over `K`. This implies the classical Krasner's lemma by taking `L` as the
+separable closure of `K`.
+
+## Reference
+
+For the classical statement of Krasner's lemma, please see the
+[wikipedia page](https://en.wikipedia.org/wiki/Krasner%27s_lemma).
+
+## Tags
+Krasner's lemma, normed field
+-/
+
+@[expose] public section
+
+open IntermediateField
+
+variable (K L : Type*) [NormedField L]
+
+/--
+Given a field extension `L / K` where `L` is a normed field, `IsKrasner K L` is the abstraction
+of the conclusion of Krasner's lemma. That is, `IsKrasner K L` means that given two elements
+`x y : L`, such that `x` is separable over `K`, all conjugate roots of `x` live in `L`,
+`y` is integral over `K`, and the distance between `x` and `y` is less than the distance between
+`x` and any other conjugate root of `x`, then `x` is in the field generated by `K` and `y`.
+-/
+class IsKrasner [Field K] [Algebra K L] : Prop where
+  krasner' {x y : L} : IsSeparable K x → ((minpoly K x).map (algebraMap K L)).Splits →
+    IsIntegral K y → (∀ x' : L, IsConjRoot K x x' →  x ≠ x' → ‖x - y‖ < ‖x - x'‖) → x ∈ K⟮y⟯
+
+namespace IsKrasner
+
+variable {K L} in
+theorem krasner [Field K] [Algebra K L]
+    [IsKrasner K L] {x y : L} (hx : (minpoly K x).Separable)
+    (sp : ((minpoly K x).map (algebraMap K L)).Splits) (hy : IsIntegral K y)
+    (h : (∀ x' : L, IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖)) : x ∈ K⟮y⟯ :=
+  IsKrasner.krasner' hx sp hy h
+
+variable [NontriviallyNormedField K] [CompleteSpace K] [IsUltrametricDist K]
+    [NormedAlgebra K L] [Algebra.IsAlgebraic K L]
+
+set_option backward.isDefEq.respectTransparency false in
+/-- Krasner's lemma assuming `Normal K L`. -/
+theorem of_completeSpace_of_normal [Normal K L] : IsKrasner K L where
+  krasner' {x} {y} xsep sp yint kr := by
+    let z := x - y
+    have := IntermediateField.adjoin.finiteDimensional yint
+    have : IsUltrametricDist L := IsUltrametricDist.of_normedAlgebra K
+    let y' : K⟮y⟯ := IntermediateField.AdjoinSimple.gen K y
+    have zsep : IsSeparable K⟮y⟯ z :=
+      Field.isSeparable_sub (IsSeparable.tower_top K⟮y⟯ xsep) (isSeparable_algebraMap y')
+    -- It suffices to show that `z = x - y ∈ K⟮y⟯`.
+    suffices z ∈ K⟮y⟯ by simpa [z, y'] using add_mem this y'.2
+    have : z ∈ K⟮y⟯ ↔ z ∈ (⊥ : Subalgebra K⟮y⟯ L) := by simp [Algebra.mem_bot]
+    rw [this]
+    -- Suppose not, then there exists nontrivial Galois conjugates `z'` of `z` over `K⟮y⟯` in `L`.
+    by_contra hz
+    obtain ⟨z', hne, h1⟩ := (notMem_iff_exists_ne_and_isConjRoot zsep
+        (minpoly_sub_algebraMap_splits y' (IsIntegral.minpoly_splits_tower_top
+          xsep.isIntegral sp))).mp hz
+    obtain ⟨σ, hσ⟩ := isConjRoot_iff_exists_algEquiv.mp h1
+    apply_fun σ.symm at hσ
+    simp only [AlgEquiv.symm_apply_apply] at hσ
+    -- However, `‖z - z'‖ ≤ max ‖z‖ ‖z'‖ = ‖z‖ = ‖x - y‖ < ‖y - y'‖ = ‖z - z'‖`, where `y' = x - z`.
+    -- This is a contradiction.
+    have : ‖z - z'‖ < ‖z - z'‖ :=
+      calc
+        _ ≤ max ‖z‖ ‖z'‖ := by
+          simpa [norm_neg, sub_eq_add_neg] using (IsUltrametricDist.norm_add_le_max z (- z'))
+        _ ≤ ‖x - y‖ := by
+          simp only [NormedAlgebra.norm_eq_spectralNorm K, hσ, sup_le_iff]
+          rw [← AlgEquiv.restrictScalars_apply K,
+              ← spectralNorm_eq_of_equiv (σ.symm.restrictScalars K)]
+          simp [z]
+        _ < ‖x - (z' + y)‖ := by
+          apply kr (z' + y)
+          · apply IsConjRoot.of_isScalarTower (L := K⟮y⟯) xsep.isIntegral
+            simpa [z, y'] using IsConjRoot.add_algebraMap y' h1
+          · simpa [z, sub_eq_iff_eq_add] using hne
+        _ = ‖z - z'‖ := by congr 1; ring
+    simp [lt_self_iff_false] at this
+
+set_option backward.isDefEq.respectTransparency false in
+/--
+If `K` is a complete nontrivially normed field and `L` is an algebraic extension of `K`
+such that the norm of `L` extends the norm on `K`, then `IsKrasner K L` holds.
+This corresponds to the classical Krasner's lemma.
+-/
+instance of_completeSpace : IsKrasner K L where
+  krasner' {x} {y} xsep sp yint kr := by
+    -- Reduce to the case `L = algebraic closure of K` to apply the previous lemma.
+    let C := AlgebraicClosure K
+    let : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
+    let : NormedAlgebra K C := spectralNorm.normedAlgebra K C
+    let iL : L →ₐ[K] C := IsAlgClosed.lift
+    algebraize [iL.toRingHom]
+    let : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
+    let := IsKrasner.of_completeSpace_of_normal K C
+    -- The norm on `L` is compatible with the norm on the algebraic closure of `K`,
+    -- this gives the result.
+    have norm_iL (x : L) : ‖iL x‖ = ‖x‖ := norm_algebraMap' _ _
+    suffices this : iL x ∈ K⟮iL y⟯ by
+      simpa [← Set.image_singleton, ← IntermediateField.adjoin_map] using this
+    refine IsKrasner.krasner ((xsep.map _ iL.injective).of_dvd dvd_rfl) ?_ (yint.map iL) ?_
+    · exact Polynomial.Splits.of_dvd (sp.of_isScalarTower C)
+        (Polynomial.map_ne_zero (minpoly.ne_zero xsep.isIntegral))
+        (Polynomial.map_dvd _ (by simpa using minpoly.dvd_map_of_isScalarTower' K K C x))
+    · intros xC' hx' hne
+      have : xC' ∈ (minpoly K x).rootSet C := by
+        rwa [isConjRoot_iff_mem_minpoly_rootSet (xsep.isIntegral.map _),
+          minpoly.algHom_eq iL iL.injective x] at hx'
+      simp only [← sp.image_rootSet iL, Set.mem_image] at this
+      obtain ⟨c, hc, rfl⟩ := this
+      rw [← isConjRoot_iff_mem_minpoly_rootSet xsep.isIntegral] at hc
+      simpa [norm_iL, ← map_sub] using kr c hc (fun h ↦ (iff_false_intro hne).mp (congrArg iL h))
+
+end IsKrasner

Mathlib/Analysis/Normed/Unbundled/AlgebraNorm.lean

@@ -179,8 +179,35 @@ theorem extends_norm' (f : MulAlgebraNorm R S) (a : R) : f (a • (1 : S)) = ‖
 theorem extends_norm (f : MulAlgebraNorm R S) (a : R) : f (algebraMap R S a) = ‖a‖ := by
   rw [Algebra.algebraMap_eq_smul_one]; exact extends_norm' _ _
 
+/-- The algebra norm underlying an multiplicative algebra norm. -/
+def toAlgebraNorm (f : MulAlgebraNorm R S) : AlgebraNorm R S where
+  __ := f
+  mul_le' _ _ := (f.map_mul' _ _).le
+
+instance instCoeAlgebraNorm : Coe (MulAlgebraNorm R S) (AlgebraNorm R S) := ⟨toAlgebraNorm⟩
+
+@[simp]
+lemma coe_AlgebraNorm (f : MulAlgebraNorm R S) : ⇑(f : AlgebraNorm R S) = ⇑f := rfl
+
 end MulAlgebraNorm
 
+namespace NormedAlgebra
+
+variable (K L : Type*) [NormedField K] [NormedField L] [NormedAlgebra K L]
+
+/-- Given a normed field extension `L / K`, the norm on `L` is a multiplicative `K`-algebra norm. -/
+def toMulAlgebraNorm : MulAlgebraNorm K L where
+  __ := NormedField.toMulRingNorm L
+  smul' r x := by
+    simp only [Algebra.smul_def, AddGroupSeminorm.toFun_eq_coe, MulRingSeminorm.toFun_eq_coe,
+      map_mul, mul_eq_mul_right_iff, map_eq_zero]
+    exact Or.inl <| norm_algebraMap' L r
+
+@[simp]
+lemma toMulAlgebraNorm_apply (x : L) : toMulAlgebraNorm K L x = ‖x‖ := rfl
+
+end NormedAlgebra
+
 namespace MulRingNorm
 
 variable {R : Type*} [NonAssocRing R]

Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean

@@ -800,6 +800,16 @@ theorem spectralNorm_unique_field_norm_ext [CompleteSpace K]
   have hgx : f x = g x := rfl
   rw [hgx, spectralNorm_unique hg_pow, spectralAlgNorm_def]
 
+variable (K) in
+/-- If `K` is a field complete with respect to a nontrivial nonarchimedean multiplicative norm and
+  `L/K` is an algebraic normed field extension, then the norm on `L` coincides with the spectral
+  norm. -/
+theorem NormedAlgebra.norm_eq_spectralNorm {L : Type*} [NormedField L] [NormedAlgebra K L]
+    [Algebra.IsAlgebraic K L] [CompleteSpace K] (x : L) : ‖x‖ = spectralNorm K L x := by
+  rw [← toMulAlgebraNorm_apply K L x, ← spectralAlgNorm_def, ← MulAlgebraNorm.coe_AlgebraNorm,
+      spectralNorm_unique (f := (toMulAlgebraNorm K L).toAlgebraNorm)
+      (MulRingNorm.isPowMul (toMulAlgebraNorm K L).toMulRingNorm)]
+
 /-- Given a nonzero `x : L`, and assuming that `(spectralAlgNorm h_alg hna) 1 ≤ 1`, this is
   the real-valued function sending `y ∈ L` to the limit of  `(f (y * x^n))/((f x)^n)`,
   regarded as an algebra norm. -/
@@ -881,24 +891,51 @@ def nontriviallyNormedField [CompleteSpace K] : NontriviallyNormedField L where
     let ⟨x, hx⟩ := NontriviallyNormedField.non_trivial (α := K)
     ⟨algebraMap K L x, hx.trans_eq <| (spectralNorm_extends _).symm⟩
 
-/-- `L` with the spectral norm is a `normed_add_comm_group`. -/
+/-- `L` with the spectral norm is a `SeminormedRing`. -/
+def seminormedRing : SeminormedRing L := by
+  letI : NormedField L := normedField K L
+  infer_instance
+
+/-- `L` with the spectral norm is a `NormedAddCommGroup`. -/
 def normedAddCommGroup : NormedAddCommGroup L := by
   haveI : NormedField L := normedField K L
   infer_instance
 
-/-- `L` with the spectral norm is a `seminormed_add_comm_group`. -/
+/-- `L` with the spectral norm is a `SeminormedAddCommGroup`. -/
 def seminormedAddCommGroup : SeminormedAddCommGroup L := by
   have : NormedField L := normedField K L
   infer_instance
 
-/-- `L` with the spectral norm is a `normed_space` over `K`. -/
+/-- `L` with the spectral norm is a `NormedSpace` over `K`. -/
 def normedSpace : @NormedSpace K L _ (seminormedAddCommGroup K L) :=
   letI _ := seminormedAddCommGroup K L
   { (inferInstance : Module K L) with
     norm_smul_le r x := by
       change spectralAlgNorm K L (r • x) ≤ ‖r‖ * spectralAlgNorm K L x
       exact le_of_eq (map_smul_eq_mul _ _ _) }
 
+/-- `L` with the spectral norm is a `NormedAlgebra` over `K`. -/
+def normedAlgebra :
+    @NormedAlgebra K L _ (seminormedRing K L) :=
+  letI _ := normedField K L
+  { normedSpace K L, (inferInstance : Algebra K L) with }
+
+set_option backward.isDefEq.respectTransparency false in
+/-- `L` with the spectral norm is a `NormedAlgebra` over any intermedate `E`
+that is a normed algebra over `K`. -/
+def normedAlgebra' (E L : Type*) [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [NormedField E]
+    [NormedAlgebra K E] [Algebra E L] [IsScalarTower K E L] :
+    @NormedAlgebra E L _ (seminormedRing K L) :=
+  letI _ := normedField K L
+  letI _ := normedAlgebra K L
+  letI _ := Algebra.IsAlgebraic.tower_bot K E L
+  { (inferInstance : Algebra E L) with
+    norm_smul_le _ _ := by
+      apply le_of_eq
+      simp only [Algebra.smul_def, norm_mul, mul_eq_mul_right_iff, _root_.norm_eq_zero]
+      simp only [NormedAlgebra.norm_eq_spectralNorm K]
+      exact Or.inl <| (spectralNorm.eq_of_tower _).symm }
+
 /-- The metric space structure on `L` induced by the spectral norm. -/
 def metricSpace : MetricSpace L := (normedField K L).toMetricSpace
 

Mathlib/FieldTheory/IntermediateField/Basic.lean

@@ -482,6 +482,18 @@ theorem toSubfield_map (f : L →ₐ[K] L') : (S.map f).toSubfield = S.toSubfiel
 theorem map_id : S.map (AlgHom.id K L) = S :=
   SetLike.coe_injective <| Set.image_id _
 
+@[simp]
+lemma mem_map {f : L →ₐ[K] L'} {y : L'} : y ∈ S.map f ↔ ∃ x ∈ S, f x = y :=
+  Set.mem_image f S y
+
+-- Higher priority to apply before `mem_map`.
+@[simp 1100]
+theorem map_mem_map (f : L →ₐ[K] L') {x : L} :
+    f x ∈ map f S ↔ x ∈ S :=
+  calc
+    _ ↔ f x ∈ (map f S : Set L') := Iff.rfl
+    _ ↔ _ := by simp [Function.Injective.mem_set_image (f := f) f.injective]
+
 theorem map_map {K L₁ L₂ L₃ : Type*} [Field K] [Field L₁] [Algebra K L₁] [Field L₂] [Algebra K L₂]
     [Field L₃] [Algebra K L₃] (E : IntermediateField K L₁) (f : L₁ →ₐ[K] L₂) (g : L₂ →ₐ[K] L₃) :
     (E.map f).map g = E.map (g.comp f) :=

Mathlib/FieldTheory/Normal/Defs.lean

@@ -71,6 +71,10 @@ theorem Normal.tower_top_of_normal [h : Normal F E] : Normal K E :=
     exact ⟨hx.tower_top, hhx.of_dvd (map_ne_zero (map_ne_zero (minpoly.ne_zero hx)))
       ((map_dvd_map' _).mpr (minpoly.dvd_map_of_isScalarTower F K x))⟩
 
+set_option backward.isDefEq.respectTransparency false in
+instance IntermediateField.normal (K : IntermediateField F E) [Normal F E] : Normal K E :=
+  Normal.tower_top_of_normal F K E
+
 theorem AlgHom.normal_bijective [h : Normal F E] (ϕ : E →ₐ[F] K) : Function.Bijective ϕ :=
   h.toIsAlgebraic.bijective_of_isScalarTower' ϕ