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 _)]