Spectral norm on algebraic extensions

TheoremSpectral-norm unit ball is the integral closure#✓fully proved

Let \(A\) be an integral domain, \(K\) a complete nontrivially normed field whose norm is ultrametric, and \(L\) a field extension of \(K\) of finite degree, where \(K\) and \(L\) are \(A\)-algebras and the algebra maps \(A \to K \to L\) compose to \(A \to L\). Suppose that for every \(y \in K\), \(\|y\| \le 1\) if and only if \(y\) is integral over \(A\). Then for every \(x \in L\), the spectral norm of \(x\) over \(K\) is at most \(1\) if and only if \(x\) is integral over \(A\).

public theorem spectralNorm_le_one_iff_isIntegral
    {A K L : Type*} [CommRing A] [IsDomain A]
    [NontriviallyNormedField K] [Field L]
    [Algebra A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L]
    [IsUltrametricDist K] [CompleteSpace K] [FiniteDimensional K L]
    (hA : ∀ y : K, ‖y‖ ≤ 1 ↔ IsIntegral A y) (x : L) :
    spectralNorm K L x ≤ 1 ↔ IsIntegral A x

Used by 1

Used bySpectral-norm unit ball as the image of an integral closure

TheoremSpectral-norm unit ball as the image of an integral closure#✓fully proved

Let \(A\) be an integral domain, \(K\) a complete nontrivially normed field whose norm is ultrametric, and \(L\) a field extension of \(K\) of finite degree, where \(K\) and \(L\) are \(A\)-algebras and the algebra maps \(A \to K \to L\) compose to \(A \to L\). Let \(B\) be an integral domain that is an \(A\)-algebra with an algebra map \(B \to L\) such that \(A \to B \to L\) composes to \(A \to L\), and suppose \(B\) is an integral closure of \(A\) in \(L\): the map \(B \to L\) is injective and its image is the set of elements of \(L\) integral over \(A\). Suppose that for every \(y \in K\), \(\|y\| \le 1\) if and only if \(y\) is integral over \(A\). Then for every \(x \in L\), the spectral norm of \(x\) over \(K\) is at most \(1\) if and only if \(x\) is the image of some element of \(B\).

public theorem spectralNorm_le_one_iff_exists_integralClosure
    {A K L B : Type*} [CommRing A] [IsDomain A]
    [NontriviallyNormedField K] [Field L]
    [Algebra A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L]
    [IsUltrametricDist K] [CompleteSpace K] [FiniteDimensional K L]
    [CommRing B] [IsDomain B] [Algebra A B] [Algebra B L]
    [IsScalarTower A B L] [IsIntegralClosure B A L]
    (hA : ∀ y : K, ‖y‖ ≤ 1 ↔ IsIntegral A y) (x : L) :
    spectralNorm K L x ≤ 1 ↔ ∃ b : B, algebraMap B L b = x

Uses 1

Proof usesSpectral-norm unit ball is the integral closure

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.