algNormOfAlgEquiv and invariantExtension

Let K be a nonarchimedean normed field and L/K be a finite algebraic extension. In the comments, ‖ ⬝ ‖ denotes any power-multiplicative K-algebra norm on L extending the norm on K.

Main Definitions

• IsUltrametricDist.algNormOfAlgEquiv : given σ : L ≃ₐ[K] L, the function L → ℝ sending x : L to ‖ σ x ‖ is a K-algebra norm on L.
• IsUltrametricDist.invariantExtension : the function L → ℝ sending x : L to the maximum of ‖ σ x ‖ over all σ : L ≃ₐ[K] L is a K-algebra norm on L.

Main Results

• IsUltrametricDist.isPowMul_algNormOfAlgEquiv : algNormOfAlgEquiv is power-multiplicative.
• IsUltrametricDist.isNonarchimedean_algNormOfAlgEquiv : algNormOfAlgEquiv is nonarchimedean.
• IsUltrametricDist.algNormOfAlgEquiv_extends : algNormOfAlgEquiv extends the norm on K.
• IsUltrametricDist.isPowMul_invariantExtension : invariantExtension is power-multiplicative.
• IsUltrametricDist.isNonarchimedean_invariantExtension : invariantExtension is nonarchimedean.
• IsUltrametricDist.invariantExtension_extends : invariantExtension extends the norm on K.

References

• [S. Bosch, U. Güntzer, R. Remmert, Non-Archimedean Analysis][bosch-guntzer-remmert]

Tags

algNormOfAlgEquiv, invariantExtension, norm, nonarchimedean

def IsUltrametricDist.algNormOfAlgEquiv {K : Type u_1} [NormedField K] {L : Type u_2} [Field L] [Algebra K L] [h_fin : FiniteDimensional K L] [hu : IsUltrametricDist K] (σ : L ≃ₐ[K] L) : AlgebraNorm K L

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.

Equations

• IsUltrametricDist.algNormOfAlgEquiv σ = { toFun := fun (x : L) => (Classical.choose ⋯) (σ x), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, mul_le' := ⋯, eq_zero_of_map_eq_zero' := ⋯, smul' := ⋯ }

theorem IsUltrametricDist.algNormOfAlgEquiv_apply {K : Type u_1} [NormedField K] {L : Type u_2} [Field L] [Algebra K L] [h_fin : FiniteDimensional K L] [hu : IsUltrametricDist K] (σ : L ≃ₐ[K] L) (x : L) : (algNormOfAlgEquiv σ) x = (Classical.choose ⋯) (σ x)

theorem IsUltrametricDist.isPowMul_algNormOfAlgEquiv {K : Type u_1} [NormedField K] {L : Type u_2} [Field L] [Algebra K L] [h_fin : FiniteDimensional K L] [hu : IsUltrametricDist K] (σ : L ≃ₐ[K] L) : IsPowMul ⇑(algNormOfAlgEquiv σ)

The algebra norm algNormOfAlgEquiv is power-multiplicative.

theorem IsUltrametricDist.isNonarchimedean_algNormOfAlgEquiv {K : Type u_1} [NormedField K] {L : Type u_2} [Field L] [Algebra K L] [h_fin : FiniteDimensional K L] [hu : IsUltrametricDist K] (σ : L ≃ₐ[K] L) : IsNonarchimedean ⇑(algNormOfAlgEquiv σ)

The algebra norm algNormOfAlgEquiv is nonarchimedean.

theorem IsUltrametricDist.algNormOfAlgEquiv_extends {K : Type u_1} [NormedField K] {L : Type u_2} [Field L] [Algebra K L] [h_fin : FiniteDimensional K L] [hu : IsUltrametricDist K] (σ : L ≃ₐ[K] L) (x : K) : (algNormOfAlgEquiv σ) ((algebraMap K L) x) = ‖x‖

The algebra norm algNormOfAlgEquiv extends the norm on K.

def IsUltrametricDist.invariantExtension (K : Type u_1) [NormedField K] (L : Type u_2) [Field L] [Algebra K L] [h_fin : FiniteDimensional K L] [hu : IsUltrametricDist K] : AlgebraNorm K L

The function L → ℝ sending x : L to the maximum of algNormOfAlgEquiv hna σ over all σ : L ≃ₐ[K] L is an algebra norm on L.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem IsUltrametricDist.invariantExtension_apply (K : Type u_1) [NormedField K] (L : Type u_2) [Field L] [Algebra K L] [h_fin : FiniteDimensional K L] [hu : IsUltrametricDist K] (x : L) : (invariantExtension K L) x = ⨆ (σ : L ≃ₐ[K] L), (algNormOfAlgEquiv σ) x

theorem IsUltrametricDist.isPowMul_invariantExtension (K : Type u_1) [NormedField K] (L : Type u_2) [Field L] [Algebra K L] [h_fin : FiniteDimensional K L] [hu : IsUltrametricDist K] : IsPowMul ⇑(invariantExtension K L)

The algebra norm invariantExtension is power-multiplicative.

theorem IsUltrametricDist.isNonarchimedean_invariantExtension (K : Type u_1) [NormedField K] (L : Type u_2) [Field L] [Algebra K L] [h_fin : FiniteDimensional K L] [hu : IsUltrametricDist K] : IsNonarchimedean ⇑(invariantExtension K L)

The algebra norm invariantExtension is nonarchimedean.

theorem IsUltrametricDist.invariantExtension_extends (K : Type u_1) [NormedField K] (L : Type u_2) [Field L] [Algebra K L] [h_fin : FiniteDimensional K L] [hu : IsUltrametricDist K] (x : K) : (invariantExtension K L) ((algebraMap K L) x) = ‖x‖

The algebra norm invariantExtension extends the norm on K.