English
For any algebra automorphism σ of L over K, algNormOfAlgEquiv σ applied at x equals the chosen nonarchimedean powMul seminorm evaluated at σ x.
Русский
Для любого автоморфизма σ пространства L над K значение algNormOfAlgEquiv σ на x равно выбранной нерегулярной powMul норме, применённой к σ x.
LaTeX
$$$\mathrm{algNormOfAlgEquiv}(σ)(x) = f(σ(x))$ where f is the chosen powMul seminorm on L extending the norm on K.$$
Lean4
/-- Given a normed field `K`, a finite algebraic extension `L/K` and `σ : L ≃ₐ[K] L`, the function
`L → ℝ` sending `x : L` to `‖ σ x ‖`, where `‖ ⬝ ‖` is any power-multiplicative algebra norm on `L`
extending the norm on `K`, is an algebra norm on `K`. -/
def algNormOfAlgEquiv (σ : L ≃ₐ[K] L) : AlgebraNorm K L
where
toFun
x :=
Classical.choose (exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional h_fin hu.isNonarchimedean_norm) (σ x)
map_zero' := by simp
add_le' x y := by simp [map_add σ, map_add_le_add]
neg' x := by simp [map_neg σ, map_neg_eq_map]
mul_le' x y := by simp [map_mul σ, map_mul_le_mul]
smul' x y := by simp [map_smul σ, map_smul_eq_mul]
eq_zero_of_map_eq_zero' x hx := EmbeddingLike.map_eq_zero_iff.mp (eq_zero_of_map_eq_zero _ hx)
