IntermediateField.fixingSubgroup_isOpen
theorem IntermediateField.fixingSubgroup_isOpen :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
(E : IntermediateField K L) [inst_3 : FiniteDimensional K ↥E], IsOpen ↑E.fixingSubgroup
The theorem `IntermediateField.fixingSubgroup_isOpen` states that for a tower of fields `L/E/K` with `E/K` being finite, the Galois group of `L` over `E`, denoted as `Gal(L/E)`, is an open subgroup of the algebraic isomorphisms from `L` to `L` over `K`, denoted as `L ≃ₐ[K] L`. Here, `IsOpen` refers to the concept of an open set in the topological space sense, `fixingSubgroup` refers to the subgroup that leaves a set invariant under a multiplication action, and `FiniteDimensional` refers to the property of a vector space having a finite basis.
More concisely: The Galois group of a finite extension `E/K` in a field tower `E/K/L` is an open subgroup of the group of algebraic isomorphisms from `L` to `L` over `K`.
|
finiteDimensional_sup
theorem finiteDimensional_sup :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
(E1 E2 : IntermediateField K L),
FiniteDimensional K ↥E1 → FiniteDimensional K ↥E2 → FiniteDimensional K ↥(E1 ⊔ E2)
The theorem `finiteDimensional_sup` states that given `E1` and `E2`, which are finite-dimensional intermediate fields between a base field `K` and an extension field `L`, their compositum (the smallest field extension that contains both `E1` and `E2`) is also a finite-dimensional intermediate field over `K`. This theorem is a restatement of an existing theorem in mathlib, adapted to be compatible with the type classes being used here.
More concisely: The compositum of two finite-dimensional intermediate fields over a base field is also a finite-dimensional intermediate field.
|
IntermediateField.fixingSubgroup_isClosed
theorem IntermediateField.fixingSubgroup_isClosed :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
(E : IntermediateField K L) [inst_3 : FiniteDimensional K ↥E], IsClosed ↑E.fixingSubgroup
The theorem `IntermediateField.fixingSubgroup_isClosed` states that, given a tower of fields `L/E/K` (where `E` is an intermediate field between `L` and `K`), and given that `E/K` is a finite dimensional field extension, the subgroup of the Galois group of `L` over `E` (denoted as `Gal(L/E)`) is a closed subgroup. This subgroup is embedded in the group of `K`-algebra automorphisms of `L` (denoted as `L ≃ₐ[K] L`). In other words, the set of all field automorphisms of `L` that keep `E` fixed is a closed set.
More concisely: The subgroup of Galois automorphisms of a field `L` over an intermediate field `E`, in a finite dimensional extension `L/E/K`, is a closed subgroup of the group of `K`-algebra automorphisms of `L`.
|
IntermediateField.mem_fixingSubgroup_iff
theorem IntermediateField.mem_fixingSubgroup_iff :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
(E : IntermediateField K L) (σ : L ≃ₐ[K] L), σ ∈ E.fixingSubgroup ↔ ∀ x ∈ E, σ x = x
The theorem `IntermediateField.mem_fixingSubgroup_iff` states that for any fields `K` and `L` with `L` being an algebra over `K`, and any intermediate field `E` of `K` and `L`, an algebra automorphism `σ` of `L` over `K` belongs to the subgroup that fixes `E` under the `MulAction` if and only if `σ` fixes every element of `E`. In other words, `σ` is in the Galois group of `L` over `E` precisely when it leaves every element of `E` unchanged.
More concisely: An algebra automorphism of field extension `L` over `K` fixes the intermediate field `E` under the multiplication action if and only if it fixes every element in `E`.
|
top_fixedByFinite
theorem top_fixedByFinite :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L], ⊤ ∈ fixedByFinite K L
This theorem states that for any field extension `L/K`, the Galois group `Gal(L/K)` is included in the set `fixedByFinite K L`. In more mathematical terms, this means for every field extension `L/K`, the Galois group of `L` over `K` is contained in the set of Galois subgroups fixed by finite field extensions of `K` in `L`.
More concisely: The Galois group of a field extension lies within the set of its fixed subfields under finite field extensions.
|
krullTopology_totallyDisconnected
theorem krullTopology_totallyDisconnected :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L],
Algebra.IsIntegral K L → IsTotallyDisconnected Set.univ
This theorem states that if `L/K` is an algebraic field extension, then the Krull topology on the set of K-algebra automorphisms of `L` is totally disconnected. In more detail, given any two types `K` and `L` where `K` and `L` are fields and `L` is an algebra over `K`, if every element of `L` is integral over `K`, then for any subset of the universal set (which contains all algebra automorphisms of `L` over `K`), if the subset is preconnected in the Krull topology, it must be either empty or contain a single element. This means that there are no nontrivial connected subsets, which is the definition of being totally disconnected.
More concisely: If `L/K` is an algebraic field extension, then the set of `K`-algebra automorphisms of `L` endowed with the Krull topology is a totally disconnected topological space.
|
IntermediateField.map_id
theorem IntermediateField.map_id :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
(E : IntermediateField K L), IntermediateField.map (AlgHom.id K L) E = E
The theorem `IntermediateField.map_id` states that for any fields `K` and `L` with a given algebra structure between them, if `E` is an intermediate field between `K` and `L`, then mapping `E` along the identity map leaves `E` unchanged. In other words, using the identity algebra homomorphism (which is essentially a function that preserves the algebra structure) to map the elements of `E` does not alter the intermediate field `E` itself.
More concisely: For any fields K, L with an algebra structure between them and an intermediate field E, the identity map from E to itself is an algebra homomorphism.
|
mem_galBasis_iff
theorem mem_galBasis_iff :
∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (U : Set (L ≃ₐ[K] L)),
U ∈ galBasis K L ↔ U ∈ (fun g => g.carrier) '' fixedByFinite K L
The theorem `mem_galBasis_iff` states that for a given field extension `L/K`, a subset `U` of the algebraic automorphisms of `L` that fix `K` is a member of the Galois group basis associated with `L/K` if and only if `U` is the underlying set of the Galois group of `L/E` for some finite subextension `E/K`. Here, `galBasis K L` represents the filter basis on the algebraic automorphisms of `L` that fix `K`, created using Galois groups of finite subextensions, and `fixedByFinite K L` represents the set of these Galois groups.
More concisely: A subset of algebraic automorphisms of a field extension fixing a base field is a Galois group basis if and only if it is the set of Galois groups of some finite subextensions.
|
IntermediateField.finiteDimensional_bot
theorem IntermediateField.finiteDimensional_bot :
∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L],
FiniteDimensional K ↥⊥
This theorem states that for any field extension `L/K`, the intermediate field `K` is finite-dimensional over `K`. A field extension is a pair of fields such that the operations of the smaller field `K` are those of the larger field `L` restricted to `K`. Finite-dimensional fields are those which have a finite number of dimensions when considered as a vector space over their field of scalars. In this case, the theorem asserts that the intermediate field between `L` and `K` (which is `K` itself, represented by `↥⊥`) is finite-dimensional as a vector space over `K`.
More concisely: For any field extension L/K, the intermediate field K has finite dimension over K as a vector space.
|
IntermediateField.fixingSubgroup.antimono
theorem IntermediateField.fixingSubgroup.antimono :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
{E1 E2 : IntermediateField K L}, E1 ≤ E2 → E2.fixingSubgroup ≤ E1.fixingSubgroup
This theorem states that the map `E ↦ Gal(L/E)`, which takes an intermediate field `E` of a field extension `L/K` to the Galois group of `L` over `E`, is inclusion-reversing. In other words, if `E1` and `E2` are intermediate fields of `L/K` such that `E1` is a subset of `E2`, then the subgroup of the Galois group that fixes `E2` is a subset of the subgroup of the Galois group that fixes `E1`. This means that a larger intermediate field corresponds to a smaller fixing subgroup in the Galois group.
More concisely: The Galois group homomorphism from intermediate fields of a field extension to their corresponding subgroups of the Galois group is inclusion-reversing.
|
krullTopology_t2
theorem krullTopology_t2 :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L],
Algebra.IsIntegral K L → T2Space (L ≃ₐ[K] L)
The theorem `krullTopology_t2` asserts that for any two types `K` and `L`, which are fields, if `L` is an algebra over `K` and every element of the algebra `L` is integral over `K` (i.e., `L/K` is an algebraic extension), then the Krull topology on the set of K-algebra isomorphisms from `L` to `L` is a Hausdorff space. In other words, if `L/K` is an algebraic extension, then in the Krull topology, any two distinct points (i.e., K-algebra isomorphisms) can be separated by open sets.
More concisely: If `L` is a field algebraically extended by `K`, then the Krull topology on the set of `K`-algebra isomorphisms from `L` to `L` is a Hausdorff space.
|
IntermediateField.fixingSubgroup.bot
theorem IntermediateField.fixingSubgroup.bot :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L], ⊥.fixingSubgroup = ⊤
This theorem states that for any two types `K` and `L`, where `K` and `L` are fields and `L` is an algebra over `K`, the subgroup that fixes the bottom element of `L` (denoted by `⊥`) under the algebra action is actually the top element of the subgroup lattice (denoted by `⊤`). In other words, every element of the group fixes the bottom element. This is a statement in Galois theory, where `Gal(L/K)` refers to the Galois group of the field extension `L` over `K`, and `L ≃ₐ[K] L` refers to the set of K-algebra isomorphisms from `L` to `L`.
More concisely: For any field extension L of a field K, the subgroup of Gal(L/K) stabilizing the bottom element of L is the identity subgroup.
|