# Galois Extensions #

In this file we define Galois extensions as extensions which are both separable and normal.

## Main definitions #

- `IsGalois F E` where `E` is an extension of `F`
- `fixedField H` where `H : Subgroup Gal(E/F)`
- `fixingSubgroup K` where `K : IntermediateField F E`
- `intermediateFieldEquivSubgroup` where `E/F` is finite dimensional and Galois

## Main results #

- `IntermediateField.fixingSubgroup_fixedField` : If `E/F` is finite dimensional (but not necessarily Galois) then `fixingSubgroup (fixedField H) = H`
- `IsGalois.fixedField_fixingSubgroup`: If `E/F` is finite dimensional and Galois then `fixedField (fixingSubgroup K) = K`

Together, these two results prove the Galois correspondence.

- `IsGalois.tfae` : Equivalent characterizations of a Galois extension of finite degree

## Additional results #

- Instances for `Algebra.IsQuadraticExtension`: a quadratic extension is Galois (if separable) with cyclic and thus abelian Galois group.

source
class IsGalois (F : Type u_1) [Field F] (E : Type u_2) [Field E] [Algebra F E] :
Prop

A field extension E/F is Galois if it is both separable and normal. Note that in mathlib a separable extension of fields is by definition algebraic.

- to_isSeparable : Algebra.IsSeparable F E
- to_normal : Normal F E

Instances

source
theorem isGalois_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
IsGalois F E ↔ Algebra.IsSeparable F E ∧ Normal F E
source
instance IsGalois.self (F : Type u_1) [Field F] :
IsGalois F F
source
theorem IsGalois.integral (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] [IsGalois F E] (x : E) :
IsIntegral F x
source
theorem IsGalois.separable (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] [IsGalois F E] (x : E) :
IsSeparable F x
source
theorem IsGalois.splits (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] [IsGalois F E] (x : E) :
Polynomial.Splits (algebraMap F E) (minpoly F x)
source
instance IsGalois.of_fixed_field (E : Type u_2) [Field E] (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G E] :
IsGalois (↥(FixedPoints.subfield G E)) E

Let $E$ be a field. Let $G$ be a finite group acting on $E$. Then the extension $E / E^G$ is Galois.

source
theorem IsGalois.IntermediateField.AdjoinSimple.card_aut_eq_finrank (F : Type u_1) [Field F] (E : Type u_2) [Field E] [Algebra F E] [FiniteDimensional F E] {α : E} (hα : IsIntegral F α) (h_sep : IsSeparable F α) (h_splits : Polynomial.Splits (algebraMap F ↥F⟮α⟯) (minpoly F α)) :
Nat.card Gal(↥F⟮α⟯/F) = Module.finrank F ↥F⟮α⟯
source
theorem IsGalois.card_aut_eq_finrank (F : Type u_1) [Field F] (E : Type u_2) [Field E] [Algebra F E] [FiniteDimensional F E] [IsGalois F E] :
Nat.card Gal(E/F) = Module.finrank F E

Let $E / F$ be a finite extension of fields. If $E$ is Galois over $F$, then $|\text{Aut}(E/F)| = [E : F]$.

source
theorem IsGalois.finiteDimensional_of_finite (F : Type u_1) [Field F] (E : Type u_2) [Field E] [Algebra F E] [IsGalois F E] [Finite Gal(E/F)] :
FiniteDimensional F E

A galois extension with finite galois group is finite dimensional. The dimension is then equal to the order of the galois group via `IsGalois.card_aut_eq_finrank`.

source
theorem IsGalois.tower_top_of_isGalois (F : Type u_1) (K : Type u_2) (E : Type u_3) [Field F] [Field K] [Field E] [Algebra F K] [Algebra F E] [Algebra K E] [IsScalarTower F K E] [IsGalois F E] :
IsGalois K E

Let $E / K / F$ be a tower of field extensions. If $E$ is Galois over $F$, then $E$ is Galois over $K$.

source
@[instance 100]
instance IsGalois.tower_top_intermediateField {F : Type u_1} {E : Type u_3} [Field F] [Field E] [Algebra F E] (K : IntermediateField F E) [IsGalois F E] :
IsGalois (↥K) E
source
theorem isGalois_iff_isGalois_bot {F : Type u_1} {E : Type u_3} [Field F] [Field E] [Algebra F E] :
IsGalois (↥⊥) E ↔ IsGalois F E
source
theorem IsGalois.of_algEquiv {F : Type u_1} {E : Type u_3} [Field F] [Field E] {E' : Type u_4} [Field E'] [Algebra F E'] [Algebra F E] [IsGalois F E] (f : E ≃ₐ[F] E') :
IsGalois F E'
source
theorem AlgEquiv.transfer_galois {F : Type u_1} {E : Type u_3} [Field F] [Field E] {E' : Type u_4} [Field E'] [Algebra F E'] [Algebra F E] (f : E ≃ₐ[F] E') :
IsGalois F E ↔ IsGalois F E'
source
theorem isGalois_iff_isGalois_top {F : Type u_1} {E : Type u_3} [Field F] [Field E] [Algebra F E] :
IsGalois F ↥⊤ ↔ IsGalois F E
source
instance isGalois_bot {F : Type u_1} {E : Type u_3} [Field F] [Field E] [Algebra F E] :
IsGalois F ↥⊥
source
theorem IsGalois.of_equiv_equiv {F : Type u_1} {E : Type u_3} [Field F] [Field E] [Algebra F E] {M : Type u_5} {N : Type u_6} [Field N] [Field M] [Algebra M N] [Algebra.IsAlgebraic F E] [h : IsGalois F E] {f : F ≃+* M} {g : E ≃+* N} (hcomp : (algebraMap M N).comp ↑f = (↑g).comp (algebraMap F E)) :
IsGalois M N
source
def FixedPoints.intermediateField {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (M : Type u_3) [Monoid M] [MulSemiringAction M E] [SMulCommClass M F E] :
IntermediateField F E

The intermediate field of fixed points fixed by a monoid action that commutes with the `F`-action on `E`.

Equations

- FixedPoints.intermediateField M = { carrier := MulAction.fixedPoints M E, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯, inv_mem' := ⋯ }

Instances For

source
@[simp]
theorem FixedPoints.mem_intermediateField_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {M : Type u_3} [Monoid M] [MulSemiringAction M E] [SMulCommClass M F E] {x : E} :
x ∈ intermediateField M ↔ ∀ (m : M), m • x = x
source
def IntermediateField.fixedField {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (H : Subgroup Gal(E/F)) :
IntermediateField F E

The intermediate field fixed by a subgroup.

Equations

- IntermediateField.fixedField H = FixedPoints.intermediateField ↥H

Instances For

source
@[simp]
theorem IntermediateField.mem_fixedField_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (H : Subgroup Gal(E/F)) (x : E) :
x ∈ fixedField H ↔ ∀ f ∈ H, f x = x
source
@[simp]
theorem IntermediateField.fixedField_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
fixedField ⊥ = ⊤
source
theorem IntermediateField.finrank_fixedField_eq_card {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (H : Subgroup Gal(E/F)) [FiniteDimensional F E] :
Module.finrank (↥(fixedField H)) E = Nat.card ↥H
source
def IntermediateField.fixingSubgroup {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) :
Subgroup Gal(E/F)

The subgroup fixing an intermediate field.

Equations

- K.fixingSubgroup = fixingSubgroup Gal(E/F) ↑K

Instances For

source
theorem IntermediateField.le_iff_le {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (H : Subgroup Gal(E/F)) (K : IntermediateField F E) :
K ≤ fixedField H ↔ H ≤ K.fixingSubgroup
source
theorem IntermediateField.fixingSubgroup_le {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K1 K2 : IntermediateField F E} (h12 : K1 ≤ K2) :
K2.fixingSubgroup ≤ K1.fixingSubgroup

The map `K ↦ Gal(E/K)` is inclusion-reversing.

source
@[deprecated IntermediateField.fixingSubgroup_le (since := "2025-05-02")]
theorem IntermediateField.fixingSubgroup.antimono {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K1 K2 : IntermediateField F E} (h12 : K1 ≤ K2) :
K2.fixingSubgroup ≤ K1.fixingSubgroup

Alias of `IntermediateField.fixingSubgroup_le`.

The map `K ↦ Gal(E/K)` is inclusion-reversing.

source
theorem IntermediateField.fixedField_le {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {H1 H2 : Subgroup Gal(E/F)} (h12 : H1 ≤ H2) :
fixedField H2 ≤ fixedField H1
source
theorem IntermediateField.fixingSubgroup_antitone {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
Antitone fixingSubgroup
source
@[deprecated IntermediateField.fixingSubgroup_antitone (since := "2025-05-02")]
theorem IntermediateField.fixingSubgroup_anti {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
Antitone fixingSubgroup

Alias of `IntermediateField.fixingSubgroup_antitone`.

source
theorem IntermediateField.fixedField_antitone {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
Antitone fixedField
source
@[simp]
theorem IntermediateField.mem_fixingSubgroup_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) (σ : Gal(E/F)) :
σ ∈ K.fixingSubgroup ↔ ∀ x ∈ K, σ x = x
source
@[simp]
theorem IntermediateField.fixingSubgroup_top {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
⊤.fixingSubgroup = ⊥
source
@[simp]
theorem IntermediateField.fixingSubgroup_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
⊥.fixingSubgroup = ⊤
source
theorem IntermediateField.fixingSubgroup_sup {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K L : IntermediateField F E} :
(K ⊔ L).fixingSubgroup = K.fixingSubgroup ⊓ L.fixingSubgroup
source
def IntermediateField.fixingSubgroupEquiv {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) :
↥K.fixingSubgroup ≃* Gal(E/↥K)

The fixing subgroup of `K : IntermediateField F E` is isomorphic to `Gal(E/K)`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem IntermediateField.fixingSubgroup_fixedField {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (H : Subgroup Gal(E/F)) [FiniteDimensional F E] :
(fixedField H).fixingSubgroup = H
source
def IntermediateField.subgroupEquivAlgEquiv {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [FiniteDimensional F E] (H : Subgroup Gal(E/F)) :
↥H ≃* Gal(E/↥(fixedField H))

A subgroup is isomorphic to the Galois group of its fixed field.

Equations

- IntermediateField.subgroupEquivAlgEquiv H = (MulEquiv.subgroupCongr ⋯).trans (IntermediateField.fixedField H).fixingSubgroupEquiv

Instances For

source
instance IntermediateField.fixedField.smul {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) :
SMul ↥K ↥(fixedField K.fixingSubgroup)
Equations

- IntermediateField.fixedField.smul K = { smul := fun (x : ↥K) (y : ↥(IntermediateField.fixedField K.fixingSubgroup)) => ⟨↑x * ↑y, ⋯⟩ }

source
instance IntermediateField.fixedField.algebra {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) :
Algebra ↥K ↥(fixedField K.fixingSubgroup)
Equations

- One or more equations did not get rendered due to their size.

source
instance IntermediateField.fixedField.isScalarTower {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) :
IsScalarTower (↥K) (↥(fixedField K.fixingSubgroup)) E
source
theorem IsGalois.fixedField_fixingSubgroup {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) [FiniteDimensional F E] [h : IsGalois F E] :
IntermediateField.fixedField K.fixingSubgroup = K
source
@[simp]
theorem IsGalois.fixedField_top {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [IsGalois F E] [FiniteDimensional F E] :
IntermediateField.fixedField ⊤ = ⊥
source
theorem IsGalois.mem_bot_iff_fixed {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [IsGalois F E] [FiniteDimensional F E] (x : E) :
x ∈ ⊥ ↔ ∀ (f : Gal(E/F)), f x = x
source
theorem IsGalois.mem_range_algebraMap_iff_fixed {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [IsGalois F E] [FiniteDimensional F E] (x : E) :
x ∈ Set.range ⇑(algebraMap F E) ↔ ∀ (f : Gal(E/F)), f x = x
source
theorem IsGalois.card_fixingSubgroup_eq_finrank {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) [FiniteDimensional F E] [IsGalois F E] :
Nat.card ↥K.fixingSubgroup = Module.finrank (↥K) E
source
def IsGalois.intermediateFieldEquivSubgroup {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [FiniteDimensional F E] [IsGalois F E] :
IntermediateField F E ≃o (Subgroup Gal(E/F))ᵒᵈ

The Galois correspondence from intermediate fields to subgroups.

Equations

- IsGalois.intermediateFieldEquivSubgroup = { toFun := IntermediateField.fixingSubgroup, invFun := IntermediateField.fixedField, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

Instances For

source
def IsGalois.galoisInsertionIntermediateFieldSubgroup {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [FiniteDimensional F E] :
GaloisInsertion (⇑OrderDual.toDual ∘ IntermediateField.fixingSubgroup) (IntermediateField.fixedField ∘ ⇑OrderDual.toDual)

The Galois correspondence as a `GaloisInsertion`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def IsGalois.galoisCoinsertionIntermediateFieldSubgroup {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [FiniteDimensional F E] [IsGalois F E] :
GaloisCoinsertion (⇑OrderDual.toDual ∘ IntermediateField.fixingSubgroup) (IntermediateField.fixedField ∘ ⇑OrderDual.toDual)

The Galois correspondence as a `GaloisCoinsertion`.

Equations

- IsGalois.galoisCoinsertionIntermediateFieldSubgroup = IsGalois.intermediateFieldEquivSubgroup.toGaloisCoinsertion

Instances For

source
theorem IntermediateField.restrictNormalHom_ker {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E : IntermediateField K L) [Normal K ↥E] :
(AlgEquiv.restrictNormalHom ↥E).ker = E.fixingSubgroup
source
instance IsGalois.of_fixedField_normal_subgroup {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] [IsGalois K L] (H : Subgroup Gal(L/K)) [hn : H.Normal] :
IsGalois K ↥(IntermediateField.fixedField H)

If `H` is a normal Subgroup of `Gal(L / K)`, then `fixedField H` is Galois over `K`.

source
noncomputable def IsGalois.normalAutEquivQuotient {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (H : Subgroup Gal(L/K)) [H.Normal] :
Gal(L/K) ⧸ H ≃* Gal(↥(IntermediateField.fixedField H)/K)

If `H` is a normal Subgroup of `Gal(L / K)`, then `Gal(fixedField H / K)` is isomorphic to `Gal(L / K) ⧸ H`.

Equations

- IsGalois.normalAutEquivQuotient H = (QuotientGroup.quotientMulEquivOfEq ⋯).trans (QuotientGroup.quotientKerEquivOfSurjective (AlgEquiv.restrictNormalHom ↥(IntermediateField.fixedField H)) ⋯)

Instances For

source
theorem IsGalois.normalAutEquivQuotient_apply {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (H : Subgroup Gal(L/K)) [H.Normal] (σ : Gal(L/K)) :
(normalAutEquivQuotient H) ↑σ = (AlgEquiv.restrictNormalHom ↥(IntermediateField.fixedField H)) σ
source
@[simp]
theorem IsGalois.map_fixingSubgroup {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E : IntermediateField K L) (σ : Gal(L/K)) :
(IntermediateField.map (↑σ) E).fixingSubgroup = MulAut.conj σ • E.fixingSubgroup
source
instance IsGalois.fixingSubgroup_normal_of_isGalois {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E : IntermediateField K L) [IsGalois K L] [IsGalois K ↥E] :
E.fixingSubgroup.Normal

Let `E` be an intermediateField of a Galois extension `L / K`. If `E / K` is Galois extension, then `E.fixingSubgroup` is a normal subgroup of `Gal(L / K)`.

source
theorem IsGalois.is_separable_splitting_field (F : Type u_1) [Field F] (E : Type u_2) [Field E] [Algebra F E] [FiniteDimensional F E] [IsGalois F E] :
∃ (p : Polynomial F), p.Separable ∧ Polynomial.IsSplittingField F E p
source
theorem IsGalois.of_fixedField_eq_bot (F : Type u_1) [Field F] (E : Type u_2) [Field E] [Algebra F E] [FiniteDimensional F E] (h : IntermediateField.fixedField ⊤ = ⊥) :
IsGalois F E
source
theorem IsGalois.of_card_aut_eq_finrank (F : Type u_1) [Field F] (E : Type u_2) [Field E] [Algebra F E] [FiniteDimensional F E] (h : Nat.card Gal(E/F) = Module.finrank F E) :
IsGalois F E

Let $E / F$ be a finite extension of fields. If $|\text{Aut}(E/F)| = [E : F]$, then $E$ is Galois over $F$.

source
theorem IsGalois.of_separable_splitting_field_aux {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {p : Polynomial F} [hFE : FiniteDimensional F E] [sp : Polynomial.IsSplittingField F E p] (hp : p.Separable) (K : Type u_3) [Field K] [Algebra F K] [Algebra K E] [IsScalarTower F K E] {x : E} (hx : x ∈ p.aroots E) :
Nat.card (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) = Nat.card (K →ₐ[F] E) * Module.finrank K ↥K⟮x⟯
source
theorem IsGalois.of_separable_splitting_field {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {p : Polynomial F} [sp : Polynomial.IsSplittingField F E p] (hp : p.Separable) :
IsGalois F E
source
theorem IsGalois.tfae {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [FiniteDimensional F E] :
[IsGalois F E, IntermediateField.fixedField ⊤ = ⊥, Nat.card Gal(E/F) = Module.finrank F E, ∃ (p : Polynomial F), p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE

Equivalent characterizations of a Galois extension of finite degree.

source
theorem IsGalois.sup_right {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K L : IntermediateField F E) [IsGalois F ↥K] [FiniteDimensional F ↥K] (h : K ⊔ L = ⊤) :
IsGalois (↥L) E

If `K/F` is a finite Galois extension, then for any extension `L/F`, the extension `KL/L` is also Galois.

source
instance IsGalois.normalClosure (k : Type u_1) (K : Type u_2) (F : Type u_3) [Field k] [Field K] [Field F] [Algebra k K] [Algebra k F] [IsGalois k F] :
IsGalois k ↥(IntermediateField.normalClosure k K F)

Let $F / K / k$ be a tower of field extensions. If $F$ is Galois over $k$, then the normal closure of $K$ over $k$ in $F$ is Galois over $k$.

source
@[instance 100]
instance IsAlgClosure.isGalois (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [IsAlgClosure k K] [CharZero k] :
IsGalois k K
source
noncomputable def IntermediateField.restrictRestrictAlgEquivMapHom (F : Type u_1) (K : Type u_2) (L : Type u_3) (E : Type u_4) [Field F] [Field K] [Field L] [Field E] [Algebra F K] [Algebra F L] [Algebra F E] [Algebra K E] [Algebra L E] [IsScalarTower F K E] [IsScalarTower F L E] [Normal F K] :
Gal(E/L) →* Gal(K/F)

The map from the `Gal(E/L)` to `Gal(K/F)` where `E/L/F` and `E/K/F` are two towers of extensions induced by the restriction to `K`. Note that we do require `K/F` to be normal but not `E/L`. If this is the case (and everything is finite dimensional) and `K ∩ L = F` then this map is surjective, see `IntermediateField.restrictRestrictMapHom_surjective`. This map is injective if the compositum of `K` and `L` is `E`, see `IntermediateField.restrictRestrictAlgEquivMapHom_injective`.

Equations

- IntermediateField.restrictRestrictAlgEquivMapHom F K L E = (AlgEquiv.restrictNormalHom K).comp (MulSemiringAction.toAlgAut Gal(E/L) F E)

Instances For

source
@[simp]
theorem IntermediateField.restrictRestrictAlgEquivMapHom_apply {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] (K L : IntermediateField F E) [Normal F ↥K] (φ : Gal(E/↥L)) (x : ↥K) :
↑(((restrictRestrictAlgEquivMapHom F (↥K) (↥L) E) φ) x) = φ ↑x
source
theorem IntermediateField.restrictRestrictAlgEquivMapHom_injective {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] (K L : IntermediateField F E) [Normal F ↥K] (h : K ⊔ L = ⊤) :
Function.Injective ⇑(restrictRestrictAlgEquivMapHom F (↥K) (↥L) E)
source
theorem IntermediateField.restrictRestrictAlgEquivMapHom_surjective {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] (K L : IntermediateField F E) [Normal F ↥K] [FiniteDimensional F ↥K] [FiniteDimensional (↥L) E] [IsGalois (↥L) E] (h : K ⊓ L = ⊥) :
Function.Surjective ⇑(restrictRestrictAlgEquivMapHom F (↥K) (↥L) E)
source
instance Algebra.IsQuadraticExtension.isGalois (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [IsQuadraticExtension F K] [Algebra.IsSeparable F K] :
IsGalois F K

A quadratic separable extension is Galois.

source
instance Algebra.IsQuadraticExtension.isCyclic (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [IsQuadraticExtension F K] :
IsCyclic Gal(K/F)

A quadratic extension has cyclic Galois group.

source
instance Algebra.IsQuadraticExtension.isMulCommutative_galoisGroup (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [IsQuadraticExtension F K] :
IsMulCommutative Gal(K/F)

A quadratic extension has abelian Galois group.