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 #
galois_connection: A Galois connection is a pair of functionslandusatisfyingl a ≤ b ↔ a ≤ u b. They are special cases of adjoint functors in category theory, but do not depend on the category theory library in mathlib.galois_insertion: A Galois insertion is a Galois connection wherel ∘ u = idgalois_coinsertion: A Galois coinsertion is a Galois connection whereu ∘ l = id
Implementation details #
Galois insertions can be used to lift order structures from one type to another.
For example if α is a complete lattice, and l : α → β, and u : β → α form a Galois insertion,
then β is also a complete lattice. l is the lower adjoint and u is the upper adjoint.
An example of a Galois insertion is in group theory. If G is a group, then there is a Galois
insertion between the set of subsets of G, set G, and the set of subgroups of G,
subgroup G. The lower adjoint is subgroup.closure, taking the subgroup generated by a set,
and the upper adjoint is the coercion from subgroup G to set G, taking the underlying set
of a subgroup.
Naively lifting a lattice structure along this Galois insertion would mean that the definition
of inf on subgroups would be subgroup.closure (↑S ∩ ↑T). This is an undesirable definition
because the intersection of subgroups is already a subgroup, so there is no need to take the
closure. For this reason a choice function is added as a field to the galois_insertion
structure. It has type Π S : set G, ↑(closure S) ≤ S → subgroup G. When ↑(closure S) ≤ S, then
S is already a subgroup, so this function can be defined using subgroup.mk and not closure.
This means the infimum of subgroups will be defined to be the intersection of sets, paired
with a proof that intersection of subgroups is a subgroup, rather than the closure of the
intersection.
def
galois_connection
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
(l : α → β)
(u : β → α) :
Prop
A Galois connection is a pair of functions l and u satisfying
l a ≤ b ↔ a ≤ u b. They are special cases of adjoint functors in category theory,
but do not depend on the category theory library in mathlib.
Equations
- galois_connection l u = ∀ (a : α) (b : β), l a ≤ b ↔ a ≤ u b
theorem
order_iso.to_galois_connection
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
(oi : α ≃o β) :
galois_connection ⇑oi ⇑(oi.symm)
Makes a Galois connection from an order-preserving bijection.
@[protected]
theorem
galois_connection.dual
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u) :
theorem
galois_connection.le_iff_le
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{a : α}
{b : β} :
theorem
galois_connection.l_le
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{a : α}
{b : β} :
theorem
galois_connection.le_u
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{a : α}
{b : β} :
theorem
galois_connection.le_u_l
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
(a : α) :
a ≤ u (l a)
theorem
galois_connection.l_u_le
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
(a : β) :
l (u a) ≤ a
theorem
galois_connection.monotone_u
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u) :
monotone u
theorem
galois_connection.monotone_l
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u) :
monotone l
theorem
galois_connection.upper_bounds_l_image
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
(s : set α) :
upper_bounds (l '' s) = u ⁻¹' upper_bounds s
theorem
galois_connection.lower_bounds_u_image
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
(s : set β) :
lower_bounds (u '' s) = l ⁻¹' lower_bounds s
theorem
galois_connection.bdd_above_l_image
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{s : set α} :
theorem
galois_connection.bdd_below_u_image
{α : 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 : α}
(h : is_lub s a) :
theorem
galois_connection.is_glb_u_image
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{s : set β}
{b : β}
(h : is_glb s b) :
theorem
galois_connection.is_least_l
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{a : α} :
theorem
galois_connection.is_greatest_u
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{b : β} :
is_greatest {a : α | l a ≤ b} (u b)
theorem
galois_connection.is_glb_l
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{a : α} :
theorem
galois_connection.is_lub_u
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{b : β} :
theorem
galois_connection.le_u_l_trans
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{x y z : α}
(hxy : x ≤ u (l y))
(hyz : y ≤ u (l z)) :
x ≤ u (l z)
If (l, u) is a Galois connection, then the relation x ≤ u (l y) is a transitive relation.
If l is a closure operator (submodule.span, subgroup.closure, ...) and u is the coercion to
set, this reads as "if U is in the closure of V and V is in the closure of W then U is
in the closure of W".
theorem
galois_connection.l_u_le_trans
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{x y z : β}
(hxy : l (u x) ≤ y)
(hyz : l (u y) ≤ z) :
l (u x) ≤ z
theorem
galois_connection.u_l_u_eq_u
{α : Type u}
{β : Type v}
[partial_order α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
(b : β) :
u (l (u b)) = u b
theorem
galois_connection.u_l_u_eq_u'
{α : Type u}
{β : Type v}
[partial_order α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u) :
theorem
galois_connection.u_unique
{α : Type u}
{β : Type v}
[partial_order α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{l' : α → β}
{u' : β → α}
(gc' : galois_connection l' u')
(hl : ∀ (a : α), l a = l' a)
{b : β} :
u b = u' b
theorem
galois_connection.exists_eq_u
{α : Type u}
{β : Type v}
[partial_order α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
(a : α) :
If there exists a b such that a = u a, then b = l a is one such element.
theorem
galois_connection.u_eq
{α : Type u}
{β : Type v}
[partial_order α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{z : α}
{y : β} :
theorem
galois_connection.l_u_l_eq_l
{α : Type u}
{β : Type v}
[preorder α]
[partial_order β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
(a : α) :
l (u (l a)) = l a
theorem
galois_connection.l_u_l_eq_l'
{α : Type u}
{β : Type v}
[preorder α]
[partial_order β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u) :
theorem
galois_connection.l_unique
{α : Type u}
{β : Type v}
[preorder α]
[partial_order β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{l' : α → β}
{u' : β → α}
(gc' : galois_connection l' u')
(hu : ∀ (b : β), u b = u' b)
{a : α} :
l a = l' a
theorem
galois_connection.exists_eq_l
{α : Type u}
{β : Type v}
[preorder α]
[partial_order β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
(b : β) :
If there exists an a such that b = l a, then a = u b is one such element.
theorem
galois_connection.l_eq
{α : Type u}
{β : Type v}
[preorder α]
[partial_order β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{x : α}
{z : β} :
theorem
galois_connection.u_top
{α : Type u}
{β : Type v}
[partial_order α]
[preorder β]
[order_top α]
[order_top β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u) :
theorem
galois_connection.l_bot
{α : Type u}
{β : Type v}
[preorder α]
[partial_order β]
[order_bot α]
[order_bot β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u) :
theorem
galois_connection.l_sup
{α : Type u}
{β : Type v}
{a₁ a₂ : α}
[semilattice_sup α]
[semilattice_sup β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u) :
theorem
galois_connection.u_inf
{α : Type u}
{β : Type v}
{b₁ b₂ : β}
[semilattice_inf α]
[semilattice_inf β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u) :
theorem
galois_connection.l_supr
{α : Type u}
{β : Type v}
{ι : Sort x}
[complete_lattice α]
[complete_lattice β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{f : ι → α} :
theorem
galois_connection.l_supr₂
{α : Type u}
{β : Type v}
{ι : Sort x}
{κ : ι → Sort u_1}
[complete_lattice α]
[complete_lattice β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{f : Π (i : ι), κ i → α} :
l (⨆ (i : ι) (j : κ i), f i j) = ⨆ (i : ι) (j : κ i), l (f i j)
theorem
galois_connection.u_infi
{α : Type u}
{β : Type v}
{ι : Sort x}
[complete_lattice α]
[complete_lattice β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{f : ι → β} :
theorem
galois_connection.u_infi₂
{α : Type u}
{β : Type v}
{ι : Sort x}
{κ : ι → Sort u_1}
[complete_lattice α]
[complete_lattice β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{f : Π (i : ι), κ i → β} :
u (⨅ (i : ι) (j : κ i), f i j) = ⨅ (i : ι) (j : κ i), u (f i j)
theorem
galois_connection.l_Sup
{α : Type u}
{β : Type v}
[complete_lattice α]
[complete_lattice β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{s : set α} :
theorem
galois_connection.u_Inf
{α : Type u}
{β : Type v}
[complete_lattice α]
[complete_lattice β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{s : set β} :
theorem
galois_connection.lt_iff_lt
{α : Type u}
{β : Type v}
[linear_order α]
[linear_order β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{a : α}
{b : β} :
@[protected]
@[protected]
theorem
galois_connection.compose
{α : Type u}
{β : Type v}
{γ : Type w}
[preorder α]
[preorder β]
[preorder γ]
{l1 : α → β}
{u1 : β → α}
{l2 : β → γ}
{u2 : γ → β}
(gc1 : galois_connection l1 u1)
(gc2 : galois_connection l2 u2) :
galois_connection (l2 ∘ l1) (u1 ∘ u2)
@[protected]
theorem
galois_connection.dfun
{ι : Type u}
{α : ι → Type v}
{β : ι → Type w}
[Π (i : ι), preorder (α i)]
[Π (i : ι), preorder (β i)]
(l : Π (i : ι), α i → β i)
(u : Π (i : ι), β i → α i)
(gc : ∀ (i : ι), galois_connection (l i) (u i)) :
galois_connection (λ (a : Π (i : ι), α i) (i : ι), l i (a i)) (λ (b : Π (i : ι), β i) (i : ι), u i (b i))
theorem
galois_connection.l_comm_of_u_comm
{X : Type u_1}
[preorder X]
{Y : Type u_2}
[preorder Y]
{Z : Type u_3}
[preorder Z]
{W : Type u_4}
[partial_order W]
{lYX : X → Y}
{uXY : Y → X}
(hXY : galois_connection lYX uXY)
{lWZ : Z → W}
{uZW : W → Z}
(hZW : galois_connection lWZ uZW)
{lWY : Y → W}
{uYW : W → Y}
(hWY : galois_connection lWY uYW)
{lZX : X → Z}
{uXZ : Z → X}
(hXZ : galois_connection lZX uXZ)
(h : ∀ (w : W), uXZ (uZW w) = uXY (uYW w))
{x : X} :
lWZ (lZX x) = lWY (lYX x)
theorem
galois_connection.u_comm_of_l_comm
{X : Type u_1}
[partial_order X]
{Y : Type u_2}
[preorder Y]
{Z : Type u_3}
[preorder Z]
{W : Type u_4}
[preorder W]
{lYX : X → Y}
{uXY : Y → X}
(hXY : galois_connection lYX uXY)
{lWZ : Z → W}
{uZW : W → Z}
(hZW : galois_connection lWZ uZW)
{lWY : Y → W}
{uYW : W → Y}
(hWY : galois_connection lWY uYW)
{lZX : X → Z}
{uXZ : Z → X}
(hXZ : galois_connection lZX uXZ)
(h : ∀ (x : X), lWZ (lZX x) = lWY (lYX x))
{w : W} :
uXZ (uZW w) = uXY (uYW w)
theorem
galois_connection.l_comm_iff_u_comm
{X : Type u_1}
[partial_order X]
{Y : Type u_2}
[preorder Y]
{Z : Type u_3}
[preorder Z]
{W : Type u_4}
[partial_order W]
{lYX : X → Y}
{uXY : Y → X}
(hXY : galois_connection lYX uXY)
{lWZ : Z → W}
{uZW : W → Z}
(hZW : galois_connection lWZ uZW)
{lWY : Y → W}
{uYW : W → Y}
(hWY : galois_connection lWY uYW)
{lZX : X → Z}
{uXZ : Z → X}
(hXZ : galois_connection lZX uXZ) :
theorem
nat.galois_connection_mul_div
{k : ℕ}
(h : 0 < k) :
galois_connection (λ (n : ℕ), n * k) (λ (n : ℕ), n / k)
@[nolint]
structure
galois_insertion
{α : Type u_2}
{β : Type u_3}
[preorder α]
[preorder β]
(l : α → β)
(u : β → α) :
Type (max u_2 u_3)
- choice : Π (x : α), u (l x) ≤ x → β
- gc : galois_connection l u
- le_l_u : ∀ (x : β), x ≤ l (u x)
- choice_eq : ∀ (a : α) (h : u (l a) ≤ a), self.choice a h = l a
A Galois insertion is a Galois connection where l ∘ u = id. It also contains a constructive
choice function, to give better definitional equalities when lifting order structures. Dual
to galois_coinsertion
def
galois_insertion.monotone_intro
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α}
(hu : monotone u)
(hl : monotone l)
(hul : ∀ (a : α), a ≤ u (l a))
(hlu : ∀ (b : β), l (u b) = b) :
galois_insertion l u
A constructor for a Galois insertion with the trivial choice function.
@[protected]
def
order_iso.to_galois_insertion
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
(oi : α ≃o β) :
galois_insertion ⇑oi ⇑(oi.symm)
Makes a Galois insertion from an order-preserving bijection.
def
galois_connection.to_galois_insertion
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
(h : ∀ (b : β), b ≤ l (u b)) :
galois_insertion l u
Make a galois_insertion l u from a galois_connection l u such that ∀ b, b ≤ l (u b)
def
galois_connection.lift_order_bot
{α : Type u_1}
{β : Type u_2}
[preorder α]
[order_bot α]
[partial_order β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u) :
Lift the bottom along a Galois connection
theorem
galois_insertion.l_u_eq
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[preorder α]
[partial_order β]
(gi : galois_insertion l u)
(b : β) :
l (u b) = b
theorem
galois_insertion.left_inverse_l_u
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[preorder α]
[partial_order β]
(gi : galois_insertion l u) :
theorem
galois_insertion.l_surjective
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[preorder α]
[partial_order β]
(gi : galois_insertion l u) :
theorem
galois_insertion.u_injective
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[preorder α]
[partial_order β]
(gi : galois_insertion l u) :
theorem
galois_insertion.l_sup_u
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[semilattice_sup α]
[semilattice_sup β]
(gi : galois_insertion l u)
(a b : β) :
theorem
galois_insertion.l_supr_u
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[complete_lattice α]
[complete_lattice β]
(gi : galois_insertion l u)
{ι : Sort x}
(f : ι → β) :
l (⨆ (i : ι), u (f i)) = ⨆ (i : ι), f i
theorem
galois_insertion.l_bsupr_u
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[complete_lattice α]
[complete_lattice β]
(gi : galois_insertion l u)
{ι : Sort x}
{p : ι → Prop}
(f : Π (i : ι), p i → β) :
l (⨆ (i : ι) (hi : p i), u (f i hi)) = ⨆ (i : ι) (hi : p i), f i hi
theorem
galois_insertion.l_Sup_u_image
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[complete_lattice α]
[complete_lattice β]
(gi : galois_insertion l u)
(s : set β) :
theorem
galois_insertion.l_inf_u
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[semilattice_inf α]
[semilattice_inf β]
(gi : galois_insertion l u)
(a b : β) :
theorem
galois_insertion.l_infi_u
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[complete_lattice α]
[complete_lattice β]
(gi : galois_insertion l u)
{ι : Sort x}
(f : ι → β) :
l (⨅ (i : ι), u (f i)) = ⨅ (i : ι), f i
theorem
galois_insertion.l_binfi_u
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[complete_lattice α]
[complete_lattice β]
(gi : galois_insertion l u)
{ι : Sort x}
{p : ι → Prop}
(f : Π (i : ι), p i → β) :
l (⨅ (i : ι) (hi : p i), u (f i hi)) = ⨅ (i : ι) (hi : p i), f i hi
theorem
galois_insertion.l_Inf_u_image
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[complete_lattice α]
[complete_lattice β]
(gi : galois_insertion l u)
(s : set β) :
theorem
galois_insertion.l_infi_of_ul_eq_self
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[complete_lattice α]
[complete_lattice β]
(gi : galois_insertion l u)
{ι : Sort x}
(f : ι → α)
(hf : ∀ (i : ι), u (l (f i)) = f i) :
l (⨅ (i : ι), f i) = ⨅ (i : ι), l (f i)
theorem
galois_insertion.l_binfi_of_ul_eq_self
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[complete_lattice α]
[complete_lattice β]
(gi : galois_insertion l u)
{ι : Sort x}
{p : ι → Prop}
(f : Π (i : ι), p i → α)
(hf : ∀ (i : ι) (hi : p i), u (l (f i hi)) = f i hi) :
l (⨅ (i : ι) (hi : p i), f i hi) = ⨅ (i : ι) (hi : p i), l (f i hi)
theorem
galois_insertion.u_le_u_iff
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[preorder α]
[preorder β]
(gi : galois_insertion l u)
{a b : β} :
theorem
galois_insertion.strict_mono_u
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[preorder α]
[preorder β]
(gi : galois_insertion l u) :
theorem
galois_insertion.is_lub_of_u_image
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[preorder α]
[preorder β]
(gi : galois_insertion l u)
{s : set β}
{a : α}
(hs : is_lub (u '' s) a) :
is_lub s (l a)
theorem
galois_insertion.is_glb_of_u_image
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[preorder α]
[preorder β]
(gi : galois_insertion l u)
{s : set β}
{a : α}
(hs : is_glb (u '' s) a) :
is_glb s (l a)
def
galois_insertion.lift_semilattice_sup
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[partial_order β]
[semilattice_sup α]
(gi : galois_insertion l u) :
Lift the suprema along a Galois insertion
Equations
- gi.lift_semilattice_sup = {sup := λ (a b : β), l (u a ⊔ u b), le := partial_order.le _inst_1, lt := partial_order.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}
def
galois_insertion.lift_semilattice_inf
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[partial_order β]
[semilattice_inf α]
(gi : galois_insertion l u) :
Lift the infima along a Galois insertion
Equations
- gi.lift_semilattice_inf = {inf := λ (a b : β), gi.choice (u a ⊓ u b) _, le := partial_order.le _inst_1, lt := partial_order.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}
def
galois_insertion.lift_lattice
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[partial_order β]
[lattice α]
(gi : galois_insertion l u) :
lattice β
Lift the suprema and infima along a Galois insertion
Equations
- gi.lift_lattice = {sup := semilattice_sup.sup gi.lift_semilattice_sup, le := semilattice_sup.le gi.lift_semilattice_sup, lt := semilattice_sup.lt gi.lift_semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf gi.lift_semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}
def
galois_insertion.lift_order_top
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[partial_order β]
[preorder α]
[order_top α]
(gi : galois_insertion l u) :
Lift the top along a Galois insertion
def
galois_insertion.lift_bounded_order
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[partial_order β]
[preorder α]
[bounded_order α]
(gi : galois_insertion l u) :
Lift the top, bottom, suprema, and infima along a Galois insertion
Equations
- gi.lift_bounded_order = {top := order_top.top gi.lift_order_top, le_top := _, bot := order_bot.bot _.lift_order_bot, bot_le := _}
def
galois_insertion.lift_complete_lattice
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[partial_order β]
[complete_lattice α]
(gi : galois_insertion l u) :
Lift all suprema and infima along a Galois insertion
Equations
- gi.lift_complete_lattice = {sup := lattice.sup gi.lift_lattice, le := lattice.le gi.lift_lattice, lt := lattice.lt gi.lift_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf gi.lift_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := λ (s : set β), l (Sup (u '' s)), le_Sup := _, Sup_le := _, Inf := λ (s : set β), gi.choice (Inf (u '' s)) _, Inf_le := _, le_Inf := _, top := bounded_order.top gi.lift_bounded_order, bot := bounded_order.bot gi.lift_bounded_order, le_top := _, bot_le := _}
@[nolint]
structure
galois_coinsertion
{α : Type u_2}
{β : Type u_3}
[preorder α]
[preorder β]
(l : α → β)
(u : β → α) :
Type (max u_2 u_3)
- choice : Π (x : β), x ≤ l (u x) → α
- gc : galois_connection l u
- u_l_le : ∀ (x : α), u (l x) ≤ x
- choice_eq : ∀ (a : β) (h : a ≤ l (u a)), self.choice a h = u a
A Galois coinsertion is a Galois connection where u ∘ l = id. It also contains a constructive
choice function, to give better definitional equalities when lifting order structures. Dual to
galois_insertion
def
galois_coinsertion.dual
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α} :
galois_coinsertion l u → galois_insertion u l
Make a galois_insertion u l in the order_dual, from a galois_coinsertion l u
Equations
- galois_coinsertion.dual = λ (x : galois_coinsertion l u), {choice := x.choice, gc := _, le_l_u := _, choice_eq := _}
def
galois_insertion.dual
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α} :
galois_insertion l u → galois_coinsertion u l
Make a galois_coinsertion u l in the order_dual, from a galois_insertion l u
Equations
- galois_insertion.dual = λ (x : galois_insertion l u), {choice := x.choice, gc := _, u_l_le := _, choice_eq := _}
def
galois_coinsertion.of_dual
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α} :
galois_insertion u l → galois_coinsertion l u
Make a galois_coinsertion l u from a galois_insertion l u in the order_dual
Equations
- galois_coinsertion.of_dual = λ (x : galois_insertion u l), {choice := x.choice, gc := _, u_l_le := _, choice_eq := _}
def
galois_insertion.of_dual
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α} :
galois_coinsertion u l → galois_insertion l u
Make a galois_insertion l u from a galois_coinsertion l u in the order_dual
Equations
- galois_insertion.of_dual = λ (x : galois_coinsertion u l), {choice := x.choice, gc := _, le_l_u := _, choice_eq := _}
@[protected]
def
rel_iso.to_galois_coinsertion
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
(oi : α ≃o β) :
galois_coinsertion ⇑oi ⇑(oi.symm)
Makes a Galois coinsertion from an order-preserving bijection.
def
galois_coinsertion.monotone_intro
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α}
(hu : monotone u)
(hl : monotone l)
(hlu : ∀ (b : β), l (u b) ≤ b)
(hul : ∀ (a : α), u (l a) = a) :
A constructor for a Galois coinsertion with the trivial choice function.
Equations
- galois_coinsertion.monotone_intro hu hl hlu hul = galois_coinsertion.of_dual (galois_insertion.monotone_intro _ _ hlu hul)
def
galois_connection.to_galois_coinsertion
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
(h : ∀ (a : α), u (l a) ≤ a) :
Make a galois_coinsertion l u from a galois_connection l u such that ∀ b, b ≤ l (u b)
def
galois_connection.lift_order_top
{α : Type u_1}
{β : Type u_2}
[partial_order α]
[preorder β]
[order_top β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u) :
Lift the top along a Galois connection
theorem
galois_coinsertion.u_l_eq
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[partial_order α]
[preorder β]
(gi : galois_coinsertion l u)
(a : α) :
u (l a) = a
theorem
galois_coinsertion.u_l_left_inverse
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[partial_order α]
[preorder β]
(gi : galois_coinsertion l u) :
theorem
galois_coinsertion.u_surjective
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[partial_order α]
[preorder β]
(gi : galois_coinsertion l u) :
theorem
galois_coinsertion.l_injective
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[partial_order α]
[preorder β]
(gi : galois_coinsertion l u) :
theorem
galois_coinsertion.u_inf_l
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[semilattice_inf α]
[semilattice_inf β]
(gi : galois_coinsertion l u)
(a b : α) :
theorem
galois_coinsertion.u_infi_l
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[complete_lattice α]
[complete_lattice β]
(gi : galois_coinsertion l u)
{ι : Sort x}
(f : ι → α) :
u (⨅ (i : ι), l (f i)) = ⨅ (i : ι), f i
theorem
galois_coinsertion.u_Inf_l_image
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[complete_lattice α]
[complete_lattice β]
(gi : galois_coinsertion l u)
(s : set α) :
theorem
galois_coinsertion.u_sup_l
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[semilattice_sup α]
[semilattice_sup β]
(gi : galois_coinsertion l u)
(a b : α) :
theorem
galois_coinsertion.u_supr_l
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[complete_lattice α]
[complete_lattice β]
(gi : galois_coinsertion l u)
{ι : Sort x}
(f : ι → α) :
u (⨆ (i : ι), l (f i)) = ⨆ (i : ι), f i
theorem
galois_coinsertion.u_bsupr_l
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[complete_lattice α]
[complete_lattice β]
(gi : galois_coinsertion l u)
{ι : Sort x}
{p : ι → Prop}
(f : Π (i : ι), p i → α) :
u (⨆ (i : ι) (hi : p i), l (f i hi)) = ⨆ (i : ι) (hi : p i), f i hi
theorem
galois_coinsertion.u_Sup_l_image
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[complete_lattice α]
[complete_lattice β]
(gi : galois_coinsertion l u)
(s : set α) :
theorem
galois_coinsertion.u_supr_of_lu_eq_self
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[complete_lattice α]
[complete_lattice β]
(gi : galois_coinsertion l u)
{ι : Sort x}
(f : ι → β)
(hf : ∀ (i : ι), l (u (f i)) = f i) :
u (⨆ (i : ι), f i) = ⨆ (i : ι), u (f i)
theorem
galois_coinsertion.u_bsupr_of_lu_eq_self
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[complete_lattice α]
[complete_lattice β]
(gi : galois_coinsertion l u)
{ι : Sort x}
{p : ι → Prop}
(f : Π (i : ι), p i → β)
(hf : ∀ (i : ι) (hi : p i), l (u (f i hi)) = f i hi) :
u (⨆ (i : ι) (hi : p i), f i hi) = ⨆ (i : ι) (hi : p i), u (f i hi)
theorem
galois_coinsertion.l_le_l_iff
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[preorder α]
[preorder β]
(gi : galois_coinsertion l u)
{a b : α} :
theorem
galois_coinsertion.strict_mono_l
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[preorder α]
[preorder β]
(gi : galois_coinsertion l u) :
theorem
galois_coinsertion.is_glb_of_l_image
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[preorder α]
[preorder β]
(gi : galois_coinsertion l u)
{s : set α}
{a : β}
(hs : is_glb (l '' s) a) :
is_glb s (u a)
theorem
galois_coinsertion.is_lub_of_l_image
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[preorder α]
[preorder β]
(gi : galois_coinsertion l u)
{s : set α}
{a : β}
(hs : is_lub (l '' s) a) :
is_lub s (u a)
def
galois_coinsertion.lift_semilattice_inf
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[partial_order α]
[semilattice_inf β]
(gi : galois_coinsertion l u) :
Lift the infima along a Galois coinsertion
Equations
- gi.lift_semilattice_inf = {inf := λ (a b : α), u (l a ⊓ l b), le := partial_order.le _inst_1, lt := partial_order.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}
def
galois_coinsertion.lift_semilattice_sup
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[partial_order α]
[semilattice_sup β]
(gi : galois_coinsertion l u) :
Lift the suprema along a Galois coinsertion
Equations
- gi.lift_semilattice_sup = {sup := λ (a b : α), gi.choice (l a ⊔ l b) _, le := partial_order.le _inst_1, lt := partial_order.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}
def
galois_coinsertion.lift_lattice
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[partial_order α]
[lattice β]
(gi : galois_coinsertion l u) :
lattice α
Lift the suprema and infima along a Galois coinsertion
Equations
- gi.lift_lattice = {sup := semilattice_sup.sup gi.lift_semilattice_sup, le := semilattice_sup.le gi.lift_semilattice_sup, lt := semilattice_sup.lt gi.lift_semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf gi.lift_semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}
def
galois_coinsertion.lift_order_bot
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[partial_order α]
[preorder β]
[order_bot β]
(gi : galois_coinsertion l u) :
Lift the bot along a Galois coinsertion
def
galois_coinsertion.lift_bounded_order
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[partial_order α]
[preorder β]
[bounded_order β]
(gi : galois_coinsertion l u) :
Lift the top, bottom, suprema, and infima along a Galois coinsertion
Equations
- gi.lift_bounded_order = {top := order_top.top _.lift_order_top, le_top := _, bot := order_bot.bot gi.lift_order_bot, bot_le := _}
def
galois_coinsertion.lift_complete_lattice
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[partial_order α]
[complete_lattice β]
(gi : galois_coinsertion l u) :
Lift all suprema and infima along a Galois coinsertion
Equations
- gi.lift_complete_lattice = {sup := complete_lattice.sup (order_dual.complete_lattice (order_dual α)), le := complete_lattice.le (order_dual.complete_lattice (order_dual α)), lt := complete_lattice.lt (order_dual.complete_lattice (order_dual α)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := complete_lattice.inf (order_dual.complete_lattice (order_dual α)), inf_le_left := _, inf_le_right := _, le_inf := _, Sup := λ (s : set α), gi.choice (Sup (l '' s)) _, le_Sup := _, Sup_le := _, Inf := λ (s : set α), u (Inf (l '' s)), Inf_le := _, le_Inf := _, top := complete_lattice.top (order_dual.complete_lattice (order_dual α)), bot := complete_lattice.bot (order_dual.complete_lattice (order_dual α)), le_top := _, bot_le := _}
def
with_bot.gi_get_or_else_bot
{α : Type u}
[preorder α]
[order_bot α] :
galois_insertion (λ (o : with_bot α), option.get_or_else o ⊥) coe
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
- with_bot.gi_get_or_else_bot = {choice := λ (o : with_bot α) (ho : ↑(option.get_or_else o ⊥) ≤ o), option.get_or_else o ⊥, gc := _, le_l_u := _, choice_eq := _}