Mathlib.FieldTheory.Galois.Basic

IsGalois structure

Full source

/-- 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. -/
@[stacks 09I0]
class IsGalois : Prop where
  [to_isSeparable : Algebra.IsSeparable F E]
  [to_normal : Normal F E]

Galois extension

Informal description

A field extension $ E/F $ is called a Galois extension if it is both separable and normal. Here, a separable extension is by definition algebraic.

isGalois_iff theorem

: IsGalois F E ↔ Algebra.IsSeparable F E ∧ Normal F E

Full source

theorem isGalois_iff : IsGaloisIsGalois F E ↔ Algebra.IsSeparable F E ∧ Normal F E :=
  ⟨fun h => ⟨h.1, h.2⟩, fun h =>
    { to_isSeparable := h.1
      to_normal := h.2 }⟩

Characterization of Galois Extensions: Separable and Normal

Informal description

A field extension $E/F$ is Galois if and only if it is both separable and normal.

IsGalois.self instance

: IsGalois F F

Full source

instance self : IsGalois F F :=
  ⟨⟩

Trivial Galois Extension

Informal description

For any field $F$, the extension $F/F$ is a Galois extension.

IsGalois.integral theorem

[IsGalois F E] (x : E) : IsIntegral F x

Full source

theorem integral [IsGalois F E] (x : E) : IsIntegral F x :=
  to_normal.isIntegral x

Integrality of Elements in Galois Extensions

Informal description

For any Galois extension $E/F$ and any element $x \in E$, the element $x$ is integral over $F$.

IsGalois.separable theorem

[IsGalois F E] (x : E) : IsSeparable F x

Full source

theorem separable [IsGalois F E] (x : E) : IsSeparable F x :=
  Algebra.IsSeparable.isSeparable F x

Separability in Galois Extensions

Informal description

For any field extension $ E/F $ that is Galois and any element $ x \in E $, the minimal polynomial of $ x $ over $ F $ is separable.

IsGalois.splits theorem

[IsGalois F E] (x : E) : (minpoly F x).Splits (algebraMap F E)

Full source

theorem splits [IsGalois F E] (x : E) : (minpoly F x).Splits (algebraMap F E) :=
  Normal.splits' x

Splitting of Minimal Polynomials in Galois Extensions

Informal description

For any Galois extension $E/F$ and any element $x \in E$, the minimal polynomial of $x$ over $F$ splits completely in $E$ via the algebra map $F \to E$.

IsGalois.of_fixed_field instance

(G : Type*) [Group G] [Finite G] [MulSemiringAction G E] : IsGalois (FixedPoints.subfield G E) E

Full source

/-- Let $E$ be a field. Let $G$ be a finite group acting on $E$.
Then the extension $E / E^G$ is Galois. -/
@[stacks 09I3 "first part"]
instance of_fixed_field (G : Type*) [Group G] [Finite G] [MulSemiringAction G E] :
    IsGalois (FixedPoints.subfield G E) E :=
  ⟨⟩

Galois Extension from Fixed Field of Finite Group Action

Informal description

Let $E$ be a field and $G$ be a finite group acting on $E$ via ring automorphisms. Then the field extension $E / E^G$ is Galois, where $E^G$ denotes the fixed field of $G$.

IsGalois.IntermediateField.AdjoinSimple.card_aut_eq_finrank theorem

 [FiniteDimensional F E] {α : E} (hα : IsIntegral F α) (h_sep : IsSeparable F α)
  (h_splits : (minpoly F α).Splits (algebraMap F F⟮α⟯)) : Fintype.card (F⟮α⟯ ≃ₐ[F] F⟮α⟯) = finrank F F⟮α⟯

Full source

theorem IntermediateField.AdjoinSimple.card_aut_eq_finrank [FiniteDimensional F E] {α : E}
    (hα : IsIntegral F α) (h_sep : IsSeparable F α)
    (h_splits : (minpoly F α).Splits (algebraMap F F⟮α⟯)) :
    Fintype.card (F⟮α⟯F⟮α⟯ ≃ₐ[F] F⟮α⟯) = finrank F F⟮α⟯ := by
  letI : Fintype (F⟮α⟯F⟮α⟯ →ₐ[F] F⟮α⟯) := IntermediateField.fintypeOfAlgHomAdjoinIntegral F hα
  rw [IntermediateField.adjoin.finrank hα]
  rw [← IntermediateField.card_algHom_adjoin_integral F hα h_sep h_splits]
  exact Fintype.card_congr (algEquivEquivAlgHom F F⟮α⟯)

Number of Automorphisms Equals Degree for Simple Algebraic Extensions

Informal description

Let $E/F$ be a finite-dimensional field extension and $\alpha \in E$ an element that is integral and separable over $F$. If the minimal polynomial of $\alpha$ over $F$ splits completely in the extension $F(\alpha)$, then the number of $F$-algebra automorphisms of $F(\alpha)$ equals the degree of the field extension $[F(\alpha) : F]$, i.e., \[ |\text{Aut}(F(\alpha)/F)| = [F(\alpha) : F]. \]

IsGalois.card_aut_eq_finrank theorem

[FiniteDimensional F E] [IsGalois F E] : Fintype.card (E ≃ₐ[F] E) = finrank F E

Full source

/-- Let $E / F$ be a finite extension of fields. If $E$ is Galois over $F$, then
$|\text{Aut}(E/F)| = [E : F]$. -/
@[stacks 09I1 "'only if' part"]
theorem card_aut_eq_finrank [FiniteDimensional F E] [IsGalois F E] :
    Fintype.card (E ≃ₐ[F] E) = finrank F E := by
  obtain ⟨α, hα⟩ := Field.exists_primitive_element F E
  let iso : F⟮α⟯F⟮α⟯ ≃ₐ[F] E :=
    { toFun := fun e => e.val
      invFun := fun e => ⟨e, by rw [hα]; exact IntermediateField.mem_top⟩
      left_inv := fun _ => by ext; rfl
      right_inv := fun _ => rfl
      map_mul' := fun _ _ => rfl
      map_add' := fun _ _ => rfl
      commutes' := fun _ => rfl }
  have H : IsIntegral F α := IsGalois.integral F α
  have h_sep : IsSeparable F α := IsGalois.separable F α
  have h_splits : (minpoly F α).Splits (algebraMap F E) := IsGalois.splits F α
  replace h_splits : Polynomial.Splits (algebraMap F F⟮α⟯) (minpoly F α) := by
    simpa using
      Polynomial.splits_comp_of_splits (algebraMap F E) iso.symm.toAlgHom.toRingHom h_splits
  rw [← LinearEquiv.finrank_eq iso.toLinearEquiv]
  rw [← IntermediateField.AdjoinSimple.card_aut_eq_finrank F E H h_sep h_splits]
  apply Fintype.card_congr
  apply Equiv.mk (fun ϕ => iso.trans (ϕ.trans iso.symm)) fun ϕ => iso.symm.trans (ϕ.trans iso)
  · intro ϕ; ext1; simp only [trans_apply, apply_symm_apply]
  · intro ϕ; ext1; simp only [trans_apply, symm_apply_apply]

Galois Extension Automorphism Count: $|\text{Aut}(E/F)| = [E : F]$

Informal description

Let $E/F$ be a finite-dimensional Galois extension of fields. Then the number of $F$-algebra automorphisms of $E$ equals the degree of the field extension, i.e., \[ |\text{Aut}(E/F)| = [E : F]. \]

IsGalois.tower_top_of_isGalois theorem

[IsGalois F E] : IsGalois K E

Full source

/-- Let $E / K / F$ be a tower of field extensions.
If $E$ is Galois over $F$, then $E$ is Galois over $K$. -/
@[stacks 09I2]
theorem IsGalois.tower_top_of_isGalois [IsGalois F E] : IsGalois K E :=
  { to_isSeparable := Algebra.isSeparable_tower_top_of_isSeparable F K E
    to_normal := Normal.tower_top_of_normal F K E }

Galois Extensions in Tower: $E/K$ is Galois when $E/F$ is Galois

Informal description

Let $F \subseteq K \subseteq E$ be a tower of field extensions. If $E/F$ is a Galois extension, then $E/K$ is also a Galois extension.

IsGalois.tower_top_intermediateField instance

(K : IntermediateField F E) [IsGalois F E] : IsGalois K E

Full source

instance (priority := 100) IsGalois.tower_top_intermediateField (K : IntermediateField F E)
    [IsGalois F E] : IsGalois K E :=
  IsGalois.tower_top_of_isGalois F K E

Galois Property Preserved Under Intermediate Field Extensions

Informal description

For any intermediate field $K$ in a Galois extension $E/F$, the extension $E/K$ is also Galois.

isGalois_iff_isGalois_bot theorem

: IsGalois (⊥ : IntermediateField F E) E ↔ IsGalois F E

Full source

theorem isGalois_iff_isGalois_bot : IsGaloisIsGalois (⊥ : IntermediateField F E) E ↔ IsGalois F E := by
  constructor
  · intro h
    exact IsGalois.tower_top_of_isGalois (⊥ : IntermediateField F E) F E
  · intro h; infer_instance

Galois Extension Equivalence via Bottom Intermediate Field

Informal description

For a field extension $E/F$, the extension $E/F$ is Galois if and only if the extension $E/\bot$ is Galois, where $\bot$ denotes the smallest intermediate field between $F$ and $E$.

IsGalois.of_algEquiv theorem

[IsGalois F E] (f : E ≃ₐ[F] E') : IsGalois F E'

Full source

theorem IsGalois.of_algEquiv [IsGalois F E] (f : E ≃ₐ[F] E') : IsGalois F E' :=
  { to_isSeparable := Algebra.IsSeparable.of_algHom F E f.symm
    to_normal := Normal.of_algEquiv f }

Galois extension is preserved under algebra isomorphism

Informal description

Let $E/F$ be a Galois extension and $f \colon E \to E'$ be an $F$-algebra isomorphism. Then $E'/F$ is also a Galois extension.

AlgEquiv.transfer_galois theorem

(f : E ≃ₐ[F] E') : IsGalois F E ↔ IsGalois F E'

Full source

theorem AlgEquiv.transfer_galois (f : E ≃ₐ[F] E') : IsGaloisIsGalois F E ↔ IsGalois F E' :=
  ⟨fun _ => IsGalois.of_algEquiv f, fun _ => IsGalois.of_algEquiv f.symm⟩

Galois Extension Invariance under Algebra Isomorphism

Informal description

Given an $F$-algebra isomorphism $f \colon E \to E'$, the extension $E/F$ is Galois if and only if $E'/F$ is Galois.

isGalois_iff_isGalois_top theorem

: IsGalois F (⊤ : IntermediateField F E) ↔ IsGalois F E

Full source

theorem isGalois_iff_isGalois_top : IsGaloisIsGalois F (⊤ : IntermediateField F E) ↔ IsGalois F E :=
  (IntermediateField.topEquiv : (⊤ : IntermediateField F E) ≃ₐ[F] E).transfer_galois

Galois Extension Criterion via Top Intermediate Field: $E/F$ Galois $\leftrightarrow$ $\top/F$ Galois

Informal description

The extension $E/F$ is Galois if and only if the top intermediate field $\top$ (which is isomorphic to $E$) is a Galois extension of $F$.

isGalois_bot instance

: IsGalois F (⊥ : IntermediateField F E)

Full source

instance isGalois_bot : IsGalois F (⊥ : IntermediateField F E) :=
  (IntermediateField.botEquiv F E).transfer_galois.mpr (IsGalois.self F)

Trivial Extension is Galois

Informal description

The trivial extension $F/F$ is a Galois extension, where $F$ is viewed as the bottom intermediate field $\bot$ in any field extension $E/F$.

FixedPoints.intermediateField definition

(M : Type*) [Monoid M] [MulSemiringAction M E] [SMulCommClass M F E] : IntermediateField F E

Full source

/-- The intermediate field of fixed points fixed by a monoid action that commutes with the
`F`-action on `E`. -/
def FixedPoints.intermediateField (M : Type*) [Monoid M] [MulSemiringAction M E]
    [SMulCommClass M F E] : IntermediateField F E :=
  { FixedPoints.subfield M E with
    carrier := MulAction.fixedPoints M E
    algebraMap_mem' := fun a g => smul_algebraMap g a }

Fixed points intermediate field under monoid action

Informal description

The intermediate field consisting of all elements in $ E $ that are fixed by every element of the monoid $ M $ under its multiplicative semiring action on $ E $, where the action of $ M $ commutes with the $ F $-action on $ E $.

IntermediateField.fixedField definition

: IntermediateField F E

Full source

/-- The intermediate field fixed by a subgroup -/
def fixedField : IntermediateField F E :=
  FixedPoints.intermediateField H

Fixed field of a Galois subgroup

Informal description

The intermediate field consisting of all elements in $ E $ that are fixed by every automorphism in the subgroup $ H $ of the Galois group $ \text{Aut}(E/F) $. That is, an element $ x \in E $ belongs to the fixed field of $ H $ if and only if $ f(x) = x $ for every $ f \in H $.

IntermediateField.mem_fixedField_iff theorem

(x) : x ∈ fixedField H ↔ ∀ f ∈ H, f x = x

Full source

theorem mem_fixedField_iff (x) :
    x ∈ fixedField Hx ∈ fixedField H ↔ ∀ f ∈ H, f x = x := by
  show x ∈ MulAction.fixedPoints H Ex ∈ MulAction.fixedPoints H E ↔ _
  simp only [MulAction.mem_fixedPoints, Subtype.forall, Subgroup.mk_smul, AlgEquiv.smul_def]

Characterization of Fixed Field Elements: $x \in E^H \leftrightarrow \forall f \in H, f(x) = x$

Informal description

An element $x$ in the extension field $E$ belongs to the fixed field of the subgroup $H$ of $\text{Aut}(E/F)$ if and only if every automorphism $f$ in $H$ fixes $x$, i.e., $f(x) = x$ for all $f \in H$.

IntermediateField.finrank_fixedField_eq_card theorem

[FiniteDimensional F E] [DecidablePred (· ∈ H)] : finrank (fixedField H) E = Fintype.card H

Full source

theorem finrank_fixedField_eq_card [FiniteDimensional F E] [DecidablePred (· ∈ H)] :
    finrank (fixedField H) E = Fintype.card H :=
  FixedPoints.finrank_eq_card H E

Fixed Field Dimension Equals Subgroup Cardinality in Finite Galois Extension

Informal description

Let $E/F$ be a finite-dimensional field extension and let $H$ be a subgroup of the automorphism group $\text{Aut}(E/F)$. Then the dimension of $E$ over its fixed field $E^H$ is equal to the cardinality of $H$, i.e., $\text{dim}_{E^H}(E) = |H|$.

IntermediateField.fixingSubgroup definition

: Subgroup (E ≃ₐ[F] E)

Full source

/-- The subgroup fixing an intermediate field -/
nonrec def fixingSubgroup : Subgroup (E ≃ₐ[F] E) :=
  fixingSubgroup (E ≃ₐ[F] E) (K : Set E)

Fixing subgroup of an intermediate field

Informal description

Given an intermediate field $ K $ between fields $ F $ and $ E $, the fixing subgroup is the subgroup of $ E $-automorphisms over $ F $ (i.e., elements of $ \text{Aut}_F(E) $) that fix every element of $ K $. In other words, it consists of all automorphisms $ \sigma \in \text{Aut}_F(E) $ such that $ \sigma(x) = x $ for all $ x \in K $.

IntermediateField.le_iff_le theorem

: K ≤ fixedField H ↔ H ≤ fixingSubgroup K

Full source

theorem le_iff_le : K ≤ fixedField H ↔ H ≤ fixingSubgroup K :=
  ⟨fun h g hg x => h (Subtype.mem x) ⟨g, hg⟩, fun h x hx g => h (Subtype.mem g) ⟨x, hx⟩⟩

Galois Correspondence: Intermediate Field Inclusion vs. Subgroup Inclusion

Informal description

For an intermediate field $ K $ between fields $ F $ and $ E $, and a subgroup $ H $ of the automorphism group $\text{Aut}(E/F)$, the following are equivalent: 1. $ K $ is contained in the fixed field of $ H $, i.e., $ K \subseteq E^H $. 2. $ H $ is contained in the fixing subgroup of $ K $, i.e., $ H \leq \text{Aut}(E/K) $.

IntermediateField.fixingSubgroup_anti theorem

: Antitone (IntermediateField.fixingSubgroup (F := F) (E := E))

Full source

lemma fixingSubgroup_anti : Antitone (IntermediateField.fixingSubgroup (F := F) (E := E)) := by
  intro K K' h
  rw [← le_iff_le]
  exact le_trans h ((le_iff_le _ _).mpr (le_refl K'.fixingSubgroup))

Antitonicity of the Fixing Subgroup Map in Field Extensions

Informal description

The function that maps an intermediate field $K$ between fields $F$ and $E$ to its fixing subgroup $\text{Aut}(E/K)$ is antitone. That is, for any intermediate fields $K_1$ and $K_2$ with $K_1 \leq K_2$, we have $\text{Aut}(E/K_2) \leq \text{Aut}(E/K_1)$.

IntermediateField.fixingSubgroupEquiv definition

: fixingSubgroup K ≃* E ≃ₐ[K] E

Full source

/-- The fixing subgroup of `K : IntermediateField F E` is isomorphic to `E ≃ₐ[K] E` -/
def fixingSubgroupEquiv : fixingSubgroupfixingSubgroup K ≃* E ≃ₐ[K] E where
  toFun ϕ := { AlgEquiv.toRingEquiv (ϕ : E ≃ₐ[F] E) with commutes' := ϕ.mem }
  invFun ϕ := ⟨ϕ.restrictScalars _, ϕ.commutes⟩
  left_inv _ := by ext; rfl
  right_inv _ := by ext; rfl
  map_mul' _ _ := by ext; rfl

Isomorphism between fixing subgroup and $ K $-algebra automorphisms of $ E $

Informal description

Given an intermediate field $ K $ between fields $ F $ and $ E $, the fixing subgroup of $ K $ (i.e., the subgroup of $ F $-algebra automorphisms of $ E $ that fix $ K $ pointwise) is multiplicatively isomorphic to the group of $ K $-algebra automorphisms of $ E $. More precisely, the isomorphism maps each automorphism $ \phi $ in the fixing subgroup to its restriction as a $ K $-algebra automorphism, and conversely, any $ K $-algebra automorphism of $ E $ can be uniquely extended to an $ F $-algebra automorphism that fixes $ K $.

IntermediateField.fixingSubgroup_fixedField theorem

[FiniteDimensional F E] : fixingSubgroup (fixedField H) = H

Full source

theorem fixingSubgroup_fixedField [FiniteDimensional F E] : fixingSubgroup (fixedField H) = H := by
  have H_le : H ≤ fixingSubgroup (fixedField H) := (le_iff_le _ _).mp le_rfl
  classical
  suffices Fintype.card H = Fintype.card (fixingSubgroup (fixedField H)) by
    exact SetLike.coe_injective (Set.eq_of_inclusion_surjective
      ((Fintype.bijective_iff_injective_and_card (Set.inclusion H_le)).mpr
        ⟨Set.inclusion_injective H_le, this⟩).2).symm
  apply Fintype.card_congr
  refine (FixedPoints.toAlgHomEquiv H E).trans ?_
  refine (algEquivEquivAlgHom (fixedField H) E).toEquiv.symm.trans ?_
  exact (fixingSubgroupEquiv (fixedField H)).toEquiv.symm

Galois Correspondence: Fixing Subgroup of Fixed Field Equals Original Subgroup

Informal description

For a finite-dimensional field extension $E$ of $F$, the fixing subgroup of the fixed field of any subgroup $H$ of $\text{Aut}(E/F)$ equals $H$ itself. In other words, if we first take the fixed field of $H$ (the elements of $E$ fixed by all automorphisms in $H$) and then take the fixing subgroup of this fixed field (the automorphisms fixing all elements of this fixed field), we recover the original subgroup $H$.

IntermediateField.fixedField.smul instance

: SMul K (fixedField (fixingSubgroup K))

Full source

instance fixedField.smul : SMul K (fixedField (fixingSubgroup K)) where
  smul x y := ⟨x * y, fun ϕ => by
    rw [smul_mul', show ϕ • (x : E) = ↑x from ϕ.2 x, show ϕ • (y : E) = ↑y from y.2 ϕ]⟩

Scalar Multiplication on the Fixed Field of the Fixing Subgroup

Informal description

For any intermediate field $K$ between fields $F$ and $E$, the fixed field of the fixing subgroup of $K$ has a scalar multiplication structure induced by $K$. That is, for any $k \in K$ and $x$ in the fixed field of the automorphisms fixing $K$, the product $k \cdot x$ is well-defined and lies in the fixed field.

IntermediateField.fixedField.algebra instance

: Algebra K (fixedField (fixingSubgroup K))

Full source

instance fixedField.algebra : Algebra K (fixedField (fixingSubgroup K)) where
  algebraMap :=
  { toFun x := ⟨x, fun ϕ => Subtype.mem ϕ x⟩
    map_zero' := rfl
    map_add' _ _ := rfl
    map_one' := rfl
    map_mul' _ _ := rfl }
  commutes' _ _ := mul_comm _ _
  smul_def' _ _ := rfl

Algebra Structure on the Fixed Field of the Fixing Subgroup

Informal description

For any intermediate field $K$ between fields $F$ and $E$, the fixed field of the fixing subgroup of $K$ has a canonical $K$-algebra structure.

IntermediateField.fixedField.isScalarTower instance

: IsScalarTower K (fixedField (fixingSubgroup K)) E

Full source

instance fixedField.isScalarTower : IsScalarTower K (fixedField (fixingSubgroup K)) E :=
  ⟨fun _ _ _ => mul_assoc _ _ _⟩

Scalar Tower Structure on Fixed Field of Fixing Subgroup

Informal description

For any intermediate field $K$ between fields $F$ and $E$, the scalar multiplication action of $K$ on $E$ restricts to the fixed field of the fixing subgroup of $K$, and this restriction forms a scalar tower structure. That is, for any $k \in K$, $x$ in the fixed field, and $y \in E$, we have $k \cdot (x \cdot y) = (k \cdot x) \cdot y$.

IsGalois.fixedField_fixingSubgroup theorem

[FiniteDimensional F E] [h : IsGalois F E] : IntermediateField.fixedField (IntermediateField.fixingSubgroup K) = K

Full source

theorem fixedField_fixingSubgroup [FiniteDimensional F E] [h : IsGalois F E] :
    IntermediateField.fixedField (IntermediateField.fixingSubgroup K) = K := by
  have K_le : K ≤ IntermediateField.fixedField (IntermediateField.fixingSubgroup K) :=
    (IntermediateField.le_iff_le _ _).mpr le_rfl
  suffices
    finrank K E = finrank (IntermediateField.fixedField (IntermediateField.fixingSubgroup K)) E by
    exact (IntermediateField.eq_of_le_of_finrank_eq' K_le this).symm
  classical
  rw [IntermediateField.finrank_fixedField_eq_card,
    Fintype.card_congr (IntermediateField.fixingSubgroupEquiv K).toEquiv]
  exact (card_aut_eq_finrank K E).symm

Galois Correspondence: Fixed Field of Fixing Subgroup Equals Original Field

Informal description

Let $E/F$ be a finite-dimensional Galois extension of fields. For any intermediate field $K$ between $F$ and $E$, the fixed field of the fixing subgroup of $K$ equals $K$ itself, i.e., \[ E^{\text{Aut}(E/K)} = K. \]

IsGalois.card_fixingSubgroup_eq_finrank theorem

 [DecidablePred (· ∈ IntermediateField.fixingSubgroup K)] [FiniteDimensional F E] [IsGalois F E] :
  Fintype.card (IntermediateField.fixingSubgroup K) = finrank K E

Full source

theorem card_fixingSubgroup_eq_finrank [DecidablePred (· ∈ IntermediateField.fixingSubgroup K)]
    [FiniteDimensional F E] [IsGalois F E] :
    Fintype.card (IntermediateField.fixingSubgroup K) = finrank K E := by
  conv_rhs => rw [← fixedField_fixingSubgroup K, IntermediateField.finrank_fixedField_eq_card]

Cardinality of Fixing Subgroup Equals Extension Dimension in Galois Extension

Informal description

Let $E/F$ be a finite-dimensional Galois extension of fields, and let $K$ be an intermediate field between $F$ and $E$. Then the cardinality of the fixing subgroup $\text{Aut}(E/K)$ is equal to the dimension of $E$ as a vector space over $K$, i.e., \[ |\text{Aut}(E/K)| = \text{dim}_K(E). \]

IsGalois.intermediateFieldEquivSubgroup definition

[FiniteDimensional F E] [IsGalois F E] : IntermediateField F E ≃o (Subgroup (E ≃ₐ[F] E))ᵒᵈ

Full source

/-- The Galois correspondence from intermediate fields to subgroups. -/
@[stacks 09DW]
def intermediateFieldEquivSubgroup [FiniteDimensional F E] [IsGalois F E] :
    IntermediateFieldIntermediateField F E ≃o (Subgroup (E ≃ₐ[F] E))ᵒᵈ where
  toFun := IntermediateField.fixingSubgroup
  invFun := IntermediateField.fixedField
  left_inv K := fixedField_fixingSubgroup K
  right_inv H := IntermediateField.fixingSubgroup_fixedField H
  map_rel_iff' {K L} := by
    rw [← fixedField_fixingSubgroup L, IntermediateField.le_iff_le, fixedField_fixingSubgroup L]
    rfl

Galois Correspondence: Intermediate Fields and Subgroups of the Galois Group

Informal description

For a finite-dimensional Galois extension $ E/F $, there is an order-reversing isomorphism between the lattice of intermediate fields $ K $ (with $ F \subseteq K \subseteq E $) and the lattice of subgroups of the Galois group $ \text{Aut}_F(E) $. The isomorphism is given by: - The map $ K \mapsto \text{Aut}_K(E) $, which sends an intermediate field $ K $ to the subgroup of automorphisms fixing $ K $ pointwise. - The inverse map $ H \mapsto E^H $, which sends a subgroup $ H $ to the fixed field of $ H $. This correspondence reverses the inclusion order, meaning that $ K \subseteq L $ if and only if $ \text{Aut}_L(E) \subseteq \text{Aut}_K(E) $.

IsGalois.galoisInsertionIntermediateFieldSubgroup definition

 [FiniteDimensional F E] :
  GaloisInsertion (OrderDual.toDual ∘ (IntermediateField.fixingSubgroup : IntermediateField F E → Subgroup (E ≃ₐ[F] E)))
    ((IntermediateField.fixedField : Subgroup (E ≃ₐ[F] E) → IntermediateField F E) ∘ OrderDual.toDual)

Full source

/-- The Galois correspondence as a `GaloisInsertion` -/
def galoisInsertionIntermediateFieldSubgroup [FiniteDimensional F E] :
    GaloisInsertion (OrderDual.toDualOrderDual.toDual ∘
      (IntermediateField.fixingSubgroup : IntermediateField F E → Subgroup (E ≃ₐ[F] E)))
      ((IntermediateField.fixedField : Subgroup (E ≃ₐ[F] E) → IntermediateField F E) ∘
        OrderDual.toDual) where
  choice K _ := IntermediateField.fixingSubgroup K
  gc K H := (IntermediateField.le_iff_le H K).symm
  le_l_u H := le_of_eq (IntermediateField.fixingSubgroup_fixedField H).symm
  choice_eq _ _ := rfl

Galois Correspondence as a Galois Insertion for Finite-Dimensional Extensions

Informal description

For a finite-dimensional field extension $ E/F $, the Galois correspondence between intermediate fields and subgroups of the Galois group $\text{Aut}_F(E)$ forms a Galois insertion. Specifically, the composition of the order-reversing map $\text{fixingSubgroup}$ (sending an intermediate field $ K $ to the subgroup of automorphisms fixing $ K $) with the order dual map $\text{OrderDual.toDual}$ is the left adjoint, and the composition of the order-reversing map $\text{fixedField}$ (sending a subgroup $ H $ to the intermediate field fixed by $ H $) with $\text{OrderDual.toDual}$ is the right adjoint. This means that for any intermediate field $ K $ and subgroup $ H $, the subgroup $\text{fixingSubgroup}(K)$ is contained in $ H $ (in the dual order) if and only if $ K $ is contained in $\text{fixedField}(H)$.

IsGalois.galoisCoinsertionIntermediateFieldSubgroup definition

 [FiniteDimensional F E] [IsGalois F E] :
  GaloisCoinsertion
    (OrderDual.toDual ∘ (IntermediateField.fixingSubgroup : IntermediateField F E → Subgroup (E ≃ₐ[F] E)))
    ((IntermediateField.fixedField : Subgroup (E ≃ₐ[F] E) → IntermediateField F E) ∘ OrderDual.toDual)

Full source

/-- The Galois correspondence as a `GaloisCoinsertion` -/
def galoisCoinsertionIntermediateFieldSubgroup [FiniteDimensional F E] [IsGalois F E] :
    GaloisCoinsertion (OrderDual.toDualOrderDual.toDual ∘
      (IntermediateField.fixingSubgroup : IntermediateField F E → Subgroup (E ≃ₐ[F] E)))
      ((IntermediateField.fixedField : Subgroup (E ≃ₐ[F] E) → IntermediateField F E) ∘
        OrderDual.toDual) :=
  OrderIso.toGaloisCoinsertion intermediateFieldEquivSubgroup

Galois Correspondence as a Galois Coinsertion for Finite-Dimensional Galois Extensions

Informal description

For a finite-dimensional Galois extension $ E/F $, the Galois correspondence between intermediate fields and subgroups of the Galois group $\text{Aut}_F(E)$ forms a Galois coinsertion. Specifically, the composition of the order-reversing map $\text{fixingSubgroup}$ (sending an intermediate field $ K $ to the subgroup of automorphisms fixing $ K $) with the order dual map $\text{OrderDual.toDual}$ is the left adjoint, and the composition of the order-reversing map $\text{fixedField}$ (sending a subgroup $ H $ to the intermediate field fixed by $ H $) with $\text{OrderDual.toDual}$ is the right adjoint. This means that for any intermediate field $ K $ and subgroup $ H $, the subgroup $\text{fixingSubgroup}(K)$ is contained in $ H $ (in the dual order) if and only if $ K $ is contained in $\text{fixedField}(H)$.

IntermediateField.restrictNormalHom_ker theorem

(E : IntermediateField K L) [Normal K E] : (restrictNormalHom E).ker = E.fixingSubgroup

Full source

lemma IntermediateField.restrictNormalHom_ker (E : IntermediateField K L) [Normal K E] :
    (restrictNormalHom E).ker = E.fixingSubgroup := by
  simp [fixingSubgroup, Subgroup.ext_iff, AlgEquiv.ext_iff, Subtype.ext_iff,
    restrictNormalHom_apply, mem_fixingSubgroup_iff]

Kernel of Restriction Homomorphism Equals Fixing Subgroup for Normal Intermediate Fields

Informal description

Let $E$ be an intermediate field in the field extension $L/K$ such that $E$ is normal over $K$. Then the kernel of the restriction homomorphism $\text{restrictNormalHom} \colon \text{Aut}_K(L) \to \text{Aut}_K(E)$ is equal to the fixing subgroup of $E$, i.e., the subgroup of $K$-automorphisms of $L$ that fix every element of $E$.

IsGalois.of_fixedField_normal_subgroup instance

[IsGalois K L] (H : Subgroup (L ≃ₐ[K] L)) [hn : Subgroup.Normal H] : IsGalois K (fixedField H)

Full source

/-- If `H` is a normal Subgroup of `Gal(L / K)`, then `fixedField H` is Galois over `K`. -/
instance of_fixedField_normal_subgroup [IsGalois K L]
    (H : Subgroup (L ≃ₐ[K] L)) [hn : Subgroup.Normal H] : IsGalois K (fixedField H) where
  to_isSeparable := Algebra.isSeparable_tower_bot_of_isSeparable K (fixedField H) L
  to_normal := by
    apply normal_iff_forall_map_le'.mpr
    rintro σ x ⟨a, ha, rfl⟩ τ
    exact (symm_apply_eq σ).mp (ha ⟨σ⁻¹ * τ * σ, Subgroup.Normal.conj_mem' hn τ.1 τ.2 σ⟩)

Galois Property of Fixed Fields under Normal Subgroups

Informal description

For any Galois extension $ L/K $ and any normal subgroup $ H $ of the Galois group $ \text{Aut}_K(L) $, the fixed field $ \text{fixedField}(H) $ is a Galois extension of $ K $.

IsGalois.normalAutEquivQuotient definition

 [FiniteDimensional K L] [IsGalois K L] (H : Subgroup (L ≃ₐ[K] L)) [Subgroup.Normal H] :
  (L ≃ₐ[K] L) ⧸ H ≃* ((fixedField H) ≃ₐ[K] (fixedField H))

Full source

/-- If `H` is a normal Subgroup of `Gal(L / K)`, then `Gal(fixedField H / K)` is isomorphic to
`Gal(L / K) ⧸ H`. -/
noncomputable def normalAutEquivQuotient [FiniteDimensional K L] [IsGalois K L]
    (H : Subgroup (L ≃ₐ[K] L)) [Subgroup.Normal H] :
    (L ≃ₐ[K] L) ⧸ H(L ≃ₐ[K] L) ⧸ H ≃* ((fixedField H) ≃ₐ[K] (fixedField H)) :=
  (QuotientGroup.quotientMulEquivOfEq ((fixingSubgroup_fixedField H).symm.trans
  (fixedField H).restrictNormalHom_ker.symm)).trans <|
  QuotientGroup.quotientKerEquivOfSurjective (restrictNormalHom (fixedField H)) <|
  restrictNormalHom_surjective L

Isomorphism between quotient of Galois group and automorphism group of fixed field

Informal description

Let $ L/K $ be a finite-dimensional Galois extension, and let $ H $ be a normal subgroup of the Galois group $ \text{Aut}_K(L) $. Then there is a multiplicative isomorphism between the quotient group $ \text{Aut}_K(L) / H $ and the automorphism group $ \text{Aut}_K(\text{fixedField}(H)) $. This isomorphism is constructed by first identifying $ H $ with the kernel of the restriction homomorphism to $ \text{fixedField}(H) $, then applying the first isomorphism theorem to obtain the desired equivalence.

IsGalois.normalAutEquivQuotient_apply theorem

 [FiniteDimensional K L] [IsGalois K L] (H : Subgroup (L ≃ₐ[K] L)) [Subgroup.Normal H] (σ : (L ≃ₐ[K] L)) :
  normalAutEquivQuotient H σ = (restrictNormalHom (fixedField H)) σ

Full source

lemma normalAutEquivQuotient_apply [FiniteDimensional K L] [IsGalois K L]
    (H : Subgroup (L ≃ₐ[K] L)) [Subgroup.Normal H] (σ : (L ≃ₐ[K] L)) :
    normalAutEquivQuotient H σ = (restrictNormalHom (fixedField H)) σ := rfl

Image of Galois Automorphism under Quotient-to-Fixed-Field Isomorphism

Informal description

Let $L/K$ be a finite-dimensional Galois extension, and let $H$ be a normal subgroup of the Galois group $\mathrm{Aut}_K(L)$. For any automorphism $\sigma \in \mathrm{Aut}_K(L)$, the image of $\sigma$ under the isomorphism $\mathrm{Aut}_K(L)/H \cong \mathrm{Aut}_K(\mathrm{fixedField}(H))$ is equal to the restriction of $\sigma$ to $\mathrm{fixedField}(H)$.

IsGalois.map_fixingSubgroup theorem

(σ : L ≃ₐ[K] L) : (E.map σ).fixingSubgroup = (MulAut.conj σ) • E.fixingSubgroup

Full source

@[simp]
theorem map_fixingSubgroup (σ : L ≃ₐ[K] L) :
    (E.map σ).fixingSubgroup = (MulAut.conj σ) • E.fixingSubgroup := by
  ext τ
  simp only [coe_map, AlgHom.coe_coe, Set.mem_image, SetLike.mem_coe, AlgEquiv.smul_def,
    forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, Subtype.forall,
    Subgroup.mem_pointwise_smul_iff_inv_smul_mem, ← symm_apply_eq,
    IntermediateField.fixingSubgroup, mem_fixingSubgroup_iff]
  rfl

Conjugation of Fixing Subgroup under Automorphism in Galois Extension

Informal description

Let $L/K$ be a Galois extension, and let $E$ be an intermediate field between $K$ and $L$. For any $K$-algebra automorphism $\sigma \colon L \to L$, the fixing subgroup of the image $\sigma(E)$ is equal to the conjugate of the fixing subgroup of $E$ by $\sigma$, i.e., \[ \text{fixingSubgroup}(\sigma(E)) = \sigma \cdot \text{fixingSubgroup}(E) \cdot \sigma^{-1}. \]

IsGalois.fixingSubgroup_normal_of_isGalois instance

[IsGalois K L] [IsGalois K E] : E.fixingSubgroup.Normal

Full source

/-- 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)`. -/
instance fixingSubgroup_normal_of_isGalois [IsGalois K L] [IsGalois K E] :
    E.fixingSubgroup.Normal := by
  apply Subgroup.Normal.of_conjugate_fixed (fun σ ↦ ?_)
  rw [← map_fixingSubgroup, normal_iff_forall_map_eq'.mp inferInstance σ]

Normality of Fixing Subgroup for Galois Intermediate Fields

Informal description

Let $L/K$ be a Galois extension and $E$ be an intermediate field between $K$ and $L$. If $E/K$ is also a Galois extension, then the fixing subgroup of $E$ is a normal subgroup of the Galois group $\mathrm{Gal}(L/K)$.

IsGalois.is_separable_splitting_field theorem

[FiniteDimensional F E] [IsGalois F E] : ∃ p : F[X], p.Separable ∧ p.IsSplittingField F E

Full source

theorem is_separable_splitting_field [FiniteDimensional F E] [IsGalois F E] :
    ∃ p : F[X], p.Separable ∧ p.IsSplittingField F E := by
  obtain ⟨α, h1⟩ := Field.exists_primitive_element F E
  use minpoly F α, separable F α, IsGalois.splits F α
  rw [eq_top_iff, ← IntermediateField.top_toSubalgebra, ← h1]
  rw [IntermediateField.adjoin_simple_toSubalgebra_of_integral (integral F α)]
  apply Algebra.adjoin_mono
  rw [Set.singleton_subset_iff, Polynomial.mem_rootSet]
  exact ⟨minpoly.ne_zero (integral F α), minpoly.aeval _ _⟩

Existence of Separable Splitting Field for Finite-Dimensional Galois Extensions

Informal description

For any finite-dimensional Galois extension $E/F$, there exists a separable polynomial $p \in F[X]$ such that $E$ is the splitting field of $p$ over $F$.

IsGalois.of_fixedField_eq_bot theorem

[FiniteDimensional F E] (h : IntermediateField.fixedField (⊤ : Subgroup (E ≃ₐ[F] E)) = ⊥) : IsGalois F E

Full source

theorem of_fixedField_eq_bot [FiniteDimensional F E]
    (h : IntermediateField.fixedField (⊤ : Subgroup (E ≃ₐ[F] E)) = ⊥) : IsGalois F E := by
  rw [← isGalois_iff_isGalois_bot, ← h]
  classical exact IsGalois.of_fixed_field E (⊤ : Subgroup (E ≃ₐ[F] E))

Galois Extension Criterion via Fixed Field of Full Automorphism Group

Informal description

Let $E/F$ be a finite-dimensional field extension. If the fixed field of the full Galois group $\mathrm{Aut}(E/F)$ is equal to the base field $F$ (i.e., $\mathrm{Fix}(\mathrm{Aut}(E/F)) = F$), then $E/F$ is a Galois extension.

IsGalois.of_card_aut_eq_finrank theorem

[FiniteDimensional F E] (h : Fintype.card (E ≃ₐ[F] E) = finrank F E) : IsGalois F E

Full source

/-- Let $E / F$ be a finite extension of fields. If $|\text{Aut}(E/F)| = [E : F]$, then
$E$ is Galois over $F$. -/
@[stacks 09I1 "'if' part"]
theorem of_card_aut_eq_finrank [FiniteDimensional F E]
    (h : Fintype.card (E ≃ₐ[F] E) = finrank F E) : IsGalois F E := by
  apply of_fixedField_eq_bot
  have p : 0 < finrank (IntermediateField.fixedField (⊤ : Subgroup (E ≃ₐ[F] E))) E := finrank_pos
  classical
  rw [← IntermediateField.finrank_eq_one_iff, ← mul_left_inj' (ne_of_lt p).symm,
    finrank_mul_finrank, ← h, one_mul, IntermediateField.finrank_fixedField_eq_card]
  apply Fintype.card_congr
  exact
    { toFun := fun g => ⟨g, Subgroup.mem_top g⟩
      invFun := (↑)
      left_inv := fun g => rfl
      right_inv := fun _ => by ext; rfl }

Cardinality Criterion for Galois Extensions: $|\mathrm{Aut}(E/F)| = [E:F] \Rightarrow E/F$ is Galois

Informal description

Let $E/F$ be a finite-dimensional field extension. If the cardinality of the automorphism group $\mathrm{Aut}(E/F)$ equals the degree $[E:F]$, then $E/F$ is a Galois extension.

IsGalois.of_separable_splitting_field_aux theorem

 [hFE : FiniteDimensional F E] [sp : p.IsSplittingField F E] (hp : p.Separable) (K : Type*) [Field K] [Algebra F K]
  [Algebra K E] [IsScalarTower F K E] {x : E}
  (hx : x ∈ p.aroots E)
    -- these are both implied by `hFE`, but as they carry data this makes the lemma more general
  [Fintype (K →ₐ[F] E)] [Fintype (K⟮x⟯.restrictScalars F →ₐ[F] E)] :
  Fintype.card (K⟮x⟯.restrictScalars F →ₐ[F] E) = Fintype.card (K →ₐ[F] E) * finrank K K⟮x⟯

Full source

theorem of_separable_splitting_field_aux [hFE : FiniteDimensional F E] [sp : p.IsSplittingField F E]
    (hp : p.Separable) (K : Type*) [Field K] [Algebra F K] [Algebra K E] [IsScalarTower F K E]
    {x : E} (hx : x ∈ p.aroots E)
    -- these are both implied by `hFE`, but as they carry data this makes the lemma more general
    [Fintype (K →ₐ[F] E)]
    [Fintype (K⟮x⟯K⟮x⟯.restrictScalars F →ₐ[F] E)] :
    Fintype.card (K⟮x⟯K⟮x⟯.restrictScalars F →ₐ[F] E) = Fintype.card (K →ₐ[F] E) * finrank K K⟮x⟯ := by
  have h : IsIntegral K x := (isIntegral_of_noetherian (IsNoetherian.iff_fg.2 hFE) x).tower_top
  have h1 : p ≠ 0 := fun hp => by
    rw [hp, Polynomial.aroots_zero] at hx
    exact Multiset.not_mem_zero x hx
  have h2 : minpolyminpoly K x ∣ p.map (algebraMap F K) := by
    apply minpoly.dvd
    rw [Polynomial.aeval_def, Polynomial.eval₂_map, ← Polynomial.eval_map, ←
      IsScalarTower.algebraMap_eq]
    exact (Polynomial.mem_roots (Polynomial.map_ne_zero h1)).mp hx
  let key_equiv : (K⟮x⟯.restrictScalars F →ₐ[F] E) ≃
      Σ f : K →ₐ[F] E, @AlgHom K K⟮x⟯ E _ _ _ _ (RingHom.toAlgebra f) := by
    change (K⟮x⟯ →ₐ[F] E) ≃ Σ f : K →ₐ[F] E, _
    exact algHomEquivSigma
  haveI : ∀ f : K →ₐ[F] E, Fintype (@AlgHom K K⟮x⟯ E _ _ _ _ (RingHom.toAlgebra f)) := fun f => by
    have := Fintype.ofEquiv _ key_equiv
    apply Fintype.ofInjective (Sigma.mk f) fun _ _ H => eq_of_heq (Sigma.ext_iff.mp H).2
  rw [Fintype.card_congr key_equiv, Fintype.card_sigma, IntermediateField.adjoin.finrank h]
  apply Finset.sum_const_nat
  intro f _
  rw [← @IntermediateField.card_algHom_adjoin_integral K _ E _ _ x E _ (RingHom.toAlgebra f) h]
  · congr!
  · exact Polynomial.Separable.of_dvd ((Polynomial.separable_map (algebraMap F K)).mpr hp) h2
  · refine Polynomial.splits_of_splits_of_dvd _ (Polynomial.map_ne_zero h1) ?_ h2
    -- Porting note: use unification instead of synthesis for one argument of `algebraMap_eq`
    rw [Polynomial.splits_map_iff, ← @IsScalarTower.algebraMap_eq _ _ _ _ _ _ _ (_) _ _]
    exact sp.splits

Cardinality of Homomorphisms in Separable Splitting Field Extension: $|\mathrm{Hom}_F(K(\alpha), E)| = |\mathrm{Hom}_F(K, E)| \cdot [K(\alpha):K]$

Informal description

Let $E/F$ be a finite-dimensional field extension and let $p \in F[X]$ be a separable polynomial that splits completely in $E$ (i.e., $E$ is a splitting field of $p$ over $F$). Consider a field $K$ with $F \subseteq K \subseteq E$ forming a scalar tower, and let $x \in E$ be a root of $p$ in $E$. Under these conditions, the number of $F$-algebra homomorphisms from $K(x)$ (viewed as an intermediate field via restriction of scalars) to $E$ is equal to the product of: 1. The number of $F$-algebra homomorphisms from $K$ to $E$, and 2. The degree of the field extension $[K(x) : K]$. In symbols: \[ |\mathrm{Hom}_F(K(x), E)| = |\mathrm{Hom}_F(K, E)| \cdot [K(x) : K]. \]

IsGalois.of_separable_splitting_field theorem

[sp : p.IsSplittingField F E] (hp : p.Separable) : IsGalois F E

Full source

theorem of_separable_splitting_field [sp : p.IsSplittingField F E] (hp : p.Separable) :
    IsGalois F E := by
  haveI hFE : FiniteDimensional F E := Polynomial.IsSplittingField.finiteDimensional E p
  letI := Classical.decEq E
  let s := p.rootSet E
  have adjoin_root : IntermediateField.adjoin F s = ⊤ := by
    apply IntermediateField.toSubalgebra_injective
    rw [IntermediateField.top_toSubalgebra, ← top_le_iff, ← sp.adjoin_rootSet]
    apply IntermediateField.algebra_adjoin_le_adjoin
  let P : IntermediateField F E → Prop := fun K => Fintype.card (K →ₐ[F] E) = finrank F K
  suffices P (IntermediateField.adjoin F s) by
    rw [adjoin_root] at this
    apply of_card_aut_eq_finrank
    rw [← Eq.trans this (LinearEquiv.finrank_eq IntermediateField.topEquiv.toLinearEquiv)]
    exact Fintype.card_congr ((algEquivEquivAlgHom F E).toEquiv.trans
      (IntermediateField.topEquiv.symm.arrowCongr AlgEquiv.refl))
  apply IntermediateField.induction_on_adjoin_finset _ P
  · have key := IntermediateField.card_algHom_adjoin_integral F (K := E)
      (show IsIntegral F (0 : E) from isIntegral_zero)
    rw [IsSeparable, minpoly.zero, Polynomial.natDegree_X] at key
    specialize key Polynomial.separable_X (Polynomial.splits_X (algebraMap F E))
    rw [← @Subalgebra.finrank_bot F E _ _ _, ← IntermediateField.bot_toSubalgebra] at key
    refine Eq.trans ?_ key
    -- Porting note: use unification instead of synthesis for one argument of `card_congr`
    apply @Fintype.card_congr _ _ _ (_) _
    rw [IntermediateField.adjoin_zero]
  intro K x hx hK
  simp only [P] at *
  rw [of_separable_splitting_field_aux hp K (Multiset.mem_toFinset.mp hx), hK, finrank_mul_finrank]
  symm
  refine LinearEquiv.finrank_eq ?_
  rfl

Splitting Field of Separable Polynomial is Galois Extension

Informal description

Let $E/F$ be a field extension and $p \in F[X]$ be a separable polynomial. If $E$ is a splitting field of $p$ over $F$, then $E/F$ is a Galois extension.

IsGalois.tfae theorem

 [FiniteDimensional F E] :
  List.TFAE
    [IsGalois F E, IntermediateField.fixedField (⊤ : Subgroup (E ≃ₐ[F] E)) = ⊥, Fintype.card (E ≃ₐ[F] E) = finrank F E,
      ∃ p : F[X], p.Separable ∧ p.IsSplittingField F E]

Full source

/-- Equivalent characterizations of a Galois extension of finite degree -/
theorem tfae [FiniteDimensional F E] : List.TFAE [
    IsGalois F E,
    IntermediateField.fixedField (⊤ : Subgroup (E ≃ₐ[F] E)) = ⊥,
    Fintype.card (E ≃ₐ[F] E) = finrank F E,
    ∃ p : F[X], p.Separable ∧ p.IsSplittingField F E] := by
  tfae_have 1 → 2 := fun h ↦ OrderIso.map_bot (@intermediateFieldEquivSubgroup F _ E _ _ _ h).symm
  tfae_have 1 → 3 := fun _ ↦ card_aut_eq_finrank F E
  tfae_have 1 → 4 := fun _ ↦ is_separable_splitting_field F E
  tfae_have 2 → 1 := of_fixedField_eq_bot F E
  tfae_have 3 → 1 := of_card_aut_eq_finrank F E
  tfae_have 4 → 1 := fun ⟨h, hp1, _⟩ ↦ of_separable_splitting_field hp1
  tfae_finish

Equivalent Characterizations of Finite-Dimensional Galois Extensions (TFAE)

Informal description

For a finite-dimensional field extension $E/F$, the following conditions are equivalent: 1. $E/F$ is a Galois extension (i.e., it is both separable and normal). 2. The fixed field of the full Galois group $\mathrm{Aut}(E/F)$ is equal to $F$. 3. The number of $F$-algebra automorphisms of $E$ equals the degree $[E:F]$. 4. There exists a separable polynomial $p \in F[X]$ such that $E$ is the splitting field of $p$ over $F$.

IsGalois.normalClosure instance

: IsGalois k (normalClosure k K F)

Full source

/-- 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$. -/
@[stacks 0EXM]
instance IsGalois.normalClosure : IsGalois k (normalClosure k K F) where
  to_isSeparable := Algebra.isSeparable_tower_bot_of_isSeparable k _ F

Galois Property of Normal Closure in Field Extensions

Informal description

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$.

IsAlgClosure.isGalois instance

(k K : Type*) [Field k] [Field K] [Algebra k K] [IsAlgClosure k K] [CharZero k] : IsGalois k K

Full source

instance (priority := 100) IsAlgClosure.isGalois (k K : Type*) [Field k] [Field K] [Algebra k K]
    [IsAlgClosure k K] [CharZero k] : IsGalois k K where

Algebraic Closures in Characteristic Zero are Galois Extensions

Informal description

For any fields $k$ and $K$ with $K$ an algebraic closure of $k$ and $k$ of characteristic zero, the extension $K/k$ is Galois.

Algebra.IsQuadraticExtension.isGalois instance

[Algebra.IsSeparable F K] : IsGalois F K

Full source

/--
A quadratic separable extension is Galois.
-/
instance IsQuadraticExtension.isGalois [Algebra.IsSeparable F K] : IsGalois F K where

Quadratic Separable Extensions are Galois

Informal description

For any quadratic separable field extension $K/F$, the extension $K/F$ is Galois.

Algebra.IsQuadraticExtension.isCyclic instance

: IsCyclic (K ≃ₐ[F] K)

Full source

/--
A quadratic extension has cyclic Galois group.
-/
instance IsQuadraticExtension.isCyclic : IsCyclic (K ≃ₐ[F] K) := by
  have := finrank_eq_two F K ▸ AlgEquiv.card_le
  interval_cases h : Fintype.card (K ≃ₐ[F] K)
  · simp_all
  · exact @isCyclic_of_subsingleton _ _ (Fintype.card_le_one_iff_subsingleton.mp h.le)
  · rw [← Nat.card_eq_fintype_card] at h
    exact isCyclic_of_prime_card h

Cyclicity of Galois Group in Quadratic Extensions

Informal description

For any quadratic field extension $K/F$, the Galois group $\mathrm{Gal}(K/F)$ is cyclic.

Algebra.IsQuadraticExtension.isMulCommutative_galoisGroup instance

: IsMulCommutative (K ≃ₐ[F] K)

Full source

/--
A quadratic extension has abelian Galois group.
-/
instance IsQuadraticExtension.isMulCommutative_galoisGroup :
    IsMulCommutative (K ≃ₐ[F] K) := ⟨IsCyclic.commutative⟩

Galois Group of Quadratic Extensions is Abelian

Informal description

For any quadratic field extension $K/F$, the Galois group $\mathrm{Gal}(K/F)$ is abelian.

Mathlib.FieldTheory.Galois.Basic

Main definitions

Main results

Additional results