DEV Community

I'm studying math.
I'm studying math.

Posted on • Originally published at imstudyingmath.com

Galois Correspondence In Lean

#lean #lean4 #math #mathematics

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
  ...
Enter fullscreen mode Exit fullscreen mode

Hypotheses 

def intermediateFieldEquivSubgroup [FiniteDimensional F E] [IsGalois F E] :
Enter fullscreen mode Exit fullscreen mode

FiniteDimensional 

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

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
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode
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
Enter fullscreen mode Exit fullscreen mode

In this case, an instance is defined as follows:

let inst := Module.Finite.mk H
Enter fullscreen mode Exit fullscreen mode

On the other hand, when :: is used:

of_fg_top ::
  fg_top : ...
Enter fullscreen mode Exit fullscreen mode

The instance is defined like this:

let inst := Module.Finite.of_fg_top H
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

IntermediateField

Refers to an intermediate field.

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

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
Enter fullscreen mode Exit fullscreen mode

≃o

Refers to an order isomorphism.

A ≃o B represents OrderIso A B.

abbrev OrderIso (α β : Type*) [LE α] [LE β] :=
  @RelIso α β (· ≤ ·) (· ≤ ·)
Enter fullscreen mode Exit fullscreen mode 
structure RelIso {α β : Type*} (r : α → α → Prop) (s : β → β → Prop) extends α ≃ β where
  map_rel_iff' : ∀ {a b}, s (toEquiv a) (toEquiv b) ↔ r a b
Enter fullscreen mode Exit fullscreen mode

ᵒᵈ

Refers to the reverse order (Order Dual).

αᵒᵈ represents OrderDual α.

def OrderDual (α : Type*) : Type _ :=
  α
Enter fullscreen mode Exit fullscreen mode

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⟩
Enter fullscreen mode Exit fullscreen mode

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

Top comments (0)