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 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 β]
(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 ⇑(rel_iso.symm oi)
Makes a Galois connection from an order-preserving bijection.
theorem
galois_connection.l_le
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{a : α}
{b : β}
(a_1 : a ≤ u b) :
l a ≤ b
theorem
galois_connection.le_u
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{a : α}
{b : β}
(a_1 : l a ≤ b) :
a ≤ u b
theorem
galois_connection.le_u_l
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
(a : α) :
a ≤ u (l a)
theorem
galois_connection.l_u_le
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
(a : β) :
l (u a) ≤ a
theorem
galois_connection.monotone_u
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u) :
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_subset
{α : 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_subset
{α : 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.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_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.u_l_u_eq_u
{α : Type u}
{β : Type v}
[partial_order α]
[partial_order β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u) :
theorem
galois_connection.l_u_l_eq_l
{α : Type u}
{β : Type v}
[partial_order α]
[partial_order β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u) :
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 : β → α}
(gc : galois_connection l u) :
theorem
galois_connection.l_bot
{α : Type u}
{β : Type v}
[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.u_infi
{α : Type u}
{β : Type v}
{ι : Sort x}
[complete_lattice α]
[complete_lattice β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u)
{f : ι → β} :
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.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)
theorem
galois_connection.dual
{α : Type u}
{β : Type v}
[pα : preorder α]
[pβ : preorder β]
{l : α → β}
{u : β → α}
(gc : galois_connection 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)
(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
nat.galois_connection_mul_div
{k : ℕ}
(h : 0 < k) :
galois_connection (λ (n : ℕ), n * k) (λ (n : ℕ), n / k)
@[nolint]
structure
galois_insertion
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
(l : α → β)
(u : β → α) :
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 : β → α}
(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.
def
rel_iso.to_galois_insertion
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
(oi : α ≃o β) :
galois_insertion ⇑oi ⇑(rel_iso.symm oi)
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}
[order_bot α]
[partial_order β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u) :
Lift the bottom along a Galois connection
Equations
- gc.lift_order_bot = {bot := l ⊥, le := partial_order.le _inst_2, lt := partial_order.lt _inst_2, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _}
theorem
galois_insertion.l_u_eq
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[preorder α]
[partial_order β]
(gi : galois_insertion l u)
(b : β) :
l (u b) = b
theorem
galois_insertion.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_supr_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_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_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.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 α]
[partial_order β]
(gi : galois_insertion l u) :
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 β]
[order_top α]
(gi : galois_insertion l u) :
Lift the top along a Galois insertion
Equations
- gi.lift_order_top = {top := gi.choice ⊤ galois_insertion.lift_order_top._proof_1, le := partial_order.le _inst_1, lt := partial_order.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _}
def
galois_insertion.lift_bounded_lattice
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[partial_order β]
[bounded_lattice α]
(gi : galois_insertion l u) :
Lift the top, bottom, suprema, and infima along a Galois insertion
Equations
- gi.lift_bounded_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 := _, 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 := bounded_lattice.sup gi.lift_bounded_lattice, le := bounded_lattice.le gi.lift_bounded_lattice, lt := bounded_lattice.lt gi.lift_bounded_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := bounded_lattice.inf gi.lift_bounded_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, top := bounded_lattice.top gi.lift_bounded_lattice, le_top := _, bot := bounded_lattice.bot gi.lift_bounded_lattice, bot_le := _, Sup := λ (s : set β), l (⨆ (b : β) (H : b ∈ s), u b), Inf := λ (s : set β), gi.choice (⨅ (b : β) (H : b ∈ s), u b) _, le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _}
@[nolint]
structure
galois_coinsertion
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
(l : α → β)
(u : β → α) :
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 : β → α}
(a : 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 : β → α}
(a : galois_insertion l u) :
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 : β → α}
(a : galois_insertion u l) :
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 : β → α}
(a : 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 := _}
def
rel_iso.to_galois_coinsertion
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
(oi : α ≃o β) :
galois_coinsertion ⇑oi ⇑(rel_iso.symm oi)
Makes a Galois coinsertion from an order-preserving bijection.
Equations
- rel_iso.to_galois_coinsertion oi = {choice := λ (b : β) (h : b ≤ ⇑oi (⇑(rel_iso.symm oi) b)), ⇑(rel_iso.symm oi) b, gc := _, u_l_le := _, choice_eq := _}
def
galois_coinsertion.monotone_intro
{α : Type u_1}
{β : Type u_2}
[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 α]
[order_top β]
{l : α → β}
{u : β → α}
(gc : galois_connection l u) :
Lift the top along a Galois connection
Equations
- gc.lift_order_top = {top := u ⊤, le := partial_order.le _inst_1, lt := partial_order.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _}
theorem
galois_coinsertion.u_l_eq
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[partial_order α]
[preorder β]
(gi : galois_coinsertion l u)
(a : α) :
u (l a) = a
theorem
galois_coinsertion.u_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_infi_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_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_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.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 : β → α}
[partial_order α]
[preorder β]
(gi : galois_coinsertion l u) :
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 α]
[order_bot β]
(gi : galois_coinsertion l u) :
Lift the bot along a Galois coinsertion
Equations
- gi.lift_order_bot = {bot := gi.choice ⊥ galois_coinsertion.lift_order_bot._proof_1, le := partial_order.le _inst_1, lt := partial_order.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _}
def
galois_coinsertion.lift_bounded_lattice
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[partial_order α]
[bounded_lattice β]
(gi : galois_coinsertion l u) :
Lift the top, bottom, suprema, and infima along a Galois coinsertion
Equations
- gi.lift_bounded_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 := _, 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 := bounded_lattice.sup gi.lift_bounded_lattice, le := bounded_lattice.le gi.lift_bounded_lattice, lt := bounded_lattice.lt gi.lift_bounded_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := bounded_lattice.inf gi.lift_bounded_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, top := bounded_lattice.top gi.lift_bounded_lattice, le_top := _, bot := bounded_lattice.bot gi.lift_bounded_lattice, bot_le := _, Sup := λ (s : set α), gi.choice (⨆ (a : α) (H : a ∈ s), l a) _, Inf := λ (s : set α), u (⨅ (a : α) (H : a ∈ s), l a), le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _}