Documentation

Mathlib.RingTheory.Discriminant

Discriminant of a family of vectors #

Given an A-algebra B and b, an ι-indexed family of elements of B, we define the discriminant of b as the determinant of the matrix whose (i j)-th element is the trace of b i * b j.

Main definition #

Main results #

Implementation details #

Our definition works for any A-algebra B, but note that if B is not free as an A-module, then trace A B = 0 by definition, so discr A b = 0 for any b.

noncomputable def Algebra.discr {ι : Type w} [DecidableEq ι] (A : Type u) {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [Fintype ι] (b : ιB) :
A

Given an A-algebra B and b, an ι-indexed family of elements of B, we define discr A ι b as the determinant of traceMatrix A ι b.

Equations
Instances For
    theorem Algebra.discr_def (A : Type u) {B : Type v} {ι : Type w} [DecidableEq ι] [CommRing A] [CommRing B] [Algebra A B] [Fintype ι] (b : ιB) :
    theorem Algebra.discr_eq_discr_of_algEquiv {A : Type u} {B : Type v} {C : Type z} {ι : Type w} [DecidableEq ι] [CommRing A] [CommRing B] [Algebra A B] [CommRing C] [Algebra A C] [Fintype ι] (b : ιB) (f : B ≃ₐ[A] C) :

    Mapping a family of vectors along an AlgEquiv preserves the discriminant.

    @[simp]
    theorem Algebra.discr_reindex (A : Type u) {B : Type v} {ι : Type w} [DecidableEq ι] [CommRing A] [CommRing B] [Algebra A B] {ι' : Type u_1} [Fintype ι'] [Fintype ι] [DecidableEq ι'] (b : Basis ι A B) (f : ι ι') :
    Algebra.discr A (b f.symm) = Algebra.discr A b
    theorem Algebra.discr_zero_of_not_linearIndependent (A : Type u) {B : Type v} {ι : Type w} [DecidableEq ι] [CommRing A] [CommRing B] [Algebra A B] [Fintype ι] [IsDomain A] {b : ιB} (hli : ¬LinearIndependent A b) :

    If b is not linear independent, then Algebra.discr A b = 0.

    theorem Algebra.discr_of_matrix_vecMul {A : Type u} {B : Type v} {ι : Type w} [DecidableEq ι] [CommRing A] [CommRing B] [Algebra A B] [Fintype ι] (b : ιB) (P : Matrix ι ι A) :

    Relation between Algebra.discr A ι b and Algebra.discr A (b ᵥ* P.map (algebraMap A B)).

    theorem Algebra.discr_of_matrix_mulVec {A : Type u} {B : Type v} {ι : Type w} [DecidableEq ι] [CommRing A] [CommRing B] [Algebra A B] [Fintype ι] (b : ιB) (P : Matrix ι ι A) :

    Relation between Algebra.discr A ι b and Algebra.discr A ((P.map (algebraMap A B)) *ᵥ b).

    theorem Algebra.discr_not_zero_of_basis {ι : Type w} [DecidableEq ι] [Fintype ι] (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L] [Module.Finite K L] [IsSeparable K L] (b : Basis ι K L) :

    If b is a basis of a finite separable field extension L/K, then Algebra.discr K b ≠ 0.

    theorem Algebra.discr_isUnit_of_basis {ι : Type w} [DecidableEq ι] [Fintype ι] (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L] [Module.Finite K L] [IsSeparable K L] (b : Basis ι K L) :

    If b is a basis of a finite separable field extension L/K, then Algebra.discr K b is a unit.

    theorem Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two {ι : Type w} [DecidableEq ι] [Fintype ι] (K : Type u) {L : Type v} (E : Type z) [Field K] [Field L] [Field E] [Algebra K L] [Algebra K E] [Module.Finite K L] [IsAlgClosed E] (b : ιL) [IsSeparable K L] (e : ι (L →ₐ[K] E)) :

    If L/K is a field extension and b : ι → L, then discr K b is the square of the determinant of the matrix whose (i, j) coefficient is σⱼ (b i), where σⱼ : L →ₐ[K] E is the embedding in an algebraically closed field E corresponding to j : ι via a bijection e : ι ≃ (L →ₐ[K] E).

    theorem Algebra.discr_powerBasis_eq_prod (K : Type u) {L : Type v} (E : Type z) [Field K] [Field L] [Field E] [Algebra K L] [Algebra K E] [Module.Finite K L] [IsAlgClosed E] (pb : PowerBasis K L) (e : Fin pb.dim (L →ₐ[K] E)) [IsSeparable K L] :
    (algebraMap K E) (Algebra.discr K pb.basis) = Finset.prod Finset.univ fun (i : Fin pb.dim) => Finset.prod (Finset.Ioi i) fun (j : Fin pb.dim) => ((e j) pb.gen - (e i) pb.gen) ^ 2

    The discriminant of a power basis.

    theorem Algebra.discr_powerBasis_eq_prod' (K : Type u) {L : Type v} (E : Type z) [Field K] [Field L] [Field E] [Algebra K L] [Algebra K E] [Module.Finite K L] [IsAlgClosed E] (pb : PowerBasis K L) [IsSeparable K L] (e : Fin pb.dim (L →ₐ[K] E)) :
    (algebraMap K E) (Algebra.discr K pb.basis) = Finset.prod Finset.univ fun (i : Fin pb.dim) => Finset.prod (Finset.Ioi i) fun (j : Fin pb.dim) => -(((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen))

    A variation of Algebra.discr_powerBasis_eq_prod.

    theorem Algebra.discr_powerBasis_eq_prod'' (K : Type u) {L : Type v} (E : Type z) [Field K] [Field L] [Field E] [Algebra K L] [Algebra K E] [Module.Finite K L] [IsAlgClosed E] (pb : PowerBasis K L) [IsSeparable K L] (e : Fin pb.dim (L →ₐ[K] E)) :
    (algebraMap K E) (Algebra.discr K pb.basis) = (-1) ^ (FiniteDimensional.finrank K L * (FiniteDimensional.finrank K L - 1) / 2) * Finset.prod Finset.univ fun (i : Fin pb.dim) => Finset.prod (Finset.Ioi i) fun (j : Fin pb.dim) => ((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen)

    A variation of Algebra.discr_powerBasis_eq_prod.

    theorem Algebra.discr_powerBasis_eq_norm (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L] [Module.Finite K L] (pb : PowerBasis K L) [IsSeparable K L] :
    Algebra.discr K pb.basis = (-1) ^ (FiniteDimensional.finrank K L * (FiniteDimensional.finrank K L - 1) / 2) * (Algebra.norm K) ((Polynomial.aeval pb.gen) (Polynomial.derivative (minpoly K pb.gen)))

    Formula for the discriminant of a power basis using the norm of the field extension.

    theorem Algebra.discr_isIntegral {ι : Type w} [DecidableEq ι] [Fintype ι] (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L] [Module.Finite K L] {R : Type z} [CommRing R] [Algebra R K] [Algebra R L] [IsScalarTower R K L] {b : ιL} (h : ∀ (i : ι), IsIntegral R (b i)) :

    If K and L are fields and IsScalarTower R K L, and b : ι → L satisfies ∀ i, IsIntegral R (b i), then IsIntegral R (discr K b).

    theorem Algebra.discr_mul_isIntegral_mem_adjoin (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L] [Module.Finite K L] {R : Type z} [CommRing R] [Algebra R K] [Algebra R L] [IsScalarTower R K L] [IsSeparable K L] [IsIntegrallyClosed R] [IsFractionRing R K] {B : PowerBasis K L} (hint : IsIntegral R B.gen) {z : L} (hz : IsIntegral R z) :
    Algebra.discr K B.basis z Algebra.adjoin R {B.gen}

    Let K be the fraction field of an integrally closed domain R and let L be a finite separable extension of K. Let B : PowerBasis K L be such that IsIntegral R B.gen. Then for all, z : L that are integral over R, we have (discr K B.basis) • z ∈ adjoin R ({B.gen} : Set L).

    theorem Algebra.discr_eq_discr (A : Type u) {ι : Type w} [DecidableEq ι] [CommRing A] [Fintype ι] (b : Basis ι A) (b' : Basis ι A) :

    Two (finite) ℤ-bases have the same discriminant.