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
noncomputable def
Algebra.norm
(R : Type u_1)
{S : Type u_2}
[CommRing R]
[Ring S]
[Algebra R S]
:
S →* R
The norm of an element s of an R-algebra is the determinant of (*) s.
Equations
- Algebra.norm R = MonoidHom.comp LinearMap.det ↑(Algebra.lmul R S).toRingHom
Instances For
theorem
Algebra.norm_apply
(R : Type u_1)
{S : Type u_2}
[CommRing R]
[Ring S]
[Algebra R S]
(x : S)
:
(Algebra.norm R) x = LinearMap.det ((Algebra.lmul R S) x)
theorem
Algebra.norm_eq_one_of_not_module_finite
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[Ring S]
[Algebra R S]
(h : ¬Module.Finite R S)
(x : S)
:
(Algebra.norm R) x = 1
theorem
Algebra.norm_eq_matrix_det
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[Ring S]
[Algebra R S]
{ι : Type w}
[Fintype ι]
[DecidableEq ι]
(b : Basis ι R S)
(s : S)
:
(Algebra.norm R) s = Matrix.det ((Algebra.leftMulMatrix b) s)
theorem
Algebra.norm_algebraMap_of_basis
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[Ring S]
[Algebra R S]
{ι : Type w}
[Fintype ι]
(b : Basis ι R S)
(x : R)
:
(Algebra.norm R) ((algebraMap R S) x) = x ^ Fintype.card ι
If x is in the base ring K, then the norm is x ^ [L : K].
@[simp]
theorem
Algebra.norm_algebraMap
{K : Type u_4}
[Field K]
{L : Type u_7}
[Ring L]
[Algebra K L]
(x : K)
:
(Algebra.norm K) ((algebraMap K L) x) = x ^ FiniteDimensional.finrank K L
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).)
theorem
Algebra.PowerBasis.norm_gen_eq_coeff_zero_minpoly
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[Ring S]
[Algebra R S]
(pb : PowerBasis R S)
:
(Algebra.norm R) pb.gen = (-1) ^ pb.dim * Polynomial.coeff (minpoly R pb.gen) 0
Given pb : PowerBasis K S, then the norm of pb.gen is
(-1) ^ pb.dim * coeff (minpoly K pb.gen) 0.
theorem
Algebra.PowerBasis.norm_gen_eq_prod_roots
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[Ring S]
[Algebra R S]
{F : Type u_6}
[Field F]
[Algebra R F]
(pb : PowerBasis R S)
(hf : Polynomial.Splits (algebraMap R F) (minpoly R pb.gen))
:
(algebraMap R F) ((Algebra.norm R) pb.gen) = Multiset.prod (Polynomial.aroots (minpoly R pb.gen) F)
Given pb : PowerBasis R S, then the norm of pb.gen is
((minpoly R pb.gen).aroots F).prod.
@[simp]
theorem
Algebra.norm_zero
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[Ring S]
[Algebra R S]
[Nontrivial S]
[Module.Free R S]
[Module.Finite R S]
:
(Algebra.norm R) 0 = 0
@[simp]
theorem
Algebra.norm_eq_zero_iff
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[Ring S]
[Algebra R S]
[IsDomain R]
[IsDomain S]
[Module.Free R S]
[Module.Finite R S]
{x : S}
:
(Algebra.norm R) x = 0 ↔ x = 0
theorem
Algebra.norm_ne_zero_iff
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[Ring S]
[Algebra R S]
[IsDomain R]
[IsDomain S]
[Module.Free R S]
[Module.Finite R S]
{x : S}
:
(Algebra.norm R) x ≠ 0 ↔ x ≠ 0
@[simp]
theorem
Algebra.norm_eq_zero_iff'
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[Ring S]
[Algebra R S]
[IsDomain R]
[IsDomain S]
[Module.Free R S]
[Module.Finite R S]
{x : S}
:
LinearMap.det ((LinearMap.mul R S) x) = 0 ↔ x = 0
This is Algebra.norm_eq_zero_iff composed with Algebra.norm_apply.
theorem
Algebra.norm_eq_norm_adjoin
(K : Type u_4)
{L : Type u_5}
[Field K]
[Field L]
[Algebra K L]
[FiniteDimensional K L]
[IsSeparable K L]
(x : L)
:
(Algebra.norm K) x = (Algebra.norm K) (IntermediateField.AdjoinSimple.gen K x) ^ FiniteDimensional.finrank (↥K⟮x⟯) L
theorem
IntermediateField.AdjoinSimple.norm_gen_eq_one
{K : Type u_4}
{L : Type u_5}
[Field K]
[Field L]
[Algebra K L]
{x : L}
(hx : ¬IsIntegral K x)
:
(Algebra.norm K) (IntermediateField.AdjoinSimple.gen K x) = 1
theorem
IntermediateField.AdjoinSimple.norm_gen_eq_prod_roots
{K : Type u_4}
{L : Type u_5}
{F : Type u_6}
[Field K]
[Field L]
[Field F]
[Algebra K L]
[Algebra K F]
(x : L)
(hf : Polynomial.Splits (algebraMap K F) (minpoly K x))
:
(algebraMap K F) ((Algebra.norm K) (IntermediateField.AdjoinSimple.gen K x)) = Multiset.prod (Polynomial.aroots (minpoly K x) F)
theorem
Algebra.norm_eq_prod_embeddings_gen
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[Ring S]
[Algebra R S]
(F : Type u_6)
[Field F]
[Algebra R F]
(pb : PowerBasis R S)
(hE : Polynomial.Splits (algebraMap R F) (minpoly R pb.gen))
(hfx : Polynomial.Separable (minpoly R pb.gen))
:
(algebraMap R F) ((Algebra.norm R) pb.gen) = Finset.prod Finset.univ fun (σ : S →ₐ[R] F) => σ pb.gen
theorem
Algebra.norm_eq_prod_roots
{K : Type u_4}
{L : Type u_5}
(F : Type u_6)
[Field K]
[Field L]
[Field F]
[Algebra K L]
[Algebra K F]
[IsSeparable K L]
[FiniteDimensional K L]
{x : L}
(hF : Polynomial.Splits (algebraMap K F) (minpoly K x))
:
(algebraMap K F) ((Algebra.norm K) x) = Multiset.prod (Polynomial.aroots (minpoly K x) F) ^ FiniteDimensional.finrank (↥K⟮x⟯) L
theorem
Algebra.prod_embeddings_eq_finrank_pow
{K : Type u_4}
{L : Type u_5}
(F : Type u_6)
[Field K]
[Field L]
[Field F]
[Algebra K L]
[Algebra K F]
(E : Type u_7)
[Field E]
[Algebra K E]
[Algebra L F]
[IsScalarTower K L F]
[IsAlgClosed E]
[IsSeparable K F]
[FiniteDimensional K F]
(pb : PowerBasis K L)
:
(Finset.prod Finset.univ fun (σ : F →ₐ[K] E) => σ ((algebraMap L F) pb.gen)) = (Finset.prod Finset.univ fun (σ : L →ₐ[K] E) => σ pb.gen) ^ FiniteDimensional.finrank L F
theorem
Algebra.norm_eq_prod_embeddings
(K : Type u_4)
{L : Type u_5}
[Field K]
[Field L]
[Algebra K L]
(E : Type u_7)
[Field E]
[Algebra K E]
[FiniteDimensional K L]
[IsSeparable K L]
[IsAlgClosed E]
(x : L)
:
(algebraMap K E) ((Algebra.norm K) x) = Finset.prod Finset.univ fun (σ : L →ₐ[K] E) => σ x
For L/K a finite separable extension of fields and E an algebraically closed extension
of K, the norm (down to K) of an element x of L is equal to the product of the images
of x over all the K-embeddings σ of L into E.
theorem
Algebra.norm_eq_prod_automorphisms
(K : Type u_4)
{L : Type u_5}
[Field K]
[Field L]
[Algebra K L]
[FiniteDimensional K L]
[IsGalois K L]
(x : L)
:
(algebraMap K L) ((Algebra.norm K) x) = Finset.prod Finset.univ fun (σ : L ≃ₐ[K] L) => σ x
theorem
Algebra.isIntegral_norm
{R : Type u_1}
[CommRing R]
(K : Type u_4)
{L : Type u_5}
[Field K]
[Field L]
[Algebra K L]
[Algebra R L]
[Algebra R K]
[IsScalarTower R K L]
[IsSeparable K L]
[FiniteDimensional K L]
{x : L}
(hx : IsIntegral R x)
:
IsIntegral R ((Algebra.norm K) x)
theorem
Algebra.norm_eq_of_algEquiv
{R : Type u_1}
{S : Type u_2}
{T : Type u_3}
[CommRing R]
[Ring S]
[Algebra R S]
[Ring T]
[Algebra R T]
(e : S ≃ₐ[R] T)
(x : S)
:
(Algebra.norm R) (e x) = (Algebra.norm R) x
theorem
Algebra.norm_eq_of_ringEquiv
{A : Type u_8}
{B : Type u_9}
{C : Type u_10}
[CommRing A]
[CommRing B]
[Ring C]
[Algebra A C]
[Algebra B C]
(e : A ≃+* B)
(he : RingHom.comp (algebraMap B C) ↑e = algebraMap A C)
(x : C)
:
e ((Algebra.norm A) x) = (Algebra.norm B) x
theorem
Algebra.norm_eq_of_equiv_equiv
{A₁ : Type u_8}
{B₁ : Type u_9}
{A₂ : Type u_10}
{B₂ : Type u_11}
[CommRing A₁]
[Ring B₁]
[CommRing A₂]
[Ring B₂]
[Algebra A₁ B₁]
[Algebra A₂ B₂]
(e₁ : A₁ ≃+* A₂)
(e₂ : B₁ ≃+* B₂)
(he : RingHom.comp (algebraMap A₂ B₂) ↑e₁ = RingHom.comp (↑e₂) (algebraMap A₁ B₁))
(x : B₁)
:
(Algebra.norm A₁) x = (RingEquiv.symm e₁) ((Algebra.norm A₂) (e₂ x))
theorem
Algebra.norm_norm
(K : Type u_4)
(L : Type u_5)
{F : Type u_6}
[Field K]
[Field L]
[Field F]
[Algebra K L]
[Algebra K F]
[Algebra L F]
[IsScalarTower K L F]
[IsSeparable K F]
(x : F)
:
(Algebra.norm K) ((Algebra.norm L) x) = (Algebra.norm K) x