Galois Correspondence In Lean

I'm studying math. — Sat, 21 Mar 2026 11:35:10 +0000

This article was originally published on "I'm studying math.".

In mathlib, this is defined as intermediateFieldEquivSubgroup.

def intermediateFieldEquivSubgroup [FiniteDimensional F E] [IsGalois F E] :
    IntermediateField F E ≃o (Subgroup Gal(E/F))ᵒᵈ where
  ...

Hypotheses

def intermediateFieldEquivSubgroup [FiniteDimensional F E] [IsGalois F E] :

`FiniteDimensional`

abbrev FiniteDimensional (K V : Type*) [DivisionRing K] [AddCommGroup V] [Module K V] :=
  Module.Finite K V

`FiniteDimensional` > `Module`

Module refers to a module over a ring.

class Module (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] extends
  DistribMulAction R M where
  protected add_smul : ∀ (r s : R) (x : M), (r + s) • x = r • x + s • x
  protected zero_smul : ∀ x : M, (0 : R) • x = 0

`FiniteDimensional` > `Module.Finite`

Module.Finite refers to a finitely generated module.

protected class Module.Finite [Semiring R] [AddCommMonoid M] [Module R M] : Prop where
  of_fg_top ::
    fg_top : (⊤ : Submodule R M).FG

Note regarding `::`

If :: is not used:

protected class Module.Finite [Semiring R] [AddCommMonoid M] [Module R M] : Prop where
  fg_top : (⊤ : Submodule R M).FG

In this case, an instance is defined as follows:

let inst := Module.Finite.mk H

On the other hand, when :: is used:

of_fg_top ::
  fg_top : ...

The instance is defined like this:

let inst := Module.Finite.of_fg_top H

In short, it seems :: is used to give an alias to mk.

`IsGalois`

This represents a Galois extension.

The Statement

    IntermediateField F E ≃o (Subgroup Gal(E/F))ᵒᵈ where

`IntermediateField`

Refers to an intermediate field.

structure IntermediateField extends Subalgebra K L where
  inv_mem' : ∀ x ∈ carrier, x⁻¹ ∈ carrier

`IntermediateField` > `Subalgebra`

structure Subalgebra (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] : Type v
    extends Subsemiring A where
  algebraMap_mem' : ∀ r, algebraMap R A r ∈ carrier
  zero_mem' := (algebraMap R A).map_zero ▸ algebraMap_mem' 0
  one_mem' := (algebraMap R A).map_one ▸ algebraMap_mem' 1

`≃o`

Refers to an order isomorphism.

A ≃o B represents OrderIso A B.

abbrev OrderIso (α β : Type*) [LE α] [LE β] :=
  @RelIso α β (· ≤ ·) (· ≤ ·)

structure RelIso {α β : Type*} (r : α → α → Prop) (s : β → β → Prop) extends α ≃ β where
  map_rel_iff' : ∀ {a b}, s (toEquiv a) (toEquiv b) ↔ r a b

`ᵒᵈ`

Refers to the reverse order (Order Dual).

αᵒᵈ represents OrderDual α.

def OrderDual (α : Type*) : Type _ :=
  α

OrderDual reverses the order.

Because of the following instance definitions, the order becomes inverted:

instance (α : Type*) [LE α] : LE αᵒᵈ :=
  ⟨fun x y : α ↦ y ≤ x⟩

instance (α : Type*) [LT α] : LT αᵒᵈ :=
  ⟨fun x y : α ↦ y < x⟩

Summary of the Statement

In conclusion:

Intermediate Fields and
The reverse order of Subgroups(Subgroup) of the Galois Group (Gal(E/F))

are order-isomorphic (they correspond to each other).

DEV Community: I'm studying math.

Galois Correspondence In Lean

Hypotheses

FiniteDimensional

FiniteDimensional > Module

FiniteDimensional > Module.Finite

Note regarding ::

IsGalois