doc-next-gen

Mathlib.Order.GaloisConnection.Basic

Module docstring

{"# Galois connections, insertions and coinsertions

This file contains basic results on Galois connections, insertions and coinsertions in various order structures, and provides constructions that lift order structures from one type to another.

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. "}

GaloisConnection.upperBounds_l_image theorem
(s : Set α) : upperBounds (l '' s) = u ⁻¹' upperBounds s
Full source 
theorem upperBounds_l_image (s : Set α) :
    upperBounds (l '' s) = u ⁻¹' upperBounds s :=
  Set.ext fun b => by simp [upperBounds, gc _ _]
Galois Connection Preserves Upper Bounds via Preimage
Informal description
Let $\alpha$ and $\beta$ be preorders with a Galois connection given by functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$. For any subset $s \subseteq \alpha$, the set of upper bounds of the image $l(s)$ under $l$ is equal to the preimage under $u$ of the set of upper bounds of $s$. In symbols: \[ \text{upperBounds}(l(s)) = u^{-1}(\text{upperBounds}(s)) \]
GaloisConnection.lowerBounds_u_image theorem
(s : Set β) : lowerBounds (u '' s) = l ⁻¹' lowerBounds s
Full source 
theorem lowerBounds_u_image (s : Set β) :
    lowerBounds (u '' s) = l ⁻¹' lowerBounds s :=
  gc.dual.upperBounds_l_image s
Galois Connection Preserves Lower Bounds via Preimage
Informal description
Let $\alpha$ and $\beta$ be preorders with a Galois connection given by functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$. For any subset $s \subseteq \beta$, the set of lower bounds of the image $u(s)$ under $u$ is equal to the preimage under $l$ of the set of lower bounds of $s$. In symbols: \[ \text{lowerBounds}(u(s)) = l^{-1}(\text{lowerBounds}(s)) \]
GaloisConnection.bddAbove_l_image theorem
{s : Set α} : BddAbove (l '' s) ↔ BddAbove s
Full source 
theorem bddAbove_l_image {s : Set α} : BddAboveBddAbove (l '' s) ↔ BddAbove s :=
  ⟨fun ⟨x, hx⟩ => ⟨u x, by rwa [gc.upperBounds_l_image] at hx⟩, gc.monotone_l.map_bddAbove⟩
Bounded Above Image under Lower Adjoint in Galois Connection
Informal description
Let $\alpha$ and $\beta$ be preorders with a Galois connection given by functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$. For any subset $s \subseteq \alpha$, the image $l(s)$ is bounded above in $\beta$ if and only if $s$ is bounded above in $\alpha$.
GaloisConnection.bddBelow_u_image theorem
{s : Set β} : BddBelow (u '' s) ↔ BddBelow s
Full source 
theorem bddBelow_u_image {s : Set β} : BddBelowBddBelow (u '' s) ↔ BddBelow s :=
  gc.dual.bddAbove_l_image
Bounded Below Image under Upper Adjoint in Galois Connection
Informal description
Let $\alpha$ and $\beta$ be preorders with a Galois connection given by functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$. For any subset $s \subseteq \beta$, the image $u(s)$ is bounded below in $\alpha$ if and only if $s$ is bounded below in $\beta$.
GaloisConnection.isLUB_l_image theorem
{s : Set α} {a : α} (h : IsLUB s a) : IsLUB (l '' s) (l a)
Full source 
theorem isLUB_l_image {s : Set α} {a : α} (h : IsLUB s a) : IsLUB (l '' s) (l a) :=
  ⟨gc.monotone_l.mem_upperBounds_image h.left, fun b hb =>
    gc.l_le <| h.right <| by rwa [gc.upperBounds_l_image] at hb⟩
Galois Connection Preserves Least Upper Bounds Under Image
Informal description
Let $\alpha$ and $\beta$ be preorders with a Galois connection given by functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$. For any subset $s \subseteq \alpha$ and element $a \in \alpha$, if $a$ is the least upper bound of $s$, then $l(a)$ is the least upper bound of the image $l(s)$.
GaloisConnection.isGLB_u_image theorem
{s : Set β} {b : β} (h : IsGLB s b) : IsGLB (u '' s) (u b)
Full source 
theorem isGLB_u_image {s : Set β} {b : β} (h : IsGLB s b) : IsGLB (u '' s) (u b) :=
  gc.dual.isLUB_l_image h
Galois Connection Preserves Greatest Lower Bounds Under Image
Informal description
Let $\alpha$ and $\beta$ be preorders with a Galois connection given by functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$. For any subset $s \subseteq \beta$ and element $b \in \beta$, if $b$ is the greatest lower bound of $s$, then $u(b)$ is the greatest lower bound of the image $u(s)$.
GaloisConnection.isLeast_l theorem
{a : α} : IsLeast {b | a ≤ u b} (l a)
Full source 
theorem isLeast_l {a : α} : IsLeast { b | a ≤ u b } (l a) :=
  ⟨gc.le_u_l _, fun _ hb => gc.l_le hb⟩
$l(a)$ is the least element of $\{b \mid a \leq u(b)\}$ in a Galois connection
Informal description
Given a Galois connection $(l, u)$ between preorders $\alpha$ and $\beta$, for any element $a \in \alpha$, the image $l(a)$ is the least element of the set $\{b \in \beta \mid a \leq u(b)\}$.
GaloisConnection.isGreatest_u theorem
{b : β} : IsGreatest {a | l a ≤ b} (u b)
Full source 
theorem isGreatest_u {b : β} : IsGreatest { a | l a ≤ b } (u b) :=
  gc.dual.isLeast_l
$u(b)$ is the greatest element of $\{a \mid l(a) \leq b\}$ in a Galois connection
Informal description
Given a Galois connection $(l, u)$ between preorders $\alpha$ and $\beta$, for any element $b \in \beta$, the image $u(b)$ is the greatest element of the set $\{a \in \alpha \mid l(a) \leq b\}$.
GaloisConnection.isGLB_l theorem
{a : α} : IsGLB {b | a ≤ u b} (l a)
Full source 
theorem isGLB_l {a : α} : IsGLB { b | a ≤ u b } (l a) :=
  gc.isLeast_l.isGLB
$l(a)$ is the greatest lower bound of $\{b \mid a \leq u(b)\}$ in a Galois connection
Informal description
Given a Galois connection $(l, u)$ between preorders $\alpha$ and $\beta$, for any element $a \in \alpha$, the image $l(a)$ is the greatest lower bound (infimum) of the set $\{b \in \beta \mid a \leq u(b)\}$.
GaloisConnection.isLUB_u theorem
{b : β} : IsLUB {a | l a ≤ b} (u b)
Full source 
theorem isLUB_u {b : β} : IsLUB { a | l a ≤ b } (u b) :=
  gc.isGreatest_u.isLUB
$u(b)$ is the supremum of $\{a \mid l(a) \leq b\}$ in a Galois connection
Informal description
Given a Galois connection $(l, u)$ between preorders $\alpha$ and $\beta$, for any element $b \in \beta$, the image $u(b)$ is the least upper bound (supremum) of the set $\{a \in \alpha \mid l(a) \leq b\}$.
GaloisConnection.l_sup theorem
(gc : GaloisConnection l u) : l (a₁ ⊔ a₂) = l a₁ ⊔ l a₂
Full source 
theorem l_sup (gc : GaloisConnection l u) : l (a₁ ⊔ a₂) = l a₁ ⊔ l a₂ :=
  (gc.isLUB_l_image isLUB_pair).unique <| by simp only [image_pair, isLUB_pair]
Galois Connection Preserves Suprema: $l(a_1 \sqcup a_2) = l(a_1) \sqcup l(a_2)$
Informal description
Let $\alpha$ and $\beta$ be preorders with a Galois connection given by functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$. For any two elements $a_1, a_2 \in \alpha$, the image under $l$ of their supremum $a_1 \sqcup a_2$ equals the supremum of their images, i.e., $l(a_1 \sqcup a_2) = l(a_1) \sqcup l(a_2)$.
GaloisConnection.u_inf theorem
(gc : GaloisConnection l u) : u (b₁ ⊓ b₂) = u b₁ ⊓ u b₂
Full source 
theorem u_inf (gc : GaloisConnection l u) : u (b₁ ⊓ b₂) = u b₁ ⊓ u b₂ := gc.dual.l_sup
Upper Adjoint Preserves Infima in Galois Connection: $u(b_1 \sqcap b_2) = u(b_1) \sqcap u(b_2)$
Informal description
Let $\alpha$ and $\beta$ be preorders with a Galois connection given by functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$. For any two elements $b_1, b_2 \in \beta$, the image under $u$ of their infimum $b_1 \sqcap b_2$ equals the infimum of their images, i.e., $u(b_1 \sqcap b_2) = u(b_1) \sqcap u(b_2)$.
GaloisConnection.l_iSup theorem
(gc : GaloisConnection l u) {f : ι → α} : l (iSup f) = ⨆ i, l (f i)
Full source 
theorem l_iSup (gc : GaloisConnection l u) {f : ι → α} : l (iSup f) = ⨆ i, l (f i) :=
  Eq.symm <|
    IsLUB.iSup_eq <|
      show IsLUB (range (l ∘ f)) (l (iSup f)) by
        rw [range_comp, ← sSup_range]; exact gc.isLUB_l_image (isLUB_sSup _)
Lower Adjoint Preserves Indexed Suprema in Galois Connection
Informal description
Let $\alpha$ and $\beta$ be preorders with a Galois connection given by functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$. For any indexed family $f : \iota \to \alpha$, the lower adjoint $l$ preserves suprema, i.e., $l(\bigsqcup_i f(i)) = \bigsqcup_i l(f(i))$.
GaloisConnection.l_iSup₂ theorem
(gc : GaloisConnection l u) {f : ∀ i, κ i → α} : l (⨆ (i) (j), f i j) = ⨆ (i) (j), l (f i j)
Full source 
theorem l_iSup₂ (gc : GaloisConnection l u) {f : ∀ i, κ i → α} :
    l (⨆ (i) (j), f i j) = ⨆ (i) (j), l (f i j) := by
  simp_rw [gc.l_iSup]
Lower Adjoint Preserves Doubly Indexed Suprema in Galois Connection
Informal description
Let $\alpha$ and $\beta$ be preorders with a Galois connection given by functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$. For any doubly indexed family $f : \forall i, \kappa_i \to \alpha$, the lower adjoint $l$ preserves suprema, i.e., $l\left(\bigsqcup_{i,j} f(i,j)\right) = \bigsqcup_{i,j} l(f(i,j))$.
GaloisConnection.u_iInf theorem
{f : ι → β} : u (iInf f) = ⨅ i, u (f i)
Full source 
theorem u_iInf {f : ι → β} : u (iInf f) = ⨅ i, u (f i) :=
  gc.dual.l_iSup
Upper Adjoint Preserves Indexed Infima in Galois Connection
Informal description
Let $\alpha$ and $\beta$ be preorders with a Galois connection given by functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$. For any indexed family $f : \iota \to \beta$, the upper adjoint $u$ preserves infima, i.e., $u(\bigsqcap_i f(i)) = \bigsqcap_i u(f(i))$.
GaloisConnection.u_iInf₂ theorem
{f : ∀ i, κ i → β} : u (⨅ (i) (j), f i j) = ⨅ (i) (j), u (f i j)
Full source 
theorem u_iInf₂ {f : ∀ i, κ i → β} : u (⨅ (i) (j), f i j) = ⨅ (i) (j), u (f i j) :=
  gc.dual.l_iSup₂
Upper Adjoint Preserves Doubly Indexed Infima in Galois Connection
Informal description
Let $\alpha$ and $\beta$ be preorders with a Galois connection given by functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$. For any doubly indexed family $f : \forall i, \kappa_i \to \beta$, the upper adjoint $u$ preserves infima, i.e., $u\left(\bigsqcap_{i,j} f(i,j)\right) = \bigsqcap_{i,j} u(f(i,j))$.
GaloisConnection.l_sSup theorem
{s : Set α} : l (sSup s) = ⨆ a ∈ s, l a
Full source 
theorem l_sSup {s : Set α} : l (sSup s) = ⨆ a ∈ s, l a := by
  simp only [sSup_eq_iSup, gc.l_iSup]
Lower Adjoint Preserves Suprema in Galois Connection
Informal description
Let $\alpha$ and $\beta$ be preorders with a Galois connection given by functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$. For any subset $s \subseteq \alpha$, the lower adjoint $l$ preserves suprema, i.e., $l(\sup s) = \bigsqcup_{a \in s} l(a)$.
GaloisConnection.u_sInf theorem
{s : Set β} : u (sInf s) = ⨅ a ∈ s, u a
Full source 
theorem u_sInf {s : Set β} : u (sInf s) = ⨅ a ∈ s, u a :=
  gc.dual.l_sSup
Upper Adjoint Preserves Infima in Galois Connection
Informal description
Let $\alpha$ and $\beta$ be preorders with a Galois connection given by functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$. For any subset $s \subseteq \beta$, the upper adjoint $u$ preserves infima, i.e., $u(\inf s) = \bigsqcap_{a \in s} u(a)$.
GaloisConnection.compl theorem
[BooleanAlgebra α] [BooleanAlgebra β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : GaloisConnection (compl ∘ u ∘ compl) (compl ∘ l ∘ compl)
Full source 
protected theorem compl [BooleanAlgebra α] [BooleanAlgebra β] {l : α → β} {u : β → α}
    (gc : GaloisConnection l u) :
    GaloisConnection (complcompl ∘ u ∘ compl) (complcompl ∘ l ∘ compl) := fun a b ↦ by
  dsimp
  rw [le_compl_iff_le_compl, gc, compl_le_iff_compl_le]
Galois Connection Induced by Complements in Boolean Algebras
Informal description
Let $\alpha$ and $\beta$ be Boolean algebras, and let $l : \alpha \to \beta$ and $u : \beta \to \alpha$ form a Galois connection. Then the pair of functions $(x \mapsto u(x^\complement)^\complement, y \mapsto l(y^\complement)^\complement)$ also forms a Galois connection between $\alpha$ and $\beta$.
gc_sSup_Iic theorem
[CompleteSemilatticeSup α] : GaloisConnection (sSup : Set α → α) (Iic : α → Set α)
Full source 
/-- `sSup` and `Iic` form a Galois connection. -/
theorem gc_sSup_Iic [CompleteSemilatticeSup α] :
    GaloisConnection (sSup : Set α → α) (Iic : α → Set α) :=
  fun _ _ ↦ sSup_le_iff
Galois Connection Between Suprema and Lower Sets in Complete Semilattices
Informal description
For any complete semilattice with supremum $\alpha$, the pair of functions $\operatorname{sSup} : \mathcal{P}(\alpha) \to \alpha$ (taking the supremum of a set) and $\operatorname{Iic} : \alpha \to \mathcal{P}(\alpha)$ (mapping an element to its lower set $\{x \in \alpha \mid x \leq a\}$) forms a Galois connection. This means that for any subset $S \subseteq \alpha$ and any element $a \in \alpha$, we have $\operatorname{sSup}(S) \leq a$ if and only if $S \subseteq \operatorname{Iic}(a)$.
gc_Ici_sInf theorem
[CompleteSemilatticeInf α] : GaloisConnection (toDual ∘ Ici : α → (Set α)ᵒᵈ) (sInf ∘ ofDual : (Set α)ᵒᵈ → α)
Full source 
/-- `toDual ∘ Ici` and `sInf ∘ ofDual` form a Galois connection. -/
theorem gc_Ici_sInf [CompleteSemilatticeInf α] :
    GaloisConnection (toDualtoDual ∘ Ici : α → (Set α)ᵒᵈ) (sInfsInf ∘ ofDual : (Set α)ᵒᵈ → α) :=
  fun _ _ ↦ le_sInf_iff.symm
Galois Connection Between Meet-Semilattice and Dual Power Set via Upper Closures and Infima
Informal description
Let $\alpha$ be a complete meet-semilattice. The pair of functions $(f, g)$, where $f : \alpha \to (\mathcal{P}(\alpha))^{\text{op}}$ is defined by $f(a) = [a, \infty)$ (interpreted in the dual order) and $g : (\mathcal{P}(\alpha))^{\text{op}} \to \alpha$ is defined by $g(S) = \bigwedge S$, forms a Galois connection. That is, for all $a \in \alpha$ and $S \in \mathcal{P}(\alpha)^{\text{op}}$, we have $f(a) \leq^{\text{op}} S$ if and only if $a \leq g(S)$.
sSup_image2_eq_sSup_sSup theorem
(h₁ : ∀ b, GaloisConnection (swap l b) (u₁ b)) (h₂ : ∀ a, GaloisConnection (l a) (u₂ a)) : sSup (image2 l s t) = l (sSup s) (sSup t)
Full source 
theorem sSup_image2_eq_sSup_sSup (h₁ : ∀ b, GaloisConnection (swap l b) (u₁ b))
    (h₂ : ∀ a, GaloisConnection (l a) (u₂ a)) : sSup (image2 l s t) = l (sSup s) (sSup t) := by
  simp_rw [sSup_image2, ← (h₂ _).l_sSup, ← (h₁ _).l_sSup]
Supremum of Binary Image Equals Binary Supremum under Galois Connections
Informal description
Let $\alpha$ and $\beta$ be preorders, and let $l : \alpha \times \beta \to \gamma$ be a binary function. Suppose that for every $b \in \beta$, the function $l(\cdot, b) : \alpha \to \gamma$ forms a Galois connection with $u_1(b) : \gamma \to \alpha$, and for every $a \in \alpha$, the function $l(a, \cdot) : \beta \to \gamma$ forms a Galois connection with $u_2(a) : \gamma \to \beta$. Then, for any subsets $s \subseteq \alpha$ and $t \subseteq \beta$, the supremum of the image $\{l(a, b) \mid a \in s, b \in t\}$ equals $l(\sup s, \sup t)$.
sSup_image2_eq_sSup_sInf theorem
(h₁ : ∀ b, GaloisConnection (swap l b) (u₁ b)) (h₂ : ∀ a, GaloisConnection (l a ∘ ofDual) (toDual ∘ u₂ a)) : sSup (image2 l s t) = l (sSup s) (sInf t)
Full source 
theorem sSup_image2_eq_sSup_sInf (h₁ : ∀ b, GaloisConnection (swap l b) (u₁ b))
    (h₂ : ∀ a, GaloisConnection (l a ∘ ofDual) (toDualtoDual ∘ u₂ a)) :
    sSup (image2 l s t) = l (sSup s) (sInf t) :=
  sSup_image2_eq_sSup_sSup (β := βᵒᵈ) h₁ h₂
Supremum of Binary Image under Galois Connections Equals $l(\sup s, \inf t)$
Informal description
Let $\alpha$, $\beta$, and $\gamma$ be preorders, and let $l : \alpha \times \beta \to \gamma$ be a binary function. Suppose that: 1. For every $b \in \beta$, the function $l(\cdot, b) : \alpha \to \gamma$ forms a Galois connection with $u_1(b) : \gamma \to \alpha$. 2. For every $a \in \alpha$, the function $l(a, \cdot) : \beta \to \gamma$ forms a Galois connection with $u_2(a) : \gamma \to \beta^{\text{op}}$ (where $\beta^{\text{op}}$ is the order dual of $\beta$). Then, for any subsets $s \subseteq \alpha$ and $t \subseteq \beta$, the supremum of the image $\{l(a, b) \mid a \in s, b \in t\}$ equals $l(\sup s, \inf t)$.
sSup_image2_eq_sInf_sSup theorem
(h₁ : ∀ b, GaloisConnection (swap l b ∘ ofDual) (toDual ∘ u₁ b)) (h₂ : ∀ a, GaloisConnection (l a) (u₂ a)) : sSup (image2 l s t) = l (sInf s) (sSup t)
Full source 
theorem sSup_image2_eq_sInf_sSup (h₁ : ∀ b, GaloisConnection (swapswap l b ∘ ofDual) (toDualtoDual ∘ u₁ b))
    (h₂ : ∀ a, GaloisConnection (l a) (u₂ a)) : sSup (image2 l s t) = l (sInf s) (sSup t) :=
  sSup_image2_eq_sSup_sSup (α := αᵒᵈ) h₁ h₂
Supremum of Binary Image Equals Binary Infimum-Supremum under Galois Connections
Informal description
Let $\alpha$, $\beta$, and $\gamma$ be preorders, and let $l : \alpha \times \beta \to \gamma$ be a binary function. Suppose that: 1. For every $b \in \beta$, the function $l(\cdot, b) \circ \text{ofDual} : \alpha^{\text{op}} \to \gamma$ forms a Galois connection with $\text{toDual} \circ u_1(b) : \gamma \to \alpha^{\text{op}}$, and 2. For every $a \in \alpha$, the function $l(a, \cdot) : \beta \to \gamma$ forms a Galois connection with $u_2(a) : \gamma \to \beta$. Then, for any subsets $s \subseteq \alpha$ and $t \subseteq \beta$, the supremum of the image $\{l(a, b) \mid a \in s, b \in t\}$ equals $l(\inf s, \sup t)$.
sSup_image2_eq_sInf_sInf theorem
(h₁ : ∀ b, GaloisConnection (swap l b ∘ ofDual) (toDual ∘ u₁ b)) (h₂ : ∀ a, GaloisConnection (l a ∘ ofDual) (toDual ∘ u₂ a)) : sSup (image2 l s t) = l (sInf s) (sInf t)
Full source 
theorem sSup_image2_eq_sInf_sInf (h₁ : ∀ b, GaloisConnection (swapswap l b ∘ ofDual) (toDualtoDual ∘ u₁ b))
    (h₂ : ∀ a, GaloisConnection (l a ∘ ofDual) (toDualtoDual ∘ u₂ a)) :
    sSup (image2 l s t) = l (sInf s) (sInf t) :=
  sSup_image2_eq_sSup_sSup (α := αᵒᵈ) (β := βᵒᵈ) h₁ h₂
Supremum of Binary Image Equals Binary Infimum under Dual Galois Connections
Informal description
Let $\alpha$, $\beta$, and $\gamma$ be preorders, and let $l : \alpha \times \beta \to \gamma$ be a binary function. Suppose that for every $b \in \beta$, the function $l(\cdot, b) \circ \text{ofDual} : \alpha^{\text{op}} \to \gamma$ forms a Galois connection with $\text{toDual} \circ u_1(b) : \gamma \to \alpha^{\text{op}}$, and for every $a \in \alpha$, the function $l(a, \cdot) \circ \text{ofDual} : \beta^{\text{op}} \to \gamma$ forms a Galois connection with $\text{toDual} \circ u_2(a) : \gamma \to \beta^{\text{op}}$. Then, for any subsets $s \subseteq \alpha$ and $t \subseteq \beta$, the supremum of the image $\{l(a, b) \mid a \in s, b \in t\}$ equals $l(\inf s, \inf t)$.
sInf_image2_eq_sInf_sInf theorem
(h₁ : ∀ b, GaloisConnection (l₁ b) (swap u b)) (h₂ : ∀ a, GaloisConnection (l₂ a) (u a)) : sInf (image2 u s t) = u (sInf s) (sInf t)
Full source 
theorem sInf_image2_eq_sInf_sInf (h₁ : ∀ b, GaloisConnection (l₁ b) (swap u b))
    (h₂ : ∀ a, GaloisConnection (l₂ a) (u a)) : sInf (image2 u s t) = u (sInf s) (sInf t) := by
  simp_rw [sInf_image2, ← (h₂ _).u_sInf, ← (h₁ _).u_sInf]
Infimum of Binary Image under Galois Connections: $\inf \{u(a, b)\} = u(\inf s, \inf t)$
Informal description
Let $\alpha$ and $\beta$ be preorders, and let $u : \alpha \times \beta \to \gamma$ be a function. Suppose that for every $b \in \beta$, the function $l_1(b) : \alpha \to \gamma$ and the swapped function $\operatorname{swap} u(b) : \gamma \to \alpha$ form a Galois connection. Additionally, suppose that for every $a \in \alpha$, the function $l_2(a) : \beta \to \gamma$ and $u(a) : \gamma \to \beta$ form a Galois connection. Then, for any sets $s \subseteq \alpha$ and $t \subseteq \beta$, the infimum of the image $\{u(a, b) \mid a \in s, b \in t\}$ is equal to $u(\inf s, \inf t)$.
sInf_image2_eq_sInf_sSup theorem
(h₁ : ∀ b, GaloisConnection (l₁ b) (swap u b)) (h₂ : ∀ a, GaloisConnection (toDual ∘ l₂ a) (u a ∘ ofDual)) : sInf (image2 u s t) = u (sInf s) (sSup t)
Full source 
theorem sInf_image2_eq_sInf_sSup (h₁ : ∀ b, GaloisConnection (l₁ b) (swap u b))
    (h₂ : ∀ a, GaloisConnection (toDualtoDual ∘ l₂ a) (u a ∘ ofDual)) :
    sInf (image2 u s t) = u (sInf s) (sSup t) :=
  sInf_image2_eq_sInf_sInf (β := βᵒᵈ) h₁ h₂
Infimum of Binary Image under Mixed Galois Connections: $\inf \{u(a, b)\} = u(\inf s, \sup t)$
Informal description
Let $\alpha$, $\beta$, and $\gamma$ be preorders, and let $u : \alpha \times \beta \to \gamma$ be a function. Suppose that for every $b \in \beta$, the function $l_1(b) : \alpha \to \gamma$ and the swapped function $\operatorname{swap} u(b) : \gamma \to \alpha$ form a Galois connection. Additionally, suppose that for every $a \in \alpha$, the function $\text{toDual} \circ l_2(a) : \beta \to \gamma^{\text{op}}$ and $u(a) \circ \text{ofDual} : \gamma^{\text{op}} \to \beta$ form a Galois connection. Then, for any subsets $s \subseteq \alpha$ and $t \subseteq \beta$, the infimum of the image $\{u(a, b) \mid a \in s, b \in t\}$ is equal to $u(\inf s, \sup t)$.
sInf_image2_eq_sSup_sInf theorem
(h₁ : ∀ b, GaloisConnection (toDual ∘ l₁ b) (swap u b ∘ ofDual)) (h₂ : ∀ a, GaloisConnection (l₂ a) (u a)) : sInf (image2 u s t) = u (sSup s) (sInf t)
Full source 
theorem sInf_image2_eq_sSup_sInf (h₁ : ∀ b, GaloisConnection (toDualtoDual ∘ l₁ b) (swapswap u b ∘ ofDual))
    (h₂ : ∀ a, GaloisConnection (l₂ a) (u a)) : sInf (image2 u s t) = u (sSup s) (sInf t) :=
  sInf_image2_eq_sInf_sInf (α := αᵒᵈ) h₁ h₂
Infimum of Binary Image under Galois Connections: $\inf \{u(a, b)\} = u(\sup s, \inf t)$
Informal description
Let $\alpha$, $\beta$, and $\gamma$ be preorders, and let $u : \alpha \times \beta \to \gamma$ be a function. Suppose that for every $b \in \beta$, the composition $\text{toDual} \circ l_1(b) : \alpha \to \gamma^{\text{op}}$ and the composition $\text{swap}\, u(b) \circ \text{ofDual} : \gamma^{\text{op}} \to \alpha$ form a Galois connection. Additionally, suppose that for every $a \in \alpha$, the function $l_2(a) : \beta \to \gamma$ and $u(a) : \gamma \to \beta$ form a Galois connection. Then, for any sets $s \subseteq \alpha$ and $t \subseteq \beta$, the infimum of the image $\{u(a, b) \mid a \in s, b \in t\}$ is equal to $u(\sup s, \inf t)$.
sInf_image2_eq_sSup_sSup theorem
(h₁ : ∀ b, GaloisConnection (toDual ∘ l₁ b) (swap u b ∘ ofDual)) (h₂ : ∀ a, GaloisConnection (toDual ∘ l₂ a) (u a ∘ ofDual)) : sInf (image2 u s t) = u (sSup s) (sSup t)
Full source 
theorem sInf_image2_eq_sSup_sSup (h₁ : ∀ b, GaloisConnection (toDualtoDual ∘ l₁ b) (swapswap u b ∘ ofDual))
    (h₂ : ∀ a, GaloisConnection (toDualtoDual ∘ l₂ a) (u a ∘ ofDual)) :
    sInf (image2 u s t) = u (sSup s) (sSup t) :=
  sInf_image2_eq_sInf_sInf (α := αᵒᵈ) (β := βᵒᵈ) h₁ h₂
Infimum of Binary Image under Dual Galois Connections: $\inf \{u(a, b)\} = u(\sup s, \sup t)$
Informal description
Let $\alpha$, $\beta$, and $\gamma$ be preorders, and let $u : \alpha \times \beta \to \gamma$ be a function. Suppose that for every $b \in \beta$, the composition $\text{toDual} \circ l_1(b) : \alpha \to \gamma^{\text{op}}$ and $\text{swap}\, u(b) \circ \text{ofDual} : \gamma^{\text{op}} \to \alpha$ form a Galois connection. Additionally, suppose that for every $a \in \alpha$, the composition $\text{toDual} \circ l_2(a) : \beta \to \gamma^{\text{op}}$ and $u(a) \circ \text{ofDual} : \gamma^{\text{op}} \to \beta$ form a Galois connection. Then, for any sets $s \subseteq \alpha$ and $t \subseteq \beta$, the infimum of the image $\{u(a, b) \mid a \in s, b \in t\}$ is equal to $u(\sup s, \sup t)$.
OrderIso.to_galoisConnection theorem
(e : α ≃o β) : GaloisConnection e e.symm
Full source 
/-- Makes a Galois connection from an order-preserving bijection. -/
lemma to_galoisConnection (e : α ≃o β) : GaloisConnection e e.symm :=
  fun _ _ => e.rel_symm_apply.symm
Order isomorphism induces Galois connection $(e, e^{-1})$
Informal description
Given an order isomorphism $e : \alpha \simeq_o \beta$ between two preordered types $\alpha$ and $\beta$, the pair $(e, e^{-1})$ forms a Galois connection. That is, for all $a \in \alpha$ and $b \in \beta$, we have $e(a) \leq b$ if and only if $a \leq e^{-1}(b)$.
OrderIso.toGaloisInsertion definition
(e : α ≃o β) : GaloisInsertion e e.symm
Full source 
/-- Makes a Galois insertion from an order-preserving bijection. -/
protected def toGaloisInsertion (e : α ≃o β) : GaloisInsertion e e.symm where
  choice b _ := e b
  gc := e.to_galoisConnection
  le_l_u g := le_of_eq (e.right_inv g).symm
  choice_eq _ _ := rfl
Galois insertion induced by an order isomorphism
Informal description
Given an order isomorphism $e : \alpha \simeq_o \beta$ between two preordered types $\alpha$ and $\beta$, the pair $(e, e^{-1})$ forms a Galois insertion. This means that $(e, e^{-1})$ is a Galois connection (i.e., $e(a) \leq b \leftrightarrow a \leq e^{-1}(b)$ for all $a \in \alpha$, $b \in \beta$) with the additional property that $e \circ e^{-1} = \text{id}_\beta$.
OrderIso.toGaloisCoinsertion definition
(e : α ≃o β) : GaloisCoinsertion e e.symm
Full source 
/-- Makes a Galois coinsertion from an order-preserving bijection. -/
protected def toGaloisCoinsertion (e : α ≃o β) : GaloisCoinsertion e e.symm where
  choice b _ := e.symm b
  gc := e.to_galoisConnection
  u_l_le g := le_of_eq (e.left_inv g)
  choice_eq _ _ := rfl
Galois coinsertion induced by an order isomorphism
Informal description
Given an order isomorphism \( e : \alpha \simeq_o \beta \) between two preordered types \(\alpha\) and \(\beta\), the pair \((e, e^{-1})\) forms a Galois coinsertion. This means: 1. \( e \) and \( e^{-1} \) form a Galois connection (i.e., \( e(a) \leq b \leftrightarrow a \leq e^{-1}(b) \) for all \( a \in \alpha \), \( b \in \beta \)), and 2. \( e^{-1} \circ e = \text{id}_\alpha \).
OrderIso.bddAbove_image theorem
(e : α ≃o β) {s : Set α} : BddAbove (e '' s) ↔ BddAbove s
Full source 
@[simp]
theorem bddAbove_image (e : α ≃o β) {s : Set α} : BddAboveBddAbove (e '' s) ↔ BddAbove s :=
  e.to_galoisConnection.bddAbove_l_image
Order isomorphism preserves boundedness above of images ($e(s)$ is bounded above iff $s$ is bounded above)
Informal description
Let $\alpha$ and $\beta$ be preordered types, and let $e : \alpha \simeq_o \beta$ be an order isomorphism between them. For any subset $s \subseteq \alpha$, the image $e(s)$ is bounded above in $\beta$ if and only if $s$ is bounded above in $\alpha$.
OrderIso.bddBelow_image theorem
(e : α ≃o β) {s : Set α} : BddBelow (e '' s) ↔ BddBelow s
Full source 
@[simp]
theorem bddBelow_image (e : α ≃o β) {s : Set α} : BddBelowBddBelow (e '' s) ↔ BddBelow s :=
  e.dual.bddAbove_image
Order isomorphism preserves boundedness below of images ($e(s)$ is bounded below iff $s$ is bounded below)
Informal description
Let $\alpha$ and $\beta$ be preordered types, and let $e : \alpha \simeq_o \beta$ be an order isomorphism between them. For any subset $s \subseteq \alpha$, the image $e(s)$ is bounded below in $\beta$ if and only if $s$ is bounded below in $\alpha$.
OrderIso.bddAbove_preimage theorem
(e : α ≃o β) {s : Set β} : BddAbove (e ⁻¹' s) ↔ BddAbove s
Full source 
@[simp]
theorem bddAbove_preimage (e : α ≃o β) {s : Set β} : BddAboveBddAbove (e ⁻¹' s) ↔ BddAbove s := by
  rw [← e.bddAbove_image, e.image_preimage]
Order isomorphism preserves boundedness above of preimages ($e^{-1}(s)$ is bounded above iff $s$ is bounded above)
Informal description
Let $\alpha$ and $\beta$ be preordered types, and let $e : \alpha \simeq_o \beta$ be an order isomorphism between them. For any subset $s \subseteq \beta$, the preimage $e^{-1}(s)$ is bounded above in $\alpha$ if and only if $s$ is bounded above in $\beta$.
OrderIso.bddBelow_preimage theorem
(e : α ≃o β) {s : Set β} : BddBelow (e ⁻¹' s) ↔ BddBelow s
Full source 
@[simp]
theorem bddBelow_preimage (e : α ≃o β) {s : Set β} : BddBelowBddBelow (e ⁻¹' s) ↔ BddBelow s := by
  rw [← e.bddBelow_image, e.image_preimage]
Order isomorphism preserves boundedness below of preimages ($e^{-1}(s)$ is bounded below iff $s$ is bounded below)
Informal description
Let $\alpha$ and $\beta$ be preordered types, and let $e : \alpha \simeq_o \beta$ be an order isomorphism between them. For any subset $s \subseteq \beta$, the preimage $e^{-1}(s)$ is bounded below in $\alpha$ if and only if $s$ is bounded below in $\beta$.
Nat.galoisConnection_mul_div theorem
{k : ℕ} (h : 0 < k) : GaloisConnection (fun n => n * k) fun n => n / k
Full source 
theorem galoisConnection_mul_div {k : ℕ} (h : 0 < k) :
    GaloisConnection (fun n => n * k) fun n => n / k := fun _ _ => (le_div_iff_mul_le h).symm
Galois connection between multiplication and division by a positive natural number
Informal description
For any positive natural number $k > 0$, the functions $n \mapsto n \cdot k$ (multiplication by $k$) and $n \mapsto \lfloor n / k \rfloor$ (division by $k$ with floor) form a Galois connection between the natural numbers $\mathbb{N}$ with their usual order. That is, for all $m, n \in \mathbb{N}$, we have $m \cdot k \leq n$ if and only if $m \leq \lfloor n / k \rfloor$.
GaloisInsertion.l_sup_u theorem
[SemilatticeSup α] [SemilatticeSup β] (gi : GaloisInsertion l u) (a b : β) : l (u a ⊔ u b) = a ⊔ b
Full source 
theorem l_sup_u [SemilatticeSup α] [SemilatticeSup β] (gi : GaloisInsertion l u) (a b : β) :
    l (u a ⊔ u b) = a ⊔ b :=
  calc
    l (u a ⊔ u b) = l (u a) ⊔ l (u b) := gi.gc.l_sup
    _ = a ⊔ b := by simp only [gi.l_u_eq]
Galois insertion preserves suprema: $l(u(a) \sqcup u(b)) = a \sqcup b$
Informal description
Let $\alpha$ and $\beta$ be join-semilattices, and let $(l, u)$ be a Galois insertion between them. For any two elements $a, b \in \beta$, the image under $l$ of the supremum of their preimages under $u$ equals the supremum of $a$ and $b$, i.e., $l(u(a) \sqcup u(b)) = a \sqcup b$.
GaloisInsertion.l_iSup_u theorem
[CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) {ι : Sort x} (f : ι → β) : l (⨆ i, u (f i)) = ⨆ i, f i
Full source 
theorem l_iSup_u [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) {ι : Sort x}
    (f : ι → β) : l (⨆ i, u (f i)) = ⨆ i, f i :=
  calc
    l (⨆ i : ι, u (f i)) = ⨆ i : ι, l (u (f i)) := gi.gc.l_iSup
    _ = ⨆ i : ι, f i := congr_arg _ <| funext fun i => gi.l_u_eq (f i)
Lower adjoint preserves suprema under Galois insertion: $l(\bigsqcup_i u(f_i)) = \bigsqcup_i f_i$
Informal description
Let $\alpha$ and $\beta$ be complete lattices, and let $(l, u)$ be a Galois insertion between them. For any indexed family of elements $f : \iota \to \beta$, the lower adjoint $l$ satisfies: \[ l\left(\bigsqcup_{i} u(f(i))\right) = \bigsqcup_{i} f(i). \]
GaloisInsertion.l_biSup_u theorem
[CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) {ι : Sort x} {p : ι → Prop} (f : ∀ i, p i → β) : l (⨆ (i) (hi), u (f i hi)) = ⨆ (i) (hi), f i hi
Full source 
theorem l_biSup_u [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) {ι : Sort x}
    {p : ι → Prop} (f : ∀ i, p i → β) : l (⨆ (i) (hi), u (f i hi)) = ⨆ (i) (hi), f i hi := by
  simp only [iSup_subtype', gi.l_iSup_u]
Lower adjoint preserves bounded suprema under Galois insertion: $l(\bigsqcup_{i,p(i)} u(f_i)) = \bigsqcup_{i,p(i)} f_i$
Informal description
Let $\alpha$ and $\beta$ be complete lattices, and let $(l, u)$ be a Galois insertion between them. For any indexed family of elements $f : \iota \to \beta$ defined on a predicate $p : \iota \to \text{Prop}$, the lower adjoint $l$ satisfies: \[ l\left(\bigsqcup_{\substack{i \\ p(i)}} u(f(i))\right) = \bigsqcup_{\substack{i \\ p(i)}} f(i). \]
GaloisInsertion.l_sSup_u_image theorem
[CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) (s : Set β) : l (sSup (u '' s)) = sSup s
Full source 
theorem l_sSup_u_image [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u)
    (s : Set β) : l (sSup (u '' s)) = sSup s := by rw [sSup_image, gi.l_biSup_u, sSup_eq_iSup]
Lower adjoint preserves suprema of images under upper adjoint in Galois insertion: $l(\bigsqcup u[s]) = \bigsqcup s$
Informal description
Let $\alpha$ and $\beta$ be complete lattices, and let $(l, u)$ be a Galois insertion between them. For any subset $s \subseteq \beta$, the lower adjoint $l$ satisfies: \[ l\left(\bigsqcup (u \text{''} s)\right) = \bigsqcup s \] where $u \text{''} s$ denotes the image of $s$ under $u$.
GaloisInsertion.l_inf_u theorem
[SemilatticeInf α] [SemilatticeInf β] (gi : GaloisInsertion l u) (a b : β) : l (u a ⊓ u b) = a ⊓ b
Full source 
theorem l_inf_u [SemilatticeInf α] [SemilatticeInf β] (gi : GaloisInsertion l u) (a b : β) :
    l (u a ⊓ u b) = a ⊓ b :=
  calc
    l (u a ⊓ u b) = l (u (a ⊓ b)) := congr_arg l gi.gc.u_inf.symm
    _ = a ⊓ b := by simp only [gi.l_u_eq]
Lower Adjoint Preserves Infima in Galois Insertion: $l(u(a) \sqcap u(b)) = a \sqcap b$
Informal description
Let $\alpha$ and $\beta$ be meet-semilattices, and let $(l, u)$ be a Galois insertion between them. For any two elements $a, b \in \beta$, the image under $l$ of the infimum of their upper adjoints equals the infimum of $a$ and $b$, i.e., $l(u(a) \sqcap u(b)) = a \sqcap b$.
GaloisInsertion.l_iInf_u theorem
[CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) {ι : Sort x} (f : ι → β) : l (⨅ i, u (f i)) = ⨅ i, f i
Full source 
theorem l_iInf_u [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) {ι : Sort x}
    (f : ι → β) : l (⨅ i, u (f i)) = ⨅ i, f i :=
  calc
    l (⨅ i : ι, u (f i)) = l (u (⨅ i : ι, f i)) := congr_arg l gi.gc.u_iInf.symm
    _ = ⨅ i : ι, f i := gi.l_u_eq _
Lower Adjoint Preserves Indexed Infima in Galois Insertion
Informal description
Let $\alpha$ and $\beta$ be complete lattices, and let $(l, u)$ be a Galois insertion between them. For any indexed family of elements $f : \iota \to \beta$, the lower adjoint $l$ satisfies the identity: \[ l\left(\bigsqcap_{i} u(f(i))\right) = \bigsqcap_{i} f(i). \]
GaloisInsertion.l_biInf_u theorem
[CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) {ι : Sort x} {p : ι → Prop} (f : ∀ (i) (_ : p i), β) : l (⨅ (i) (hi), u (f i hi)) = ⨅ (i) (hi), f i hi
Full source 
theorem l_biInf_u [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) {ι : Sort x}
    {p : ι → Prop} (f : ∀ (i) (_ : p i), β) : l (⨅ (i) (hi), u (f i hi)) = ⨅ (i) (hi), f i hi := by
  simp only [iInf_subtype', gi.l_iInf_u]
Lower Adjoint Preserves Bounded Indexed Infima in Galois Insertion: $l(\bigsqcap_{p(i)} u(f(i))) = \bigsqcap_{p(i)} f(i)$
Informal description
Let $\alpha$ and $\beta$ be complete lattices, and let $(l, u)$ be a Galois insertion between them. For any indexed family of elements $f : \iota \to \beta$ with a predicate $p : \iota \to \text{Prop}$, the lower adjoint $l$ satisfies: \[ l\left(\bigsqcap_{\substack{i \\ p(i)}} u(f(i))\right) = \bigsqcap_{\substack{i \\ p(i)}} f(i). \]
GaloisInsertion.l_sInf_u_image theorem
[CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) (s : Set β) : l (sInf (u '' s)) = sInf s
Full source 
theorem l_sInf_u_image [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u)
    (s : Set β) : l (sInf (u '' s)) = sInf s := by rw [sInf_image, gi.l_biInf_u, sInf_eq_iInf]
Lower Adjoint Preserves Infimum of Image under Upper Adjoint in Galois Insertion: $l(\bigsqcap u[s]) = \bigsqcap s$
Informal description
Let $\alpha$ and $\beta$ be complete lattices, and let $(l, u)$ be a Galois insertion between them. For any subset $s \subseteq \beta$, the lower adjoint $l$ satisfies: \[ l\left(\bigsqcap (u '' s)\right) = \bigsqcap s, \] where $u '' s$ denotes the image of $s$ under $u$.
GaloisInsertion.l_iInf_of_ul_eq_self theorem
[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)
Full source 
theorem l_iInf_of_ul_eq_self [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) :=
  calc
    l (⨅ i, f i) = l (⨅ i : ι, u (l (f i))) := by simp [hf]
    _ = ⨅ i, l (f i) := gi.l_iInf_u _
Lower Adjoint Preserves Indexed Infima under Galois Insertion with Fixed Point Condition
Informal description
Let $\alpha$ and $\beta$ be complete lattices, and let $(l, u)$ be a Galois insertion between them. For any indexed family of elements $f : \iota \to \alpha$ such that $u(l(f(i))) = f(i)$ for all $i$, the lower adjoint $l$ satisfies: \[ l\left(\bigsqcap_{i} f(i)\right) = \bigsqcap_{i} l(f(i)). \]
GaloisInsertion.l_biInf_of_ul_eq_self theorem
[CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) {ι : Sort x} {p : ι → Prop} (f : ∀ (i) (_ : p i), α) (hf : ∀ i hi, u (l (f i hi)) = f i hi) : l (⨅ (i) (hi), f i hi) = ⨅ (i) (hi), l (f i hi)
Full source 
theorem l_biInf_of_ul_eq_self [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u)
    {ι : Sort x} {p : ι → Prop} (f : ∀ (i) (_ : p i), α) (hf : ∀ i hi, u (l (f i hi)) = f i hi) :
    l (⨅ (i) (hi), f i hi) = ⨅ (i) (hi), l (f i hi) := by
  rw [iInf_subtype', iInf_subtype']
  exact gi.l_iInf_of_ul_eq_self _ fun _ => hf _ _
Lower Adjoint Preserves Bounded Indexed Infima under Galois Insertion with Fixed Point Condition
Informal description
Let $\alpha$ and $\beta$ be complete lattices, and let $(l, u)$ be a Galois insertion between them. For any indexed family of elements $f : \iota \to \alpha$ (where $p(i)$ holds for each $i \in \iota$) such that $u(l(f(i, hi))) = f(i, hi)$ for all $i$ and $hi : p(i)$, the lower adjoint $l$ satisfies: \[ l\left(\bigsqcap_{\substack{i \\ p(i)}} f(i, hi)\right) = \bigsqcap_{\substack{i \\ p(i)}} l(f(i, hi)). \]
GaloisInsertion.isLUB_of_u_image theorem
[Preorder α] [Preorder β] (gi : GaloisInsertion l u) {s : Set β} {a : α} (hs : IsLUB (u '' s) a) : IsLUB s (l a)
Full source 
theorem isLUB_of_u_image [Preorder α] [Preorder β] (gi : GaloisInsertion l u) {s : Set β} {a : α}
    (hs : IsLUB (u '' s) a) : IsLUB s (l a) :=
  ⟨fun x hx => (gi.le_l_u x).trans <| gi.gc.monotone_l <| hs.1 <| mem_image_of_mem _ hx, fun _ hx =>
    gi.gc.l_le <| hs.2 <| gi.gc.monotone_u.mem_upperBounds_image hx⟩
Least Upper Bound Preservation under Galois Insertion
Informal description
Let $\alpha$ and $\beta$ be preorders, and let $l : \alpha \to \beta$ and $u : \beta \to \alpha$ form a Galois insertion. For any subset $s \subseteq \beta$ and element $a \in \alpha$, if $a$ is the least upper bound of the image $u(s) \subseteq \alpha$, then $l(a)$ is the least upper bound of $s$ in $\beta$.
GaloisInsertion.isGLB_of_u_image theorem
[Preorder α] [Preorder β] (gi : GaloisInsertion l u) {s : Set β} {a : α} (hs : IsGLB (u '' s) a) : IsGLB s (l a)
Full source 
theorem isGLB_of_u_image [Preorder α] [Preorder β] (gi : GaloisInsertion l u) {s : Set β} {a : α}
    (hs : IsGLB (u '' s) a) : IsGLB s (l a) :=
  ⟨fun _ hx => gi.gc.l_le <| hs.1 <| mem_image_of_mem _ hx, fun x hx =>
    (gi.le_l_u x).trans <| gi.gc.monotone_l <| hs.2 <| gi.gc.monotone_u.mem_lowerBounds_image hx⟩
Greatest lower bound preservation under Galois insertion
Informal description
Let $\alpha$ and $\beta$ be preorders, and let $(l, u)$ be a Galois insertion between them. For any subset $s \subseteq \beta$ and element $a \in \alpha$, if $a$ is the greatest lower bound of the image $u(s) \subseteq \alpha$, then $l(a)$ is the greatest lower bound of $s$ in $\beta$.
GaloisInsertion.liftSemilatticeSup abbrev
[SemilatticeSup α] (gi : GaloisInsertion l u) : SemilatticeSup β
Full source 
/-- Lift the suprema along a Galois insertion -/
abbrev liftSemilatticeSup [SemilatticeSup α] (gi : GaloisInsertion l u) : SemilatticeSup β :=
  { ‹PartialOrder β› with
    sup := fun a b => l (u a ⊔ u b)
    le_sup_left := fun a _ => (gi.le_l_u a).trans <| gi.gc.monotone_l <| le_sup_left
    le_sup_right := fun _ b => (gi.le_l_u b).trans <| gi.gc.monotone_l <| le_sup_right
    sup_le := fun _ _ _ hac hbc =>
      gi.gc.l_le <| sup_le (gi.gc.monotone_u hac) (gi.gc.monotone_u hbc) }
Lifting Join-Semilattice Structure via Galois Insertion
Informal description
Given a Galois insertion between preorders $\alpha$ and $\beta$ (with $l : \alpha \to \beta$ and $u : \beta \to \alpha$), if $\alpha$ is a join-semilattice, then $\beta$ can be equipped with a join-semilattice structure where the join operation is defined via the Galois insertion.
GaloisInsertion.liftSemilatticeInf abbrev
[SemilatticeInf α] (gi : GaloisInsertion l u) : SemilatticeInf β
Full source 
/-- Lift the infima along a Galois insertion -/
abbrev liftSemilatticeInf [SemilatticeInf α] (gi : GaloisInsertion l u) : SemilatticeInf β :=
  { ‹PartialOrder β› with
    inf := fun a b =>
      gi.choice (u a ⊓ u b) <|
        le_inf (gi.gc.monotone_u <| gi.gc.l_le <| inf_le_left)
          (gi.gc.monotone_u <| gi.gc.l_le <| inf_le_right)
    inf_le_left := by simp only [gi.choice_eq]; exact fun a b => gi.gc.l_le inf_le_left
    inf_le_right := by simp only [gi.choice_eq]; exact fun a b => gi.gc.l_le inf_le_right
    le_inf := by
      simp only [gi.choice_eq]
      exact fun a b c hac hbc =>
        (gi.le_l_u a).trans <|
          gi.gc.monotone_l <| le_inf (gi.gc.monotone_u hac) (gi.gc.monotone_u hbc) }
Lifting Meet-Semilattice Structure via Galois Insertion
Informal description
Given a Galois insertion between preorders $\alpha$ and $\beta$ (with $l : \alpha \to \beta$ and $u : \beta \to \alpha$), if $\alpha$ is a meet-semilattice, then $\beta$ can be equipped with a meet-semilattice structure where the meet operation is defined via the Galois insertion.
GaloisInsertion.liftLattice abbrev
[Lattice α] (gi : GaloisInsertion l u) : Lattice β
Full source 
/-- Lift the suprema and infima along a Galois insertion -/
abbrev liftLattice [Lattice α] (gi : GaloisInsertion l u) : Lattice β :=
  { gi.liftSemilatticeSup, gi.liftSemilatticeInf with }
Lifting Lattice Structure via Galois Insertion
Informal description
Given a Galois insertion between preorders $\alpha$ and $\beta$ (with $l : \alpha \to \beta$ and $u : \beta \to \alpha$), if $\alpha$ is a lattice, then $\beta$ can be equipped with a lattice structure where the join and meet operations are defined via the Galois insertion.
GaloisInsertion.liftOrderTop abbrev
[Preorder α] [OrderTop α] (gi : GaloisInsertion l u) : OrderTop β
Full source 
/-- Lift the top along a Galois insertion -/
abbrev liftOrderTop [Preorder α] [OrderTop α] (gi : GaloisInsertion l u) :
    OrderTop β where
  top := gi.choice ⊤ <| le_top
  le_top := by
    simp only [gi.choice_eq]; exact fun b => (gi.le_l_u b).trans (gi.gc.monotone_l le_top)
Lifting of Top Element via Galois Insertion
Informal description
Given a Galois insertion between preorders $\alpha$ and $\beta$ (with $l : \alpha \to \beta$ and $u : \beta \to \alpha$), if $\alpha$ has a greatest element $\top_\alpha$, then $\beta$ can be equipped with a greatest element $\top_\beta$ defined via the Galois insertion.
GaloisInsertion.liftBoundedOrder abbrev
[Preorder α] [BoundedOrder α] (gi : GaloisInsertion l u) : BoundedOrder β
Full source 
/-- Lift the top, bottom, suprema, and infima along a Galois insertion -/
abbrev liftBoundedOrder [Preorder α] [BoundedOrder α] (gi : GaloisInsertion l u) : BoundedOrder β :=
  { gi.liftOrderTop, gi.gc.liftOrderBot with }
Lifting Bounded Order Structure via Galois Insertion
Informal description
Given a Galois insertion $(l, u)$ between preorders $\alpha$ and $\beta$, if $\alpha$ is a bounded order (i.e., has both a greatest element $\top$ and a least element $\bot$), then $\beta$ can be equipped with a bounded order structure where the top and bottom elements are defined via the Galois insertion.
GaloisInsertion.liftCompleteLattice abbrev
[CompleteLattice α] (gi : GaloisInsertion l u) : CompleteLattice β
Full source 
/-- Lift all suprema and infima along a Galois insertion -/
abbrev liftCompleteLattice [CompleteLattice α] (gi : GaloisInsertion l u) : CompleteLattice β :=
  { gi.liftBoundedOrder, gi.liftLattice with
    sSup := fun s => l (sSup (u '' s))
    sSup_le := fun _ => (gi.isLUB_of_u_image (isLUB_sSup _)).2
    le_sSup := fun _ => (gi.isLUB_of_u_image (isLUB_sSup _)).1
    sInf := fun s =>
      gi.choice (sInf (u '' s)) <|
        (isGLB_sInf _).2 <|
          gi.gc.monotone_u.mem_lowerBounds_image (gi.isGLB_of_u_image <| isGLB_sInf _).1
    sInf_le := fun s => by rw [gi.choice_eq]; exact (gi.isGLB_of_u_image (isGLB_sInf _)).1
    le_sInf := fun s => by rw [gi.choice_eq]; exact (gi.isGLB_of_u_image (isGLB_sInf _)).2 }
Lifting Complete Lattice Structure via Galois Insertion
Informal description
Given a Galois insertion $(l, u)$ between preorders $\alpha$ and $\beta$, if $\alpha$ is a complete lattice, then $\beta$ can be equipped with a complete lattice structure where all suprema and infima are defined via the Galois insertion.
GaloisCoinsertion.u_inf_l theorem
[SemilatticeInf α] [SemilatticeInf β] (gi : GaloisCoinsertion l u) (a b : α) : u (l a ⊓ l b) = a ⊓ b
Full source 
theorem u_inf_l [SemilatticeInf α] [SemilatticeInf β] (gi : GaloisCoinsertion l u) (a b : α) :
    u (l a ⊓ l b) = a ⊓ b :=
  gi.dual.l_sup_u a b
Galois coinsertion preserves infima: $u(l(a) \sqcap l(b)) = a \sqcap b$
Informal description
Let $\alpha$ and $\beta$ be meet-semilattices, and let $(l, u)$ be a Galois coinsertion between them. For any two elements $a, b \in \alpha$, the image under $u$ of the infimum of their images under $l$ equals the infimum of $a$ and $b$, i.e., $u(l(a) \sqcap l(b)) = a \sqcap b$.
GaloisCoinsertion.u_iInf_l theorem
[CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u) {ι : Sort x} (f : ι → α) : u (⨅ i, l (f i)) = ⨅ i, f i
Full source 
theorem u_iInf_l [CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u) {ι : Sort x}
    (f : ι → α) : u (⨅ i, l (f i)) = ⨅ i, f i :=
  gi.dual.l_iSup_u _
Upper Adjoint Preserves Infima under Galois Coinsertion: $u(\bigsqcap_i l(f_i)) = \bigsqcap_i f_i$
Informal description
Let $\alpha$ and $\beta$ be complete lattices, and let $(l, u)$ be a Galois coinsertion between them. For any indexed family of elements $f : \iota \to \alpha$, the upper adjoint $u$ satisfies: \[ u\left(\bigsqcap_{i} l(f(i))\right) = \bigsqcap_{i} f(i). \]
GaloisCoinsertion.u_sInf_l_image theorem
[CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u) (s : Set α) : u (sInf (l '' s)) = sInf s
Full source 
theorem u_sInf_l_image [CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u)
    (s : Set α) : u (sInf (l '' s)) = sInf s :=
  gi.dual.l_sSup_u_image _
Upper Adjoint Preserves Infima of Images under Lower Adjoint in Galois Coinsertion: $u(\bigsqcap l[s]) = \bigsqcap s$
Informal description
Let $\alpha$ and $\beta$ be complete lattices, and let $(l, u)$ be a Galois coinsertion between them. For any subset $s \subseteq \alpha$, the upper adjoint $u$ satisfies: \[ u\left(\bigsqcap (l \text{''} s)\right) = \bigsqcap s \] where $l \text{''} s$ denotes the image of $s$ under $l$.
GaloisCoinsertion.u_sup_l theorem
[SemilatticeSup α] [SemilatticeSup β] (gi : GaloisCoinsertion l u) (a b : α) : u (l a ⊔ l b) = a ⊔ b
Full source 
theorem u_sup_l [SemilatticeSup α] [SemilatticeSup β] (gi : GaloisCoinsertion l u) (a b : α) :
    u (l a ⊔ l b) = a ⊔ b :=
  gi.dual.l_inf_u _ _
Upper Adjoint Preserves Suprema in Galois Coinsertion: $u(l(a) \sqcup l(b)) = a \sqcup b$
Informal description
Let $\alpha$ and $\beta$ be join-semilattices, and let $(l, u)$ be a Galois coinsertion between them. For any two elements $a, b \in \alpha$, the upper adjoint $u$ satisfies: \[ u(l(a) \sqcup l(b)) = a \sqcup b. \]
GaloisCoinsertion.u_iSup_l theorem
[CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u) {ι : Sort x} (f : ι → α) : u (⨆ i, l (f i)) = ⨆ i, f i
Full source 
theorem u_iSup_l [CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u) {ι : Sort x}
    (f : ι → α) : u (⨆ i, l (f i)) = ⨆ i, f i :=
  gi.dual.l_iInf_u _
Upper Adjoint Preserves Indexed Suprema in Galois Coinsertion: $u(\bigsqcup_i l(f(i))) = \bigsqcup_i f(i)$
Informal description
Let $\alpha$ and $\beta$ be complete lattices, and let $(l, u)$ be a Galois coinsertion between them. For any indexed family of elements $f : \iota \to \alpha$, the upper adjoint $u$ satisfies: \[ u\left(\bigsqcup_{i} l(f(i))\right) = \bigsqcup_{i} f(i). \]
GaloisCoinsertion.u_biSup_l theorem
[CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u) {ι : Sort x} {p : ι → Prop} (f : ∀ (i) (_ : p i), α) : u (⨆ (i) (hi), l (f i hi)) = ⨆ (i) (hi), f i hi
Full source 
theorem u_biSup_l [CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u) {ι : Sort x}
    {p : ι → Prop} (f : ∀ (i) (_ : p i), α) : u (⨆ (i) (hi), l (f i hi)) = ⨆ (i) (hi), f i hi :=
  gi.dual.l_biInf_u _
Upper Adjoint Preserves Bounded Indexed Suprema in Galois Coinsertion: $u(\bigsqcup_{p(i)} l(f(i))) = \bigsqcup_{p(i)} f(i)$
Informal description
Let $\alpha$ and $\beta$ be complete lattices, and let $(l, u)$ be a Galois coinsertion between them. For any indexed family of elements $f : \iota \to \alpha$ with a predicate $p : \iota \to \text{Prop}$, the upper adjoint $u$ satisfies: \[ u\left(\bigsqcup_{\substack{i \\ p(i)}} l(f(i))\right) = \bigsqcup_{\substack{i \\ p(i)}} f(i). \]
GaloisCoinsertion.u_sSup_l_image theorem
[CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u) (s : Set α) : u (sSup (l '' s)) = sSup s
Full source 
theorem u_sSup_l_image [CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u)
    (s : Set α) : u (sSup (l '' s)) = sSup s :=
  gi.dual.l_sInf_u_image _
Upper Adjoint Preserves Supremum of Image under Lower Adjoint in Galois Coinsertion: $u(\bigsqcup l[s]) = \bigsqcup s$
Informal description
Let $\alpha$ and $\beta$ be complete lattices, and let $(l, u)$ be a Galois coinsertion between them. For any subset $s \subseteq \alpha$, the upper adjoint $u$ satisfies: \[ u\left(\bigsqcup (l '' s)\right) = \bigsqcup s, \] where $l '' s$ denotes the image of $s$ under $l$.
GaloisCoinsertion.u_iSup_of_lu_eq_self theorem
[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)
Full source 
theorem u_iSup_of_lu_eq_self [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) :=
  gi.dual.l_iInf_of_ul_eq_self _ hf
Upper Adjoint Preserves Indexed Suprema under Galois Coinsertion with Fixed Point Condition
Informal description
Let $\alpha$ and $\beta$ be complete lattices, and let $(l, u)$ form a Galois coinsertion between them. For any indexed family of elements $f : \iota \to \beta$ such that $l(u(f(i))) = f(i)$ for all $i$, the upper adjoint $u$ satisfies: \[ u\left(\bigsqcup_{i} f(i)\right) = \bigsqcup_{i} u(f(i)). \]
GaloisCoinsertion.u_biSup_of_lu_eq_self theorem
[CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u) {ι : Sort x} {p : ι → Prop} (f : ∀ (i) (_ : p i), β) (hf : ∀ i hi, l (u (f i hi)) = f i hi) : u (⨆ (i) (hi), f i hi) = ⨆ (i) (hi), u (f i hi)
Full source 
theorem u_biSup_of_lu_eq_self [CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u)
    {ι : Sort x} {p : ι → Prop} (f : ∀ (i) (_ : p i), β) (hf : ∀ i hi, l (u (f i hi)) = f i hi) :
    u (⨆ (i) (hi), f i hi) = ⨆ (i) (hi), u (f i hi) :=
  gi.dual.l_biInf_of_ul_eq_self _ hf
Upper Adjoint Preserves Bounded Indexed Suprema under Galois Coinsertion with Fixed Point Condition
Informal description
Let $\alpha$ and $\beta$ be complete lattices, and let $(l, u)$ form a Galois coinsertion between them. For any indexed family of elements $f : \iota \to \beta$ (where $p(i)$ holds for each $i \in \iota$) such that $l(u(f(i, hi))) = f(i, hi)$ for all $i$ and $hi : p(i)$, the upper adjoint $u$ satisfies: \[ u\left(\bigsqcup_{\substack{i \\ p(i)}} f(i, hi)\right) = \bigsqcup_{\substack{i \\ p(i)}} u(f(i, hi)). \]
GaloisCoinsertion.isGLB_of_l_image theorem
[Preorder α] [Preorder β] (gi : GaloisCoinsertion l u) {s : Set α} {a : β} (hs : IsGLB (l '' s) a) : IsGLB s (u a)
Full source 
theorem isGLB_of_l_image [Preorder α] [Preorder β] (gi : GaloisCoinsertion l u) {s : Set α} {a : β}
    (hs : IsGLB (l '' s) a) : IsGLB s (u a) :=
  gi.dual.isLUB_of_u_image hs
Greatest Lower Bound Preservation under Galois Coinsertion
Informal description
Let $\alpha$ and $\beta$ be preorders, and let $l : \alpha \to \beta$ and $u : \beta \to \alpha$ form a Galois coinsertion. For any subset $s \subseteq \alpha$ and element $a \in \beta$, if $a$ is the greatest lower bound of the image $l(s) \subseteq \beta$, then $u(a)$ is the greatest lower bound of $s$ in $\alpha$.
GaloisCoinsertion.isLUB_of_l_image theorem
[Preorder α] [Preorder β] (gi : GaloisCoinsertion l u) {s : Set α} {a : β} (hs : IsLUB (l '' s) a) : IsLUB s (u a)
Full source 
theorem isLUB_of_l_image [Preorder α] [Preorder β] (gi : GaloisCoinsertion l u) {s : Set α} {a : β}
    (hs : IsLUB (l '' s) a) : IsLUB s (u a) :=
  gi.dual.isGLB_of_u_image hs
Least upper bound preservation under Galois coinsertion
Informal description
Let $\alpha$ and $\beta$ be preorders, and let $(l, u)$ be a Galois coinsertion between them. For any subset $s \subseteq \alpha$ and element $a \in \beta$, if $a$ is the least upper bound of the image $l(s) \subseteq \beta$, then $u(a)$ is the least upper bound of $s$ in $\alpha$.
GaloisCoinsertion.liftSemilatticeInf abbrev
[SemilatticeInf β] (gi : GaloisCoinsertion l u) : SemilatticeInf α
Full source 
/-- Lift the infima along a Galois coinsertion -/
abbrev liftSemilatticeInf [SemilatticeInf β] (gi : GaloisCoinsertion l u) : SemilatticeInf α :=
  { ‹PartialOrder α› with
    inf_le_left := fun a b =>
      (@OrderDual.instSemilatticeInf αᵒᵈ gi.dual.liftSemilatticeSup).inf_le_left a b
    inf_le_right := fun a b =>
      (@OrderDual.instSemilatticeInf αᵒᵈ gi.dual.liftSemilatticeSup).inf_le_right a b
    le_inf := fun a b c =>
      (@OrderDual.instSemilatticeInf αᵒᵈ gi.dual.liftSemilatticeSup).le_inf a b c
    inf := fun a b => u (l a ⊓ l b) }
Lifting of Meet-Semilattice Structure via Galois Coinsertion
Informal description
Given a Galois coinsertion between preorders $\alpha$ and $\beta$ with functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$, if $\beta$ is a meet-semilattice, then $\alpha$ can be equipped with a meet-semilattice structure where the meet operation is defined via the Galois coinsertion.
GaloisCoinsertion.liftSemilatticeSup abbrev
[SemilatticeSup β] (gi : GaloisCoinsertion l u) : SemilatticeSup α
Full source 
/-- Lift the suprema along a Galois coinsertion -/
abbrev liftSemilatticeSup [SemilatticeSup β] (gi : GaloisCoinsertion l u) : SemilatticeSup α :=
  { ‹PartialOrder α› with
    sup := fun a b =>
      gi.choice (l a ⊔ l b) <|
        sup_le (gi.gc.monotone_l <| gi.gc.le_u <| le_sup_left)
          (gi.gc.monotone_l <| gi.gc.le_u <| le_sup_right)
    le_sup_left := fun a b =>
      (@OrderDual.instSemilatticeSup αᵒᵈ gi.dual.liftSemilatticeInf).le_sup_left a b
    le_sup_right := fun a b =>
      (@OrderDual.instSemilatticeSup αᵒᵈ gi.dual.liftSemilatticeInf).le_sup_right a b
    sup_le := fun a b c =>
      (@OrderDual.instSemilatticeSup αᵒᵈ gi.dual.liftSemilatticeInf).sup_le a b c }
Lifting of Join-Semilattice Structure via Galois Coinsertion
Informal description
Given a Galois coinsertion between preorders $\alpha$ and $\beta$ with functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$, if $\beta$ is a join-semilattice, then $\alpha$ can be equipped with a join-semilattice structure where the join operation is defined via the Galois coinsertion.
GaloisCoinsertion.liftLattice abbrev
[Lattice β] (gi : GaloisCoinsertion l u) : Lattice α
Full source 
/-- Lift the suprema and infima along a Galois coinsertion -/
abbrev liftLattice [Lattice β] (gi : GaloisCoinsertion l u) : Lattice α :=
  { gi.liftSemilatticeSup, gi.liftSemilatticeInf with }
Lifting of Lattice Structure via Galois Coinsertion
Informal description
Given a Galois coinsertion between preorders $\alpha$ and $\beta$ with functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$, if $\beta$ is a lattice, then $\alpha$ can be equipped with a lattice structure where the join and meet operations are defined via the Galois coinsertion.
GaloisCoinsertion.liftOrderBot abbrev
[Preorder β] [OrderBot β] (gi : GaloisCoinsertion l u) : OrderBot α
Full source 
/-- Lift the bot along a Galois coinsertion -/
abbrev liftOrderBot [Preorder β] [OrderBot β] (gi : GaloisCoinsertion l u) : OrderBot α :=
  { @OrderDual.instOrderBot _ _ gi.dual.liftOrderTop with bot := gi.choice ⊥ <| bot_le }
Lifting of Bottom Element via Galois Coinsertion
Informal description
Given a Galois coinsertion between preorders $\alpha$ and $\beta$ with functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$, if $\beta$ has a least element $\bot_\beta$, then $\alpha$ can be equipped with a least element $\bot_\alpha$ defined via the Galois coinsertion.
GaloisCoinsertion.liftBoundedOrder abbrev
[Preorder β] [BoundedOrder β] (gi : GaloisCoinsertion l u) : BoundedOrder α
Full source 
/-- Lift the top, bottom, suprema, and infima along a Galois coinsertion -/
abbrev liftBoundedOrder
    [Preorder β] [BoundedOrder β] (gi : GaloisCoinsertion l u) : BoundedOrder α :=
  { gi.liftOrderBot, gi.gc.liftOrderTop with }
Lifting Bounded Order Structure via Galois Coinsertion
Informal description
Given a Galois coinsertion between preorders $\alpha$ and $\beta$ with functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$, if $\beta$ is a bounded order (i.e., has both a greatest element $\top_\beta$ and a least element $\bot_\beta$), then $\alpha$ can be equipped with a bounded order structure where: - The greatest element is defined as $u(\top_\beta)$ - The least element is defined as $u(\bot_\beta)$
GaloisCoinsertion.liftCompleteLattice abbrev
[CompleteLattice β] (gi : GaloisCoinsertion l u) : CompleteLattice α
Full source 
/-- Lift all suprema and infima along a Galois coinsertion -/
abbrev liftCompleteLattice [CompleteLattice β] (gi : GaloisCoinsertion l u) : CompleteLattice α :=
  { @OrderDual.instCompleteLattice αᵒᵈ gi.dual.liftCompleteLattice with
    sInf := fun s => u (sInf (l '' s))
    sSup := fun s => gi.choice (sSup (l '' s)) _ }
Lifting Complete Lattice Structure via Galois Coinsertion
Informal description
Given a Galois coinsertion $(l, u)$ between preorders $\alpha$ and $\beta$, if $\beta$ is a complete lattice, then $\alpha$ can be equipped with a complete lattice structure where all suprema and infima are defined via the Galois coinsertion.
gi_sSup_Iic definition
[CompleteSemilatticeSup α] : GaloisInsertion (sSup : Set α → α) (Iic : α → Set α)
Full source 
/-- `sSup` and `Iic` form a Galois insertion. -/
def gi_sSup_Iic [CompleteSemilatticeSup α] :
    GaloisInsertion (sSup : Set α → α) (Iic : α → Set α) :=
  gc_sSup_Iic.toGaloisInsertion fun _ ↦ le_sSup le_rfl
Galois insertion between suprema and lower sets in complete semilattices
Informal description
For any complete semilattice with supremum $\alpha$, the pair of functions $\operatorname{sSup} : \mathcal{P}(\alpha) \to \alpha$ (taking the supremum of a set) and $\operatorname{Iic} : \alpha \to \mathcal{P}(\alpha)$ (mapping an element to its lower set $\{x \in \alpha \mid x \leq a\}$) forms a Galois insertion. This means that: 1. They form a Galois connection: $\operatorname{sSup}(S) \leq a$ if and only if $S \subseteq \operatorname{Iic}(a)$ for any $S \subseteq \alpha$ and $a \in \alpha$. 2. The composition $\operatorname{sSup} \circ \operatorname{Iic}$ is the identity on $\alpha$, i.e., $\operatorname{sSup}(\operatorname{Iic}(a)) = a$ for all $a \in \alpha$.
gci_Ici_sInf definition
[CompleteSemilatticeInf α] : GaloisCoinsertion (toDual ∘ Ici : α → (Set α)ᵒᵈ) (sInf ∘ ofDual : (Set α)ᵒᵈ → α)
Full source 
/-- `toDual ∘ Ici` and `sInf ∘ ofDual` form a Galois coinsertion. -/
def gci_Ici_sInf [CompleteSemilatticeInf α] :
    GaloisCoinsertion (toDualtoDual ∘ Ici : α → (Set α)ᵒᵈ) (sInfsInf ∘ ofDual : (Set α)ᵒᵈ → α) :=
  gc_Ici_sInf.toGaloisCoinsertion fun _ ↦ sInf_le le_rfl
Galois coinsertion between meet-semilattice and dual power set via upper closures and infima
Informal description
For a complete meet-semilattice $\alpha$, the pair of functions $(f, g)$, where $f : \alpha \to (\mathcal{P}(\alpha))^{\text{op}}$ is defined by $f(a) = [a, \infty)$ (interpreted in the dual order) and $g : (\mathcal{P}(\alpha))^{\text{op}} \to \alpha$ is defined by $g(S) = \bigwedge S$, forms a Galois coinsertion. That is: 1. $f$ and $g$ form a Galois connection (i.e., $f(a) \leq^{\text{op}} S$ if and only if $a \leq g(S)$ for all $a \in \alpha$ and $S \in \mathcal{P}(\alpha)^{\text{op}}$). 2. The composition $g \circ f$ is the identity function on $\alpha$ (i.e., $\bigwedge [a, \infty) = a$ for all $a \in \alpha$).
WithBot.giUnbotDBot definition
[Preorder α] [OrderBot α] : GaloisInsertion (WithBot.unbotD ⊥) (some : α → WithBot α)
Full source 
/-- If `α` is a partial order with bottom element (e.g., `ℕ`, `ℝ≥0`), then `WithBot.unbot' ⊥` and
coercion form a Galois insertion. -/
def WithBot.giUnbotDBot [Preorder α] [OrderBot α] :
    GaloisInsertion (WithBot.unbotD ⊥) (some : α → WithBot α) where
  gc _ _ := WithBot.unbotD_le_iff (fun _ ↦ bot_le)
  le_l_u _ := le_rfl
  choice o _ := o.unbotD ⊥
  choice_eq _ _ := rfl
Galois insertion between $\alpha$ and $\text{WithBot }\alpha$ via default extraction and embedding
Informal description
Given a preorder $\alpha$ with a bottom element $\bot$, the functions $\text{WithBot.unbotD} \bot$ (which extracts the value from $\text{WithBot }\alpha$ using $\bot$ as the default) and the embedding $\text{WithBot.some} : \alpha \to \text{WithBot }\alpha$ form a Galois insertion. Specifically: 1. For any $x \in \alpha$ and $y \in \text{WithBot }\alpha$, we have $\text{WithBot.unbotD} \bot y \leq x$ if and only if $y \leq \text{WithBot.some} x$. 2. For any $x \in \alpha$, we have $x \leq \text{WithBot.unbotD} \bot (\text{WithBot.some} x)$ (which simplifies to $x \leq x$ by reflexivity). 3. The choice function for the Galois insertion is defined to be $\text{WithBot.unbotD} \bot$ applied to the input.