Mathlib.Order.GaloisConnection.Defs

GaloisConnection definition

[Preorder α] [Preorder β] (l : α → β) (u : β → α)

Full source

/-- 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. -/
def GaloisConnection [Preorder α] [Preorder β] (l : α → β) (u : β → α) :=
  ∀ a b, l a ≤ b ↔ a ≤ u b

Galois connection

Informal description

Given two preorders $\alpha$ and $\beta$, a Galois connection between them is a pair of functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$ such that for all $a \in \alpha$ and $b \in \beta$, the inequality $l(a) \leq b$ holds if and only if $a \leq u(b)$. This condition captures an adjoint-like relationship between the two functions without relying on category theory.

GaloisConnection.monotone_intro theorem

(hu : Monotone u) (hl : Monotone l) (hul : ∀ a, a ≤ u (l a)) (hlu : ∀ a, l (u a) ≤ a) : GaloisConnection l u

Full source

theorem monotone_intro (hu : Monotone u) (hl : Monotone l) (hul : ∀ a, a ≤ u (l a))
    (hlu : ∀ a, l (u a) ≤ a) : GaloisConnection l u := fun _ _ =>
  ⟨fun h => (hul _).trans (hu h), fun h => (hl h).trans (hlu _)⟩

Monotonicity Conditions for Galois Connection

Informal description

Let $\alpha$ and $\beta$ be preorders, and let $l : \alpha \to \beta$ and $u : \beta \to \alpha$ be monotone functions. If for all $a \in \alpha$ we have $a \leq u(l(a))$, and for all $a \in \beta$ we have $l(u(a)) \leq a$, then $(l, u)$ forms a Galois connection between $\alpha$ and $\beta$.

GaloisConnection.dual theorem

 {l : α → β} {u : β → α} (gc : GaloisConnection l u) :
  GaloisConnection (OrderDual.toDual ∘ u ∘ OrderDual.ofDual) (OrderDual.toDual ∘ l ∘ OrderDual.ofDual)

Full source

protected theorem dual {l : α → β} {u : β → α} (gc : GaloisConnection l u) :
    GaloisConnection (OrderDual.toDualOrderDual.toDual ∘ u ∘ OrderDual.ofDual)
      (OrderDual.toDualOrderDual.toDual ∘ l ∘ OrderDual.ofDual) :=
  fun a b => (gc b a).symm

Dual Galois Connection: $(u^{\text{op}}, l^{\text{op}})$ forms a Galois connection between $\beta^{\text{op}}$ and $\alpha^{\text{op}}$

Informal description

Given a Galois connection $(l, u)$ between preorders $\alpha$ and $\beta$, the pair $(u^{\text{op}}, l^{\text{op}})$ forms a Galois connection between the order duals $\beta^{\text{op}}$ and $\alpha^{\text{op}}$, where $u^{\text{op}} = \text{toDual} \circ u \circ \text{ofDual}$ and $l^{\text{op}} = \text{toDual} \circ l \circ \text{ofDual}$.

GaloisConnection.le_iff_le theorem

{a : α} {b : β} : l a ≤ b ↔ a ≤ u b

Full source

theorem le_iff_le {a : α} {b : β} : l a ≤ b ↔ a ≤ u b :=
  gc _ _

Characterization of Galois Connection via Inequalities

Informal description

Given a Galois connection between preorders $\alpha$ and $\beta$ with functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$, for any elements $a \in \alpha$ and $b \in \beta$, the inequality $l(a) \leq b$ holds if and only if $a \leq u(b)$.

GaloisConnection.l_le theorem

{a : α} {b : β} : a ≤ u b → l a ≤ b

Full source

theorem l_le {a : α} {b : β} : a ≤ u b → l a ≤ b :=
  (gc _ _).mpr

Forward implication of Galois connection: $a \leq u(b) \Rightarrow l(a) \leq b$

Informal description

Given a Galois connection between preorders $\alpha$ and $\beta$ with functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$, for any elements $a \in \alpha$ and $b \in \beta$, if $a \leq u(b)$, then $l(a) \leq b$.

GaloisConnection.le_u theorem

{a : α} {b : β} : l a ≤ b → a ≤ u b

Full source

theorem le_u {a : α} {b : β} : l a ≤ b → a ≤ u b :=
  (gc _ _).mp

Reverse implication of Galois connection: $l(a) \leq b \Rightarrow a \leq u(b)$

Informal description

Given a Galois connection between preorders $\alpha$ and $\beta$ with functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$, for any elements $a \in \alpha$ and $b \in \beta$, if $l(a) \leq b$, then $a \leq u(b)$.

GaloisConnection.le_u_l theorem

(a) : a ≤ u (l a)

Full source

theorem le_u_l (a) : a ≤ u (l a) :=
  gc.le_u <| le_rfl

Lower bound property of Galois connection: $a \leq u(l(a))$

Informal description

For any element $a$ in a preorder $\alpha$ with a Galois connection $(l, u)$ between preorders $\alpha$ and $\beta$, we have $a \leq u(l(a))$.

GaloisConnection.l_u_le theorem

(a) : l (u a) ≤ a

Full source

theorem l_u_le (a) : l (u a) ≤ a :=
  gc.l_le <| le_rfl

Galois connection inequality: $l(u(a)) \leq a$

Informal description

Given a Galois connection between preorders $\alpha$ and $\beta$ with functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$, for any element $a \in \beta$, the inequality $l(u(a)) \leq a$ holds.

GaloisConnection.monotone_u theorem

: Monotone u

Full source

theorem monotone_u : Monotone u := fun a _ H => gc.le_u ((gc.l_u_le a).trans H)

Monotonicity of the Upper Adjoint in a Galois Connection

Informal description

Given a Galois connection between preorders $\alpha$ and $\beta$ with functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$, the function $u$ is monotone, meaning that for any $b_1, b_2 \in \beta$, if $b_1 \leq b_2$, then $u(b_1) \leq u(b_2)$.

GaloisConnection.monotone_l theorem

: Monotone l

Full source

theorem monotone_l : Monotone l :=
  gc.dual.monotone_u.dual

Monotonicity of the Lower Adjoint in a Galois Connection

Informal description

Given a Galois connection between preorders $\alpha$ and $\beta$ with functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$, the function $l$ is monotone, meaning that for any $a_1, a_2 \in \alpha$, if $a_1 \leq a_2$, then $l(a_1) \leq l(a_2)$.

GaloisConnection.le_u_l_trans theorem

{x y z : α} (hxy : x ≤ u (l y)) (hyz : y ≤ u (l z)) : x ≤ u (l z)

Full source

/-- 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 le_u_l_trans {x y z : α} (hxy : x ≤ u (l y)) (hyz : y ≤ u (l z)) : x ≤ u (l z) :=
  hxy.trans (gc.monotone_u <| gc.l_le hyz)

Transitivity of the relation $x \leq u(l(y))$ in a Galois connection

Informal description

Let $(l, u)$ be a Galois connection between preorders $\alpha$ and $\beta$. For any elements $x, y, z \in \alpha$, if $x \leq u(l(y))$ and $y \leq u(l(z))$, then $x \leq u(l(z))$.

GaloisConnection.l_u_le_trans theorem

{x y z : β} (hxy : l (u x) ≤ y) (hyz : l (u y) ≤ z) : l (u x) ≤ z

Full source

theorem l_u_le_trans {x y z : β} (hxy : l (u x) ≤ y) (hyz : l (u y) ≤ z) : l (u x) ≤ z :=
  (gc.monotone_l <| gc.le_u hxy).trans hyz

Transitivity of $l(u(x)) \leq y$ in a Galois connection

Informal description

Let $(l, u)$ be a Galois connection between preorders $\alpha$ and $\beta$. For any elements $x, y, z \in \beta$, if $l(u(x)) \leq y$ and $l(u(y)) \leq z$, then $l(u(x)) \leq z$.

GaloisConnection.u_l_u_eq_u theorem

(b : β) : u (l (u b)) = u b

Full source

theorem u_l_u_eq_u (b : β) : u (l (u b)) = u b :=
  (gc.monotone_u (gc.l_u_le _)).antisymm (gc.le_u_l _)

Idempotence of $u \circ l \circ u$ in a Galois connection

Informal description

For any element $b$ in a preorder $\beta$ with a Galois connection $(l, u)$ between preorders $\alpha$ and $\beta$, the composition $u \circ l \circ u$ satisfies $u(l(u(b))) = u(b)$.

GaloisConnection.u_l_u_eq_u' theorem

: u ∘ l ∘ u = u

Full source

theorem u_l_u_eq_u' : u ∘ l ∘ u = u :=
  funext gc.u_l_u_eq_u

Idempotence of $u \circ l \circ u$ in a Galois connection

Informal description

For a Galois connection $(l, u)$ between preorders $\alpha$ and $\beta$, the composition $u \circ l \circ u$ equals $u$.

GaloisConnection.u_unique theorem

{l' : α → β} {u' : β → α} (gc' : GaloisConnection l' u') (hl : ∀ a, l a = l' a) {b : β} : u b = u' b

Full source

theorem u_unique {l' : α → β} {u' : β → α} (gc' : GaloisConnection l' u') (hl : ∀ a, l a = l' a)
    {b : β} : u b = u' b :=
  le_antisymm (gc'.le_u <| hl (u b) ▸ gc.l_u_le _) (gc.le_u <| (hl (u' b)).symm ▸ gc'.l_u_le _)

Uniqueness of Right Adjoint in Galois Connection Given Left Adjoint Equality

Informal description

Let $\alpha$ and $\beta$ be preorders, and let $(l, u)$ and $(l', u')$ be two Galois connections between them. If $l(a) = l'(a)$ for all $a \in \alpha$, then $u(b) = u'(b)$ for all $b \in \beta$.

GaloisConnection.exists_eq_u theorem

(a : α) : (∃ b : β, a = u b) ↔ a = u (l a)

Full source

/-- If there exists a `b` such that `a = u a`, then `b = l a` is one such element. -/
theorem exists_eq_u (a : α) : (∃ b : β, a = u b) ↔ a = u (l a) :=
  ⟨fun ⟨_, hS⟩ => hS.symm ▸ (gc.u_l_u_eq_u _).symm, fun HI => ⟨_, HI⟩⟩

Existence of $b$ with $a = u(b)$ is equivalent to $a = u(l(a))$ in a Galois connection

Informal description

Let $\alpha$ and $\beta$ be preorders with a Galois connection $(l, u)$ between them. For any element $a \in \alpha$, there exists an element $b \in \beta$ such that $a = u(b)$ if and only if $a = u(l(a))$.

GaloisConnection.u_eq theorem

{z : α} {y : β} : u y = z ↔ ∀ x, x ≤ z ↔ l x ≤ y

Full source

theorem u_eq {z : α} {y : β} : u y = z ↔ ∀ x, x ≤ z ↔ l x ≤ y := by
  constructor
  · rintro rfl x
    exact (gc x y).symm
  · intro H
    exact ((H <| u y).mpr (gc.l_u_le y)).antisymm ((gc _ _).mp <| (H z).mp le_rfl)

Characterization of Galois Connection via Equality: $u(y) = z \leftrightarrow (\forall x, x \leq z \leftrightarrow l(x) \leq y)$

Informal description

Given a Galois connection between preorders $\alpha$ and $\beta$ with functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$, for any elements $z \in \alpha$ and $y \in \beta$, the equality $u(y) = z$ holds if and only if for all $x \in \alpha$, the inequality $x \leq z$ is equivalent to $l(x) \leq y$.

GaloisConnection.l_u_l_eq_l theorem

(a : α) : l (u (l a)) = l a

Full source

theorem l_u_l_eq_l (a : α) : l (u (l a)) = l a := gc.dual.u_l_u_eq_u _

Idempotence of $l \circ u \circ l$ in a Galois connection

Informal description

For any element $a$ in a preorder $\alpha$ with a Galois connection $(l, u)$ between preorders $\alpha$ and $\beta$, the composition $l \circ u \circ l$ satisfies $l(u(l(a))) = l(a)$.

GaloisConnection.l_u_l_eq_l' theorem

: l ∘ u ∘ l = l

Full source

theorem l_u_l_eq_l' : l ∘ u ∘ l = l := funext gc.l_u_l_eq_l

Idempotence of $l \circ u \circ l$ in a Galois connection

Informal description

For a Galois connection between preorders $\alpha$ and $\beta$ with functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$, the composition $l \circ u \circ l$ equals $l$, i.e., $l(u(l(a))) = l(a)$ for all $a \in \alpha$.

GaloisConnection.l_unique theorem

{l' : α → β} {u' : β → α} (gc' : GaloisConnection l' u') (hu : ∀ b, u b = u' b) {a : α} : l a = l' a

Full source

theorem l_unique {l' : α → β} {u' : β → α} (gc' : GaloisConnection l' u') (hu : ∀ b, u b = u' b)
    {a : α} : l a = l' a :=
  gc.dual.u_unique gc'.dual hu

Uniqueness of Left Adjoint in Galois Connection Given Right Adjoint Equality

Informal description

Let $\alpha$ and $\beta$ be preorders, and let $(l, u)$ and $(l', u')$ be two Galois connections between them. If $u(b) = u'(b)$ for all $b \in \beta$, then $l(a) = l'(a)$ for all $a \in \alpha$.

GaloisConnection.exists_eq_l theorem

(b : β) : (∃ a : α, b = l a) ↔ b = l (u b)

Full source

/-- If there exists an `a` such that `b = l a`, then `a = u b` is one such element. -/
theorem exists_eq_l (b : β) : (∃ a : α, b = l a) ↔ b = l (u b) := gc.dual.exists_eq_u _

Existence of Preimage in Galois Connection: $(\exists a, b = l(a)) \leftrightarrow b = l(u(b))$

Informal description

Let $\alpha$ and $\beta$ be preorders with a Galois connection $(l, u)$ between them. For any element $b \in \beta$, there exists an element $a \in \alpha$ such that $b = l(a)$ if and only if $b = l(u(b))$.

GaloisConnection.l_eq theorem

{x : α} {z : β} : l x = z ↔ ∀ y, z ≤ y ↔ x ≤ u y

Full source

theorem l_eq {x : α} {z : β} : l x = z ↔ ∀ y, z ≤ y ↔ x ≤ u y := gc.dual.u_eq

Characterization of Galois Connection via Equality: $l(x) = z \leftrightarrow (\forall y, z \leq y \leftrightarrow x \leq u(y))$

Informal description

Let $\alpha$ and $\beta$ be preorders with a Galois connection $(l, u)$ between them. For any $x \in \alpha$ and $z \in \beta$, the equality $l(x) = z$ holds if and only if for all $y \in \beta$, the inequality $z \leq y$ is equivalent to $x \leq u(y)$.

GaloisConnection.u_eq_top theorem

{l : α → β} {u : β → α} (gc : GaloisConnection l u) {x} : u x = ⊤ ↔ l ⊤ ≤ x

Full source

theorem u_eq_top {l : α → β} {u : β → α} (gc : GaloisConnection l u) {x} : u x = ⊤ ↔ l ⊤ ≤ x :=
  top_le_iff.symm.trans gc.le_iff_le.symm

Characterization of Top Element in Galois Connection: $u(x) = \top \leftrightarrow l(\top) \leq x$

Informal description

Let $\alpha$ and $\beta$ be preorders with a greatest element $\top$ in $\alpha$. Given a Galois connection $(l, u)$ between $\alpha$ and $\beta$, for any $x \in \beta$, we have $u(x) = \top$ if and only if $l(\top) \leq x$.

GaloisConnection.u_top theorem

[OrderTop β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : u ⊤ = ⊤

Full source

theorem u_top [OrderTop β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : u ⊤ = ⊤ :=
  gc.u_eq_top.2 le_top

Preservation of Top Element by Upper Adjoint in Galois Connection

Informal description

Let $\alpha$ and $\beta$ be preorders where $\beta$ has a greatest element $\top$. Given a Galois connection $(l, u)$ between $\alpha$ and $\beta$, the upper adjoint $u$ maps the top element of $\beta$ to the top element of $\alpha$, i.e., $u(\top) = \top$.

GaloisConnection.u_l_top theorem

{l : α → β} {u : β → α} (gc : GaloisConnection l u) : u (l ⊤) = ⊤

Full source

theorem u_l_top {l : α → β} {u : β → α} (gc : GaloisConnection l u) : u (l ⊤) = ⊤ :=
  gc.u_eq_top.mpr le_rfl

Upper Adjoint Maps Lower Adjoint of Top to Top in Galois Connection

Informal description

Let $\alpha$ and $\beta$ be preorders with a greatest element $\top$ in $\alpha$. Given a Galois connection $(l, u)$ between $\alpha$ and $\beta$, the upper adjoint $u$ evaluated at $l(\top)$ equals $\top$, i.e., $u(l(\top)) = \top$.

GaloisConnection.l_eq_bot theorem

{l : α → β} {u : β → α} (gc : GaloisConnection l u) {x} : l x = ⊥ ↔ x ≤ u ⊥

Full source

theorem l_eq_bot {l : α → β} {u : β → α} (gc : GaloisConnection l u) {x} : l x = ⊥ ↔ x ≤ u ⊥ :=
  gc.dual.u_eq_top

Characterization of Bottom Element in Galois Connection: $l(x) = \bot \leftrightarrow x \leq u(\bot)$

Informal description

Let $\alpha$ and $\beta$ be preorders, with $\beta$ having a least element $\bot$. Given a Galois connection $(l, u)$ between $\alpha$ and $\beta$, for any $x \in \alpha$, we have $l(x) = \bot$ if and only if $x \leq u(\bot)$.

GaloisConnection.l_bot theorem

[OrderBot α] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : l ⊥ = ⊥

Full source

theorem l_bot [OrderBot α] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : l ⊥ = ⊥ :=
  gc.dual.u_top

Preservation of Bottom Element by Lower Adjoint in Galois Connection

Informal description

Let $\alpha$ and $\beta$ be preorders, with $\alpha$ having a least element $\bot$. Given a Galois connection $(l, u)$ between $\alpha$ and $\beta$, the lower adjoint $l$ maps the bottom element of $\alpha$ to the bottom element of $\beta$, i.e., $l(\bot) = \bot$.

GaloisConnection.l_u_bot theorem

{l : α → β} {u : β → α} (gc : GaloisConnection l u) : l (u ⊥) = ⊥

Full source

theorem l_u_bot {l : α → β} {u : β → α} (gc : GaloisConnection l u) : l (u ⊥) = ⊥ :=
  gc.l_eq_bot.mpr le_rfl

Galois connection property: $l(u(\bot)) = \bot$

Informal description

Let $\alpha$ and $\beta$ be preorders, with $\beta$ having a least element $\bot$. Given a Galois connection $(l, u)$ between $\alpha$ and $\beta$, the composition $l \circ u$ applied to $\bot$ yields $\bot$, i.e., $l(u(\bot)) = \bot$.

GaloisConnection.lt_iff_lt theorem

(gc : GaloisConnection l u) {a : α} {b : β} : b < l a ↔ u b < a

Full source

theorem lt_iff_lt (gc : GaloisConnection l u) {a : α} {b : β} : b < l a ↔ u b < a :=
  lt_iff_lt_of_le_iff_le (gc a b)

Strict Inequality Characterization in Galois Connection

Informal description

Let $\alpha$ and $\beta$ be preorders, and let $(l, u)$ be a Galois connection between them. For any $a \in \alpha$ and $b \in \beta$, the strict inequality $b < l(a)$ holds if and only if $u(b) < a$.

GaloisConnection.id theorem

[pα : Preorder α] : @GaloisConnection α α pα pα id id

Full source

protected theorem id [pα : Preorder α] : @GaloisConnection α α pα pα id id := fun _ _ =>
  Iff.intro (fun x => x) fun x => x

Identity Galois Connection on a Preorder

Informal description

For any preorder $\alpha$, the pair of identity functions forms a Galois connection between $\alpha$ and itself. That is, for all $a, b \in \alpha$, we have $a \leq b$ if and only if $a \leq b$.

GaloisConnection.compose theorem

 [Preorder α] [Preorder β] [Preorder γ] {l1 : α → β} {u1 : β → α} {l2 : β → γ} {u2 : γ → β}
  (gc1 : GaloisConnection l1 u1) (gc2 : GaloisConnection l2 u2) : GaloisConnection (l2 ∘ l1) (u1 ∘ u2)

Full source

protected theorem compose [Preorder α] [Preorder β] [Preorder γ] {l1 : α → β} {u1 : β → α}
    {l2 : β → γ} {u2 : γ → β} (gc1 : GaloisConnection l1 u1) (gc2 : GaloisConnection l2 u2) :
    GaloisConnection (l2 ∘ l1) (u1 ∘ u2) := fun _ _ ↦ (gc2 _ _).trans (gc1 _ _)

Composition of Galois Connections

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be preorders, and let $l_1 : \alpha \to \beta$, $u_1 : \beta \to \alpha$ and $l_2 : \beta \to \gamma$, $u_2 : \gamma \to \beta$ be functions forming Galois connections $(l_1, u_1)$ and $(l_2, u_2)$, respectively. Then the composition $(l_2 \circ l_1, u_1 \circ u_2)$ also forms a Galois connection between $\alpha$ and $\gamma$.

GaloisConnection.dfun theorem

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

Full source

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

Pointwise Galois Connection on Function Spaces

Informal description

Let $\iota$ be a type, and for each $i \in \iota$, let $\alpha_i$ and $\beta_i$ be preorders. Given for each $i$ a pair of functions $l_i : \alpha_i \to \beta_i$ and $u_i : \beta_i \to \alpha_i$ forming a Galois connection (i.e., for all $a_i \in \alpha_i$ and $b_i \in \beta_i$, $l_i(a_i) \leq b_i$ if and only if $a_i \leq u_i(b_i)$), then the pointwise-defined functions $L : (\forall i, \alpha_i) \to (\forall i, \beta_i)$ and $U : (\forall i, \beta_i) \to (\forall i, \alpha_i)$, where $L(f)(i) = l_i(f(i))$ and $U(g)(i) = u_i(g(i))$, form a Galois connection between the function spaces $\forall i, \alpha_i$ and $\forall i, \beta_i$ with the pointwise order.

GaloisConnection.l_comm_of_u_comm theorem

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

Full source

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

Commutativity of Left Adjoints in Galois Connections Given Right Adjoint Commutativity

Informal description

Let $X$, $Y$, $Z$ be preorders and $W$ be a partial order. Suppose we have Galois connections $(l_{YX}, u_{XY})$ between $X$ and $Y$, $(l_{WZ}, u_{ZW})$ between $Z$ and $W$, $(l_{WY}, u_{YW})$ between $Y$ and $W$, and $(l_{ZX}, u_{XZ})$ between $X$ and $Z$. If for all $w \in W$ we have $u_{XZ}(u_{ZW}(w)) = u_{XY}(u_{YW}(w))$, then for any $x \in X$ it follows that $l_{WZ}(l_{ZX}(x)) = l_{WY}(l_{YX}(x))$.

GaloisConnection.u_comm_of_l_comm theorem

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

Full source

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

Commutativity of Right Adjoints in Galois Connections Given Left Adjoint Commutativity

Informal description

Let $X$ be a partially ordered set, and $Y, Z, W$ be preordered sets. Suppose we have Galois connections $(l_{YX}, u_{XY})$ between $X$ and $Y$, $(l_{WZ}, u_{ZW})$ between $Z$ and $W$, $(l_{WY}, u_{YW})$ between $Y$ and $W$, and $(l_{ZX}, u_{XZ})$ between $X$ and $Z$. If for all $x \in X$ we have $l_{WZ}(l_{ZX}(x)) = l_{WY}(l_{YX}(x))$, then for any $w \in W$ it follows that $u_{XZ}(u_{ZW}(w)) = u_{XY}(u_{YW}(w))$.

GaloisConnection.l_comm_iff_u_comm theorem

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

Full source

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

Equivalence of Left and Right Adjoint Commutativity in Galois Connections

Informal description

Let $X$ and $W$ be partially ordered sets, and $Y, Z$ be preordered sets. Suppose we have Galois connections $(l_{YX}, u_{XY})$ between $X$ and $Y$, $(l_{WZ}, u_{ZW})$ between $Z$ and $W$, $(l_{WY}, u_{YW})$ between $Y$ and $W$, and $(l_{ZX}, u_{XZ})$ between $X$ and $Z$. Then for all $w \in W$, $u_{XZ}(u_{ZW}(w)) = u_{XY}(u_{YW}(w))$ if and only if for all $x \in X$, $l_{WZ}(l_{ZX}(x)) = l_{WY}(l_{YX}(x))$.

GaloisInsertion structure

{α β : Type*} [Preorder α] [Preorder β] (l : α → β) (u : β → α)

Full source

/-- A Galois insertion is a Galois connection where `l ∘ u = id`. It also contains a constructive
choice function, to give better definitional equalities when lifting order structures. Dual
to `GaloisCoinsertion` -/
structure GaloisInsertion {α β : Type*} [Preorder α] [Preorder β] (l : α → β) (u : β → α) where
  /-- A contructive choice function for images of `l`. -/
  choice : ∀ x : α, u (l x) ≤ x → β
  /-- The Galois connection associated to a Galois insertion. -/
  gc : GaloisConnection l u
  /-- Main property of a Galois insertion. -/
  le_l_u : ∀ x, x ≤ l (u x)
  /-- Property of the choice function. -/
  choice_eq : ∀ a h, choice a h = l a

Galois Insertion

Informal description

A Galois insertion is a structure consisting of two monotone functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$ between preorders $\alpha$ and $\beta$, forming a Galois connection (i.e., $l(a) \leq b \leftrightarrow a \leq u(b)$ for all $a \in \alpha$, $b \in \beta$) with the additional property that $l \circ u = \text{id}_\beta$. This means that $u$ is a section of $l$, and $l$ is a retraction of $u$.

GaloisInsertion.monotoneIntro definition

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

Full source

/-- A constructor for a Galois insertion with the trivial `choice` function. -/
def GaloisInsertion.monotoneIntro {α β : Type*} [Preorder α] [Preorder β] {l : α → β} {u : β → α}
    (hu : Monotone u) (hl : Monotone l) (hul : ∀ a, a ≤ u (l a)) (hlu : ∀ b, l (u b) = b) :
    GaloisInsertion l u where
  choice x _ := l x
  gc := GaloisConnection.monotone_intro hu hl hul fun b => le_of_eq (hlu b)
  le_l_u b := le_of_eq <| (hlu b).symm
  choice_eq _ _ := rfl

Construction of Galois Insertion from Monotone Section and Retraction

Informal description

Given two monotone functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$ between preorders $\alpha$ and $\beta$, if $u$ is a section of $l$ (i.e., $l(u(b)) = b$ for all $b \in \beta$) and $l$ is a retraction of $u$ (i.e., $a \leq u(l(a))$ for all $a \in \alpha$), then $(l, u)$ forms a Galois insertion. This means that $(l, u)$ is a Galois connection where $l \circ u$ is the identity on $\beta$.

GaloisConnection.toGaloisInsertion definition

 {α β : Type*} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (h : ∀ b, b ≤ l (u b)) :
  GaloisInsertion l u

Full source

/-- Make a `GaloisInsertion l u` from a `GaloisConnection l u` such that `∀ b, b ≤ l (u b)` -/
def GaloisConnection.toGaloisInsertion {α β : Type*} [Preorder α] [Preorder β] {l : α → β}
    {u : β → α} (gc : GaloisConnection l u) (h : ∀ b, b ≤ l (u b)) : GaloisInsertion l u :=
  { choice := fun x _ => l x
    gc
    le_l_u := h
    choice_eq := fun _ _ => rfl }

Galois connection to Galois insertion

Informal description

Given a Galois connection $(l, u)$ between preorders $\alpha$ and $\beta$ (i.e., $l(a) \leq b \leftrightarrow a \leq u(b)$ for all $a \in \alpha$, $b \in \beta$), if additionally for every $b \in \beta$ we have $b \leq l(u(b))$, then $(l, u)$ forms a Galois insertion. This means that $l \circ u$ is the identity on $\beta$, making $u$ a section of $l$ and $l$ a retraction of $u$.

GaloisConnection.liftOrderBot definition

 {α β : Type*} [Preorder α] [OrderBot α] [PartialOrder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) :
  OrderBot β

Full source

/-- Lift the bottom along a Galois connection -/
def GaloisConnection.liftOrderBot {α β : Type*} [Preorder α] [OrderBot α] [PartialOrder β]
    {l : α → β} {u : β → α} (gc : GaloisConnection l u) :
    OrderBot β where
  bot := l ⊥
  bot_le _ := gc.l_le <| bot_le

Lifting a bottom element along a Galois connection

Informal description

Given a Galois connection $(l, u)$ between a preorder $\alpha$ with a least element $\bot$ and a partial order $\beta$, the function $l$ lifts the least element of $\alpha$ to a least element of $\beta$, making $\beta$ an order with a bottom element. Specifically, the bottom element of $\beta$ is defined as $l(\bot)$, and for any $b \in \beta$, we have $l(\bot) \leq b$.

GaloisInsertion.l_u_eq theorem

[Preorder α] [PartialOrder β] (gi : GaloisInsertion l u) (b : β) : l (u b) = b

Full source

theorem l_u_eq [Preorder α] [PartialOrder β] (gi : GaloisInsertion l u) (b : β) : l (u b) = b :=
  (gi.gc.l_u_le _).antisymm (gi.le_l_u _)

Galois insertion identity: $l(u(b)) = b$ for all $b \in \beta$

Informal description

Let $\alpha$ be a preorder and $\beta$ be a partial order. Given a Galois insertion $(l, u)$ between $\alpha$ and $\beta$ (i.e., $l \circ u = \text{id}_\beta$), for any element $b \in \beta$, we have $l(u(b)) = b$.

GaloisInsertion.leftInverse_l_u theorem

[Preorder α] [PartialOrder β] (gi : GaloisInsertion l u) : LeftInverse l u

Full source

theorem leftInverse_l_u [Preorder α] [PartialOrder β] (gi : GaloisInsertion l u) :
    LeftInverse l u :=
  gi.l_u_eq

Galois insertion property: $l$ is a left inverse of $u$

Informal description

Let $\alpha$ be a preorder and $\beta$ be a partial order. Given a Galois insertion $(l, u)$ between $\alpha$ and $\beta$, the function $l$ is a left inverse of $u$, i.e., $l(u(b)) = b$ for all $b \in \beta$.

GaloisInsertion.l_top theorem

[Preorder α] [PartialOrder β] [OrderTop α] [OrderTop β] (gi : GaloisInsertion l u) : l ⊤ = ⊤

Full source

theorem l_top [Preorder α] [PartialOrder β] [OrderTop α] [OrderTop β]
    (gi : GaloisInsertion l u) : l ⊤ = ⊤ :=
  top_unique <| (gi.le_l_u _).trans <| gi.gc.monotone_l le_top

Preservation of Top Element by Lower Adjoint in Galois Insertion

Informal description

Let $\alpha$ be a preorder with a greatest element $\top_\alpha$, and $\beta$ be a partial order with a greatest element $\top_\beta$. Given a Galois insertion $(l, u)$ between $\alpha$ and $\beta$, the lower adjoint $l$ preserves the top element, i.e., $l(\top_\alpha) = \top_\beta$.

GaloisInsertion.l_surjective theorem

[Preorder α] [PartialOrder β] (gi : GaloisInsertion l u) : Surjective l

Full source

theorem l_surjective [Preorder α] [PartialOrder β] (gi : GaloisInsertion l u) : Surjective l :=
  gi.leftInverse_l_u.surjective

Surjectivity of Lower Adjoint in Galois Insertion

Informal description

Let $\alpha$ be a preorder and $\beta$ be a partial order. Given a Galois insertion $(l, u)$ between $\alpha$ and $\beta$, the lower adjoint function $l : \alpha \to \beta$ is surjective.

GaloisInsertion.u_injective theorem

[Preorder α] [PartialOrder β] (gi : GaloisInsertion l u) : Injective u

Full source

theorem u_injective [Preorder α] [PartialOrder β] (gi : GaloisInsertion l u) : Injective u :=
  gi.leftInverse_l_u.injective

Injectivity of the Upper Adjoint in a Galois Insertion

Informal description

Let $\alpha$ be a preorder and $\beta$ be a partial order. Given a Galois insertion $(l, u)$ between $\alpha$ and $\beta$, the upper adjoint function $u : \beta \to \alpha$ is injective.

GaloisInsertion.u_le_u_iff theorem

[Preorder α] [Preorder β] (gi : GaloisInsertion l u) {a b} : u a ≤ u b ↔ a ≤ b

Full source

theorem u_le_u_iff [Preorder α] [Preorder β] (gi : GaloisInsertion l u) {a b} : u a ≤ u b ↔ a ≤ b :=
  ⟨fun h => (gi.le_l_u _).trans (gi.gc.l_le h), fun h => gi.gc.monotone_u h⟩

Monotonicity of Upper Adjoint in Galois Insertion: $u(a) \leq u(b) \leftrightarrow a \leq b$

Informal description

Let $\alpha$ and $\beta$ be preorders, and let $(l, u)$ be a Galois insertion between them. For any elements $a, b \in \beta$, the inequality $u(a) \leq u(b)$ holds if and only if $a \leq b$.

GaloisInsertion.strictMono_u theorem

[Preorder α] [Preorder β] (gi : GaloisInsertion l u) : StrictMono u

Full source

theorem strictMono_u [Preorder α] [Preorder β] (gi : GaloisInsertion l u) : StrictMono u :=
  strictMono_of_le_iff_le fun _ _ => gi.u_le_u_iff.symm

Strict Monotonicity of the Upper Adjoint in a Galois Insertion

Informal description

Let $\alpha$ and $\beta$ be preorders, and let $(l, u)$ be a Galois insertion between them. Then the upper adjoint $u : \beta \to \alpha$ is strictly monotone, meaning that for any $a, b \in \beta$, if $a < b$ then $u(a) < u(b)$.

GaloisCoinsertion structure

[Preorder α] [Preorder β] (l : α → β) (u : β → α)

Full source

/-- A Galois coinsertion is a Galois connection where `u ∘ l = id`. It also contains a constructive
choice function, to give better definitional equalities when lifting order structures. Dual to
`GaloisInsertion` -/
structure GaloisCoinsertion [Preorder α] [Preorder β] (l : α → β) (u : β → α) where
  /-- A contructive choice function for images of `u`. -/
  choice : ∀ x : β, x ≤ l (u x) → α
  /-- The Galois connection associated to a Galois coinsertion. -/
  gc : GaloisConnection l u
  /-- Main property of a Galois coinsertion. -/
  u_l_le : ∀ x, u (l x) ≤ x
  /-- Property of the choice function. -/
  choice_eq : ∀ a h, choice a h = u a

Galois coinsertion

Informal description

A Galois coinsertion between preorders $\alpha$ and $\beta$ consists of two functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$ forming a Galois connection (i.e., $l(a) \leq b \leftrightarrow a \leq u(b)$ for all $a \in \alpha$, $b \in \beta$) with the additional property that $u \circ l = \text{id}$. This is the dual notion of a Galois insertion.

GaloisCoinsertion.dual definition

 [Preorder α] [Preorder β] {l : α → β} {u : β → α} :
  GaloisCoinsertion l u → GaloisInsertion (toDual ∘ u ∘ ofDual) (toDual ∘ l ∘ ofDual)

Full source

/-- Make a `GaloisInsertion` between `αᵒᵈ` and `βᵒᵈ` from a `GaloisCoinsertion` between `α` and
`β`. -/
def GaloisCoinsertion.dual [Preorder α] [Preorder β] {l : α → β} {u : β → α} :
    GaloisCoinsertion l u → GaloisInsertion (toDualtoDual ∘ u ∘ ofDual) (toDualtoDual ∘ l ∘ ofDual) :=
  fun x => ⟨x.1, x.2.dual, x.3, x.4⟩

Dual of a Galois coinsertion

Informal description

Given a Galois coinsertion between preorders $\alpha$ and $\beta$ with functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$, the dual construction yields a Galois insertion between the order duals $\alpha^{\text{op}}$ and $\beta^{\text{op}}$ with functions $u^{\text{op}} : \beta^{\text{op}} \to \alpha^{\text{op}}$ and $l^{\text{op}} : \alpha^{\text{op}} \to \beta^{\text{op}}$, where $u^{\text{op}} = \text{toDual} \circ u \circ \text{ofDual}$ and $l^{\text{op}} = \text{toDual} \circ l \circ \text{ofDual}$.

GaloisInsertion.dual definition

 [Preorder α] [Preorder β] {l : α → β} {u : β → α} :
  GaloisInsertion l u → GaloisCoinsertion (toDual ∘ u ∘ ofDual) (toDual ∘ l ∘ ofDual)

Full source

/-- Make a `GaloisCoinsertion` between `αᵒᵈ` and `βᵒᵈ` from a `GaloisInsertion` between `α` and
`β`. -/
def GaloisInsertion.dual [Preorder α] [Preorder β] {l : α → β} {u : β → α} :
    GaloisInsertion l u → GaloisCoinsertion (toDualtoDual ∘ u ∘ ofDual) (toDualtoDual ∘ l ∘ ofDual) :=
  fun x => ⟨x.1, x.2.dual, x.3, x.4⟩

Galois insertion to dual Galois coinsertion

Informal description

Given a Galois insertion between preorders $\alpha$ and $\beta$ with functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$, this constructs the corresponding Galois coinsertion between the order duals $\alpha^{\text{op}}$ and $\beta^{\text{op}}$ using the composition of the dualizing maps with $u$ and $l$.

GaloisCoinsertion.ofDual definition

 [Preorder α] [Preorder β] {l : αᵒᵈ → βᵒᵈ} {u : βᵒᵈ → αᵒᵈ} :
  GaloisCoinsertion l u → GaloisInsertion (ofDual ∘ u ∘ toDual) (ofDual ∘ l ∘ toDual)

Full source

/-- Make a `GaloisInsertion` between `α` and `β` from a `GaloisCoinsertion` between `αᵒᵈ` and
`βᵒᵈ`. -/
def GaloisCoinsertion.ofDual [Preorder α] [Preorder β] {l : αᵒᵈ → βᵒᵈ} {u : βᵒᵈ → αᵒᵈ} :
    GaloisCoinsertion l u → GaloisInsertion (ofDualofDual ∘ u ∘ toDual) (ofDualofDual ∘ l ∘ toDual) :=
  fun x => ⟨x.1, x.2.dual, x.3, x.4⟩

Galois insertion from order dual coinsertion

Informal description

Given a Galois coinsertion between the order duals $\alpha^{\text{op}}$ and $\beta^{\text{op}}$ (i.e., a Galois connection where $u \circ l = \text{id}$), this constructs a Galois insertion between the original preorders $\alpha$ and $\beta$ by composing with the order dual isomorphisms. Specifically, if $(l, u)$ is a Galois coinsertion between $\alpha^{\text{op}}$ and $\beta^{\text{op}}$, then $(ofDual \circ u \circ toDual, ofDual \circ l \circ toDual)$ is a Galois insertion between $\alpha$ and $\beta$.

GaloisInsertion.ofDual definition

 [Preorder α] [Preorder β] {l : αᵒᵈ → βᵒᵈ} {u : βᵒᵈ → αᵒᵈ} :
  GaloisInsertion l u → GaloisCoinsertion (ofDual ∘ u ∘ toDual) (ofDual ∘ l ∘ toDual)

Full source

/-- Make a `GaloisCoinsertion` between `α` and `β` from a `GaloisInsertion` between `αᵒᵈ` and
`βᵒᵈ`. -/
def GaloisInsertion.ofDual [Preorder α] [Preorder β] {l : αᵒᵈ → βᵒᵈ} {u : βᵒᵈ → αᵒᵈ} :
    GaloisInsertion l u → GaloisCoinsertion (ofDualofDual ∘ u ∘ toDual) (ofDualofDual ∘ l ∘ toDual) :=
  fun x => ⟨x.1, x.2.dual, x.3, x.4⟩

Galois coinsertion from Galois insertion on order duals

Informal description

Given a Galois insertion $(l, u)$ between the order duals $\alpha^{\text{op}}$ and $\beta^{\text{op}}$, this constructs a Galois coinsertion between $\alpha$ and $\beta$ by composing $l$ and $u$ with the order dual isomorphisms. Specifically, the resulting Galois coinsertion consists of the functions $\text{ofDual} \circ u \circ \text{toDual}$ and $\text{ofDual} \circ l \circ \text{toDual}$, where $\text{toDual} : \alpha \to \alpha^{\text{op}}$ and $\text{ofDual} : \beta^{\text{op}} \to \beta$ are the canonical order-reversing bijections.

GaloisCoinsertion.monotoneIntro definition

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

Full source

/-- A constructor for a Galois coinsertion with the trivial `choice` function. -/
def GaloisCoinsertion.monotoneIntro [Preorder α] [Preorder β] {l : α → β} {u : β → α}
    (hu : Monotone u) (hl : Monotone l) (hlu : ∀ b, l (u b) ≤ b) (hul : ∀ a, u (l a) = a) :
    GaloisCoinsertion l u :=
  (GaloisInsertion.monotoneIntro hl.dual hu.dual hlu hul).ofDual

Construction of Galois coinsertion from monotone section and retraction

Informal description

Given two monotone functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$ between preorders $\alpha$ and $\beta$, if $l$ is a section of $u$ (i.e., $u(l(a)) = a$ for all $a \in \alpha$) and $u$ is a retraction of $l$ (i.e., $l(u(b)) \leq b$ for all $b \in \beta$), then $(l, u)$ forms a Galois coinsertion. This means that $(l, u)$ is a Galois connection where $u \circ l$ is the identity on $\alpha$.

GaloisConnection.toGaloisCoinsertion definition

 {α β : Type*} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (h : ∀ a, u (l a) ≤ a) :
  GaloisCoinsertion l u

Full source

/-- Make a `GaloisCoinsertion l u` from a `GaloisConnection l u` such that `∀ a, u (l a) ≤ a` -/
def GaloisConnection.toGaloisCoinsertion {α β : Type*} [Preorder α] [Preorder β] {l : α → β}
    {u : β → α} (gc : GaloisConnection l u) (h : ∀ a, u (l a) ≤ a) : GaloisCoinsertion l u :=
  { choice := fun x _ => u x
    gc
    u_l_le := h
    choice_eq := fun _ _ => rfl }

Construction of Galois coinsertion from Galois connection with $u \circ l \leq \text{id}$

Informal description

Given a Galois connection $(l, u)$ between preorders $\alpha$ and $\beta$ (i.e., $l(a) \leq b \leftrightarrow a \leq u(b)$ for all $a \in \alpha$, $b \in \beta$) with the additional property that $u(l(a)) \leq a$ for all $a \in \alpha$, this constructs a Galois coinsertion from $(l, u)$. A Galois coinsertion is a Galois connection where $u \circ l = \text{id}$.

GaloisConnection.liftOrderTop definition

 {α β : Type*} [PartialOrder α] [Preorder β] [OrderTop β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) :
  OrderTop α

Full source

/-- Lift the top along a Galois connection -/
def GaloisConnection.liftOrderTop {α β : Type*} [PartialOrder α] [Preorder β] [OrderTop β]
    {l : α → β} {u : β → α} (gc : GaloisConnection l u) :
    OrderTop α where
  top := u ⊤
  le_top _ := gc.le_u <| le_top

Lifting an order with top element via a Galois connection

Informal description

Given a Galois connection $(l, u)$ between a partial order $\alpha$ and a preorder $\beta$ with a top element $\top$, the structure `OrderTop` is lifted to $\alpha$ by defining the top element of $\alpha$ as $u(\top)$. For any $a \in \alpha$, we have $a \leq u(\top)$ because $l(a) \leq \top$ holds by the property of the top element in $\beta$ and the Galois connection condition.

GaloisCoinsertion.u_l_eq theorem

[PartialOrder α] [Preorder β] (gi : GaloisCoinsertion l u) (a : α) : u (l a) = a

Full source

theorem u_l_eq [PartialOrder α] [Preorder β] (gi : GaloisCoinsertion l u) (a : α) : u (l a) = a :=
  gi.dual.l_u_eq a

Galois coinsertion identity: $u(l(a)) = a$ for all $a \in \alpha$

Informal description

Let $\alpha$ be a partially ordered set and $\beta$ be a preordered set. Given a Galois coinsertion $(l, u)$ between $\alpha$ and $\beta$ (i.e., $u \circ l = \text{id}_\alpha$), for any element $a \in \alpha$, we have $u(l(a)) = a$.

GaloisCoinsertion.u_l_leftInverse theorem

[PartialOrder α] [Preorder β] (gi : GaloisCoinsertion l u) : LeftInverse u l

Full source

theorem u_l_leftInverse [PartialOrder α] [Preorder β] (gi : GaloisCoinsertion l u) :
    LeftInverse u l :=
  gi.u_l_eq

Left inverse property of Galois coinsertion: $u \circ l = \text{id}_\alpha$

Informal description

Let $\alpha$ be a partially ordered set and $\beta$ be a preordered set. Given a Galois coinsertion $(l, u)$ between $\alpha$ and $\beta$, the function $u$ is a left inverse of $l$, meaning that for all $a \in \alpha$, we have $u(l(a)) = a$.

GaloisCoinsertion.u_bot theorem

[PartialOrder α] [Preorder β] [OrderBot α] [OrderBot β] (gi : GaloisCoinsertion l u) : u ⊥ = ⊥

Full source

theorem u_bot [PartialOrder α] [Preorder β] [OrderBot α] [OrderBot β] (gi : GaloisCoinsertion l u) :
    u ⊥ = ⊥ :=
  gi.dual.l_top

Preservation of Bottom Element by Upper Adjoint in Galois Coinsertion

Informal description

Let $\alpha$ be a partially ordered set with a least element $\bot_\alpha$, and $\beta$ be a preordered set with a least element $\bot_\beta$. Given a Galois coinsertion $(l, u)$ between $\alpha$ and $\beta$, the upper adjoint $u$ preserves the bottom element, i.e., $u(\bot_\beta) = \bot_\alpha$.

GaloisCoinsertion.u_surjective theorem

[PartialOrder α] [Preorder β] (gi : GaloisCoinsertion l u) : Surjective u

Full source

theorem u_surjective [PartialOrder α] [Preorder β] (gi : GaloisCoinsertion l u) : Surjective u :=
  gi.dual.l_surjective

Surjectivity of Upper Adjoint in Galois Coinsertion

Informal description

Let $\alpha$ be a partially ordered set and $\beta$ be a preordered set. Given a Galois coinsertion $(l, u)$ between $\alpha$ and $\beta$, the upper adjoint function $u : \beta \to \alpha$ is surjective.

GaloisCoinsertion.l_injective theorem

[PartialOrder α] [Preorder β] (gi : GaloisCoinsertion l u) : Injective l

Full source

theorem l_injective [PartialOrder α] [Preorder β] (gi : GaloisCoinsertion l u) : Injective l :=
  gi.dual.u_injective

Injectivity of the Lower Adjoint in a Galois Coinsertion

Informal description

Let $\alpha$ be a partial order and $\beta$ be a preorder. Given a Galois coinsertion $(l, u)$ between $\alpha$ and $\beta$, the lower adjoint function $l : \alpha \to \beta$ is injective.

GaloisCoinsertion.l_le_l_iff theorem

[Preorder α] [Preorder β] (gi : GaloisCoinsertion l u) {a b} : l a ≤ l b ↔ a ≤ b

Full source

theorem l_le_l_iff [Preorder α] [Preorder β] (gi : GaloisCoinsertion l u) {a b} :
    l a ≤ l b ↔ a ≤ b :=
  gi.dual.u_le_u_iff

Monotonicity of Lower Adjoint in Galois Coinsertion: $l(a) \leq l(b) \leftrightarrow a \leq b$

Informal description

Let $\alpha$ and $\beta$ be preorders, and let $(l, u)$ be a Galois coinsertion between them. For any elements $a, b \in \alpha$, the inequality $l(a) \leq l(b)$ holds if and only if $a \leq b$.

GaloisCoinsertion.strictMono_l theorem

[Preorder α] [Preorder β] (gi : GaloisCoinsertion l u) : StrictMono l

Full source

theorem strictMono_l [Preorder α] [Preorder β] (gi : GaloisCoinsertion l u) : StrictMono l :=
  fun _ _ h => gi.dual.strictMono_u h

Strict Monotonicity of the Lower Adjoint in a Galois Coinsertion

Informal description

Let $\alpha$ and $\beta$ be preorders, and let $(l, u)$ be a Galois coinsertion between them. Then the lower adjoint $l : \alpha \to \beta$ is strictly monotone, meaning that for any $a, b \in \alpha$, if $a < b$ then $l(a) < l(b)$.

Main definitions