Field.sepDegree_mul_insepDegree
theorem Field.sepDegree_mul_insepDegree :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
Field.sepDegree F E * Field.insepDegree F E = Module.rank F E
The theorem `Field.sepDegree_mul_insepDegree` asserts that for any algebraic field extension `E / F`, the product of the separable degree and the inseparable degree of that field extension is equal to the degree of the field extension itself. In other words, it expresses that the degree of an algebraic field extension is equivalent to the product of the degree of separability and the degree of inseparability. This is similar to the fundamental theorem of field theory which states that the total degree of a field extension is the product of the separable degree and the purely inseparable degree.
More concisely: The separable degree and inseparable degree of an algebraic field extension multiply to equal the degree of the extension.
|
Field.lift_insepDegree_eq_of_equiv
theorem Field.lift_insepDegree_eq_of_equiv :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w)
[inst_3 : Field K] [inst_4 : Algebra F K],
(E ≃ₐ[F] K) → Cardinal.lift.{w, v} (Field.insepDegree F E) = Cardinal.lift.{v, w} (Field.insepDegree F K)
This theorem states that if two fields `E` and `K` are isomorphic as `F`-algebras (i.e., they have the same algebraic structure over a common base field `F`), then their inseparable degrees over `F` are equal. The inseparable degree of a field extension `E / F` is defined to be the degree of `E / separableClosure F E`. The cardinality of these inseparable degrees is then lifted to the maximum of the universes in which `E` and `K` reside. In other words, despite possibly living in different universes, if `E` and `K` have the same algebraic structure over `F`, they also have the same inseparable degree over `F`.
More concisely: If two fields `E` and `K` are isomorphic as `F`-algebras, then they have equal inseparable degrees over the base field `F`.
|
map_mem_separableClosure_iff
theorem map_mem_separableClosure_iff :
∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type w}
[inst_3 : Field K] [inst_4 : Algebra F K] (i : E →ₐ[F] K) {x : E},
i x ∈ separableClosure F K ↔ x ∈ separableClosure F E
This theorem states that for any field `F` and any two other fields `E` and `K` where `E` and `K` are both `F`-algebras, if there exists an algebra homomorphism `i` from `E` to `K`, then an element `x` from `E` is contained in the separable closure of `F` in `K` (or, in other words, `i x` is in the separable closure of `F` in `K`) if and only if `x` is itself contained in the separable closure of `F` in `E`. In mathematical terms, this theorem asserts the compatibility of algebra homomorphisms with the operation of taking separable closures.
More concisely: If `F` is a field, `E` and `K` are `F`-algebras, and there exists an algebra homomorphism from `E` to `K`, then for any element `x` in `E`, `x` is in the separable closure of `F` in `E` if and only if `i(x)` is in the separable closure of `F` in `K`.
|
IntermediateField.isSeparable_adjoin_iff_separable
theorem IntermediateField.isSeparable_adjoin_iff_separable :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {S : Set E},
IsSeparable F ↥(IntermediateField.adjoin F S) ↔ ∀ x ∈ S, (minpoly F x).Separable
This theorem states that for any given field `F` and `E`, where `E` is an algebra over `F`, and a set `S` of elements in `E`, the field extension `F(S) / F` is separable if and only if every element `x` in `S` has a separable minimal polynomial over `F`. In other words, the set `S` is adjoined to `F` to form a new field, and the separability of this extension field is equivalent to the separability of all the elements in the set `S`.
More concisely: A field extension F(S)/F is separable if and only if every element x in S has a separable minimal polynomial over F.
|
Field.lift_sepDegree_eq_of_equiv
theorem Field.lift_sepDegree_eq_of_equiv :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w)
[inst_3 : Field K] [inst_4 : Algebra F K],
(E ≃ₐ[F] K) → Cardinal.lift.{w, v} (Field.sepDegree F E) = Cardinal.lift.{v, w} (Field.sepDegree F K)
The theorem `Field.lift_sepDegree_eq_of_equiv` states that for any two types `E` and `K` that are isomorphic as `F`-algebras, their separable degrees over `F` are equal. Here, `E` and `K` are assumed to be fields, and `F` is a field that is an algebra over both `E` and `K`. In particular, the separable degrees of `E` and `K` over `F` are lifted to the same cardinality, indicating that the separable degrees are identical when considering the infinite, or general, case. This implies that the structure of `E` and `K` as extensions of `F` are identical in terms of their separability, a key concept in field theory and algebra.
More concisely: The separable degrees of two isomorphic F-algebras (as fields) E and K over a common field F are equal.
|
separableClosure.separableClosure_eq_bot
theorem separableClosure.separableClosure_eq_bot :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
separableClosure (↥(separableClosure F E)) E = ⊥
This theorem states that for any two types `F` and `E` where both `F` and `E` are fields and `F` is an algebra over `E`, the separable closure in `E` of the separable closure of `F` in `E` is the zero element (or bottom element) of the lattice of subalgebras of `E`. In other words, taking the separable closure twice in this manner yields no new elements.
More concisely: The separable closure of a field `F` in a field `E`, and then the separable closure of the resulting extension in `E`, is the same subfield of `E`.
|
separableClosure.adjoin_le
theorem separableClosure.adjoin_le :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w)
[inst_3 : Field K] [inst_4 : Algebra F K] [inst_5 : Algebra E K] [inst_6 : IsScalarTower F E K],
IntermediateField.adjoin E ↑(separableClosure F K) ≤ separableClosure E K
This theorem states that, given a particular field extension tower `K / E / F`, if we extend the field `E` by adjoining the separable closure of `F` and `K`, the resultant field is a subset of the separable closure of `E` and `K`. Here, a field extension is a situation where one field (a set with two operations, addition and multiplication, following certain rules) is contained within another field. The separable closure is the smallest separable extension that contains a given field. The `≤` symbol represents the subset or containment relationship between sets. So, if we were to visualize the fields as sets, the set that results from adjoining the separable closure of `F` and `K` to `E` would be entirely contained within the separable closure of `E` and `K`.
More concisely: The separable closure of a field K contained in a field E, is contained in the field extension E.(F.sep-clos ⊆ E.alg-clos F), where F.sep-clos is the separable closure of F in E and E.alg-clos F is the field obtained by adjoining the separable closure of F to E.
|
le_separableClosure_iff
theorem le_separableClosure_iff :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (L : IntermediateField F E),
L ≤ separableClosure F E ↔ IsSeparable F ↥L
This theorem states that for any two types `F` and `E`, both of which are fields, and `F` is also an algebra over `E`, an intermediate field `L` of `E / F` is contained in the separable closure of `F` in `E` if and only if `L` is separable over `F`. In the context of field theory, an intermediate field is separable over the base field if every element of the intermediate field is a root of a polynomial with coefficients in the base field that has distinct roots. The separable closure of a field is the smallest separable extension containing that field.
More concisely: A field extension L of a field F is contained in the separable closure of F if and only if L is separable over F.
|
separableClosure.map_le_of_algHom
theorem separableClosure.map_le_of_algHom :
∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type w}
[inst_3 : Field K] [inst_4 : Algebra F K] (i : E →ₐ[F] K),
IntermediateField.map i (separableClosure F E) ≤ separableClosure F K
The theorem `separableClosure.map_le_of_algHom` states that given `i`, an algebra homomorphism from a field `E` to a field `K` both over a common base field `F`, the image of the separable closure of `F` in `E` under the map `i` is contained within the separable closure of `F` in `K`. This condition is denoted as `IntermediateField.map i (separableClosure F E) ≤ separableClosure F K` in Lean, where `IntermediateField.map` is a function that takes a map and an intermediate field between `K` and `L` and returns a new intermediate field. The ≤ symbol signifies the subset relation in the context of intermediate fields.
More concisely: The separable closure of a field in a larger field under an algebra homomorphism is contained within the separable closure of that field in the larger field's extension.
|
separableClosure.eq_top_iff
theorem separableClosure.eq_top_iff :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
separableClosure F E = ⊤ ↔ IsSeparable F E
This theorem states that for any two types `F` and `E` that are fields, with an algebra structure from `F` to `E`, the separable closure of `F` in `E` is equal to `E` (represented as `⊤` here) if and only if the field extension `E / F` is separable. In other words, it is saying that the entire field `E` is the separable closure of `F` in `E` exactly when `E` over `F` is a separable extension.
More concisely: The separable closure of a field `F` in a field `E` is equal to `E` if and only if the extension `E/F` is separable.
|
le_separableClosure
theorem le_separableClosure :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (L : IntermediateField F E)
[inst_3 : IsSeparable F ↥L], L ≤ separableClosure F E
This theorem states that for any intermediate field `L` of a field extension `E / F`, if `L` is separable over `F`, then `L` is contained in the separable closure of `F` in `E`. Here, a field is separable if its elements are roots of a separable polynomial, and the separable closure of a field `F` in an extension `E` is the subfield generated by the separable elements of `E` over `F`.
More concisely: If `L` is an intermediate field of a field extension `E/F` that is separable over `F`, then `L` is contained in the separable closure of `F` in `E`.
|
separableClosure.eq_restrictScalars_of_isSeparable
theorem separableClosure.eq_restrictScalars_of_isSeparable :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w)
[inst_3 : Field K] [inst_4 : Algebra F K] [inst_5 : Algebra E K] [inst_6 : IsScalarTower F E K]
[inst_7 : IsSeparable F E], separableClosure F K = IntermediateField.restrictScalars F (separableClosure E K)
This theorem states that for a tower of field extensions `K / E / F`, if the extension `E / F` is separable, then the separable closure of `F` in `K` is equivalent to the separable closure of `E` in `K`, where the latter is restricted to the scalars of `F`. Here, a field extension refers to a pair of fields such that one field is a subset of the other. Separability of a field extension is a property that says every element of the larger field is a root of a polynomial with coefficients in the smaller field and has distinct roots. The separable closure of a field in another is the smallest separable extension of the field within the other.
More concisely: If `K / E / F` is a tower of separable field extensions, then the separable closure of `F` in `K` equals the separable closure of `E` in `K` restricted to `F`.
|
Field.sepDegree_eq_of_equiv
theorem Field.sepDegree_eq_of_equiv :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type v)
[inst_3 : Field K] [inst_4 : Algebra F K], (E ≃ₐ[F] K) → Field.sepDegree F E = Field.sepDegree F K
In natural language, this theorem states that for any two field extensions `E` and `K` over a base field `F`, if `E` and `K` are algebraically equivalent over `F`, then the separable degree of `F` to `E` is equal to the separable degree of `F` to `K`. Here, the separable degree of a field extension `E / F` is defined as the degree of the separable closure of `E` over `F`. In mathematical terms, this theorem asserts that for two field extensions `E / F` and `K / F`, if there exists an algebra isomorphism between `E` and `K` that fixes `F`, then the separable degrees of these extensions are equal.
More concisely: If two field extensions are algebraically equivalent over a base field, then they have equal separable degrees.
|
IsSepClosed.separableClosure_eq_bot_iff
theorem IsSepClosed.separableClosure_eq_bot_iff :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [inst_3 : IsSepClosed E],
separableClosure F E = ⊥ ↔ IsSepClosed F
The theorem `IsSepClosed.separableClosure_eq_bot_iff` states that for any two types `F` and `E`, where both `F` and `E` are fields and `F` is an algebra over `E`, if `E` is a separably closed field, then the separable closure of `F` in `E` is equal to the zero ideal (i.e., it contains only the zero element) if and only if `F` is also separably closed. In mathematical terms, if `E / F` is a field extension and `E` is separably closed, then `F` is separably closed if and only if the separable closure of `F` in `E` is trivial.
More concisely: For a field extension `E/F` with `F` an algebra over `E` and `E` separably closed, the separable closure of `F` in `E` is the zero ideal if and only if `F` is separably closed.
|
le_separableClosure'
theorem le_separableClosure' :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {L : IntermediateField F E},
(∀ (x : ↥L), (minpoly F x).Separable) → L ≤ separableClosure F E
This theorem states that for any two given types `F` and `E` which are fields, with `F` being an algebra over `E`, if `L` is an intermediate field of `E / F` and every element of `L` is separable over `F` (`separable` here refers to the concept of separable polynomials in field theory, meaning the minimal polynomial of the element has no repeated roots), then `L` is contained in the separable closure of `F` in `E`. The separable closure of `F` in `E` is the largest separable extension of `F` in `E`.
More concisely: If `F` is a field embedded in `E` as an algebra, `L` is an intermediate separable field of `E/F`, then `L` is contained in the separable closure of `F` in `E`.
|
Field.finInsepDegree_eq_of_equiv
theorem Field.finInsepDegree_eq_of_equiv :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w)
[inst_3 : Field K] [inst_4 : Algebra F K], (E ≃ₐ[F] K) → Field.finInsepDegree F E = Field.finInsepDegree F K
The theorem `Field.finInsepDegree_eq_of_equiv` states that if two fields `E` and `K` are isomorphic as `F`-algebras, then they have the same finite inseparable degree over `F`. This finite inseparable degree is defined as the degree of a field `E` over its separable closure with `F`, denoted as `E / separableClosure F E`, and is defined to be zero if the field extension is infinite. The isomorphism between the fields `E` and `K` is expressed as `(E ≃ₐ[F] K)` in Lean 4.
More concisely: If two fields `E` and `K` are isomorphic as `F`-algebras, then they have equal finite inseparable degrees over `F`.
|
separableClosure.normalClosure_eq_self
theorem separableClosure.normalClosure_eq_self :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
normalClosure F (↥(separableClosure F E)) E = separableClosure F E
This theorem states that for any two types `F` and `E` which are fields with an algebra structure defined from `F` to `E`, the normal closure in `E/F` of the separable closure of `F` in `E` is equal to the separable closure of `F` in `E` itself.
In terms of field theory, this theorem is saying that if you take the separable closure of a field `F` within a field extension `E`, and then take the normal closure of that within `E/F`, you end up back at the separable closure you started with. This provides valuable insight into the structure of separable extensions and normal extensions in field theory.
More concisely: The normal closure of the separable closure of a field `F` in a field extension `E` equals the separable closure of `F` in `E`.
|
Field.insepDegree_eq_of_equiv
theorem Field.insepDegree_eq_of_equiv :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type v)
[inst_3 : Field K] [inst_4 : Algebra F K], (E ≃ₐ[F] K) → Field.insepDegree F E = Field.insepDegree F K
This theorem states that for any two field extensions `E` and `K` over a common field `F`, if `E` and `K` are algebraically equivalent over `F`, then the inseparable degree of `E` over `F` is the same as the inseparable degree of `K` over `F`.
In more detail, the inseparable degree is a measure of how inseparable a field extension is. It is defined as the degree of the extension `E` over the separable closure of `E` in `F`. If `E` and `K` are algebraically equivalent, it means that there is an algebraic isomorphism between them that respects the field structure, so any algebraic properties, such as the inseparable degree, should be preserved under this isomorphism.
More concisely: If two field extensions E and K over a common field F are algebraically equivalent, then their inseparable degrees over F are equal.
|
separableClosure.le_restrictScalars
theorem separableClosure.le_restrictScalars :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w)
[inst_3 : Field K] [inst_4 : Algebra F K] [inst_5 : Algebra E K] [inst_6 : IsScalarTower F E K],
separableClosure F K ≤ IntermediateField.restrictScalars F (separableClosure E K)
This theorem states that, given a tower of field extensions `K / E / F`, the separable closure of `F` and `K` is contained within the separable closure of `E` and `K`. In other words, any root of a polynomial with coefficients in `F` which is separable over `K`, can also be viewed as a root of a polynomial with coefficients in `E` which is separable over `K`. This is subject to the algebraic structures and scalar tower condition specified in the prerequisites.
More concisely: The separable closures of a field `K` in a field extension `E`, and then in `F`, are equal.
|
separableClosure.isAlgebraic
theorem separableClosure.isAlgebraic :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
Algebra.IsAlgebraic F ↥(separableClosure F E)
The theorem `separableClosure.isAlgebraic` states that for any types `F` and `E`, where `F` and `E` are fields and there exists an algebra structure from `F` to `E`, the separable closure of `F` in `E` is algebraic over `F`. In other words, for every element in the separable closure of `F` in `E`, there exists a non-zero polynomial of `F` such that this element is a root of the polynomial. This essentially means that each element in the separable closure can be described as the root of some polynomial with coefficients in `F`.
More concisely: The separable closure of a field `F` in an extension field `E` is algebraic over `F`. That is, every element in the separable closure is a root of some non-zero polynomial with coefficients in `F`.
|
mem_separableClosure_iff
theorem mem_separableClosure_iff :
∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x : E},
x ∈ separableClosure F E ↔ (minpoly F x).Separable
This theorem states that for any fields `F` and `E` and for any element `x` from `E`, `x` is contained in the separable closure of `F` in `E` if and only if the minimal polynomial of `x` over `F` is a separable polynomial. Here, a polynomial is defined as separable if it is coprime with its derivative in the commutative semiring `R`.
More concisely: A field element `x` is in the separable closure of field `F` in `E` if and only if the minimal polynomial of `x` over `F` is separable.
|