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

Implementation details

Galois insertions can be used to lift order structures from one type to another. For example if α is a complete lattice, and l : α → β, and u : β → α form a Galois insertion, then β is also a complete lattice. l is the lower adjoint and u is the upper adjoint.

An example of a Galois insertion is in group theory. If G is a group, then there is a Galois insertion between the set of subsets of G, Set G, and the set of subgroups of G, Subgroup G. The lower adjoint is Subgroup.closure, taking the Subgroup generated by a Set, and the upper adjoint is the coercion from Subgroup G to Set G, taking the underlying set of a subgroup.

Naively lifting a lattice structure along this Galois insertion would mean that the definition of inf on subgroups would be Subgroup.closure (↑S ∩ ↑T). This is an undesirable definition because the intersection of subgroups is already a subgroup, so there is no need to take the closure. For this reason a choice function is added as a field to the GaloisInsertion structure. It has type Π S : Set G, ↑(closure S) ≤ S → Subgroup G. When ↑(closure S) ≤ S, then S is already a subgroup, so this function can be defined using Subgroup.mk and not closure. This means the infimum of subgroups will be defined to be the intersection of sets, paired with a proof that intersection of subgroups is a subgroup, rather than the closure of the intersection.

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.

theorem OrderIso.to_galoisConnection {α : Type u} {β : Type v} [Preorder α] [Preorder β] (oi : α ≃o β) : GaloisConnection ↑oi ↑(OrderIso.symm oi)

Makes a Galois connection from an order-preserving bijection.

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.upperBounds_l_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (s : Set α) : upperBounds (l '' s) = u ⁻¹' upperBounds s

theorem GaloisConnection.lowerBounds_u_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (s : Set β) : lowerBounds (u '' s) = l ⁻¹' lowerBounds s

theorem GaloisConnection.bddAbove_l_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {s : Set α} : BddAbove (l '' s) ↔ BddAbove s

theorem GaloisConnection.bddBelow_u_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {s : Set β} : BddBelow (u '' s) ↔ BddBelow s

theorem GaloisConnection.isLUB_l_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {s : Set α} {a : α} (h : IsLUB s a) : IsLUB (l '' s) (l a)

theorem GaloisConnection.isGLB_u_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {s : Set β} {b : β} (h : IsGLB s b) : IsGLB (u '' s) (u b)

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

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

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

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

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.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_sup {α : Type u} {β : Type v} {a₁ : α} {a₂ : α} [SemilatticeSup α] [SemilatticeSup β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : l (a₁ ⊔ a₂) = l a₁ ⊔ l a₂

theorem GaloisConnection.u_inf {α : Type u} {β : Type v} {b₁ : β} {b₂ : β} [SemilatticeInf α] [SemilatticeInf β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : u (b₁ ⊓ b₂) = u b₁ ⊓ u b₂

theorem GaloisConnection.l_iSup {α : Type u} {β : Type v} {ι : Sort x} [CompleteLattice α] [CompleteLattice β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {f : ι → α} : l (iSup f) = ⨆ (i : ι), l (f i)

theorem GaloisConnection.l_iSup₂ {α : Type u} {β : Type v} {ι : Sort x} {κ : ι → Sort u_1} [CompleteLattice α] [CompleteLattice β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {f : (i : ι) → κ i → α} : l (⨆ (i : ι) (j : κ i), f i j) = ⨆ (i : ι) (j : κ i), l (f i j)

theorem GaloisConnection.u_iInf {α : Type u} {β : Type v} {ι : Sort x} [CompleteLattice α] [CompleteLattice β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {f : ι → β} : u (iInf f) = ⨅ (i : ι), u (f i)

theorem GaloisConnection.u_iInf₂ {α : Type u} {β : Type v} {ι : Sort x} {κ : ι → Sort u_1} [CompleteLattice α] [CompleteLattice β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {f : (i : ι) → κ i → β} : u (⨅ (i : ι) (j : κ i), f i j) = ⨅ (i : ι) (j : κ i), u (f i j)

theorem GaloisConnection.l_sSup {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {s : Set α} : l (sSup s) = ⨆ (a : α) (_ : a ∈ s), l a

theorem GaloisConnection.u_sInf {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {s : Set β} : u (sInf s) = ⨅ (a : β) (_ : a ∈ s), u a

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 => l i (a i)) fun b i => u i (b i)

theorem GaloisConnection.compl {α : Type u} {β : Type v} [BooleanAlgebra α] [BooleanAlgebra β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : GaloisConnection (compl ∘ u ∘ compl) (compl ∘ l ∘ compl)

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)

theorem gc_sSup_Iic {α : Type u} [CompleteSemilatticeSup α] : GaloisConnection sSup Set.Iic

sSup and Iic form a Galois connection.

theorem gc_Ici_sInf {α : Type u} [CompleteSemilatticeInf α] : GaloisConnection (↑OrderDual.toDual ∘ Set.Ici) (sInf ∘ ↑OrderDual.ofDual)

toDual ∘ Ici and sInf ∘ ofDual form a Galois connection.

theorem sSup_image2_eq_sSup_sSup {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)) : sSup (Set.image2 l s t) = l (sSup s) (sSup t)

theorem sSup_image2_eq_sSup_sInf {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a ∘ ↑OrderDual.ofDual) (↑OrderDual.toDual ∘ u₂ a)) : sSup (Set.image2 l s t) = l (sSup s) (sInf t)

theorem sSup_image2_eq_sInf_sSup {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b ∘ ↑OrderDual.ofDual) (↑OrderDual.toDual ∘ u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)) : sSup (Set.image2 l s t) = l (sInf s) (sSup t)

theorem sSup_image2_eq_sInf_sInf {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b ∘ ↑OrderDual.ofDual) (↑OrderDual.toDual ∘ u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a ∘ ↑OrderDual.ofDual) (↑OrderDual.toDual ∘ u₂ a)) : sSup (Set.image2 l s t) = l (sInf s) (sInf t)

theorem sInf_image2_eq_sInf_sInf {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (l₁ b) (Function.swap u b)) (h₂ : ∀ (a : α), GaloisConnection (l₂ a) (u a)) : sInf (Set.image2 u s t) = u (sInf s) (sInf t)

theorem sInf_image2_eq_sInf_sSup {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (l₁ b) (Function.swap u b)) (h₂ : ∀ (a : α), GaloisConnection (↑OrderDual.toDual ∘ l₂ a) (u a ∘ ↑OrderDual.ofDual)) : sInf (Set.image2 u s t) = u (sInf s) (sSup t)

theorem sInf_image2_eq_sSup_sInf {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (↑OrderDual.toDual ∘ l₁ b) (Function.swap u b ∘ ↑OrderDual.ofDual)) (h₂ : ∀ (a : α), GaloisConnection (l₂ a) (u a)) : sInf (Set.image2 u s t) = u (sSup s) (sInf t)

theorem sInf_image2_eq_sSup_sSup {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (↑OrderDual.toDual ∘ l₁ b) (Function.swap u b ∘ ↑OrderDual.ofDual)) (h₂ : ∀ (a : α), GaloisConnection (↑OrderDual.toDual ∘ l₂ a) (u a ∘ ↑OrderDual.ofDual)) : sInf (Set.image2 u s t) = u (sSup s) (sSup t)

@[simp]

theorem OrderIso.bddAbove_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] (e : α ≃o β) {s : Set α} : BddAbove (↑e '' s) ↔ BddAbove s

@[simp]

theorem OrderIso.bddBelow_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] (e : α ≃o β) {s : Set α} : BddBelow (↑e '' s) ↔ BddBelow s

@[simp]

theorem OrderIso.bddAbove_preimage {α : Type u} {β : Type v} [Preorder α] [Preorder β] (e : α ≃o β) {s : Set β} : BddAbove (↑e ⁻¹' s) ↔ BddAbove s

@[simp]

theorem OrderIso.bddBelow_preimage {α : Type u} {β : Type v} [Preorder α] [Preorder β] (e : α ≃o β) {s : Set β} : BddBelow (↑e ⁻¹' s) ↔ BddBelow s

theorem Nat.galoisConnection_mul_div {k : ℕ} (h : 0 < k) : GaloisConnection (fun n => n * k) fun n => n / k

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

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

  A contructive 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), GaloisInsertion.choice s a h = l a

  Property of the choice function.

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

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.

def OrderIso.toGaloisInsertion {α : Type u} {β : Type v} [Preorder α] [Preorder β] (oi : α ≃o β) : GaloisInsertion ↑oi ↑(OrderIso.symm oi)

Makes a Galois insertion from an order-preserving bijection.

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)

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

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.l_sup_u {α : Type u} {β : Type v} {l : α → β} {u : β → α} [SemilatticeSup α] [SemilatticeSup β] (gi : GaloisInsertion l u) (a : β) (b : β) : l (u a ⊔ u b) = a ⊔ b

theorem GaloisInsertion.l_iSup_u {α : Type u} {β : Type v} {l : α → β} {u : β → α} [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) {ι : Sort x} (f : ι → β) : l (⨆ (i : ι), u (f i)) = ⨆ (i : ι), f i

theorem GaloisInsertion.l_biSup_u {α : Type u} {β : Type v} {l : α → β} {u : β → α} [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) {ι : Sort x} {p : ι → Prop} (f : (i : ι) → p i → β) : l (⨆ (i : ι) (hi : p i), u (f i hi)) = ⨆ (i : ι) (hi : p i), f i hi

theorem GaloisInsertion.l_sSup_u_image {α : Type u} {β : Type v} {l : α → β} {u : β → α} [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) (s : Set β) : l (sSup (u '' s)) = sSup s

theorem GaloisInsertion.l_inf_u {α : Type u} {β : Type v} {l : α → β} {u : β → α} [SemilatticeInf α] [SemilatticeInf β] (gi : GaloisInsertion l u) (a : β) (b : β) : l (u a ⊓ u b) = a ⊓ b

theorem GaloisInsertion.l_iInf_u {α : Type u} {β : Type v} {l : α → β} {u : β → α} [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) {ι : Sort x} (f : ι → β) : l (⨅ (i : ι), u (f i)) = ⨅ (i : ι), f i

theorem GaloisInsertion.l_biInf_u {α : Type u} {β : Type v} {l : α → β} {u : β → α} [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) {ι : Sort x} {p : ι → Prop} (f : (i : ι) → p i → β) : l (⨅ (i : ι) (hi : p i), u (f i hi)) = ⨅ (i : ι) (hi : p i), f i hi

theorem GaloisInsertion.l_sInf_u_image {α : Type u} {β : Type v} {l : α → β} {u : β → α} [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) (s : Set β) : l (sInf (u '' s)) = sInf s

theorem GaloisInsertion.l_iInf_of_ul_eq_self {α : Type u} {β : Type v} {l : α → β} {u : β → α} [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) {ι : Sort x} (f : ι → α) (hf : ∀ (i : ι), u (l (f i)) = f i) : l (⨅ (i : ι), f i) = ⨅ (i : ι), l (f i)

theorem GaloisInsertion.l_biInf_of_ul_eq_self {α : Type u} {β : Type v} {l : α → β} {u : β → α} [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) {ι : Sort x} {p : ι → Prop} (f : (i : ι) → p i → α) (hf : ∀ (i : ι) (hi : p i), u (l (f i hi)) = f i hi) : l (⨅ (i : ι) (hi : p i), f i hi) = ⨅ (i : ι) (hi : p i), l (f i hi)

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

theorem GaloisInsertion.isLUB_of_u_image {α : Type u} {β : Type v} {l : α → β} {u : β → α} [Preorder α] [Preorder β] (gi : GaloisInsertion l u) {s : Set β} {a : α} (hs : IsLUB (u '' s) a) : IsLUB s (l a)

theorem GaloisInsertion.isGLB_of_u_image {α : Type u} {β : Type v} {l : α → β} {u : β → α} [Preorder α] [Preorder β] (gi : GaloisInsertion l u) {s : Set β} {a : α} (hs : IsGLB (u '' s) a) : IsGLB s (l a)

@[reducible]

def GaloisInsertion.liftSemilatticeSup {α : Type u} {β : Type v} {l : α → β} {u : β → α} [PartialOrder β] [SemilatticeSup α] (gi : GaloisInsertion l u) : SemilatticeSup β

Lift the suprema along a Galois insertion

@[reducible]

def GaloisInsertion.liftSemilatticeInf {α : Type u} {β : Type v} {l : α → β} {u : β → α} [PartialOrder β] [SemilatticeInf α] (gi : GaloisInsertion l u) : SemilatticeInf β

Lift the infima along a Galois insertion

@[reducible]

def GaloisInsertion.liftLattice {α : Type u} {β : Type v} {l : α → β} {u : β → α} [PartialOrder β] [Lattice α] (gi : GaloisInsertion l u) : Lattice β

Lift the suprema and infima along a Galois insertion

@[reducible]

def GaloisInsertion.liftOrderTop {α : Type u} {β : Type v} {l : α → β} {u : β → α} [PartialOrder β] [Preorder α] [OrderTop α] (gi : GaloisInsertion l u) : OrderTop β

Lift the top along a Galois insertion

@[reducible]

def GaloisInsertion.liftBoundedOrder {α : Type u} {β : Type v} {l : α → β} {u : β → α} [PartialOrder β] [Preorder α] [BoundedOrder α] (gi : GaloisInsertion l u) : BoundedOrder β

Lift the top, bottom, suprema, and infima along a Galois insertion

@[reducible]

def GaloisInsertion.liftCompleteLattice {α : Type u} {β : Type v} {l : α → β} {u : β → α} [PartialOrder β] [CompleteLattice α] (gi : GaloisInsertion l u) : CompleteLattice β

Lift all suprema and infima along a Galois insertion

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

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

  A contructive 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)), GaloisCoinsertion.choice s a h = u a

  Property of the choice function.

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

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

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

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 βᵒᵈ.

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 βᵒᵈ.

def OrderIso.toGaloisCoinsertion {α : Type u} {β : Type v} [Preorder α] [Preorder β] (oi : α ≃o β) : GaloisCoinsertion ↑oi ↑(OrderIso.symm oi)

Makes a Galois coinsertion from an order-preserving bijection.

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.

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

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

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.u_inf_l {α : Type u} {β : Type v} {l : α → β} {u : β → α} [SemilatticeInf α] [SemilatticeInf β] (gi : GaloisCoinsertion l u) (a : α) (b : α) : u (l a ⊓ l b) = a ⊓ b

theorem GaloisCoinsertion.u_iInf_l {α : Type u} {β : Type v} {l : α → β} {u : β → α} [CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u) {ι : Sort x} (f : ι → α) : u (⨅ (i : ι), l (f i)) = ⨅ (i : ι), f i

theorem GaloisCoinsertion.u_sInf_l_image {α : Type u} {β : Type v} {l : α → β} {u : β → α} [CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u) (s : Set α) : u (sInf (l '' s)) = sInf s

theorem GaloisCoinsertion.u_sup_l {α : Type u} {β : Type v} {l : α → β} {u : β → α} [SemilatticeSup α] [SemilatticeSup β] (gi : GaloisCoinsertion l u) (a : α) (b : α) : u (l a ⊔ l b) = a ⊔ b

theorem GaloisCoinsertion.u_iSup_l {α : Type u} {β : Type v} {l : α → β} {u : β → α} [CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u) {ι : Sort x} (f : ι → α) : u (⨆ (i : ι), l (f i)) = ⨆ (i : ι), f i

theorem GaloisCoinsertion.u_biSup_l {α : Type u} {β : Type v} {l : α → β} {u : β → α} [CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u) {ι : Sort x} {p : ι → Prop} (f : (i : ι) → p i → α) : u (⨆ (i : ι) (hi : p i), l (f i hi)) = ⨆ (i : ι) (hi : p i), f i hi

theorem GaloisCoinsertion.u_sSup_l_image {α : Type u} {β : Type v} {l : α → β} {u : β → α} [CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u) (s : Set α) : u (sSup (l '' s)) = sSup s

theorem GaloisCoinsertion.u_iSup_of_lu_eq_self {α : Type u} {β : Type v} {l : α → β} {u : β → α} [CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u) {ι : Sort x} (f : ι → β) (hf : ∀ (i : ι), l (u (f i)) = f i) : u (⨆ (i : ι), f i) = ⨆ (i : ι), u (f i)

theorem GaloisCoinsertion.u_biSup_of_lu_eq_self {α : Type u} {β : Type v} {l : α → β} {u : β → α} [CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u) {ι : Sort x} {p : ι → Prop} (f : (i : ι) → p i → β) (hf : ∀ (i : ι) (hi : p i), l (u (f i hi)) = f i hi) : u (⨆ (i : ι) (hi : p i), f i hi) = ⨆ (i : ι) (hi : p i), u (f i hi)

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

theorem GaloisCoinsertion.isGLB_of_l_image {α : Type u} {β : Type v} {l : α → β} {u : β → α} [Preorder α] [Preorder β] (gi : GaloisCoinsertion l u) {s : Set α} {a : β} (hs : IsGLB (l '' s) a) : IsGLB s (u a)

theorem GaloisCoinsertion.isLUB_of_l_image {α : Type u} {β : Type v} {l : α → β} {u : β → α} [Preorder α] [Preorder β] (gi : GaloisCoinsertion l u) {s : Set α} {a : β} (hs : IsLUB (l '' s) a) : IsLUB s (u a)

@[reducible]

def GaloisCoinsertion.liftSemilatticeInf {α : Type u} {β : Type v} {l : α → β} {u : β → α} [PartialOrder α] [SemilatticeInf β] (gi : GaloisCoinsertion l u) : SemilatticeInf α

Lift the infima along a Galois coinsertion

@[reducible]

def GaloisCoinsertion.liftSemilatticeSup {α : Type u} {β : Type v} {l : α → β} {u : β → α} [PartialOrder α] [SemilatticeSup β] (gi : GaloisCoinsertion l u) : SemilatticeSup α

Lift the suprema along a Galois coinsertion

@[reducible]

def GaloisCoinsertion.liftLattice {α : Type u} {β : Type v} {l : α → β} {u : β → α} [PartialOrder α] [Lattice β] (gi : GaloisCoinsertion l u) : Lattice α

Lift the suprema and infima along a Galois coinsertion

@[reducible]

def GaloisCoinsertion.liftOrderBot {α : Type u} {β : Type v} {l : α → β} {u : β → α} [PartialOrder α] [Preorder β] [OrderBot β] (gi : GaloisCoinsertion l u) : OrderBot α

Lift the bot along a Galois coinsertion

@[reducible]

def GaloisCoinsertion.liftBoundedOrder {α : Type u} {β : Type v} {l : α → β} {u : β → α} [PartialOrder α] [Preorder β] [BoundedOrder β] (gi : GaloisCoinsertion l u) : BoundedOrder α

Lift the top, bottom, suprema, and infima along a Galois coinsertion

@[reducible]

def GaloisCoinsertion.liftCompleteLattice {α : Type u} {β : Type v} {l : α → β} {u : β → α} [PartialOrder α] [CompleteLattice β] (gi : GaloisCoinsertion l u) : CompleteLattice α

Lift all suprema and infima along a Galois coinsertion

def gi_sSup_Iic {α : Type u} [CompleteSemilatticeSup α] : GaloisInsertion sSup Set.Iic

sSup and Iic form a Galois insertion.

def gci_Ici_sInf {α : Type u} [CompleteSemilatticeInf α] : GaloisCoinsertion (↑OrderDual.toDual ∘ Set.Ici) (sInf ∘ ↑OrderDual.ofDual)

toDual ∘ Ici and sInf ∘ ofDual form a Galois coinsertion.

def WithBot.giUnbot'Bot {α : Type u} [Preorder α] [OrderBot α] : GaloisInsertion (WithBot.unbot' ⊥) WithBot.some

If α is a partial order with bottom element (e.g., ℕ, ℝ≥0), then WithBot.unbot' ⊥ and coercion form a Galois insertion.