mathlib3 documentation

order.galois_connection

Galois connections, insertions and coinsertions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

galois_connection: 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.
galois_insertion: A Galois insertion is a Galois connection where l ∘ u = id
galois_coinsertion: 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 galois_insertion 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 galois_connection {α : 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

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

theorem order_iso.to_galois_connection {α : Type u} {β : Type v} [preorder α] [preorder β] (oi : α ≃o β) :

galois_connection ⇑oi ⇑(oi.symm)

Makes a Galois connection from an order-preserving bijection.

theorem galois_connection.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) :

galois_connection l u

@[protected]

theorem galois_connection.dual {α : Type u} {β : Type v} [preorder α] [preorder β] {l : α → β} {u : β → α} (gc : galois_connection l u) :

galois_connection (⇑order_dual.to_dual ∘ u ∘ ⇑order_dual.of_dual) (⇑order_dual.to_dual ∘ l ∘ ⇑order_dual.of_dual)

theorem galois_connection.le_iff_le {α : Type u} {β : Type v} [preorder α] [preorder β] {l : α → β} {u : β → α} (gc : galois_connection l u) {a : α} {b : β} :

l a ≤ b ↔ a ≤ u b

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

a ≤ u b → l a ≤ b

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

l a ≤ b → a ≤ u b

theorem galois_connection.le_u_l {α : Type u} {β : Type v} [preorder α] [preorder β] {l : α → β} {u : β → α} (gc : galois_connection l u) (a : α) :

a ≤ u (l a)

theorem galois_connection.l_u_le {α : Type u} {β : Type v} [preorder α] [preorder β] {l : α → β} {u : β → α} (gc : galois_connection l u) (a : β) :

l (u a) ≤ a

theorem galois_connection.monotone_u {α : Type u} {β : Type v} [preorder α] [preorder β] {l : α → β} {u : β → α} (gc : galois_connection l u) :

theorem galois_connection.monotone_l {α : Type u} {β : Type v} [preorder α] [preorder β] {l : α → β} {u : β → α} (gc : galois_connection l u) :

theorem galois_connection.upper_bounds_l_image {α : Type u} {β : Type v} [preorder α] [preorder β] {l : α → β} {u : β → α} (gc : galois_connection l u) (s : set α) :

upper_bounds (l '' s) = u ⁻¹' upper_bounds s

theorem galois_connection.lower_bounds_u_image {α : Type u} {β : Type v} [preorder α] [preorder β] {l : α → β} {u : β → α} (gc : galois_connection l u) (s : set β) :

lower_bounds (u '' s) = l ⁻¹' lower_bounds s

theorem galois_connection.bdd_above_l_image {α : Type u} {β : Type v} [preorder α] [preorder β] {l : α → β} {u : β → α} (gc : galois_connection l u) {s : set α} :

bdd_above (l '' s) ↔ bdd_above s

theorem galois_connection.bdd_below_u_image {α : Type u} {β : Type v} [preorder α] [preorder β] {l : α → β} {u : β → α} (gc : galois_connection l u) {s : set β} :

bdd_below (u '' s) ↔ bdd_below s

theorem galois_connection.is_lub_l_image {α : Type u} {β : Type v} [preorder α] [preorder β] {l : α → β} {u : β → α} (gc : galois_connection l u) {s : set α} {a : α} (h : is_lub s a) :

is_lub (l '' s) (l a)

theorem galois_connection.is_glb_u_image {α : Type u} {β : Type v} [preorder α] [preorder β] {l : α → β} {u : β → α} (gc : galois_connection l u) {s : set β} {b : β} (h : is_glb s b) :

is_glb (u '' s) (u b)

theorem galois_connection.is_least_l {α : Type u} {β : Type v} [preorder α] [preorder β] {l : α → β} {u : β → α} (gc : galois_connection l u) {a : α} :

is_least {b : β | a ≤ u b} (l a)

theorem galois_connection.is_greatest_u {α : Type u} {β : Type v} [preorder α] [preorder β] {l : α → β} {u : β → α} (gc : galois_connection l u) {b : β} :

is_greatest {a : α | l a ≤ b} (u b)

theorem galois_connection.is_glb_l {α : Type u} {β : Type v} [preorder α] [preorder β] {l : α → β} {u : β → α} (gc : galois_connection l u) {a : α} :

is_glb {b : β | a ≤ u b} (l a)

theorem galois_connection.is_lub_u {α : Type u} {β : Type v} [preorder α] [preorder β] {l : α → β} {u : β → α} (gc : galois_connection l u) {b : β} :

is_lub {a : α | l a ≤ b} (u b)

theorem galois_connection.le_u_l_trans {α : Type u} {β : Type v} [preorder α] [preorder β] {l : α → β} {u : β → α} (gc : galois_connection 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 galois_connection.l_u_le_trans {α : Type u} {β : Type v} [preorder α] [preorder β] {l : α → β} {u : β → α} (gc : galois_connection l u) {x y z : β} (hxy : l (u x) ≤ y) (hyz : l (u y) ≤ z) :

l (u x) ≤ z

theorem galois_connection.u_l_u_eq_u {α : Type u} {β : Type v} [partial_order α] [preorder β] {l : α → β} {u : β → α} (gc : galois_connection l u) (b : β) :

u (l (u b)) = u b

theorem galois_connection.u_l_u_eq_u' {α : Type u} {β : Type v} [partial_order α] [preorder β] {l : α → β} {u : β → α} (gc : galois_connection l u) :

u ∘ l ∘ u = u

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

u b = u' b

theorem galois_connection.exists_eq_u {α : Type u} {β : Type v} [partial_order α] [preorder β] {l : α → β} {u : β → α} (gc : galois_connection 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 galois_connection.u_eq {α : Type u} {β : Type v} [partial_order α] [preorder β] {l : α → β} {u : β → α} (gc : galois_connection l u) {z : α} {y : β} :

u y = z ↔ ∀ (x : α), x ≤ z ↔ l x ≤ y

theorem galois_connection.l_u_l_eq_l {α : Type u} {β : Type v} [preorder α] [partial_order β] {l : α → β} {u : β → α} (gc : galois_connection l u) (a : α) :

l (u (l a)) = l a

theorem galois_connection.l_u_l_eq_l' {α : Type u} {β : Type v} [preorder α] [partial_order β] {l : α → β} {u : β → α} (gc : galois_connection l u) :

l ∘ u ∘ l = l

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

l a = l' a

theorem galois_connection.exists_eq_l {α : Type u} {β : Type v} [preorder α] [partial_order β] {l : α → β} {u : β → α} (gc : galois_connection 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 galois_connection.l_eq {α : Type u} {β : Type v} [preorder α] [partial_order β] {l : α → β} {u : β → α} (gc : galois_connection l u) {x : α} {z : β} :

l x = z ↔ ∀ (y : β), z ≤ y ↔ x ≤ u y

theorem galois_connection.u_eq_top {α : Type u} {β : Type v} [partial_order α] [preorder β] [order_top α] {l : α → β} {u : β → α} (gc : galois_connection l u) {x : β} :

u x = ⊤ ↔ l ⊤ ≤ x

theorem galois_connection.u_top {α : Type u} {β : Type v} [partial_order α] [preorder β] [order_top α] [order_top β] {l : α → β} {u : β → α} (gc : galois_connection l u) :

theorem galois_connection.l_eq_bot {α : Type u} {β : Type v} [preorder α] [partial_order β] [order_bot β] {l : α → β} {u : β → α} (gc : galois_connection l u) {x : α} :

l x = ⊥ ↔ x ≤ u ⊥

theorem galois_connection.l_bot {α : Type u} {β : Type v} [preorder α] [partial_order β] [order_bot β] [order_bot α] {l : α → β} {u : β → α} (gc : galois_connection l u) :

theorem galois_connection.l_sup {α : Type u} {β : Type v} {a₁ a₂ : α} [semilattice_sup α] [semilattice_sup β] {l : α → β} {u : β → α} (gc : galois_connection l u) :

l (a₁ ⊔ a₂) = l a₁ ⊔ l a₂

theorem galois_connection.u_inf {α : Type u} {β : Type v} {b₁ b₂ : β} [semilattice_inf α] [semilattice_inf β] {l : α → β} {u : β → α} (gc : galois_connection l u) :

u (b₁ ⊓ b₂) = u b₁ ⊓ u b₂

theorem galois_connection.l_supr {α : Type u} {β : Type v} {ι : Sort x} [complete_lattice α] [complete_lattice β] {l : α → β} {u : β → α} (gc : galois_connection l u) {f : ι → α} :

l (supr f) = ⨆ (i : ι), l (f i)

theorem galois_connection.l_supr₂ {α : Type u} {β : Type v} {ι : Sort x} {κ : ι → Sort u_1} [complete_lattice α] [complete_lattice β] {l : α → β} {u : β → α} (gc : galois_connection l u) {f : Π (i : ι), κ i → α} :

l (⨆ (i : ι) (j : κ i), f i j) = ⨆ (i : ι) (j : κ i), l (f i j)

theorem galois_connection.u_infi {α : Type u} {β : Type v} {ι : Sort x} [complete_lattice α] [complete_lattice β] {l : α → β} {u : β → α} (gc : galois_connection l u) {f : ι → β} :

u (infi f) = ⨅ (i : ι), u (f i)

theorem galois_connection.u_infi₂ {α : Type u} {β : Type v} {ι : Sort x} {κ : ι → Sort u_1} [complete_lattice α] [complete_lattice β] {l : α → β} {u : β → α} (gc : galois_connection l u) {f : Π (i : ι), κ i → β} :

u (⨅ (i : ι) (j : κ i), f i j) = ⨅ (i : ι) (j : κ i), u (f i j)

theorem galois_connection.l_Sup {α : Type u} {β : Type v} [complete_lattice α] [complete_lattice β] {l : α → β} {u : β → α} (gc : galois_connection l u) {s : set α} :

l (has_Sup.Sup s) = ⨆ (a : α) (H : a ∈ s), l a

theorem galois_connection.u_Inf {α : Type u} {β : Type v} [complete_lattice α] [complete_lattice β] {l : α → β} {u : β → α} (gc : galois_connection l u) {s : set β} :

u (has_Inf.Inf s) = ⨅ (a : β) (H : a ∈ s), u a

theorem galois_connection.lt_iff_lt {α : Type u} {β : Type v} [linear_order α] [linear_order β] {l : α → β} {u : β → α} (gc : galois_connection l u) {a : α} {b : β} :

b < l a ↔ u b < a

@[protected]

theorem galois_connection.id {α : Type u} [pα : preorder α] :

galois_connection id id

@[protected]

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

galois_connection (l2 ∘ l1) (u1 ∘ u2)

@[protected]

theorem galois_connection.dfun {ι : Type u} {α : ι → Type v} {β : ι → Type w} [Π (i : ι), preorder (α i)] [Π (i : ι), preorder (β i)] (l : Π (i : ι), α i → β i) (u : Π (i : ι), β i → α i) (gc : ∀ (i : ι), galois_connection (l i) (u i)) :

galois_connection (λ (a : Π (i : ι), α i) (i : ι), l i (a i)) (λ (b : Π (i : ι), β i) (i : ι), u i (b i))

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

lWZ (lZX x) = lWY (lYX x)

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

uXZ (uZW w) = uXY (uYW w)

theorem galois_connection.l_comm_iff_u_comm {X : Type u_1} [partial_order X] {Y : Type u_2} [preorder Y] {Z : Type u_3} [preorder Z] {W : Type u_4} [partial_order W] {lYX : X → Y} {uXY : Y → X} (hXY : galois_connection lYX uXY) {lWZ : Z → W} {uZW : W → Z} (hZW : galois_connection lWZ uZW) {lWY : Y → W} {uYW : W → Y} (hWY : galois_connection lWY uYW) {lZX : X → Z} {uXZ : Z → X} (hXZ : galois_connection lZX uXZ) :

(∀ (w : W), uXZ (uZW w) = uXY (uYW w)) ↔ ∀ (x : X), lWZ (lZX x) = lWY (lYX x)

theorem Sup_image2_eq_Sup_Sup {α : Type u} {β : Type v} {γ : Type w} [complete_lattice α] [complete_lattice β] [complete_lattice γ] {s : set α} {t : set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), galois_connection (function.swap l b) (u₁ b)) (h₂ : ∀ (a : α), galois_connection (l a) (u₂ a)) :

has_Sup.Sup (set.image2 l s t) = l (has_Sup.Sup s) (has_Sup.Sup t)

theorem Sup_image2_eq_Sup_Inf {α : Type u} {β : Type v} {γ : Type w} [complete_lattice α] [complete_lattice β] [complete_lattice γ] {s : set α} {t : set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), galois_connection (function.swap l b) (u₁ b)) (h₂ : ∀ (a : α), galois_connection (l a ∘ ⇑order_dual.of_dual) (⇑order_dual.to_dual ∘ u₂ a)) :

has_Sup.Sup (set.image2 l s t) = l (has_Sup.Sup s) (has_Inf.Inf t)

theorem Sup_image2_eq_Inf_Sup {α : Type u} {β : Type v} {γ : Type w} [complete_lattice α] [complete_lattice β] [complete_lattice γ] {s : set α} {t : set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), galois_connection (function.swap l b ∘ ⇑order_dual.of_dual) (⇑order_dual.to_dual ∘ u₁ b)) (h₂ : ∀ (a : α), galois_connection (l a) (u₂ a)) :

has_Sup.Sup (set.image2 l s t) = l (has_Inf.Inf s) (has_Sup.Sup t)

theorem Sup_image2_eq_Inf_Inf {α : Type u} {β : Type v} {γ : Type w} [complete_lattice α] [complete_lattice β] [complete_lattice γ] {s : set α} {t : set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), galois_connection (function.swap l b ∘ ⇑order_dual.of_dual) (⇑order_dual.to_dual ∘ u₁ b)) (h₂ : ∀ (a : α), galois_connection (l a ∘ ⇑order_dual.of_dual) (⇑order_dual.to_dual ∘ u₂ a)) :

has_Sup.Sup (set.image2 l s t) = l (has_Inf.Inf s) (has_Inf.Inf t)

theorem Inf_image2_eq_Inf_Inf {α : Type u} {β : Type v} {γ : Type w} [complete_lattice α] [complete_lattice β] [complete_lattice γ] {s : set α} {t : set β} {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} (h₁ : ∀ (b : β), galois_connection (l₁ b) (function.swap u b)) (h₂ : ∀ (a : α), galois_connection (l₂ a) (u a)) :

has_Inf.Inf (set.image2 u s t) = u (has_Inf.Inf s) (has_Inf.Inf t)

theorem Inf_image2_eq_Inf_Sup {α : Type u} {β : Type v} {γ : Type w} [complete_lattice α] [complete_lattice β] [complete_lattice γ] {s : set α} {t : set β} {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} (h₁ : ∀ (b : β), galois_connection (l₁ b) (function.swap u b)) (h₂ : ∀ (a : α), galois_connection (⇑order_dual.to_dual ∘ l₂ a) (u a ∘ ⇑order_dual.of_dual)) :

has_Inf.Inf (set.image2 u s t) = u (has_Inf.Inf s) (has_Sup.Sup t)

theorem Inf_image2_eq_Sup_Inf {α : Type u} {β : Type v} {γ : Type w} [complete_lattice α] [complete_lattice β] [complete_lattice γ] {s : set α} {t : set β} {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} (h₁ : ∀ (b : β), galois_connection (⇑order_dual.to_dual ∘ l₁ b) (function.swap u b ∘ ⇑order_dual.of_dual)) (h₂ : ∀ (a : α), galois_connection (l₂ a) (u a)) :

has_Inf.Inf (set.image2 u s t) = u (has_Sup.Sup s) (has_Inf.Inf t)

theorem Inf_image2_eq_Sup_Sup {α : Type u} {β : Type v} {γ : Type w} [complete_lattice α] [complete_lattice β] [complete_lattice γ] {s : set α} {t : set β} {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} (h₁ : ∀ (b : β), galois_connection (⇑order_dual.to_dual ∘ l₁ b) (function.swap u b ∘ ⇑order_dual.of_dual)) (h₂ : ∀ (a : α), galois_connection (⇑order_dual.to_dual ∘ l₂ a) (u a ∘ ⇑order_dual.of_dual)) :

has_Inf.Inf (set.image2 u s t) = u (has_Sup.Sup s) (has_Sup.Sup t)

@[simp]

theorem order_iso.bdd_above_image {α : Type u} {β : Type v} [preorder α] [preorder β] (e : α ≃o β) {s : set α} :

bdd_above (⇑e '' s) ↔ bdd_above s

@[simp]

theorem order_iso.bdd_below_image {α : Type u} {β : Type v} [preorder α] [preorder β] (e : α ≃o β) {s : set α} :

bdd_below (⇑e '' s) ↔ bdd_below s

@[simp]

theorem order_iso.bdd_above_preimage {α : Type u} {β : Type v} [preorder α] [preorder β] (e : α ≃o β) {s : set β} :

bdd_above (⇑e ⁻¹' s) ↔ bdd_above s

@[simp]

theorem order_iso.bdd_below_preimage {α : Type u} {β : Type v} [preorder α] [preorder β] (e : α ≃o β) {s : set β} :

bdd_below (⇑e ⁻¹' s) ↔ bdd_below s

theorem nat.galois_connection_mul_div {k : ℕ} (h : 0 < k) :

galois_connection (λ (n : ℕ), n * k) (λ (n : ℕ), n / k)

@[nolint]

structure galois_insertion {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (l : α → β) (u : β → α) :

Type (max u_2 u_3)

choice : Π (x : α), u (l x) ≤ x → β
gc : galois_connection l u
le_l_u : ∀ (x : β), x ≤ l (u x)
choice_eq : ∀ (a : α) (h : u (l a) ≤ a), self.choice a h = l a

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 galois_coinsertion

Instances for galois_insertion

galois_insertion.has_sizeof_inst

def galois_insertion.monotone_intro {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {l : α → β} {u : β → α} (hu : monotone u) (hl : monotone l) (hul : ∀ (a : α), a ≤ u (l a)) (hlu : ∀ (b : β), l (u b) = b) :

galois_insertion l u

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

Equations

galois_insertion.monotone_intro hu hl hul hlu = {choice := λ (x : α) (_x : u (l x) ≤ x), l x, gc := _, le_l_u := _, choice_eq := _}

@[protected]

def order_iso.to_galois_insertion {α : Type u} {β : Type v} [preorder α] [preorder β] (oi : α ≃o β) :

galois_insertion ⇑oi ⇑(oi.symm)

Makes a Galois insertion from an order-preserving bijection.

Equations

oi.to_galois_insertion = {choice := λ (b : α) (h : ⇑(oi.symm) (⇑oi b) ≤ b), ⇑oi b, gc := _, le_l_u := _, choice_eq := _}

def galois_connection.to_galois_insertion {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {l : α → β} {u : β → α} (gc : galois_connection l u) (h : ∀ (b : β), b ≤ l (u b)) :

galois_insertion l u

Make a galois_insertion l u from a galois_connection l u such that ∀ b, b ≤ l (u b)

Equations

gc.to_galois_insertion h = {choice := λ (x : α) (_x : u (l x) ≤ x), l x, gc := gc, le_l_u := h, choice_eq := _}

def galois_connection.lift_order_bot {α : Type u_1} {β : Type u_2} [preorder α] [order_bot α] [partial_order β] {l : α → β} {u : β → α} (gc : galois_connection l u) :

Lift the bottom along a Galois connection

Equations

gc.lift_order_bot = {bot := l ⊥, bot_le := _}

theorem galois_insertion.l_u_eq {α : Type u} {β : Type v} {l : α → β} {u : β → α} [preorder α] [partial_order β] (gi : galois_insertion l u) (b : β) :

l (u b) = b

theorem galois_insertion.left_inverse_l_u {α : Type u} {β : Type v} {l : α → β} {u : β → α} [preorder α] [partial_order β] (gi : galois_insertion l u) :

function.left_inverse l u

theorem galois_insertion.l_surjective {α : Type u} {β : Type v} {l : α → β} {u : β → α} [preorder α] [partial_order β] (gi : galois_insertion l u) :

function.surjective l

theorem galois_insertion.u_injective {α : Type u} {β : Type v} {l : α → β} {u : β → α} [preorder α] [partial_order β] (gi : galois_insertion l u) :

function.injective u

theorem galois_insertion.l_sup_u {α : Type u} {β : Type v} {l : α → β} {u : β → α} [semilattice_sup α] [semilattice_sup β] (gi : galois_insertion l u) (a b : β) :

l (u a ⊔ u b) = a ⊔ b

theorem galois_insertion.l_supr_u {α : Type u} {β : Type v} {l : α → β} {u : β → α} [complete_lattice α] [complete_lattice β] (gi : galois_insertion l u) {ι : Sort x} (f : ι → β) :

l (⨆ (i : ι), u (f i)) = ⨆ (i : ι), f i

theorem galois_insertion.l_bsupr_u {α : Type u} {β : Type v} {l : α → β} {u : β → α} [complete_lattice α] [complete_lattice β] (gi : galois_insertion 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 galois_insertion.l_Sup_u_image {α : Type u} {β : Type v} {l : α → β} {u : β → α} [complete_lattice α] [complete_lattice β] (gi : galois_insertion l u) (s : set β) :

l (has_Sup.Sup (u '' s)) = has_Sup.Sup s

theorem galois_insertion.l_inf_u {α : Type u} {β : Type v} {l : α → β} {u : β → α} [semilattice_inf α] [semilattice_inf β] (gi : galois_insertion l u) (a b : β) :

l (u a ⊓ u b) = a ⊓ b

theorem galois_insertion.l_infi_u {α : Type u} {β : Type v} {l : α → β} {u : β → α} [complete_lattice α] [complete_lattice β] (gi : galois_insertion l u) {ι : Sort x} (f : ι → β) :

l (⨅ (i : ι), u (f i)) = ⨅ (i : ι), f i

theorem galois_insertion.l_binfi_u {α : Type u} {β : Type v} {l : α → β} {u : β → α} [complete_lattice α] [complete_lattice β] (gi : galois_insertion 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 galois_insertion.l_Inf_u_image {α : Type u} {β : Type v} {l : α → β} {u : β → α} [complete_lattice α] [complete_lattice β] (gi : galois_insertion l u) (s : set β) :

l (has_Inf.Inf (u '' s)) = has_Inf.Inf s

theorem galois_insertion.l_infi_of_ul_eq_self {α : Type u} {β : Type v} {l : α → β} {u : β → α} [complete_lattice α] [complete_lattice β] (gi : galois_insertion l u) {ι : Sort x} (f : ι → α) (hf : ∀ (i : ι), u (l (f i)) = f i) :

l (⨅ (i : ι), f i) = ⨅ (i : ι), l (f i)

theorem galois_insertion.l_binfi_of_ul_eq_self {α : Type u} {β : Type v} {l : α → β} {u : β → α} [complete_lattice α] [complete_lattice β] (gi : galois_insertion 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 galois_insertion.u_le_u_iff {α : Type u} {β : Type v} {l : α → β} {u : β → α} [preorder α] [preorder β] (gi : galois_insertion l u) {a b : β} :

u a ≤ u b ↔ a ≤ b

theorem galois_insertion.strict_mono_u {α : Type u} {β : Type v} {l : α → β} {u : β → α} [preorder α] [preorder β] (gi : galois_insertion l u) :

theorem galois_insertion.is_lub_of_u_image {α : Type u} {β : Type v} {l : α → β} {u : β → α} [preorder α] [preorder β] (gi : galois_insertion l u) {s : set β} {a : α} (hs : is_lub (u '' s) a) :

is_lub s (l a)

theorem galois_insertion.is_glb_of_u_image {α : Type u} {β : Type v} {l : α → β} {u : β → α} [preorder α] [preorder β] (gi : galois_insertion l u) {s : set β} {a : α} (hs : is_glb (u '' s) a) :

is_glb s (l a)

@[reducible]

def galois_insertion.lift_semilattice_sup {α : Type u} {β : Type v} {l : α → β} {u : β → α} [partial_order β] [semilattice_sup α] (gi : galois_insertion l u) :

semilattice_sup β

Lift the suprema along a Galois insertion

Equations

gi.lift_semilattice_sup = {sup := λ (a b : β), l (u a ⊔ u b), le := partial_order.le _inst_1, lt := partial_order.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}

@[reducible]

def galois_insertion.lift_semilattice_inf {α : Type u} {β : Type v} {l : α → β} {u : β → α} [partial_order β] [semilattice_inf α] (gi : galois_insertion l u) :

semilattice_inf β

Lift the infima along a Galois insertion

Equations

gi.lift_semilattice_inf = {inf := λ (a b : β), gi.choice (u a ⊓ u b) _, le := partial_order.le _inst_1, lt := partial_order.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}

@[reducible]

def galois_insertion.lift_lattice {α : Type u} {β : Type v} {l : α → β} {u : β → α} [partial_order β] [lattice α] (gi : galois_insertion l u) :

Lift the suprema and infima along a Galois insertion

Equations

gi.lift_lattice = {sup := semilattice_sup.sup gi.lift_semilattice_sup, le := semilattice_sup.le gi.lift_semilattice_sup, lt := semilattice_sup.lt gi.lift_semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf gi.lift_semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}

@[reducible]

def galois_insertion.lift_order_top {α : Type u} {β : Type v} {l : α → β} {u : β → α} [partial_order β] [preorder α] [order_top α] (gi : galois_insertion l u) :

Lift the top along a Galois insertion

Equations

gi.lift_order_top = {top := gi.choice ⊤ galois_insertion.lift_order_top._proof_1, le_top := _}

@[reducible]

def galois_insertion.lift_bounded_order {α : Type u} {β : Type v} {l : α → β} {u : β → α} [partial_order β] [preorder α] [bounded_order α] (gi : galois_insertion l u) :

bounded_order β

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

Equations

gi.lift_bounded_order = {top := order_top.top gi.lift_order_top, le_top := _, bot := order_bot.bot _.lift_order_bot, bot_le := _}

@[reducible]

def galois_insertion.lift_complete_lattice {α : Type u} {β : Type v} {l : α → β} {u : β → α} [partial_order β] [complete_lattice α] (gi : galois_insertion l u) :

complete_lattice β

Lift all suprema and infima along a Galois insertion

Equations

gi.lift_complete_lattice = {sup := lattice.sup gi.lift_lattice, le := lattice.le gi.lift_lattice, lt := lattice.lt gi.lift_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf gi.lift_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := λ (s : set β), l (has_Sup.Sup (u '' s)), le_Sup := _, Sup_le := _, Inf := λ (s : set β), gi.choice (has_Inf.Inf (u '' s)) _, Inf_le := _, le_Inf := _, top := bounded_order.top gi.lift_bounded_order, bot := bounded_order.bot gi.lift_bounded_order, le_top := _, bot_le := _}

@[nolint]

structure galois_coinsertion {α : Type u} {β : Type v} [preorder α] [preorder β] (l : α → β) (u : β → α) :

Type (max u v)

choice : Π (x : β), x ≤ l (u x) → α
gc : galois_connection l u
u_l_le : ∀ (x : α), u (l x) ≤ x
choice_eq : ∀ (a : β) (h : a ≤ l (u a)), self.choice a h = u a

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 galois_insertion

Instances for galois_coinsertion

galois_coinsertion.has_sizeof_inst

def galois_coinsertion.dual {α : Type u} {β : Type v} [preorder α] [preorder β] {l : α → β} {u : β → α} :

galois_coinsertion l u → galois_insertion (⇑order_dual.to_dual ∘ u ∘ ⇑order_dual.of_dual) (⇑order_dual.to_dual ∘ l ∘ ⇑order_dual.of_dual)

Make a galois_insertion between αᵒᵈ and βᵒᵈ from a galois_coinsertion between α and β.

Equations

galois_coinsertion.dual = λ (x : galois_coinsertion l u), {choice := x.choice, gc := _, le_l_u := _, choice_eq := _}

def galois_insertion.dual {α : Type u} {β : Type v} [preorder α] [preorder β] {l : α → β} {u : β → α} :

galois_insertion l u → galois_coinsertion (⇑order_dual.to_dual ∘ u ∘ ⇑order_dual.of_dual) (⇑order_dual.to_dual ∘ l ∘ ⇑order_dual.of_dual)

Make a galois_coinsertion between αᵒᵈ and βᵒᵈ from a galois_insertion between α and β.

Equations

galois_insertion.dual = λ (x : galois_insertion l u), {choice := x.choice, gc := _, u_l_le := _, choice_eq := _}

def galois_coinsertion.of_dual {α : Type u} {β : Type v} [preorder α] [preorder β] {l : αᵒᵈ → βᵒᵈ} {u : βᵒᵈ → αᵒᵈ} :

galois_coinsertion l u → galois_insertion (⇑order_dual.of_dual ∘ u ∘ ⇑order_dual.to_dual) (⇑order_dual.of_dual ∘ l ∘ ⇑order_dual.to_dual)

Make a galois_insertion between α and β from a galois_coinsertion between αᵒᵈ and βᵒᵈ.

Equations

galois_coinsertion.of_dual = λ (x : galois_coinsertion l u), {choice := x.choice, gc := _, le_l_u := _, choice_eq := _}

def galois_insertion.of_dual {α : Type u} {β : Type v} [preorder α] [preorder β] {l : αᵒᵈ → βᵒᵈ} {u : βᵒᵈ → αᵒᵈ} :

galois_insertion l u → galois_coinsertion (⇑order_dual.of_dual ∘ u ∘ ⇑order_dual.to_dual) (⇑order_dual.of_dual ∘ l ∘ ⇑order_dual.to_dual)

Make a galois_coinsertion between α and β from a galois_insertion between αᵒᵈ and βᵒᵈ.

Equations

galois_insertion.of_dual = λ (x : galois_insertion l u), {choice := x.choice, gc := _, u_l_le := _, choice_eq := _}

@[protected]

def order_iso.to_galois_coinsertion {α : Type u} {β : Type v} [preorder α] [preorder β] (oi : α ≃o β) :

galois_coinsertion ⇑oi ⇑(oi.symm)

Makes a Galois coinsertion from an order-preserving bijection.

Equations

oi.to_galois_coinsertion = {choice := λ (b : β) (h : b ≤ ⇑oi (⇑(oi.symm) b)), ⇑(oi.symm) b, gc := _, u_l_le := _, choice_eq := _}

def galois_coinsertion.monotone_intro {α : 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) :

galois_coinsertion l u

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

Equations

galois_coinsertion.monotone_intro hu hl hlu hul = (galois_insertion.monotone_intro _ _ hlu hul).of_dual

def galois_connection.to_galois_coinsertion {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {l : α → β} {u : β → α} (gc : galois_connection l u) (h : ∀ (a : α), u (l a) ≤ a) :

galois_coinsertion l u

Make a galois_coinsertion l u from a galois_connection l u such that ∀ b, b ≤ l (u b)

Equations

gc.to_galois_coinsertion h = {choice := λ (x : β) (_x : x ≤ l (u x)), u x, gc := gc, u_l_le := h, choice_eq := _}

def galois_connection.lift_order_top {α : Type u_1} {β : Type u_2} [partial_order α] [preorder β] [order_top β] {l : α → β} {u : β → α} (gc : galois_connection l u) :

Lift the top along a Galois connection

Equations

gc.lift_order_top = {top := u ⊤, le_top := _}

theorem galois_coinsertion.u_l_eq {α : Type u} {β : Type v} {l : α → β} {u : β → α} [partial_order α] [preorder β] (gi : galois_coinsertion l u) (a : α) :

u (l a) = a

theorem galois_coinsertion.u_l_left_inverse {α : Type u} {β : Type v} {l : α → β} {u : β → α} [partial_order α] [preorder β] (gi : galois_coinsertion l u) :

function.left_inverse u l

theorem galois_coinsertion.u_surjective {α : Type u} {β : Type v} {l : α → β} {u : β → α} [partial_order α] [preorder β] (gi : galois_coinsertion l u) :

function.surjective u

theorem galois_coinsertion.l_injective {α : Type u} {β : Type v} {l : α → β} {u : β → α} [partial_order α] [preorder β] (gi : galois_coinsertion l u) :

function.injective l

theorem galois_coinsertion.u_inf_l {α : Type u} {β : Type v} {l : α → β} {u : β → α} [semilattice_inf α] [semilattice_inf β] (gi : galois_coinsertion l u) (a b : α) :

u (l a ⊓ l b) = a ⊓ b

theorem galois_coinsertion.u_infi_l {α : Type u} {β : Type v} {l : α → β} {u : β → α} [complete_lattice α] [complete_lattice β] (gi : galois_coinsertion l u) {ι : Sort x} (f : ι → α) :

u (⨅ (i : ι), l (f i)) = ⨅ (i : ι), f i

theorem galois_coinsertion.u_Inf_l_image {α : Type u} {β : Type v} {l : α → β} {u : β → α} [complete_lattice α] [complete_lattice β] (gi : galois_coinsertion l u) (s : set α) :

u (has_Inf.Inf (l '' s)) = has_Inf.Inf s

theorem galois_coinsertion.u_sup_l {α : Type u} {β : Type v} {l : α → β} {u : β → α} [semilattice_sup α] [semilattice_sup β] (gi : galois_coinsertion l u) (a b : α) :

u (l a ⊔ l b) = a ⊔ b

theorem galois_coinsertion.u_supr_l {α : Type u} {β : Type v} {l : α → β} {u : β → α} [complete_lattice α] [complete_lattice β] (gi : galois_coinsertion l u) {ι : Sort x} (f : ι → α) :

u (⨆ (i : ι), l (f i)) = ⨆ (i : ι), f i

theorem galois_coinsertion.u_bsupr_l {α : Type u} {β : Type v} {l : α → β} {u : β → α} [complete_lattice α] [complete_lattice β] (gi : galois_coinsertion 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 galois_coinsertion.u_Sup_l_image {α : Type u} {β : Type v} {l : α → β} {u : β → α} [complete_lattice α] [complete_lattice β] (gi : galois_coinsertion l u) (s : set α) :

u (has_Sup.Sup (l '' s)) = has_Sup.Sup s

theorem galois_coinsertion.u_supr_of_lu_eq_self {α : Type u} {β : Type v} {l : α → β} {u : β → α} [complete_lattice α] [complete_lattice β] (gi : galois_coinsertion l u) {ι : Sort x} (f : ι → β) (hf : ∀ (i : ι), l (u (f i)) = f i) :

u (⨆ (i : ι), f i) = ⨆ (i : ι), u (f i)

theorem galois_coinsertion.u_bsupr_of_lu_eq_self {α : Type u} {β : Type v} {l : α → β} {u : β → α} [complete_lattice α] [complete_lattice β] (gi : galois_coinsertion 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 galois_coinsertion.l_le_l_iff {α : Type u} {β : Type v} {l : α → β} {u : β → α} [preorder α] [preorder β] (gi : galois_coinsertion l u) {a b : α} :

l a ≤ l b ↔ a ≤ b

theorem galois_coinsertion.strict_mono_l {α : Type u} {β : Type v} {l : α → β} {u : β → α} [preorder α] [preorder β] (gi : galois_coinsertion l u) :

theorem galois_coinsertion.is_glb_of_l_image {α : Type u} {β : Type v} {l : α → β} {u : β → α} [preorder α] [preorder β] (gi : galois_coinsertion l u) {s : set α} {a : β} (hs : is_glb (l '' s) a) :

is_glb s (u a)

theorem galois_coinsertion.is_lub_of_l_image {α : Type u} {β : Type v} {l : α → β} {u : β → α} [preorder α] [preorder β] (gi : galois_coinsertion l u) {s : set α} {a : β} (hs : is_lub (l '' s) a) :

is_lub s (u a)

@[reducible]

def galois_coinsertion.lift_semilattice_inf {α : Type u} {β : Type v} {l : α → β} {u : β → α} [partial_order α] [semilattice_inf β] (gi : galois_coinsertion l u) :

semilattice_inf α

Lift the infima along a Galois coinsertion

Equations

gi.lift_semilattice_inf = {inf := λ (a b : α), u (l a ⊓ l b), le := partial_order.le _inst_1, lt := partial_order.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}

@[reducible]

def galois_coinsertion.lift_semilattice_sup {α : Type u} {β : Type v} {l : α → β} {u : β → α} [partial_order α] [semilattice_sup β] (gi : galois_coinsertion l u) :

semilattice_sup α

Lift the suprema along a Galois coinsertion

Equations

gi.lift_semilattice_sup = {sup := λ (a b : α), gi.choice (l a ⊔ l b) _, le := partial_order.le _inst_1, lt := partial_order.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}

@[reducible]

def galois_coinsertion.lift_lattice {α : Type u} {β : Type v} {l : α → β} {u : β → α} [partial_order α] [lattice β] (gi : galois_coinsertion l u) :

Lift the suprema and infima along a Galois coinsertion

Equations

gi.lift_lattice = {sup := semilattice_sup.sup gi.lift_semilattice_sup, le := semilattice_sup.le gi.lift_semilattice_sup, lt := semilattice_sup.lt gi.lift_semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf gi.lift_semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}

@[reducible]

def galois_coinsertion.lift_order_bot {α : Type u} {β : Type v} {l : α → β} {u : β → α} [partial_order α] [preorder β] [order_bot β] (gi : galois_coinsertion l u) :

Lift the bot along a Galois coinsertion

Equations

gi.lift_order_bot = {bot := gi.choice ⊥ galois_coinsertion.lift_order_bot._proof_1, bot_le := _}

@[reducible]

def galois_coinsertion.lift_bounded_order {α : Type u} {β : Type v} {l : α → β} {u : β → α} [partial_order α] [preorder β] [bounded_order β] (gi : galois_coinsertion l u) :

bounded_order α

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

Equations

gi.lift_bounded_order = {top := order_top.top _.lift_order_top, le_top := _, bot := order_bot.bot gi.lift_order_bot, bot_le := _}

@[reducible]

def galois_coinsertion.lift_complete_lattice {α : Type u} {β : Type v} {l : α → β} {u : β → α} [partial_order α] [complete_lattice β] (gi : galois_coinsertion l u) :

complete_lattice α

Lift all suprema and infima along a Galois coinsertion

Equations

gi.lift_complete_lattice = {sup := complete_lattice.sup (order_dual.complete_lattice αᵒᵈ), le := complete_lattice.le (order_dual.complete_lattice αᵒᵈ), lt := complete_lattice.lt (order_dual.complete_lattice αᵒᵈ), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := complete_lattice.inf (order_dual.complete_lattice αᵒᵈ), inf_le_left := _, inf_le_right := _, le_inf := _, Sup := λ (s : set α), gi.choice (has_Sup.Sup (l '' s)) _, le_Sup := _, Sup_le := _, Inf := λ (s : set α), u (has_Inf.Inf (l '' s)), Inf_le := _, le_Inf := _, top := complete_lattice.top (order_dual.complete_lattice αᵒᵈ), bot := complete_lattice.bot (order_dual.complete_lattice αᵒᵈ), le_top := _, bot_le := _}

def with_bot.gi_unbot'_bot {α : Type u} [preorder α] [order_bot α] :

galois_insertion (with_bot.unbot' ⊥) coe

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

Equations

with_bot.gi_unbot'_bot = {choice := λ (o : with_bot α) (ho : ↑(with_bot.unbot' ⊥ o) ≤ o), with_bot.unbot' ⊥ o, gc := _, le_l_u := _, choice_eq := _}