Mathlib.RingTheory.Norm.Defs

Module docstring

{"# Norm for (finite) ring extensions

Suppose we have an R-algebra S with a finite basis. For each s : S, the determinant of the linear map given by multiplying by s gives information about the roots of the minimal polynomial of s over R.

Implementation notes

Typically, the norm is defined specifically for finite field extensions. The current definition is as general as possible and the assumption that we have fields or that the extension is finite is added to the lemmas as needed.

We only define the norm for left multiplication (Algebra.leftMulMatrix, i.e. LinearMap.mulLeft). For now, the definitions assume S is commutative, so the choice doesn't matter anyway.

See also Algebra.trace, which is defined similarly as the trace of Algebra.leftMulMatrix.

References

https://en.wikipedia.org/wiki/Field_norm

Algebra.norm definition

: S →* R

Full source

/-- The norm of an element `s` of an `R`-algebra is the determinant of `(*) s`. -/
@[stacks 0BIF "Norm"]
noncomputable def norm : S →* R :=
  LinearMap.det.comp (lmul R S).toRingHom.toMonoidHom

Algebra norm of an element in an $ R $-algebra

Informal description

The norm of an element $ s $ in an $ R $-algebra $ S $ is defined as the determinant of the linear map given by left multiplication by $ s $, i.e., $ \text{norm}_R(s) = \det(\text{lmul}_R(s)) $, where $ \text{lmul}_R(s) $ is the $ R $-linear endomorphism of $ S $ defined by $ x \mapsto s \cdot x $.

Algebra.norm_apply theorem

(x : S) : norm R x = LinearMap.det (lmul R S x)

Full source

theorem norm_apply (x : S) : norm R x = LinearMap.det (lmul R S x) := rfl

Norm as Determinant of Multiplication Map in $R$-Algebra

Informal description

For any element $x$ in a commutative $R$-algebra $S$, the norm $\text{norm}_R(x)$ is equal to the determinant of the $R$-linear endomorphism given by left multiplication by $x$, i.e., $\text{norm}_R(x) = \det(\text{lmul}_R(x))$.

Algebra.norm_eq_one_of_not_exists_basis theorem

(h : ¬∃ s : Finset S, Nonempty (Basis s R S)) (x : S) : norm R x = 1

Full source

theorem norm_eq_one_of_not_exists_basis (h : ¬∃ s : Finset S, Nonempty (Basis s R S)) (x : S) :
    norm R x = 1 := by rw [norm_apply, LinearMap.det]; split_ifs <;> trivial

Norm is One When No Finite Basis Exists

Informal description

For a commutative $R$-algebra $S$, if there does not exist a finite subset $s \subseteq S$ such that $S$ has a basis over $R$ indexed by $s$, then the norm of any element $x \in S$ is equal to $1$, i.e., $\text{norm}_R(x) = 1$.

Algebra.norm_eq_one_of_not_module_finite theorem

(h : ¬Module.Finite R S) (x : S) : norm R x = 1

Full source

theorem norm_eq_one_of_not_module_finite (h : ¬Module.Finite R S) (x : S) : norm R x = 1 := by
  refine norm_eq_one_of_not_exists_basis _ (mt ?_ h) _
  rintro ⟨s, ⟨b⟩⟩
  exact Module.Finite.of_basis b

Norm is One for Non-Finitely Generated Algebra Extensions

Informal description

For a commutative $R$-algebra $S$ that is not finitely generated as an $R$-module, the norm of any element $x \in S$ is equal to $1$, i.e., $\text{norm}_R(x) = 1$.

Algebra.norm_eq_matrix_det theorem

[Fintype ι] [DecidableEq ι] (b : Basis ι R S) (s : S) : norm R s = Matrix.det (Algebra.leftMulMatrix b s)

Full source

theorem norm_eq_matrix_det [Fintype ι] [DecidableEq ι] (b : Basis ι R S) (s : S) :
    norm R s = Matrix.det (Algebra.leftMulMatrix b s) := by
  rw [norm_apply, ← LinearMap.det_toMatrix b, ← toMatrix_lmul_eq]; rfl

Norm as Determinant of Left Multiplication Matrix in Finite Algebra Extension

Informal description

Let $R$ be a commutative ring and $S$ a commutative $R$-algebra with a finite basis $b$ indexed by a finite type $\iota$. For any element $s \in S$, the norm $\text{norm}_R(s)$ is equal to the determinant of the matrix representing the left multiplication map $x \mapsto s \cdot x$ with respect to the basis $b$. That is, \[ \text{norm}_R(s) = \det(\text{leftMulMatrix}_b(s)). \]

Algebra.norm_algebraMap_of_basis theorem

[Fintype ι] (b : Basis ι R S) (x : R) : norm R (algebraMap R S x) = x ^ Fintype.card ι

Full source

/-- If `x` is in the base ring `K`, then the norm is `x ^ [L : K]`. -/
theorem norm_algebraMap_of_basis [Fintype ι] (b : Basis ι R S) (x : R) :
    norm R (algebraMap R S x) = x ^ Fintype.card ι := by
  haveI := Classical.decEq ι
  rw [norm_apply, ← det_toMatrix b, lmul_algebraMap]
  convert @det_diagonal _ _ _ _ _ fun _ : ι => x
  · ext (i j); rw [toMatrix_lsmul]
  · rw [Finset.prod_const, Finset.card_univ]

Norm of Algebra Map Element in Finite Basis Extension: $\text{norm}_R(\text{algebraMap}_R^S(x)) = x^{|\iota|}$

Informal description

Let $R$ be a commutative ring and $S$ a commutative $R$-algebra with a finite basis $b$ indexed by a finite type $\iota$. For any element $x \in R$, the norm of the image of $x$ under the algebra map $\text{algebraMap}_R^S$ is given by $x$ raised to the power of the cardinality of $\iota$, i.e., \[ \text{norm}_R(\text{algebraMap}_R^S(x)) = x^{|\iota|}. \]

Algebra.norm_algebraMap theorem

{L : Type*} [Ring L] [Algebra K L] (x : K) : norm K (algebraMap K L x) = x ^ finrank K L

Full source

/-- If `x` is in the base field `K`, then the norm is `x ^ [L : K]`.

(If `L` is not finite-dimensional over `K`, then `norm = 1 = x ^ 0 = x ^ (finrank L K)`.)
-/
@[simp]
protected theorem norm_algebraMap {L : Type*} [Ring L] [Algebra K L] (x : K) :
    norm K (algebraMap K L x) = x ^ finrank K L := by
  by_cases H : ∃ s : Finset L, Nonempty (Basis s K L)
  · rw [norm_algebraMap_of_basis H.choose_spec.some, finrank_eq_card_basis H.choose_spec.some]
  · rw [norm_eq_one_of_not_exists_basis K H, finrank_eq_zero_of_not_exists_basis, pow_zero]
    rintro ⟨s, ⟨b⟩⟩
    exact H ⟨s, ⟨b⟩⟩

Norm of Scalar in Field Extension: $\text{norm}_K(\text{algebraMap}_K^L(x)) = x^{[L:K]}$

Informal description

Let $K$ be a field and $L$ a commutative $K$-algebra. For any element $x \in K$, the norm of the image of $x$ under the algebra map $K \to L$ is given by $x$ raised to the power of the finite rank of $L$ over $K$, i.e., \[ \text{norm}_K(\text{algebraMap}_K^L(x)) = x^{\text{finrank}_K L}. \] If $L$ is not finite-dimensional over $K$, then $\text{finrank}_K L = 0$ and the norm equals $1 = x^0$.