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∀ a b, l a ≤ b ↔ a ≤ u b≤ b ↔ a ≤ u b↔ a ≤ u b≤ u b
.
Main definitions #
GaloisConnection
: A Galois connection is a pair of functionsl
andu
satisfyingl a ≤ b ↔ a ≤ u b≤ b ↔ a ≤ u b↔ a ≤ u b≤ u b
. They are special cases of adjoint functors in category theory, but do not depend on the category theory library in mathlib.GaloisInsertion
: A Galois insertion is a Galois connection wherel ∘ u = id∘ u = id
GaloisCoinsertion
: A Galois coinsertion is a Galois connection whereu ∘ l = id∘ 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)↑S ∩ ↑T)∩ ↑T)↑T)
. This is an undesirable definition
because the intersection of subgroups is already a subgroup, so there is no need to take the
closure. For this reason a choice
function is added as a field to the GaloisInsertion
structure. It has type Π S : Set G, ↑(closure S) ≤ S → Subgroup G↑(closure S) ≤ S → Subgroup G≤ S → Subgroup G→ Subgroup G
. When ↑(closure S) ≤ S↑(closure S) ≤ 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.
A Galois connection is a pair of functions l
and u
satisfying
l a ≤ b ↔ a ≤ u b≤ b ↔ a ≤ u b↔ a ≤ u b≤ u b
. They are special cases of adjoint functors in category theory,
but do not depend on the category theory library in mathlib.
Equations
- GaloisConnection l u = ∀ (a : α) (b : β), l a ≤ b ↔ a ≤ u b
Makes a Galois connection from an order-preserving bijection.
If (l, u)
is a Galois connection, then the relation x ≤ u (l y)≤ 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
".
If there exists a b
such that a = u a
, then b = l a
is one such element.
If there exists an a
such that b = l a
, then a = u b
is one such element.
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 uMain property of a Galois insertion.
le_l_u : ∀ (x : β), x ≤ l (u x)Property of the choice function.
A Galois insertion is a Galois connection where l ∘ u = id∘ u = id
. It also contains a constructive
choice function, to give better definitional equalities when lifting order structures. Dual
to GaloisCoinsertion
Instances For
A constructor for a Galois insertion with the trivial choice
function.
Equations
- One or more equations did not get rendered due to their size.
Makes a Galois insertion from an order-preserving bijection.
Equations
- One or more equations did not get rendered due to their size.
Make a GaloisInsertion l u
from a GaloisConnection l u
such that ∀ b, b ≤ l (u b)∀ b, b ≤ l (u b)≤ l (u b)
Equations
- One or more equations did not get rendered due to their size.
Lift the bottom along a Galois connection
Equations
- GaloisConnection.liftOrderBot gc = OrderBot.mk (_ : ∀ (x : β), l ⊥ ≤ x)
Lift the suprema along a Galois insertion
Equations
- One or more equations did not get rendered due to their size.
Lift the infima along a Galois insertion
Lift the suprema and infima along a Galois insertion
Equations
- One or more equations did not get rendered due to their size.
Lift the top along a Galois insertion
Equations
- GaloisInsertion.liftOrderTop gi = OrderTop.mk (_ : ∀ (a : β), a ≤ ⊤)
Lift the top, bottom, suprema, and infima along a Galois insertion
Equations
- GaloisInsertion.liftBoundedOrder gi = let src := GaloisInsertion.liftOrderTop gi; let src_1 := GaloisConnection.liftOrderBot (_ : GaloisConnection l u); BoundedOrder.mk
Lift all suprema and infima along a Galois insertion
Equations
- One or more equations did not get rendered due to their size.
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 uMain property of a Galois coinsertion.
u_l_le : ∀ (x : α), u (l x) ≤ xProperty of the choice function.
A Galois coinsertion is a Galois connection where u ∘ l = id∘ l = id
. It also contains a constructive
choice function, to give better definitional equalities when lifting order structures. Dual to
GaloisInsertion
Instances For
Make a GaloisInsertion
between αᵒᵈ
and βᵒᵈ
from a GaloisCoinsertion
between α
and
β
.
Equations
- One or more equations did not get rendered due to their size.
Make a GaloisCoinsertion
between αᵒᵈ
and βᵒᵈ
from a GaloisInsertion
between α
and
β
.
Equations
- One or more equations did not get rendered due to their size.
Make a GaloisInsertion
between α
and β
from a GaloisCoinsertion
between αᵒᵈ
and
βᵒᵈ
.
Equations
- One or more equations did not get rendered due to their size.
Make a GaloisCoinsertion
between α
and β
from a GaloisInsertion
between αᵒᵈ
and
βᵒᵈ
.
Equations
- One or more equations did not get rendered due to their size.
Makes a Galois coinsertion from an order-preserving bijection.
Equations
- One or more equations did not get rendered due to their size.
A constructor for a Galois coinsertion with the trivial choice
function.
Equations
- One or more equations did not get rendered due to their size.
Make a GaloisCoinsertion l u
from a GaloisConnection l u
such that ∀ b, b ≤ l (u b)∀ b, b ≤ l (u b)≤ l (u b)
Equations
- One or more equations did not get rendered due to their size.
Lift the top along a Galois connection
Equations
- GaloisConnection.liftOrderTop gc = OrderTop.mk (_ : ∀ (x : α), x ≤ u ⊤)
Lift the infima along a Galois coinsertion
Lift the suprema along a Galois coinsertion
Lift the suprema and infima along a Galois coinsertion
Equations
- One or more equations did not get rendered due to their size.
Lift the bot along a Galois coinsertion
Equations
- GaloisCoinsertion.liftOrderBot gi = let src := OrderDual.orderBot αᵒᵈ; OrderBot.mk (_ : ∀ (a : αᵒᵈᵒᵈ), ⊥ ≤ a)
Lift the top, bottom, suprema, and infima along a Galois coinsertion
Equations
- GaloisCoinsertion.liftBoundedOrder gi = let src := GaloisCoinsertion.liftOrderBot gi; let src_1 := GaloisConnection.liftOrderTop (_ : GaloisConnection l u); BoundedOrder.mk
Lift all suprema and infima along a Galois coinsertion
Equations
- One or more equations did not get rendered due to their size.
If α
is a partial order with bottom element (e.g., ℕ
, ℝ≥0≥0
), then WithBot.unbot' ⊥⊥
and
coercion form a Galois insertion.
Equations
- One or more equations did not get rendered due to their size.