IntermediateField.finrank_fixedField_eq_card
theorem IntermediateField.finrank_fixedField_eq_card :
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
(H : Subgroup (E ≃ₐ[F] E)) [inst_3 : FiniteDimensional F E] [inst_4 : DecidablePred fun x => x ∈ H],
FiniteDimensional.finrank (↥(IntermediateField.fixedField H)) E = Fintype.card ↥H
This theorem states that for any field `F`, any field `E` that is an algebra over `F`, and any subgroup `H` of the algebraic automorphisms of `E` over `F`, if `E` is a finite-dimensional vector space over `F` and we can decide whether an element belongs to `H`, then the rank of the intermediate field fixed by `H` as a module over `E` is equal to the number of elements in `H`.
In mathematical terms, if `F` and `E` are fields with `E` being a finite-dimensional field extension of `F`, and `H` is a subgroup of the group of `F`-automorphisms of `E`, then the dimension of the fixed field of `H` over `E` is the same as the cardinality of `H`.
More concisely: For a finite-dimensional field extension `E` over `F`, the cardinality of a subgroup `H` of `F`-automorphisms of `E` equals the dimension of the fixed field of `H` within `E` as a vector space.
|
IsGalois.of_separable_splitting_field
theorem IsGalois.of_separable_splitting_field :
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {p : Polynomial F}
[sp : Polynomial.IsSplittingField F E p], p.Separable → IsGalois F E
The theorem `IsGalois.of_separable_splitting_field` states that for any fields `F` and `E`, with `E` being an algebra over `F`, and any polynomial `p` with coefficients in `F`, if `E` is the splitting field of `p` and `p` is a separable polynomial (i.e., `p` is coprime with its derivative), then the field extension `F` to `E` is a Galois extension. In more mathematical terms, it means that if a polynomial is separable and its roots are in `E` (making `E` the splitting field of `p`), then the field extension from `F` to `E` has a property called Galois, which involves certain symmetries between the roots of the polynomial.
More concisely: If `F` is a field, `E` is the splitting field of a separable polynomial `p` over `F` with coefficients in `F`, then `F` to `E` is a Galois extension.
|
IsGalois.fixedField_fixingSubgroup
theorem IsGalois.fixedField_fixingSubgroup :
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
(K : IntermediateField F E) [inst_3 : FiniteDimensional F E] [h : IsGalois F E],
IntermediateField.fixedField K.fixingSubgroup = K
The theorem `IsGalois.fixedField_fixingSubgroup` states that for any field `F`, assuming `F` is an instance of a Field, and any field `E`, assuming `E` is an instance of a Field and there exists an algebra structure over `F` and `E`, and any intermediate field `K` of `F` and `E`, given that `E` is a finite dimensional extension over `F` and also a Galois extension over `F`, then the intermediate field which is fixed by the subgroup that fixes `K` is indeed `K` itself. In simpler terms, this theorem is a part of Galois theory, stating that the field fixed by the automorphism group that fixes a given intermediate field in a finite Galois extension is the intermediate field itself.
More concisely: In a finite Galois extension, the fixed field of the subgroup stabilizing an intermediate field is that intermediate field itself.
|
IsGalois.card_aut_eq_finrank
theorem IsGalois.card_aut_eq_finrank :
∀ (F : Type u_1) [inst : Field F] (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E]
[inst_3 : FiniteDimensional F E] [inst_4 : IsGalois F E],
Fintype.card (E ≃ₐ[F] E) = FiniteDimensional.finrank F E
The theorem `IsGalois.card_aut_eq_finrank` states that for any field `F` and any field extension `E` of `F`, if `E` is a finite-dimensional vector space over `F` and `E` is a Galois extension of `F`, then the number of F-algebra automorphisms of `E` (elements of the type `E ≃ₐ[F] E`) is equal to the rank of `E` as a module over `F` (equivalently, the dimension of `E` as a vector space over `F`). In the context of Galois theory, this is a formal statement of the fundamental theorem that the order of the Galois group of a finite Galois extension is equal to the degree of the extension.
More concisely: The number of algebra automorphisms of a finite-dimensional Galois extension equals its dimension over the base field.
|
IsGalois.tfae
theorem IsGalois.tfae :
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
[inst_3 : FiniteDimensional F E],
[IsGalois F E, IntermediateField.fixedField ⊤ = ⊥, Fintype.card (E ≃ₐ[F] E) = FiniteDimensional.finrank F E,
∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE
This theorem provides equivalent characterizations of a Galois extension of finite degree. Given fields `F` and `E` where `E` is a finite-dimensional algebra over `F`, the following are equivalent:
1. `E` is a Galois extension of `F` (`IsGalois F E`).
2. The fixed field of the automorphism group of `E` over `F` is trivial (`IntermediateField.fixedField ⊤ = ⊥`).
3. The cardinality of the automorphism group of `E` over `F` equals the dimension of `E` over `F` (`Fintype.card (E ≃ₐ[F] E) = FiniteDimensional.finrank F E`).
4. There exists a polynomial `p` over `F` which is separable and for which `E` is the splitting field (`∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p`).
In other words, these four conditions can be used interchangeably to establish that `E` is a finite Galois extension of `F`.
More concisely: A field extension E of F is a finite Galois extension if and only if its automorphism group has trivial fixed field, has the same cardinality as the dimension of E over F, and there exists a separable polynomial over F whose splitting field is E.
|
IntermediateField.le_iff_le
theorem IntermediateField.le_iff_le :
∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
(H : Subgroup (E ≃ₐ[F] E)) (K : IntermediateField F E),
K ≤ IntermediateField.fixedField H ↔ H ≤ K.fixingSubgroup
The theorem `IntermediateField.le_iff_le` states that for any field `F`, a field `E` which is an algebra over `F`, a subgroup `H` of the algebraic field automorphisms of `E` over `F`, and an intermediate field `K` of `E` over `F`, the intermediate field `K` is a subset of the field fixed by the subgroup `H` if and only if the subgroup `H` is a subset of the subgroup that fixes the intermediate field `K`.
More concisely: For any field extension E/F, subgroup H of its algebraic automorphisms, and intermediate field K between F and E, K is fixed by H if and only if H is contained in the subgroup fixing K.
|