invariantExtension — Mathlib

English

Define a norm on L by taking the supremum over all K-algebra automorphisms of L of algNormOfAlgEquiv; this is an algebra norm on L.

Русский

Определим норму на L как супремум по всем алгебраическим автоалгебрам над K: это будет алгебрическая норма на L.

LaTeX

$$invariantExtension : AlgebraNorm K L$$

Lean4

/-- The function `L → ℝ` sending `x : L` to the maximum of `algNormOfAlgEquiv hna σ` over
  all `σ : L ≃ₐ[K] L` is an algebra norm on `L`. -/
def invariantExtension : AlgebraNorm K L
    where
  toFun x := iSup fun σ : L ≃ₐ[K] L ↦ algNormOfAlgEquiv σ x
  map_zero' := by simp only [map_zero, ciSup_const]
  add_le' x
    y :=
    ciSup_le fun σ ↦
      le_trans (map_add_le_add (algNormOfAlgEquiv σ) x y)
        (add_le_add (le_ciSup_of_le (Set.finite_range _).bddAbove σ (le_refl _))
          (le_ciSup_of_le (Set.finite_range _).bddAbove σ (le_refl _)))
  neg' x := by simp only [map_neg_eq_map]
  mul_le' x
    y :=
    ciSup_le fun σ ↦
      le_trans (map_mul_le_mul (algNormOfAlgEquiv σ) x y)
        (mul_le_mul (le_ciSup_of_le (Set.finite_range _).bddAbove σ (le_refl _))
          (le_ciSup_of_le (Set.finite_range _).bddAbove σ (le_refl _)) (apply_nonneg _ _)
          (le_ciSup_of_le (Set.finite_range _).bddAbove σ (apply_nonneg _ _)))
  eq_zero_of_map_eq_zero'
    x := by
    contrapose!
    exact fun hx ↦
      ne_of_gt
        (lt_of_lt_of_le (map_pos_of_ne_zero _ hx)
          (le_ciSup (Set.range fun σ : L ≃ₐ[K] L ↦ algNormOfAlgEquiv σ x).toFinite.bddAbove AlgEquiv.refl))
  smul' r x := by simp only [AlgebraNormClass.map_smul_eq_mul, Real.mul_iSup_of_nonneg (norm_nonneg _)]

Похожие утверждения