mathlib documentation

order.galois_connection

Galois connections, insertions and coinsertions

Galois connections are order theoretic adjoints, i.e. a pair of functions u and l, such that ∀a b, l a ≤ b ↔ a ≤ u b.

Main definitions

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 this is the Galois insertion is in group thery. If G is a topological space, 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 left adjoint is subgroup.closure, taking the subgroup generated by a set, The right adjoint is the coercion from subgroup G to set G, taking the underlying set of an subgroup.

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

def galois_connection {α : Type u} {β : Type v} [preorder α] [preorder β] :
(α → β)(β → α) → Prop

A Galois connection is a pair of functions l and u satisfying l a ≤ b ↔ a ≤ u b. They are special cases of adjoint functors in category theory, but do not depend on the category theory library in mathlib.

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

Makes a Galois connection from an order-preserving bijection.

theorem galois_connection.monotone_intro {α : Type u} {β : Type v} [preorder α] [preorder β] {l : α → β} {u : β → α} :
monotone umonotone l(∀ (a : α), a u (l a))(∀ (a : β), l (u a) a)galois_connection l u

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

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

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

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

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

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

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

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

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

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

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

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

theorem galois_connection.u_l_u_eq_u {α : Type u} {β : Type v} [partial_order α] [partial_order β] {l : α → β} {u : β → α} :
galois_connection l uu l u = u

theorem galois_connection.l_u_l_eq_l {α : Type u} {β : Type v} [partial_order α] [partial_order β] {l : α → β} {u : β → α} :
galois_connection l ul u l = l

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

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

theorem galois_connection.u_top {α : Type u} {β : Type v} [order_top α] [order_top β] {l : α → β} {u : β → α} :

theorem galois_connection.l_bot {α : Type u} {β : Type v} [order_bot α] [order_bot β] {l : α → β} {u : β → α} :

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

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

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

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

theorem galois_connection.l_Sup {α : Type u} {β : Type v} [complete_lattice α] [complete_lattice β] {l : α → β} {u : β → α} (gc : galois_connection l u) {s : set α} :
l (Sup s) = ⨆ (a : α) (H : a s), l a

theorem galois_connection.u_Inf {α : Type u} {β : Type v} [complete_lattice α] [complete_lattice β] {l : α → β} {u : β → α} (gc : galois_connection l u) {s : set β} :
u (Inf s) = ⨅ (a : β) (H : a s), u a

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

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

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

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

theorem nat.galois_connection_mul_div {k : } :
0 < kgalois_connection (λ (n : ), n * k) (λ (n : ), n / k)

@[nolint]
structure galois_insertion {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
(α → β)(β → α)Type (max u_1 u_2)
  • choice : Π (x : α), u (l x) x → β
  • gc : galois_connection l u
  • le_l_u : ∀ (x : β), x l (u x)
  • choice_eq : ∀ (a : α) (h : u (l a) a), c.choice a h = l a

A Galois insertion is a Galois connection where l ∘ u = id. It also contains a constructive choice function, to give better definitional equalities when lifting order structures. Dual to galois_coinsertion

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

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

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

Makes a Galois insertion from an order-preserving bijection.

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

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

Equations
def galois_connection.lift_order_bot {α : Type u_1} {β : Type u_2} [order_bot α] [partial_order β] {l : α → β} {u : β → α} :

Lift the bottom along a Galois connection

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

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

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

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

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

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

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

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

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

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

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

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

Lift the suprema along a Galois insertion

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

Lift the infima along a Galois insertion

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

Lift the suprema and infima along a Galois insertion

Equations
def galois_insertion.lift_order_top {α : Type u} {β : Type v} {l : α → β} {u : β → α} [partial_order β] [order_top α] :

Lift the top along a Galois insertion

Equations
def galois_insertion.lift_bounded_lattice {α : Type u} {β : Type v} {l : α → β} {u : β → α} [partial_order β] [bounded_lattice α] :

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

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

Lift all suprema and infima along a Galois insertion

Equations
@[nolint]
structure galois_coinsertion {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
(α → β)(β → α)Type (max u_1 u_2)
  • choice : Π (x : β), x l (u x) → α
  • gc : galois_connection l u
  • u_l_le : ∀ (x : α), u (l x) x
  • choice_eq : ∀ (a : β) (h : a l (u a)), c.choice a h = u a

A Galois coinsertion is a Galois connection where u ∘ l = id. It also contains a constructive choice function, to give better definitional equalities when lifting order structures. Dual to galois_insertion

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

Make a galois_insertion u l in the order_dual, from a galois_coinsertion l u

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

Make a galois_coinsertion u l in the order_dual, from a galois_insertion l u

Equations
def galois_coinsertion.of_dual {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {l : α → β} {u : β → α} :

Make a galois_coinsertion l u from a galois_insertion l u in the order_dual

Equations
def galois_insertion.of_dual {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {l : α → β} {u : β → α} :

Make a galois_insertion l u from a galois_coinsertion l u in the order_dual

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

Makes a Galois coinsertion from an order-preserving bijection.

Equations
def galois_coinsertion.monotone_intro {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {l : α → β} {u : β → α} :
monotone umonotone l(∀ (b : β), l (u b) b)(∀ (a : α), u (l a) = a)galois_coinsertion l u

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

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

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

Equations
def galois_connection.lift_order_top {α : Type u_1} {β : Type u_2} [partial_order α] [order_top β] {l : α → β} {u : β → α} :

Lift the top along a Galois connection

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

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

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

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

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

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

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

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

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

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

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

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

Lift the infima along a Galois coinsertion

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

Lift the suprema along a Galois coinsertion

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

Lift the suprema and infima along a Galois coinsertion

Equations
def galois_coinsertion.lift_order_bot {α : Type u} {β : Type v} {l : α → β} {u : β → α} [partial_order α] [order_bot β] :

Lift the bot along a Galois coinsertion

Equations
def galois_coinsertion.lift_bounded_lattice {α : Type u} {β : Type v} {l : α → β} {u : β → α} [partial_order α] [bounded_lattice β] :

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

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

Lift all suprema and infima along a Galois coinsertion

Equations

If α is a partial order with bottom element (e.g., , ℝ≥0), then λ o : with_bot α, o.get_or_else ⊥ and coercion form a Galois insertion.

Equations