Galois connections, insertions and coinsertions

Galois connections are order-theoretic adjoints, i.e. a pair of functions u and l, such that ∀ a b, l a ≤ b ↔ a ≤ u b.

Main definitions

• GaloisConnection: A Galois connection is a pair of functions l and u satisfying l a ≤ b ↔ a ≤ u b. They are special cases of adjoint functors in category theory, but do not depend on the category theory library in mathlib.
• GaloisInsertion: A Galois insertion is a Galois connection where l ∘ u = id
• GaloisCoinsertion: A Galois coinsertion is a Galois connection where u ∘ l = id

def GaloisConnection {α : Type u} {β : Type v} [Preorder α] [Preorder β] (l : α → β) (u : β → α) : Prop

A Galois connection is a pair of functions l and u satisfying l a ≤ b ↔ a ≤ u b. They are special cases of adjoint functors in category theory, but do not depend on the category theory library in mathlib.

Equations

• GaloisConnection l u = ∀ (a : α) (b : β), l a ≤ b ↔ a ≤ u b

theorem GaloisConnection.monotone_intro {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (hu : Monotone u) (hl : Monotone l) (hul : ∀ (a : α), a ≤ u (l a)) (hlu : ∀ (a : β), l (u a) ≤ a) : GaloisConnection l u

theorem GaloisConnection.dual {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : GaloisConnection (⇑OrderDual.toDual ∘ u ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ l ∘ ⇑OrderDual.ofDual)

theorem GaloisConnection.le_iff_le {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {a : α} {b : β} : l a ≤ b ↔ a ≤ u b

theorem GaloisConnection.l_le {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {a : α} {b : β} : a ≤ u b → l a ≤ b

theorem GaloisConnection.le_u {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {a : α} {b : β} : l a ≤ b → a ≤ u b

theorem GaloisConnection.le_u_l {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (a : α) : a ≤ u (l a)

theorem GaloisConnection.l_u_le {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (a : β) : l (u a) ≤ a

theorem GaloisConnection.monotone_u {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : Monotone u

theorem GaloisConnection.monotone_l {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : Monotone l

theorem GaloisConnection.le_u_l_trans {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {x y z : α} (hxy : x ≤ u (l y)) (hyz : y ≤ u (l z)) : x ≤ u (l z)

If (l, u) is a Galois connection, then the relation x ≤ u (l y) is a transitive relation. If l is a closure operator (Submodule.span, Subgroup.closure, ...) and u is the coercion to Set, this reads as "if U is in the closure of V and V is in the closure of W then U is in the closure of W".

theorem GaloisConnection.l_u_le_trans {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {x y z : β} (hxy : l (u x) ≤ y) (hyz : l (u y) ≤ z) : l (u x) ≤ z

theorem GaloisConnection.u_l_u_eq_u {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (b : β) : u (l (u b)) = u b

theorem GaloisConnection.u_l_u_eq_u' {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : u ∘ l ∘ u = u

theorem GaloisConnection.u_unique {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {l' : α → β} {u' : β → α} (gc' : GaloisConnection l' u') (hl : ∀ (a : α), l a = l' a) {b : β} : u b = u' b

theorem GaloisConnection.exists_eq_u {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (a : α) : (∃ (b : β), a = u b) ↔ a = u (l a)

If there exists a b such that a = u a, then b = l a is one such element.

theorem GaloisConnection.u_eq {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {z : α} {y : β} : u y = z ↔ ∀ (x : α), x ≤ z ↔ l x ≤ y

theorem GaloisConnection.l_u_l_eq_l {α : Type u} {β : Type v} [Preorder α] [PartialOrder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (a : α) : l (u (l a)) = l a

theorem GaloisConnection.l_u_l_eq_l' {α : Type u} {β : Type v} [Preorder α] [PartialOrder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : l ∘ u ∘ l = l

theorem GaloisConnection.l_unique {α : Type u} {β : Type v} [Preorder α] [PartialOrder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {l' : α → β} {u' : β → α} (gc' : GaloisConnection l' u') (hu : ∀ (b : β), u b = u' b) {a : α} : l a = l' a

theorem GaloisConnection.exists_eq_l {α : Type u} {β : Type v} [Preorder α] [PartialOrder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (b : β) : (∃ (a : α), b = l a) ↔ b = l (u b)

If there exists an a such that b = l a, then a = u b is one such element.

theorem GaloisConnection.l_eq {α : Type u} {β : Type v} [Preorder α] [PartialOrder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {x : α} {z : β} : l x = z ↔ ∀ (y : β), z ≤ y ↔ x ≤ u y

theorem GaloisConnection.u_eq_top {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] [OrderTop α] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {x : β} : u x = ⊤ ↔ l ⊤ ≤ x

theorem GaloisConnection.u_top {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] [OrderTop α] [OrderTop β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : u ⊤ = ⊤

theorem GaloisConnection.u_l_top {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] [OrderTop α] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : u (l ⊤) = ⊤

theorem GaloisConnection.l_eq_bot {α : Type u} {β : Type v} [Preorder α] [PartialOrder β] [OrderBot β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {x : α} : l x = ⊥ ↔ x ≤ u ⊥

theorem GaloisConnection.l_bot {α : Type u} {β : Type v} [Preorder α] [PartialOrder β] [OrderBot β] [OrderBot α] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : l ⊥ = ⊥

theorem GaloisConnection.l_u_bot {α : Type u} {β : Type v} [Preorder α] [PartialOrder β] [OrderBot β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : l (u ⊥) = ⊥

theorem GaloisConnection.lt_iff_lt {α : Type u} {β : Type v} [LinearOrder α] [LinearOrder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {a : α} {b : β} : b < l a ↔ u b < a

theorem GaloisConnection.id {α : Type u} [pα : Preorder α] : GaloisConnection id id

theorem GaloisConnection.compose {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {l1 : α → β} {u1 : β → α} {l2 : β → γ} {u2 : γ → β} (gc1 : GaloisConnection l1 u1) (gc2 : GaloisConnection l2 u2) : GaloisConnection (l2 ∘ l1) (u1 ∘ u2)

theorem GaloisConnection.dfun {ι : Type u} {α : ι → Type v} {β : ι → Type w} [(i : ι) → Preorder (α i)] [(i : ι) → Preorder (β i)] (l : (i : ι) → α i → β i) (u : (i : ι) → β i → α i) (gc : ∀ (i : ι), GaloisConnection (l i) (u i)) : GaloisConnection (fun (a : (i : ι) → α i) (i : ι) => l i (a i)) fun (b : (i : ι) → β i) (i : ι) => u i (b i)

theorem GaloisConnection.l_comm_of_u_comm {X : Type u_2} [Preorder X] {Y : Type u_3} [Preorder Y] {Z : Type u_4} [Preorder Z] {W : Type u_5} [PartialOrder W] {lYX : X → Y} {uXY : Y → X} (hXY : GaloisConnection lYX uXY) {lWZ : Z → W} {uZW : W → Z} (hZW : GaloisConnection lWZ uZW) {lWY : Y → W} {uYW : W → Y} (hWY : GaloisConnection lWY uYW) {lZX : X → Z} {uXZ : Z → X} (hXZ : GaloisConnection lZX uXZ) (h : ∀ (w : W), uXZ (uZW w) = uXY (uYW w)) {x : X} : lWZ (lZX x) = lWY (lYX x)

theorem GaloisConnection.u_comm_of_l_comm {X : Type u_2} [PartialOrder X] {Y : Type u_3} [Preorder Y] {Z : Type u_4} [Preorder Z] {W : Type u_5} [Preorder W] {lYX : X → Y} {uXY : Y → X} (hXY : GaloisConnection lYX uXY) {lWZ : Z → W} {uZW : W → Z} (hZW : GaloisConnection lWZ uZW) {lWY : Y → W} {uYW : W → Y} (hWY : GaloisConnection lWY uYW) {lZX : X → Z} {uXZ : Z → X} (hXZ : GaloisConnection lZX uXZ) (h : ∀ (x : X), lWZ (lZX x) = lWY (lYX x)) {w : W} : uXZ (uZW w) = uXY (uYW w)

theorem GaloisConnection.l_comm_iff_u_comm {X : Type u_2} [PartialOrder X] {Y : Type u_3} [Preorder Y] {Z : Type u_4} [Preorder Z] {W : Type u_5} [PartialOrder W] {lYX : X → Y} {uXY : Y → X} (hXY : GaloisConnection lYX uXY) {lWZ : Z → W} {uZW : W → Z} (hZW : GaloisConnection lWZ uZW) {lWY : Y → W} {uYW : W → Y} (hWY : GaloisConnection lWY uYW) {lZX : X → Z} {uXZ : Z → X} (hXZ : GaloisConnection lZX uXZ) : (∀ (w : W), uXZ (uZW w) = uXY (uYW w)) ↔ ∀ (x : X), lWZ (lZX x) = lWY (lYX x)

structure GaloisInsertion {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (l : α → β) (u : β → α) : Type (max u_2 u_3)

A Galois insertion is a Galois connection where l ∘ u = id. It also contains a constructive choice function, to give better definitional equalities when lifting order structures. Dual to GaloisCoinsertion

• choice (x : α) : u (l x) ≤ x → β

  A constructive choice function for images of l.

• gc : GaloisConnection l u

  The Galois connection associated to a Galois insertion.

• le_l_u (x : β) : x ≤ l (u x)

  Main property of a Galois insertion.

• choice_eq (a : α) (h : u (l a) ≤ a) : self.choice a h = l a

  Property of the choice function.

def GaloisInsertion.monotoneIntro {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (hu : Monotone u) (hl : Monotone l) (hul : ∀ (a : α), a ≤ u (l a)) (hlu : ∀ (b : β), l (u b) = b) : GaloisInsertion l u

A constructor for a Galois insertion with the trivial choice function.

Equations

• GaloisInsertion.monotoneIntro hu hl hul hlu = { choice := fun (x : α) (x_1 : u (l x) ≤ x) => l x, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }

def GaloisConnection.toGaloisInsertion {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (h : ∀ (b : β), b ≤ l (u b)) : GaloisInsertion l u

Make a GaloisInsertion l u from a GaloisConnection l u such that ∀ b, b ≤ l (u b)

Equations

• gc.toGaloisInsertion h = { choice := fun (x : α) (x_1 : u (l x) ≤ x) => l x, gc := gc, le_l_u := h, choice_eq := ⋯ }

def GaloisConnection.liftOrderBot {α : Type u_2} {β : Type u_3} [Preorder α] [OrderBot α] [PartialOrder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : OrderBot β

Lift the bottom along a Galois connection

Equations

• gc.liftOrderBot = { bot := l ⊥, bot_le := ⋯ }

theorem GaloisInsertion.l_u_eq {α : Type u} {β : Type v} {l : α → β} {u : β → α} [Preorder α] [PartialOrder β] (gi : GaloisInsertion l u) (b : β) : l (u b) = b

theorem GaloisInsertion.leftInverse_l_u {α : Type u} {β : Type v} {l : α → β} {u : β → α} [Preorder α] [PartialOrder β] (gi : GaloisInsertion l u) : Function.LeftInverse l u

theorem GaloisInsertion.l_top {α : Type u} {β : Type v} {l : α → β} {u : β → α} [Preorder α] [PartialOrder β] [OrderTop α] [OrderTop β] (gi : GaloisInsertion l u) : l ⊤ = ⊤

theorem GaloisInsertion.l_surjective {α : Type u} {β : Type v} {l : α → β} {u : β → α} [Preorder α] [PartialOrder β] (gi : GaloisInsertion l u) : Function.Surjective l

theorem GaloisInsertion.u_injective {α : Type u} {β : Type v} {l : α → β} {u : β → α} [Preorder α] [PartialOrder β] (gi : GaloisInsertion l u) : Function.Injective u

theorem GaloisInsertion.u_le_u_iff {α : Type u} {β : Type v} {l : α → β} {u : β → α} [Preorder α] [Preorder β] (gi : GaloisInsertion l u) {a b : β} : u a ≤ u b ↔ a ≤ b

theorem GaloisInsertion.strictMono_u {α : Type u} {β : Type v} {l : α → β} {u : β → α} [Preorder α] [Preorder β] (gi : GaloisInsertion l u) : StrictMono u

structure GaloisCoinsertion {α : Type u} {β : Type v} [Preorder α] [Preorder β] (l : α → β) (u : β → α) : Type (max u v)

A Galois coinsertion is a Galois connection where u ∘ l = id. It also contains a constructive choice function, to give better definitional equalities when lifting order structures. Dual to GaloisInsertion

• choice (x : β) : x ≤ l (u x) → α

  A constructive choice function for images of u.

• gc : GaloisConnection l u

  The Galois connection associated to a Galois coinsertion.

• u_l_le (x : α) : u (l x) ≤ x

  Main property of a Galois coinsertion.

• choice_eq (a : β) (h : a ≤ l (u a)) : self.choice a h = u a

  Property of the choice function.

def GaloisCoinsertion.dual {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} : GaloisCoinsertion l u → GaloisInsertion (⇑OrderDual.toDual ∘ u ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ l ∘ ⇑OrderDual.ofDual)

Make a GaloisInsertion between αᵒᵈ and βᵒᵈ from a GaloisCoinsertion between α and β.

Equations

• x.dual = { choice := x.choice, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }

def GaloisInsertion.dual {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} : GaloisInsertion l u → GaloisCoinsertion (⇑OrderDual.toDual ∘ u ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ l ∘ ⇑OrderDual.ofDual)

Make a GaloisCoinsertion between αᵒᵈ and βᵒᵈ from a GaloisInsertion between α and β.

Equations

• x.dual = { choice := x.choice, gc := ⋯, u_l_le := ⋯, choice_eq := ⋯ }

def GaloisCoinsertion.ofDual {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : αᵒᵈ → βᵒᵈ} {u : βᵒᵈ → αᵒᵈ} : GaloisCoinsertion l u → GaloisInsertion (⇑OrderDual.ofDual ∘ u ∘ ⇑OrderDual.toDual) (⇑OrderDual.ofDual ∘ l ∘ ⇑OrderDual.toDual)

Make a GaloisInsertion between α and β from a GaloisCoinsertion between αᵒᵈ and βᵒᵈ.

Equations

• x.ofDual = { choice := x.choice, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }

def GaloisInsertion.ofDual {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : αᵒᵈ → βᵒᵈ} {u : βᵒᵈ → αᵒᵈ} : GaloisInsertion l u → GaloisCoinsertion (⇑OrderDual.ofDual ∘ u ∘ ⇑OrderDual.toDual) (⇑OrderDual.ofDual ∘ l ∘ ⇑OrderDual.toDual)

Make a GaloisCoinsertion between α and β from a GaloisInsertion between αᵒᵈ and βᵒᵈ.

Equations

• x.ofDual = { choice := x.choice, gc := ⋯, u_l_le := ⋯, choice_eq := ⋯ }

def GaloisCoinsertion.monotoneIntro {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (hu : Monotone u) (hl : Monotone l) (hlu : ∀ (b : β), l (u b) ≤ b) (hul : ∀ (a : α), u (l a) = a) : GaloisCoinsertion l u

A constructor for a Galois coinsertion with the trivial choice function.

Equations

• GaloisCoinsertion.monotoneIntro hu hl hlu hul = (GaloisInsertion.monotoneIntro ⋯ ⋯ hlu hul).ofDual

def GaloisConnection.toGaloisCoinsertion {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (h : ∀ (a : α), u (l a) ≤ a) : GaloisCoinsertion l u

Make a GaloisCoinsertion l u from a GaloisConnection l u such that ∀ a, u (l a) ≤ a

Equations

• gc.toGaloisCoinsertion h = { choice := fun (x : β) (x_1 : x ≤ l (u x)) => u x, gc := gc, u_l_le := h, choice_eq := ⋯ }

def GaloisConnection.liftOrderTop {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] [OrderTop β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : OrderTop α

Lift the top along a Galois connection

Equations

• gc.liftOrderTop = { top := u ⊤, le_top := ⋯ }

theorem GaloisCoinsertion.u_l_eq {α : Type u} {β : Type v} {l : α → β} {u : β → α} [PartialOrder α] [Preorder β] (gi : GaloisCoinsertion l u) (a : α) : u (l a) = a

theorem GaloisCoinsertion.u_l_leftInverse {α : Type u} {β : Type v} {l : α → β} {u : β → α} [PartialOrder α] [Preorder β] (gi : GaloisCoinsertion l u) : Function.LeftInverse u l

theorem GaloisCoinsertion.u_bot {α : Type u} {β : Type v} {l : α → β} {u : β → α} [PartialOrder α] [Preorder β] [OrderBot α] [OrderBot β] (gi : GaloisCoinsertion l u) : u ⊥ = ⊥

theorem GaloisCoinsertion.u_surjective {α : Type u} {β : Type v} {l : α → β} {u : β → α} [PartialOrder α] [Preorder β] (gi : GaloisCoinsertion l u) : Function.Surjective u

theorem GaloisCoinsertion.l_injective {α : Type u} {β : Type v} {l : α → β} {u : β → α} [PartialOrder α] [Preorder β] (gi : GaloisCoinsertion l u) : Function.Injective l

theorem GaloisCoinsertion.l_le_l_iff {α : Type u} {β : Type v} {l : α → β} {u : β → α} [Preorder α] [Preorder β] (gi : GaloisCoinsertion l u) {a b : α} : l a ≤ l b ↔ a ≤ b

theorem GaloisCoinsertion.strictMono_l {α : Type u} {β : Type v} {l : α → β} {u : β → α} [Preorder α] [Preorder β] (gi : GaloisCoinsertion l u) : StrictMono l