mathlib3 documentation

ring_theory.norm

Norm for (finite) ring extensions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.left_mul_matrix, i.e. linear_map.mul_left). 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.left_mul_matrix.

References #

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

noncomputable def algebra.norm (R : Type u_1) {S : Type u_2} [comm_ring 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 = linear_map.det.comp (algebra.lmul R S).to_ring_hom.to_monoid_hom

theorem algebra.norm_apply (R : Type u_1) {S : Type u_2} [comm_ring R] [ring S] [algebra R S] (x : S) :

⇑(algebra.norm R) x = ⇑linear_map.det (⇑(algebra.lmul R S) x)

theorem algebra.norm_eq_one_of_not_exists_basis (R : Type u_1) {S : Type u_2} [comm_ring R] [ring S] [algebra R S] (h : ¬∃ (s : finset S), nonempty (basis ↥s R S)) (x : S) :

⇑(algebra.norm R) x = 1

theorem algebra.norm_eq_one_of_not_module_finite {R : Type u_1} {S : Type u_2} [comm_ring 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} [comm_ring R] [ring S] [algebra R S] {ι : Type w} [fintype ι] [decidable_eq ι] (b : basis ι R S) (s : S) :

⇑(algebra.norm R) s = (⇑(algebra.left_mul_matrix b) s).det

theorem algebra.norm_algebra_map_of_basis {R : Type u_1} {S : Type u_2} [comm_ring R] [ring S] [algebra R S] {ι : Type w} [fintype ι] (b : basis ι R S) (x : R) :

⇑(algebra.norm R) (⇑(algebra_map R S) x) = x ^ fintype.card ι

If x is in the base ring K, then the norm is x ^ [L : K].

@[protected, simp]

theorem algebra.norm_algebra_map {K : Type u_4} [field K] {L : Type u_1} [ring L] [algebra K L] (x : K) :

⇑(algebra.norm K) (⇑(algebra_map K L) x) = x ^ finite_dimensional.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.power_basis.norm_gen_eq_coeff_zero_minpoly {R : Type u_1} {S : Type u_2} [comm_ring R] [ring S] [algebra R S] (pb : power_basis R S) :

⇑(algebra.norm R) pb.gen = (-1) ^ pb.dim * (minpoly R pb.gen).coeff 0

Given pb : power_basis K S, then the norm of pb.gen is (-1) ^ pb.dim * coeff (minpoly K pb.gen) 0.

theorem algebra.power_basis.norm_gen_eq_prod_roots {R : Type u_1} {S : Type u_2} [comm_ring R] [ring S] [algebra R S] {F : Type u_6} [field F] [algebra R F] (pb : power_basis R S) (hf : polynomial.splits (algebra_map R F) (minpoly R pb.gen)) :

⇑(algebra_map R F) (⇑(algebra.norm R) pb.gen) = (polynomial.map (algebra_map R F) (minpoly R pb.gen)).roots.prod

Given pb : power_basis R S, then the norm of pb.gen is ((minpoly R pb.gen).map (algebra_map R F)).roots.prod.

@[simp]

theorem algebra.norm_zero {R : Type u_1} {S : Type u_2} [comm_ring 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} [comm_ring R] [ring S] [algebra R S] [is_domain R] [is_domain 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} [comm_ring R] [ring S] [algebra R S] [is_domain R] [is_domain 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} [comm_ring R] [ring S] [algebra R S] [is_domain R] [is_domain S] [module.free R S] [module.finite R S] {x : S} :

⇑linear_map.det (⇑(linear_map.mul R S) x) = 0 ↔ x = 0

This is algebra.norm_eq_zero_iff composed with algebra.norm_apply.

theorem algebra.norm_eq_zero_iff_of_basis {R : Type u_1} {S : Type u_2} [comm_ring R] [ring S] [algebra R S] {ι : Type w} [finite ι] [is_domain R] [is_domain S] (b : basis ι R S) {x : S} :

⇑(algebra.norm R) x = 0 ↔ x = 0

theorem algebra.norm_ne_zero_iff_of_basis {R : Type u_1} {S : Type u_2} [comm_ring R] [ring S] [algebra R S] {ι : Type w} [finite ι] [is_domain R] [is_domain S] (b : basis ι R S) {x : S} :

⇑(algebra.norm R) x ≠ 0 ↔ x ≠ 0

theorem algebra.norm_eq_norm_adjoin (K : Type u_4) {L : Type u_5} [field K] [field L] [algebra K L] [finite_dimensional K L] [is_separable K L] (x : L) :

⇑(algebra.norm K) x = ⇑(algebra.norm K) (intermediate_field.adjoin_simple.gen K x) ^ finite_dimensional.finrank ↥K⟮x⟯ L

theorem intermediate_field.adjoin_simple.norm_gen_eq_one {K : Type u_4} {L : Type u_5} [field K] [field L] [algebra K L] {x : L} (hx : ¬is_integral K x) :

⇑(algebra.norm K) (intermediate_field.adjoin_simple.gen K x) = 1

theorem intermediate_field.adjoin_simple.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 (algebra_map K F) (minpoly K x)) :

⇑(algebra_map K F) (⇑(algebra.norm K) (intermediate_field.adjoin_simple.gen K x)) = (polynomial.map (algebra_map K F) (minpoly K x)).roots.prod

theorem algebra.norm_eq_prod_embeddings_gen {R : Type u_1} {S : Type u_2} [comm_ring R] [ring S] [algebra R S] (F : Type u_6) [field F] [algebra R F] (pb : power_basis R S) (hE : polynomial.splits (algebra_map R F) (minpoly R pb.gen)) (hfx : (minpoly R pb.gen).separable) :

⇑(algebra_map R F) (⇑(algebra.norm R) pb.gen) = finset.univ.prod (λ (σ : 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] [is_separable K L] [finite_dimensional K L] {x : L} (hF : polynomial.splits (algebra_map K F) (minpoly K x)) :

⇑(algebra_map K F) (⇑(algebra.norm K) x) = (polynomial.map (algebra_map K F) (minpoly K x)).roots.prod ^ finite_dimensional.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] [is_scalar_tower K L F] [is_alg_closed E] [is_separable K F] [finite_dimensional K F] (pb : power_basis K L) :

finset.univ.prod (λ (σ : F →ₐ[K] E), ⇑σ (⇑(algebra_map L F) pb.gen)) = finset.univ.prod (λ (σ : L →ₐ[K] E), ⇑σ pb.gen) ^ finite_dimensional.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] [finite_dimensional K L] [is_separable K L] [is_alg_closed E] (x : L) :

⇑(algebra_map K E) (⇑(algebra.norm K) x) = finset.univ.prod (λ (σ : 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] [finite_dimensional K L] [is_galois K L] (x : L) :

⇑(algebra_map K L) (⇑(algebra.norm K) x) = finset.univ.prod (λ (σ : L ≃ₐ[K] L), ⇑σ x)

theorem algebra.is_integral_norm {R : Type u_1} [comm_ring R] (K : Type u_4) {L : Type u_5} [field K] [field L] [algebra K L] [algebra R L] [algebra R K] [is_scalar_tower R K L] [is_separable K L] [finite_dimensional K L] {x : L} (hx : is_integral R x) :

is_integral R (⇑(algebra.norm K) 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] [is_scalar_tower K L F] [is_separable K F] (x : F) :

⇑(algebra.norm K) (⇑(algebra.norm L) x) = ⇑(algebra.norm K) x