English
If y is algebraic and k ∈ K, then spectralNorm(k·y) = ||k|| · spectralNorm(y).
Русский
Если y алгебраический и k ∈ K, то spectralNorm(k·y) = ||k|| · spectralNorm(y).
LaTeX
$$$\operatorname{spectralNorm}_{K,L}(k \cdot y) = \|k\| \cdot \operatorname{spectralNorm}_{K,L}(y)$, для всех $k\in K$, $y\in L$ с предположением, что \; y\ является алгебраическим$$
Lean4
/-- The spectral norm is compatible with the action of `K`. -/
theorem spectralNorm_smul (k : K) {y : L} (hy : IsAlgebraic K y) :
spectralNorm K L (k • y) = ‖k‖₊ * spectralNorm K L y :=
by
set E := K⟮y⟯
haveI h_finiteDimensional_E : FiniteDimensional K E := IntermediateField.adjoin.finiteDimensional hy.isIntegral
set g := IntermediateField.AdjoinSimple.gen K y
have hgy : k • y = (algebraMap (↥K⟮y⟯) L) (k • g) := rfl
have h :
algebraMap K⟮y⟯ (normalClosure K K⟮y⟯ (AlgebraicClosure K⟮y⟯)) (k • g) =
k • algebraMap K⟮y⟯ (normalClosure K K⟮y⟯ (AlgebraicClosure K⟮y⟯)) g :=
by rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, smul_assoc]
rw [← spectralNorm.eq_of_normalClosure g (IntermediateField.AdjoinSimple.algebraMap_gen K y), hgy, ←
spectralNorm.eq_of_normalClosure (k • g) rfl, h]
rw [← spectralAlgNorm_of_finiteDimensional_normal_def]
apply map_smul_eq_mul
