Algebra.discr_isIntegral
theorem Algebra.discr_isIntegral :
∀ {ι : Type w} [inst : DecidableEq ι] [inst_1 : Fintype ι] (K : Type u) {L : Type v} [inst_2 : Field K]
[inst_3 : Field L] [inst_4 : Algebra K L] [inst_5 : Module.Finite K L] {R : Type z} [inst_6 : CommRing R]
[inst_7 : Algebra R K] [inst_8 : Algebra R L] [inst_9 : IsScalarTower R K L] {b : ι → L},
(∀ (i : ι), IsIntegral R (b i)) → IsIntegral R (Algebra.discr K b)
This theorem states that if `K` and `L` are fields and `R` is a commutative ring such that there exists a scalar tower `R`, `K`, `L`, and `b` is a function from an index set `ι` to `L` such that each `b i` is integral over `R`, then the discriminant of `b` with respect to `K` is also integral over `R`. Here, a scalar tower `R`, `K`, `L` means that `K` is an `R`-algebra, `L` is a `K`-algebra, and the multiplication in `L` is compatible with the `R`- and `K`-actions. An element is said to be integral over a ring if it is a root of some monic polynomial with coefficients in the ring. The discriminant of `b` is the determinant of the trace matrix of `b` with respect to `K`. The trace matrix is a square matrix whose entries are the traces of the products of the elements in `b`.
More concisely: If `R` is a commutative ring, `K` and `L` are fields, `R` is a scalar tower between `K` and `L`, and each `b i` is an integral element in `L` over `R`, then the discriminant of `b : ι → L` with respect to `K` is an integral element in `R`.
|
Algebra.discr_not_zero_of_basis
theorem Algebra.discr_not_zero_of_basis :
∀ {ι : Type w} [inst : DecidableEq ι] [inst_1 : Fintype ι] (K : Type u) {L : Type v} [inst_2 : Field K]
[inst_3 : Field L] [inst_4 : Algebra K L] [inst_5 : Module.Finite K L] [inst_6 : IsSeparable K L]
(b : Basis ι K L), Algebra.discr K ⇑b ≠ 0
This theorem states that if `b` is a basis for a finite separable field extension `L/K`, then the discriminant of `K` with respect to the basis `b` is not equal to zero. Here, `L/K` represents a field extension, where `K` is a subfield of `L`, and 'separable' refers to a property of the field extension meaning there is no repeated root in the minimal polynomial of any element in `L` over `K`. The discriminant serves as a measure of the 'non-degeneracy' of the algebra structure, and in this context, its non-zeroness ensures that the basis `b` indeed forms a valid vector space basis of the field extension `L/K`.
More concisely: If `b` is a basis for a separable finite field extension `L/K`, then the discriminant of `K` with respect to `b` is non-zero.
|
Algebra.discr_zero_of_not_linearIndependent
theorem Algebra.discr_zero_of_not_linearIndependent :
∀ (A : Type u) {B : Type v} {ι : Type w} [inst : DecidableEq ι] [inst_1 : CommRing A] [inst_2 : CommRing B]
[inst_3 : Algebra A B] [inst_4 : Fintype ι] [inst_5 : IsDomain A] {b : ι → B},
¬LinearIndependent A b → Algebra.discr A b = 0
This theorem states that if the family of vectors `b`, which are elements of an `A`-algebra `B`, is not linearly independent over `A`, then the discriminant of `b` with respect to `A` equals zero. Here, `A` and `B` are types representing commutative rings, `ι` is a type with decidable equality used to index the family of vectors `b`, `A` is an algebra over `B`, and `A` is a domain (a commutative ring with no zero divisors).
More concisely: If `b` is a family of vectors in a commutative ring `B`, which is an algebra over a domain `A` with no zero divisors, then the discriminant of `b` over `A` equals zero whenever `b` is not linearly independent over `A`.
|
Algebra.discr_eq_discr_of_algEquiv
theorem Algebra.discr_eq_discr_of_algEquiv :
∀ {A : Type u} {B : Type v} {C : Type z} {ι : Type w} [inst : DecidableEq ι] [inst_1 : CommRing A]
[inst_2 : CommRing B] [inst_3 : Algebra A B] [inst_4 : CommRing C] [inst_5 : Algebra A C] [inst_6 : Fintype ι]
(b : ι → B) (f : B ≃ₐ[A] C), Algebra.discr A b = Algebra.discr A (⇑f ∘ b)
This theorem states that if you have a family of vectors (which is indexed by `ι`) in an `A`-algebra `B`, then the discriminant of this family of vectors is preserved under algebraic equivalence. More specifically, for any such family of vectors `b`, if `f` is an algebraic equivalence between `B` and another `A`-algebra `C`, then the discriminant of `b` in `B` is equal to the discriminant of the image of `b` under `f` in `C`. This holds for all commutative rings `A`, `B`, and `C` with `A`-algebra structures on `B` and `C`.
More concisely: If `f` is an algebraic equivalence between commutative `A`-algebras `B` and `C`, and `b` is a family of vectors in `B` indexed by `ι`, then the discriminant of `b` in `B` equals the discriminant of `f(b)` in `C`.
|
Algebra.discr_of_matrix_mulVec
theorem Algebra.discr_of_matrix_mulVec :
∀ {A : Type u} {B : Type v} {ι : Type w} [inst : DecidableEq ι] [inst_1 : CommRing A] [inst_2 : CommRing B]
[inst_3 : Algebra A B] [inst_4 : Fintype ι] (b : ι → B) (P : Matrix ι ι A),
Algebra.discr A ((P.map ⇑(algebraMap A B)).mulVec b) = P.det ^ 2 * Algebra.discr A b
This theorem establishes a relationship between the discriminant of an algebra and the discriminant of another algebra derived from it by applying a transformation. Specifically, it states that for any commutative ring `A`, commutative ring `B`, and an `ι`-indexed family of elements `b` of `B`, and a matrix `P` with entries in `A` and indices in `ι`, the discriminant of the algebra obtained by applying the map induced by the algebra structure from `A` to `B` to `P` and then multiplying it by the vector `b`, is equal to the square of the determinant of `P` multiplied by the discriminant of the original algebra.
More concisely: For any commutative rings `A` and `B`, an `ι-`indexed family `b` of elements in `B`, and a matrix `P` with entries in `A` and indices in `ι`, the discriminant of `P`'s image under the map induced by the algebra structure from `A` to `B`, multiplied by the vector `b`, equals the determinant squared of `P` times the discriminant of the original algebra.
|
Algebra.discr_mul_isIntegral_mem_adjoin
theorem Algebra.discr_mul_isIntegral_mem_adjoin :
∀ (K : Type u) {L : Type v} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [inst_3 : Module.Finite K L]
{R : Type z} [inst_4 : CommRing R] [inst_5 : Algebra R K] [inst_6 : Algebra R L] [inst_7 : IsScalarTower R K L]
[inst_8 : IsSeparable K L] [inst_9 : IsIntegrallyClosed R] [inst_10 : IsFractionRing R K] {B : PowerBasis K L},
IsIntegral R B.gen → ∀ {z : L}, IsIntegral R z → Algebra.discr K ⇑B.basis • z ∈ Algebra.adjoin R {B.gen}
This theorem states that given an integrally closed domain `R` and its field of fractions `K`, if we have a finite separable extension `L` of `K` and a power basis `B` for `L` over `K`, where the generator of the power basis is integral over `R`, then for any element `z` of `L` that is integral over `R`, the product of the discriminant of `B.basis` with respect to `K` and `z` belongs to the smallest `R`-subalgebra of `L` that contains the generator of the power basis.
More concisely: Given an integrally closed domain `R`, its field of fractions `K`, a finite separable extension `L` of `K` with power basis `B` having an integral generator, if `z` is any element of `L` integral over `R`, then the product of the discriminant of `B` and `z` lies in the subalgebra of `L` generated by the power basis generator over `R`.
|
Algebra.discr_eq_discr
theorem Algebra.discr_eq_discr :
∀ (A : Type u) {ι : Type w} [inst : DecidableEq ι] [inst_1 : CommRing A] [inst_2 : Fintype ι] (b b' : Basis ι ℤ A),
Algebra.discr ℤ ⇑b = Algebra.discr ℤ ⇑b'
The theorem `Algebra.discr_eq_discr` states that for any type `A` with a commutative ring structure, and for any finite type `ι` with decidable equality, if we have two ℤ-bases `b` and `b'` for `A`, then the discriminants of these bases, as calculated by the `Algebra.discr` function, are equal. In other words, the discriminant, which is the determinant of the trace matrix, is the same for any ℤ-basis of a given algebraic structure.
More concisely: For any commutative ring `A` and finite type `ι` with decidable equality, the discriminants of any two ℤ-bases for `A` are equal.
|
Algebra.discr_def
theorem Algebra.discr_def :
∀ (A : Type u) {B : Type v} {ι : Type w} [inst : DecidableEq ι] [inst_1 : CommRing A] [inst_2 : CommRing B]
[inst_3 : Algebra A B] [inst_4 : Fintype ι] (b : ι → B), Algebra.discr A b = (Algebra.traceMatrix A b).det
The theorem `Algebra.discr_def` asserts that for any type `A`, with types `B` and `ι`, where `A` and `B` are commutative rings, `A` is an algebra over `B` and `ι` is a finite type, and a function `b` from `ι` to `B`, the discriminator of `A` with respect to `b` is equal to the determinant of the trace matrix of `A` with respect to `b`. In mathematical terms, the discriminator is determined by the determinant of the trace matrix, where the `(i, j)`-th element of the trace matrix is given by the trace of the product of the `i`-th and `j`-th elements of the `ι`-indexed family of elements of `B`.
More concisely: For any commutative rings A with types B and ι, where A is an algebra over B and ι is a finite type, the discriminator of A with respect to a function b from ι to B equals the determinant of the matrix whose (i, j)-th element is the trace of the product of the i-th and j-th elements of the ι-indexed family in B.
|
Algebra.discr_of_matrix_vecMul
theorem Algebra.discr_of_matrix_vecMul :
∀ {A : Type u} {B : Type v} {ι : Type w} [inst : DecidableEq ι] [inst_1 : CommRing A] [inst_2 : CommRing B]
[inst_3 : Algebra A B] [inst_4 : Fintype ι] (b : ι → B) (P : Matrix ι ι A),
Algebra.discr A (Matrix.vecMul b (P.map ⇑(algebraMap A B))) = P.det ^ 2 * Algebra.discr A b
This theorem establishes a relationship between the discriminant of an `A`-algebra `B` when calculated with an `ι`-indexed family of elements `b` and when calculated with a matrix-vector multiplication of `b` and a mapped matrix `P`. Specifically, it states that for any given types `A`, `B`, `ι`, an `ι`-indexed family of elements `b`, and a matrix `P`, the discriminant of the `A`-algebra `B` with respect to the matrix-vector multiplication of `b` and the mapped matrix `P` (made by applying the algebra map to each entry of `P`) equals the square of the determinant of `P` multiplied by the discriminant of the `A`-algebra `B` with respect to `b`. This relationship holds under the assumptions that `A` and `B` are commutative rings, `A` is an algebra over `B`, the equality in `ι` is decidable, and `ι` is a finite type.
More concisely: For any commutative rings `A` and `B` with `A` an algebra over `B`, a finite type `ι`, an `ι`-indexed family `b` of elements in `B`, and a matrix `P` over `A`, the discriminant of `B` with respect to the matrix-vector multiplication of `b` and the mapped matrix `P` equals the determinant square of `P` times the discriminant of `B` with respect to `b`.
|
Algebra.discr_isUnit_of_basis
theorem Algebra.discr_isUnit_of_basis :
∀ {ι : Type w} [inst : DecidableEq ι] [inst_1 : Fintype ι] (K : Type u) {L : Type v} [inst_2 : Field K]
[inst_3 : Field L] [inst_4 : Algebra K L] [inst_5 : Module.Finite K L] [inst_6 : IsSeparable K L]
(b : Basis ι K L), IsUnit (Algebra.discr K ⇑b)
This theorem states that if `b` is a basis of a finite separable field extension `L/K`, then `Algebra.discr K b` is a unit. In mathematical terms, given a basis `b` of a finite separable field extension, the discriminant of the trace matrix (which is `Algebra.discr K b`) is a unit. A unit here means that this discriminant has a multiplicative inverse. The fields `L` and `K` are assumed to be fields and `L` is assumed to be a `K`-algebra. The basis `b` is assumed to be a basis for `L` as a vector space over `K`. Moreover, `L` is assumed to be a finite dimensional `K`-module and it's also assumed that `L` is a separable extension over `K`.
More concisely: Given a finite separable field extension L/K with a basis b, the discriminant of the trace matrix Algebra.discr K b is a unit in K.
|
Algebra.discr_powerBasis_eq_prod'
theorem Algebra.discr_powerBasis_eq_prod' :
∀ (K : Type u) {L : Type v} (E : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Field E]
[inst_3 : Algebra K L] [inst_4 : Algebra K E] [inst_5 : Module.Finite K L] [inst_6 : IsAlgClosed E]
(pb : PowerBasis K L) [inst_7 : IsSeparable K L] (e : Fin pb.dim ≃ (L →ₐ[K] E)),
(algebraMap K E) (Algebra.discr K ⇑pb.basis) =
Finset.univ.prod fun i =>
(Finset.Ioi i).prod fun j => -(((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen))
This theorem, named `Algebra.discr_powerBasis_eq_prod'`, states that for any fields `K`, `L`, and `E`, with `L` and `E` being `K`-algebras, and with `L` being a finite `K` module, and `E` being an algebraically closed field, given a power basis `pb` of `L` over `K`, and assuming that `L` is a separable extension of `K`, if there exists an isomorphism `e` from the set of `Fin pb.dim` to the set of `K`-algebra homomorphisms from `L` to `E`, then the image under `algebraMap` from `K` to `E` of the discriminant of the `K` algebra `L` with respect to the basis `pb.basis` is equal to the product over all elements `i` in the universal set of the product over all elements `j` in the set `{x | i < x}` of the negation of the product of `(e j pb.gen - e i pb.gen)` and `(e i pb.gen - e j pb.gen)`. In simpler terms, it relates the discriminant of a power basis for a field extension to a certain product involving the power basis elements and an algebra homomorphism.
More concisely: Given a finite separable `K`-algebra extension `L` of a field `K` within an algebraically closed field `E`, with a power basis `pb` for `L` over `K`, there exists an isomorphism from the set of `K`-algebra homomorphisms from `L` to `E` to the set of `Fin pb.dim` elements, and the discriminant of `L` with respect to `pb.basis` equals the product over distinct indices `i, j` of the negative of the difference of images under this isomorphism of the `i`th and `j`th basis elements.
|
Algebra.discr_powerBasis_eq_norm
theorem Algebra.discr_powerBasis_eq_norm :
∀ (K : Type u) {L : Type v} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [inst_3 : Module.Finite K L]
(pb : PowerBasis K L) [inst_4 : 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)))
This theorem states that for a given power basis `pb` of a field extension `L/K`, the discriminant of the power basis is equal to the (-1) raised to the power of half the product of the field extension rank and one less than the rank, times the norm of the derivative of the minimal polynomial of the power basis generator evaluated at the power basis generator. This relationship connects the discriminant of a power basis to the norm of the field extension. The fields `K` and `L` must be separable, and `L` should be a finite module over `K`.
More concisely: For a separable finite field extension L/K with a power basis pb, the discriminant of pb is equal to (-1)^(rank L/K * (rank pb - 1)) * norm(derivative of minimal polynomial of pb's generator at pb).
|
Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two
theorem Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two :
∀ {ι : Type w} [inst : DecidableEq ι] [inst_1 : Fintype ι] (K : Type u) {L : Type v} (E : Type z) [inst_2 : Field K]
[inst_3 : Field L] [inst_4 : Field E] [inst_5 : Algebra K L] [inst_6 : Algebra K E] [inst_7 : Module.Finite K L]
[inst_8 : IsAlgClosed E] (b : ι → L) [inst_9 : IsSeparable K L] (e : ι ≃ (L →ₐ[K] E)),
(algebraMap K E) (Algebra.discr K b) = (Algebra.embeddingsMatrixReindex K E b e).det ^ 2
This theorem states that if we have a field extension `L/K` and a family of elements `b : ι → L`, then the discriminant `discr K b` is the square of the determinant of a certain matrix. The entries of this matrix are obtained by applying an embedding `σⱼ : L →ₐ[K] E` to the element `b i`, where `σⱼ` is an embedding in an algebraically closed field `E` corresponding to `j : ι` via a bijection `e : ι ≃ (L →ₐ[K] E)`. In other words, the discriminant of the elements `b` (viewed as elements of `L`) when mapped to `K` via the given algebra structure, equals the square of the determinant of the matrix formed by the images of `b` under the embeddings into `E`, up to reindexing by `e`, when these images are also viewed as elements of `E` via the given algebra structure. The theorem also assumes that the field extension `L/K` is separable and the field `L` is a finite module over `K`.
More concisely: Given a separable field extension L/K, a finite K-module L, and a family b : ι → L, the discriminant of b viewed as elements of L over K equals the square of the determinant of the matrix formed by applying embeddings σⱼ : L →ₐ[K] E to b i, where E is an algebraically closed field and σⱼ corresponds to j : ι via a bijection e : ι ≃ (L →ₐ[K] E).
|
Algebra.discr_powerBasis_eq_prod
theorem Algebra.discr_powerBasis_eq_prod :
∀ (K : Type u) {L : Type v} (E : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Field E]
[inst_3 : Algebra K L] [inst_4 : Algebra K E] [inst_5 : Module.Finite K L] [inst_6 : IsAlgClosed E]
(pb : PowerBasis K L) (e : Fin pb.dim ≃ (L →ₐ[K] E)) [inst_7 : IsSeparable K L],
(algebraMap K E) (Algebra.discr K ⇑pb.basis) =
Finset.univ.prod fun i => (Finset.Ioi i).prod fun j => ((e j) pb.gen - (e i) pb.gen) ^ 2
This theorem, named `Algebra.discr_powerBasis_eq_prod`, states that for any field `K`, another field `L`, and an algebraically closed field `E`, given an algebra structure from `K` to `L` and `K` to `E`, and given a power basis `pb` of `L` over `K`, an isomorphism `e` from the finite-dimensional vector space over `K` to the set of `K`-algebra automorphisms of `L` to `E`, and assuming that `L` is a separable extension over `K`, the result of applying the algebra map from `K` to `E` to the discriminant of `pb` with respect to `K` is equal to the product, over all elements `i` of the universal set of the finite set given by the dimension of the power basis, of the product over all elements `j` in the open interval `(i, +∞)` of the square of the difference between the evaluations of the power basis generator at `j` and at `i` in the field `E`.
In mathematical terms, for a power basis $\text{pb}$ with basis vector $\text{pb.gen}$, dimension $\text{pb.dim}$, the theorem is about the relationship between the discriminant of the power basis and the differences of the roots (automorphisms) of the polynomial that the power basis spans. The theorem states that the discriminant of the power basis is equal to the product of the squares of the differences of the roots of the polynomial.
More concisely: Given a power basis `pb` over a field `K` with discriminant `D` and dimension `n`, in a separable extension `L/K`, the discriminant `D` equals the product of the squares of the differences between the `n` roots of the polynomial defining the power basis.
|
Algebra.discr_powerBasis_eq_prod''
theorem Algebra.discr_powerBasis_eq_prod'' :
∀ (K : Type u) {L : Type v} (E : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Field E]
[inst_3 : Algebra K L] [inst_4 : Algebra K E] [inst_5 : Module.Finite K L] [inst_6 : IsAlgClosed E]
(pb : PowerBasis K L) [inst_7 : 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.univ.prod fun i =>
(Finset.Ioi i).prod fun j => ((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen)
This theorem, `Algebra.discr_powerBasis_eq_prod''`, states that for any field `K`, suppose `L` and `E` are also fields, where `L` is a finite `K`-module and `E` is algebraically closed. If `pb` is a power basis of `L` over `K`, and `L` is separable over `K`, and we have a bijection `e` from the finite set of all elements of `pb.dim` to the set of `K`-algebra homomorphisms from `L` to `E`, then the image of the discriminant of the basis of `pb` under the algebraic map from `K` to `E` is equal to the product of $(-1)$ raised to the power of the product of the rank of `L` over `K` and one less than the rank of `L` over `K` divided by `2`, and the products over all elements `i` in the universal finite set, each of which is the product over all elements `j` greater than `i` in the universal finite set of the differences of the images of the generator of `pb` under `e j` and `e i`, multiplied to the differences of the images of the generator of `pb` under `e i` and `e j`. In other words, this theorem talks about a explicit formula for the discriminant of a power basis of a separable algebra.
More concisely: Given a finite separable `K`-module `L` over a field `K` with a power basis `pb` and a bijection from the set of `K`-algebra homomorphisms from `L` to an algebraically closed field `E`, the discriminant of `pb` is equal to the explicit product described in the theorem statement.
|