# 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} [] [] (l : αβ) (u : βα) :

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
Instances For
theorem OrderIso.to_galoisConnection {α : Type u} {β : Type v} [] [] (oi : α ≃o β) :
GaloisConnection oi oi.symm

Makes a Galois connection from an order-preserving bijection.

theorem GaloisConnection.monotone_intro {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (hu : ) (hl : ) (hul : ∀ (a : α), a u (l a)) (hlu : ∀ (a : β), l (u a) a) :
theorem GaloisConnection.dual {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (gc : ) :
GaloisConnection (OrderDual.toDual u OrderDual.ofDual) (OrderDual.toDual l OrderDual.ofDual)
theorem GaloisConnection.le_iff_le {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (gc : ) {a : α} {b : β} :
l a b a u b
theorem GaloisConnection.l_le {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (gc : ) {a : α} {b : β} :
a u bl a b
theorem GaloisConnection.le_u {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (gc : ) {a : α} {b : β} :
l a ba u b
theorem GaloisConnection.le_u_l {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (gc : ) (a : α) :
a u (l a)
theorem GaloisConnection.l_u_le {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (gc : ) (a : β) :
l (u a) a
theorem GaloisConnection.monotone_u {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (gc : ) :
theorem GaloisConnection.monotone_l {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (gc : ) :
theorem GaloisConnection.upperBounds_l_image {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (gc : ) (s : Set α) :
theorem GaloisConnection.lowerBounds_u_image {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (gc : ) (s : Set β) :
theorem GaloisConnection.bddAbove_l_image {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (gc : ) {s : Set α} :
BddAbove (l '' s)
theorem GaloisConnection.bddBelow_u_image {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (gc : ) {s : Set β} :
BddBelow (u '' s)
theorem GaloisConnection.isLUB_l_image {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (gc : ) {s : Set α} {a : α} (h : IsLUB s a) :
IsLUB (l '' s) (l a)
theorem GaloisConnection.isGLB_u_image {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (gc : ) {s : Set β} {b : β} (h : IsGLB s b) :
IsGLB (u '' s) (u b)
theorem GaloisConnection.isLeast_l {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (gc : ) {a : α} :
IsLeast {b : β | a u b} (l a)
theorem GaloisConnection.isGreatest_u {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (gc : ) {b : β} :
IsGreatest {a : α | l a b} (u b)
theorem GaloisConnection.isGLB_l {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (gc : ) {a : α} :
IsGLB {b : β | a u b} (l a)
theorem GaloisConnection.isLUB_u {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (gc : ) {b : β} :
IsLUB {a : α | l a b} (u b)
theorem GaloisConnection.le_u_l_trans {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (gc : ) {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} [] [] {l : αβ} {u : βα} (gc : ) {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} [] [] {l : αβ} {u : βα} (gc : ) (b : β) :
u (l (u b)) = u b
theorem GaloisConnection.u_l_u_eq_u' {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (gc : ) :
u l u = u
theorem GaloisConnection.u_unique {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (gc : ) {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} [] [] {l : αβ} {u : βα} (gc : ) (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} [] [] {l : αβ} {u : βα} (gc : ) {z : α} {y : β} :
u y = z ∀ (x : α), x z l x y
theorem GaloisConnection.l_u_l_eq_l {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (gc : ) (a : α) :
l (u (l a)) = l a
theorem GaloisConnection.l_u_l_eq_l' {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (gc : ) :
l u l = l
theorem GaloisConnection.l_unique {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (gc : ) {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} [] [] {l : αβ} {u : βα} (gc : ) (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} [] [] {l : αβ} {u : βα} (gc : ) {x : α} {z : β} :
l x = z ∀ (y : β), z y x u y
theorem GaloisConnection.u_eq_top {α : Type u} {β : Type v} [] [] [] {l : αβ} {u : βα} (gc : ) {x : β} :
u x = l x
theorem GaloisConnection.u_top {α : Type u} {β : Type v} [] [] [] [] {l : αβ} {u : βα} (gc : ) :
theorem GaloisConnection.l_eq_bot {α : Type u} {β : Type v} [] [] [] {l : αβ} {u : βα} (gc : ) {x : α} :
l x = x u
theorem GaloisConnection.l_bot {α : Type u} {β : Type v} [] [] [] [] {l : αβ} {u : βα} (gc : ) :
theorem GaloisConnection.l_sup {α : Type u} {β : Type v} {a₁ : α} {a₂ : α} [] [] {l : αβ} {u : βα} (gc : ) :
l (a₁ a₂) = l a₁ l a₂
theorem GaloisConnection.u_inf {α : Type u} {β : Type v} {b₁ : β} {b₂ : β} [] [] {l : αβ} {u : βα} (gc : ) :
u (b₁ b₂) = u b₁ u b₂
theorem GaloisConnection.l_iSup {α : Type u} {β : Type v} {ι : Sort x} [] [] {l : αβ} {u : βα} (gc : ) {f : ια} :
l (iSup f) = ⨆ (i : ι), l (f i)
theorem GaloisConnection.l_iSup₂ {α : Type u} {β : Type v} {ι : Sort x} {κ : ιSort u_1} [] [] {l : αβ} {u : βα} (gc : ) {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} [] [] {l : αβ} {u : βα} (gc : ) {f : ιβ} :
u (iInf f) = ⨅ (i : ι), u (f i)
theorem GaloisConnection.u_iInf₂ {α : Type u} {β : Type v} {ι : Sort x} {κ : ιSort u_1} [] [] {l : αβ} {u : βα} (gc : ) {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} [] [] {l : αβ} {u : βα} (gc : ) {s : Set α} :
l (sSup s) = as, l a
theorem GaloisConnection.u_sInf {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (gc : ) {s : Set β} :
u (sInf s) = as, u a
theorem GaloisConnection.lt_iff_lt {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (gc : ) {a : α} {b : β} :
b < l a u b < a
theorem GaloisConnection.id {α : Type u} [pα : ] :
theorem GaloisConnection.compose {α : Type u} {β : Type v} {γ : Type w} [] [] [] {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.compl {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (gc : ) :
GaloisConnection (compl u compl) (compl l compl)
theorem GaloisConnection.l_comm_of_u_comm {X : Type u_2} [] {Y : Type u_3} [] {Z : Type u_4} [] {W : Type u_5} [] {lYX : XY} {uXY : YX} (hXY : GaloisConnection lYX uXY) {lWZ : ZW} {uZW : WZ} (hZW : GaloisConnection lWZ uZW) {lWY : YW} {uYW : WY} (hWY : GaloisConnection lWY uYW) {lZX : XZ} {uXZ : ZX} (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} [] {Y : Type u_3} [] {Z : Type u_4} [] {W : Type u_5} [] {lYX : XY} {uXY : YX} (hXY : GaloisConnection lYX uXY) {lWZ : ZW} {uZW : WZ} (hZW : GaloisConnection lWZ uZW) {lWY : YW} {uYW : WY} (hWY : GaloisConnection lWY uYW) {lZX : XZ} {uXZ : ZX} (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} [] {Y : Type u_3} [] {Z : Type u_4} [] {W : Type u_5} [] {lYX : XY} {uXY : YX} (hXY : GaloisConnection lYX uXY) {lWZ : ZW} {uZW : WZ} (hZW : GaloisConnection lWZ uZW) {lWY : YW} {uYW : WY} (hWY : GaloisConnection lWY uYW) {lZX : XZ} {uXZ : ZX} (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} :
GaloisConnection sSup Set.Iic

sSup and Iic form a Galois connection.

theorem gc_Ici_sInf {α : Type u} :
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} [] [] [] {s : Set α} {t : Set β} {l : αβγ} {u₁ : βγα} {u₂ : αγβ} (h₁ : ∀ (b : β), GaloisConnection () (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} [] [] [] {s : Set α} {t : Set β} {l : αβγ} {u₁ : βγα} {u₂ : αγβ} (h₁ : ∀ (b : β), GaloisConnection () (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} [] [] [] {s : Set α} {t : Set β} {l : αβγ} {u₁ : βγα} {u₂ : αγβ} (h₁ : ∀ (b : β), GaloisConnection ( 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} [] [] [] {s : Set α} {t : Set β} {l : αβγ} {u₁ : βγα} {u₂ : αγβ} (h₁ : ∀ (b : β), GaloisConnection ( 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} [] [] [] {s : Set α} {t : Set β} {u : αβγ} {l₁ : βγα} {l₂ : αγβ} (h₁ : ∀ (b : β), GaloisConnection (l₁ 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} [] [] [] {s : Set α} {t : Set β} {u : αβγ} {l₁ : βγα} {l₂ : αγβ} (h₁ : ∀ (b : β), GaloisConnection (l₁ 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} [] [] [] {s : Set α} {t : Set β} {u : αβγ} {l₁ : βγα} {l₂ : αγβ} (h₁ : ∀ (b : β), GaloisConnection (OrderDual.toDual l₁ 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} [] [] [] {s : Set α} {t : Set β} {u : αβγ} {l₁ : βγα} {l₂ : αγβ} (h₁ : ∀ (b : β), GaloisConnection (OrderDual.toDual l₁ 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} [] [] (e : α ≃o β) {s : Set α} :
BddAbove (e '' s)
@[simp]
theorem OrderIso.bddBelow_image {α : Type u} {β : Type v} [] [] (e : α ≃o β) {s : Set α} :
BddBelow (e '' s)
@[simp]
theorem OrderIso.bddAbove_preimage {α : Type u} {β : Type v} [] [] (e : α ≃o β) {s : Set β} :
BddAbove (e ⁻¹' s)
@[simp]
theorem OrderIso.bddBelow_preimage {α : Type u} {β : Type v} [] [] (e : α ≃o β) {s : Set β} :
BddBelow (e ⁻¹' 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} [] [] (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 contructive choice function for images of l.

• gc :

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.

Instances For
theorem GaloisInsertion.gc {α : Type u_2} {β : Type u_3} [] [] {l : αβ} {u : βα} (self : ) :

The Galois connection associated to a Galois insertion.

theorem GaloisInsertion.le_l_u {α : Type u_2} {β : Type u_3} [] [] {l : αβ} {u : βα} (self : ) (x : β) :
x l (u x)

Main property of a Galois insertion.

theorem GaloisInsertion.choice_eq {α : Type u_2} {β : Type u_3} [] [] {l : αβ} {u : βα} (self : ) (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} [] [] {l : αβ} {u : βα} (hu : ) (hl : ) (hul : ∀ (a : α), a u (l a)) (hlu : ∀ (b : β), l (u b) = b) :

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

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

Makes a Galois insertion from an order-preserving bijection.

Equations
• oi.toGaloisInsertion = { choice := fun (b : α) (x : oi.symm (oi b) b) => oi b, gc := , le_l_u := , choice_eq := }
Instances For
def GaloisConnection.toGaloisInsertion {α : Type u_2} {β : Type u_3} [] [] {l : αβ} {u : βα} (gc : ) (h : ∀ (b : β), b l (u b)) :

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 := }
Instances For
def GaloisConnection.liftOrderBot {α : Type u_2} {β : Type u_3} [] [] [] {l : αβ} {u : βα} (gc : ) :

Lift the bottom along a Galois connection

Equations
• gc.liftOrderBot =
Instances For
theorem GaloisInsertion.l_u_eq {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) (b : β) :
l (u b) = b
theorem GaloisInsertion.leftInverse_l_u {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) :
theorem GaloisInsertion.l_top {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] [] [] (gi : ) :
theorem GaloisInsertion.l_surjective {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) :
theorem GaloisInsertion.u_injective {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) :
theorem GaloisInsertion.l_sup_u {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) (a : β) (b : β) :
l (u a u b) = a b
theorem GaloisInsertion.l_iSup_u {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) {ι : Sort x} (f : ιβ) :
l (⨆ (i : ι), u (f i)) = ⨆ (i : ι), f i
theorem GaloisInsertion.l_biSup_u {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) {ι : 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 : βα} [] [] (gi : ) (s : Set β) :
l (sSup (u '' s)) = sSup s
theorem GaloisInsertion.l_inf_u {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) (a : β) (b : β) :
l (u a u b) = a b
theorem GaloisInsertion.l_iInf_u {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) {ι : Sort x} (f : ιβ) :
l (⨅ (i : ι), u (f i)) = ⨅ (i : ι), f i
theorem GaloisInsertion.l_biInf_u {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) {ι : 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 : βα} [] [] (gi : ) (s : Set β) :
l (sInf (u '' s)) = sInf s
theorem GaloisInsertion.l_iInf_of_ul_eq_self {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) {ι : 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 : βα} [] [] (gi : ) {ι : 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 : βα} [] [] (gi : ) {a : β} {b : β} :
u a u b a b
theorem GaloisInsertion.strictMono_u {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) :
theorem GaloisInsertion.isLUB_of_u_image {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) {s : Set β} {a : α} (hs : IsLUB (u '' s) a) :
IsLUB s (l a)
theorem GaloisInsertion.isGLB_of_u_image {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) {s : Set β} {a : α} (hs : IsGLB (u '' s) a) :
IsGLB s (l a)
@[reducible, inline]
abbrev GaloisInsertion.liftSemilatticeSup {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) :

Lift the suprema along a Galois insertion

Equations
• gi.liftSemilatticeSup = let __src := inst✝;
Instances For
@[reducible, inline]
abbrev GaloisInsertion.liftSemilatticeInf {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) :

Lift the infima along a Galois insertion

Equations
• gi.liftSemilatticeInf = let __src := inst✝;
Instances For
@[reducible, inline]
abbrev GaloisInsertion.liftLattice {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) :

Lift the suprema and infima along a Galois insertion

Equations
• gi.liftLattice = let __src := gi.liftSemilatticeSup; let __src_1 := gi.liftSemilatticeInf; Lattice.mk
Instances For
@[reducible, inline]
abbrev GaloisInsertion.liftOrderTop {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] [] (gi : ) :

Lift the top along a Galois insertion

Equations
• gi.liftOrderTop =
Instances For
@[reducible, inline]
abbrev GaloisInsertion.liftBoundedOrder {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] [] (gi : ) :

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

Equations
• gi.liftBoundedOrder = let __src := gi.liftOrderTop; let __src_1 := .liftOrderBot; BoundedOrder.mk
Instances For
@[reducible, inline]
abbrev GaloisInsertion.liftCompleteLattice {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) :

Lift all suprema and infima along a Galois insertion

Equations
• gi.liftCompleteLattice = let __src := gi.liftBoundedOrder; let __src_1 := gi.liftLattice; CompleteLattice.mk
Instances For
structure GaloisCoinsertion {α : Type u} {β : Type v} [] [] (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 contructive choice function for images of u.

• gc :

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.

Instances For
theorem GaloisCoinsertion.gc {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (self : ) :

The Galois connection associated to a Galois coinsertion.

theorem GaloisCoinsertion.u_l_le {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (self : ) (x : α) :
u (l x) x

Main property of a Galois coinsertion.

theorem GaloisCoinsertion.choice_eq {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (self : ) (a : β) (h : a l (u a)) :
self.choice a h = u a

Property of the choice function.

def GaloisCoinsertion.dual {α : Type u} {β : Type v} [] [] {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 := }
Instances For
def GaloisInsertion.dual {α : Type u} {β : Type v} [] [] {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 := }
Instances For
def GaloisCoinsertion.ofDual {α : Type u} {β : Type v} [] [] {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 := }
Instances For
def GaloisInsertion.ofDual {α : Type u} {β : Type v} [] [] {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 := }
Instances For
def OrderIso.toGaloisCoinsertion {α : Type u} {β : Type v} [] [] (oi : α ≃o β) :
GaloisCoinsertion oi oi.symm

Makes a Galois coinsertion from an order-preserving bijection.

Equations
• oi.toGaloisCoinsertion = { choice := fun (b : β) (x : b oi (oi.symm b)) => oi.symm b, gc := , u_l_le := , choice_eq := }
Instances For
def GaloisCoinsertion.monotoneIntro {α : Type u} {β : Type v} [] [] {l : αβ} {u : βα} (hu : ) (hl : ) (hlu : ∀ (b : β), l (u b) b) (hul : ∀ (a : α), u (l a) = a) :

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

Equations
Instances For
def GaloisConnection.toGaloisCoinsertion {α : Type u_2} {β : Type u_3} [] [] {l : αβ} {u : βα} (gc : ) (h : ∀ (a : α), u (l a) a) :

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 := }
Instances For
def GaloisConnection.liftOrderTop {α : Type u_2} {β : Type u_3} [] [] [] {l : αβ} {u : βα} (gc : ) :

Lift the top along a Galois connection

Equations
• gc.liftOrderTop =
Instances For
theorem GaloisCoinsertion.u_l_eq {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) (a : α) :
u (l a) = a
theorem GaloisCoinsertion.u_l_leftInverse {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) :
theorem GaloisCoinsertion.u_bot {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] [] [] (gi : ) :
theorem GaloisCoinsertion.u_surjective {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) :
theorem GaloisCoinsertion.l_injective {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) :
theorem GaloisCoinsertion.u_inf_l {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) (a : α) (b : α) :
u (l a l b) = a b
theorem GaloisCoinsertion.u_iInf_l {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) {ι : Sort x} (f : ια) :
u (⨅ (i : ι), l (f i)) = ⨅ (i : ι), f i
theorem GaloisCoinsertion.u_sInf_l_image {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) (s : Set α) :
u (sInf (l '' s)) = sInf s
theorem GaloisCoinsertion.u_sup_l {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) (a : α) (b : α) :
u (l a l b) = a b
theorem GaloisCoinsertion.u_iSup_l {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) {ι : Sort x} (f : ια) :
u (⨆ (i : ι), l (f i)) = ⨆ (i : ι), f i
theorem GaloisCoinsertion.u_biSup_l {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) {ι : 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 : βα} [] [] (gi : ) (s : Set α) :
u (sSup (l '' s)) = sSup s
theorem GaloisCoinsertion.u_iSup_of_lu_eq_self {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) {ι : 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 : βα} [] [] (gi : ) {ι : 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 : βα} [] [] (gi : ) {a : α} {b : α} :
l a l b a b
theorem GaloisCoinsertion.strictMono_l {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) :
theorem GaloisCoinsertion.isGLB_of_l_image {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) {s : Set α} {a : β} (hs : IsGLB (l '' s) a) :
IsGLB s (u a)
theorem GaloisCoinsertion.isLUB_of_l_image {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) {s : Set α} {a : β} (hs : IsLUB (l '' s) a) :
IsLUB s (u a)
@[reducible, inline]
abbrev GaloisCoinsertion.liftSemilatticeInf {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) :

Lift the infima along a Galois coinsertion

Equations
• gi.liftSemilatticeInf = let __src := inst✝;
Instances For
@[reducible, inline]
abbrev GaloisCoinsertion.liftSemilatticeSup {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) :

Lift the suprema along a Galois coinsertion

Equations
• gi.liftSemilatticeSup = let __src := inst✝;
Instances For
@[reducible, inline]
abbrev GaloisCoinsertion.liftLattice {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) :

Lift the suprema and infima along a Galois coinsertion

Equations
• gi.liftLattice = let __src := gi.liftSemilatticeSup; let __src_1 := gi.liftSemilatticeInf; Lattice.mk
Instances For
@[reducible, inline]
abbrev GaloisCoinsertion.liftOrderBot {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] [] (gi : ) :

Lift the bot along a Galois coinsertion

Equations
• gi.liftOrderBot = let __src := ;
Instances For
@[reducible, inline]
abbrev GaloisCoinsertion.liftBoundedOrder {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] [] (gi : ) :

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

Equations
• gi.liftBoundedOrder = let __src := gi.liftOrderBot; let __src_1 := .liftOrderTop; BoundedOrder.mk
Instances For
@[reducible, inline]
abbrev GaloisCoinsertion.liftCompleteLattice {α : Type u} {β : Type v} {l : αβ} {u : βα} [] [] (gi : ) :

Lift all suprema and infima along a Galois coinsertion

Equations
• gi.liftCompleteLattice = let __src := OrderDual.instCompleteLattice; CompleteLattice.mk
Instances For
def gi_sSup_Iic {α : Type u} :
GaloisInsertion sSup Set.Iic

sSup and Iic form a Galois insertion.

Equations
• gi_sSup_Iic = .toGaloisInsertion
Instances For
def gci_Ici_sInf {α : Type u} :
GaloisCoinsertion (OrderDual.toDual Set.Ici) (sInf OrderDual.ofDual)

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

Equations
• gci_Ici_sInf = .toGaloisCoinsertion
Instances For
def WithBot.giUnbot'Bot {α : Type u} [] [] :
GaloisInsertion WithBot.some

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

Equations
• WithBot.giUnbot'Bot = { choice := fun (o : ) (x : () o) => , gc := , le_l_u := , choice_eq := }
Instances For