Galois connections, insertions and coinsertions #
This file contains basic results on Galois connections, insertions and coinsertions in various order structures, and provides constructions that lift order structures from one type to another.
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 GaloisInsertion
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.
theorem
GaloisConnection.upperBounds_l_image
{α : Type u}
{β : Type v}
[Preorder α]
[Preorder β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
(s : Set α)
:
upperBounds (l '' s) = u ⁻¹' upperBounds s
theorem
GaloisConnection.lowerBounds_u_image
{α : Type u}
{β : Type v}
[Preorder α]
[Preorder β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
(s : Set β)
:
lowerBounds (u '' s) = l ⁻¹' lowerBounds s
theorem
GaloisConnection.isLeast_l
{α : Type u}
{β : Type v}
[Preorder α]
[Preorder β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
{a : α}
:
theorem
GaloisConnection.isGreatest_u
{α : Type u}
{β : Type v}
[Preorder α]
[Preorder β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
{b : β}
:
IsGreatest {a : α | l a ≤ b} (u b)
theorem
GaloisConnection.isGLB_l
{α : Type u}
{β : Type v}
[Preorder α]
[Preorder β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
{a : α}
:
theorem
GaloisConnection.isLUB_u
{α : Type u}
{β : Type v}
[Preorder α]
[Preorder β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
{b : β}
:
theorem
GaloisConnection.l_sup
{α : Type u}
{β : Type v}
{a₁ a₂ : α}
[SemilatticeSup α]
[SemilatticeSup β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
:
theorem
GaloisConnection.u_inf
{α : Type u}
{β : Type v}
{b₁ b₂ : β}
[SemilatticeInf α]
[SemilatticeInf β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
:
theorem
GaloisConnection.l_iSup
{α : Type u}
{β : Type v}
{ι : Sort x}
[CompleteLattice α]
[CompleteLattice β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
{f : ι → α}
:
theorem
GaloisConnection.l_iSup₂
{α : Type u}
{β : Type v}
{ι : Sort x}
{κ : ι → Sort u_1}
[CompleteLattice α]
[CompleteLattice β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
{f : (i : ι) → κ i → α}
:
l (⨆ (i : ι), ⨆ (j : κ i), f i j) = ⨆ (i : ι), ⨆ (j : κ i), l (f i j)
theorem
GaloisConnection.u_iInf
{α : Type u}
{β : Type v}
{ι : Sort x}
[CompleteLattice α]
[CompleteLattice β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
{f : ι → β}
:
theorem
GaloisConnection.u_iInf₂
{α : Type u}
{β : Type v}
{ι : Sort x}
{κ : ι → Sort u_1}
[CompleteLattice α]
[CompleteLattice β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
{f : (i : ι) → κ i → β}
:
u (⨅ (i : ι), ⨅ (j : κ i), f i j) = ⨅ (i : ι), ⨅ (j : κ i), u (f i j)
theorem
GaloisConnection.l_sSup
{α : Type u}
{β : Type v}
[CompleteLattice α]
[CompleteLattice β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
{s : Set α}
:
theorem
GaloisConnection.u_sInf
{α : Type u}
{β : Type v}
[CompleteLattice α]
[CompleteLattice β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
{s : Set β}
:
theorem
GaloisConnection.compl
{α : Type u}
{β : Type v}
[BooleanAlgebra α]
[BooleanAlgebra β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
:
sSup and Iic form a Galois connection.
toDual ∘ Ici and sInf ∘ ofDual form a Galois connection.
theorem
sSup_image2_eq_sSup_sSup
{α : Type u}
{β : Type v}
{γ : Type w}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
{s : Set α}
{t : Set β}
{l : α → β → γ}
{u₁ : β → γ → α}
{u₂ : α → γ → β}
(h₁ : ∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b))
(h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a))
:
sSup (Set.image2 l s t) = l (sSup s) (sSup t)
theorem
sSup_image2_eq_sSup_sInf
{α : Type u}
{β : Type v}
{γ : Type w}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
{s : Set α}
{t : Set β}
{l : α → β → γ}
{u₁ : β → γ → α}
{u₂ : α → γ → β}
(h₁ : ∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b))
(h₂ : ∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a))
:
sSup (Set.image2 l s t) = l (sSup s) (sInf t)
theorem
sSup_image2_eq_sInf_sSup
{α : Type u}
{β : Type v}
{γ : Type w}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
{s : Set α}
{t : Set β}
{l : α → β → γ}
{u₁ : β → γ → α}
{u₂ : α → γ → β}
(h₁ : ∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b))
(h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a))
:
sSup (Set.image2 l s t) = l (sInf s) (sSup t)
theorem
sSup_image2_eq_sInf_sInf
{α : Type u}
{β : Type v}
{γ : Type w}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
{s : Set α}
{t : Set β}
{l : α → β → γ}
{u₁ : β → γ → α}
{u₂ : α → γ → β}
(h₁ : ∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b))
(h₂ : ∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a))
:
sSup (Set.image2 l s t) = l (sInf s) (sInf t)
theorem
sInf_image2_eq_sInf_sInf
{α : Type u}
{β : Type v}
{γ : Type w}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
{s : Set α}
{t : Set β}
{u : α → β → γ}
{l₁ : β → γ → α}
{l₂ : α → γ → β}
(h₁ : ∀ (b : β), GaloisConnection (l₁ b) (Function.swap u b))
(h₂ : ∀ (a : α), GaloisConnection (l₂ a) (u a))
:
sInf (Set.image2 u s t) = u (sInf s) (sInf t)
theorem
sInf_image2_eq_sInf_sSup
{α : Type u}
{β : Type v}
{γ : Type w}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
{s : Set α}
{t : Set β}
{u : α → β → γ}
{l₁ : β → γ → α}
{l₂ : α → γ → β}
(h₁ : ∀ (b : β), GaloisConnection (l₁ b) (Function.swap u b))
(h₂ : ∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ l₂ a) (u a ∘ ⇑OrderDual.ofDual))
:
sInf (Set.image2 u s t) = u (sInf s) (sSup t)
theorem
sInf_image2_eq_sSup_sInf
{α : Type u}
{β : Type v}
{γ : Type w}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
{s : Set α}
{t : Set β}
{u : α → β → γ}
{l₁ : β → γ → α}
{l₂ : α → γ → β}
(h₁ : ∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ l₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual))
(h₂ : ∀ (a : α), GaloisConnection (l₂ a) (u a))
:
sInf (Set.image2 u s t) = u (sSup s) (sInf t)
theorem
sInf_image2_eq_sSup_sSup
{α : Type u}
{β : Type v}
{γ : Type w}
[CompleteLattice α]
[CompleteLattice β]
[CompleteLattice γ]
{s : Set α}
{t : Set β}
{u : α → β → γ}
{l₁ : β → γ → α}
{l₂ : α → γ → β}
(h₁ : ∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ l₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual))
(h₂ : ∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ l₂ a) (u a ∘ ⇑OrderDual.ofDual))
:
sInf (Set.image2 u s t) = u (sSup s) (sSup t)
theorem
Nat.galoisConnection_mul_div
{k : ℕ}
(h : 0 < k)
:
GaloisConnection (fun (n : ℕ) => n * k) fun (n : ℕ) => n / k
theorem
GaloisInsertion.l_sup_u
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[SemilatticeSup α]
[SemilatticeSup β]
(gi : GaloisInsertion l u)
(a b : β)
:
theorem
GaloisInsertion.l_iSup_u
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[CompleteLattice α]
[CompleteLattice β]
(gi : GaloisInsertion l u)
{ι : Sort x}
(f : ι → β)
:
l (⨆ (i : ι), u (f i)) = ⨆ (i : ι), f i
theorem
GaloisInsertion.l_biSup_u
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[CompleteLattice α]
[CompleteLattice β]
(gi : GaloisInsertion 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
GaloisInsertion.l_sSup_u_image
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[CompleteLattice α]
[CompleteLattice β]
(gi : GaloisInsertion l u)
(s : Set β)
:
theorem
GaloisInsertion.l_inf_u
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[SemilatticeInf α]
[SemilatticeInf β]
(gi : GaloisInsertion l u)
(a b : β)
:
theorem
GaloisInsertion.l_iInf_u
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[CompleteLattice α]
[CompleteLattice β]
(gi : GaloisInsertion l u)
{ι : Sort x}
(f : ι → β)
:
l (⨅ (i : ι), u (f i)) = ⨅ (i : ι), f i
theorem
GaloisInsertion.l_biInf_u
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[CompleteLattice α]
[CompleteLattice β]
(gi : GaloisInsertion 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
GaloisInsertion.l_sInf_u_image
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[CompleteLattice α]
[CompleteLattice β]
(gi : GaloisInsertion l u)
(s : Set β)
:
theorem
GaloisInsertion.l_iInf_of_ul_eq_self
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[CompleteLattice α]
[CompleteLattice β]
(gi : GaloisInsertion l u)
{ι : Sort x}
(f : ι → α)
(hf : ∀ (i : ι), u (l (f i)) = f i)
:
l (⨅ (i : ι), f i) = ⨅ (i : ι), l (f i)
theorem
GaloisInsertion.l_biInf_of_ul_eq_self
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[CompleteLattice α]
[CompleteLattice β]
(gi : GaloisInsertion 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)
@[reducible, inline]
abbrev
GaloisInsertion.liftSemilatticeSup
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[PartialOrder β]
[SemilatticeSup α]
(gi : GaloisInsertion l u)
:
Lift the suprema along a Galois insertion
Equations
- gi.liftSemilatticeSup = SemilatticeSup.mk (fun (a b : β) => l (u a ⊔ u b)) ⋯ ⋯ ⋯
Instances For
@[reducible, inline]
abbrev
GaloisInsertion.liftSemilatticeInf
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[PartialOrder β]
[SemilatticeInf α]
(gi : GaloisInsertion l u)
:
Lift the infima along a Galois insertion
Equations
- gi.liftSemilatticeInf = SemilatticeInf.mk (fun (a b : β) => gi.choice (u a ⊓ u b) ⋯) ⋯ ⋯ ⋯
Instances For
@[reducible, inline]
abbrev
GaloisInsertion.liftLattice
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[PartialOrder β]
[Lattice α]
(gi : GaloisInsertion l u)
:
Lattice β
Lift the suprema and infima along a Galois insertion
Equations
- gi.liftLattice = Lattice.mk SemilatticeInf.inf ⋯ ⋯ ⋯
Instances For
@[reducible, inline]
abbrev
GaloisInsertion.liftOrderTop
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[PartialOrder β]
[Preorder α]
[OrderTop α]
(gi : GaloisInsertion l u)
:
OrderTop β
Lift the top along a Galois insertion
Equations
- gi.liftOrderTop = OrderTop.mk ⋯
Instances For
@[reducible, inline]
abbrev
GaloisInsertion.liftBoundedOrder
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[PartialOrder β]
[Preorder α]
[BoundedOrder α]
(gi : GaloisInsertion l u)
:
Lift the top, bottom, suprema, and infima along a Galois insertion
Equations
- gi.liftBoundedOrder = BoundedOrder.mk
Instances For
@[reducible, inline]
abbrev
GaloisInsertion.liftCompleteLattice
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[PartialOrder β]
[CompleteLattice α]
(gi : GaloisInsertion l u)
:
Lift all suprema and infima along a Galois insertion
Equations
- gi.liftCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Instances For
theorem
GaloisCoinsertion.u_inf_l
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[SemilatticeInf α]
[SemilatticeInf β]
(gi : GaloisCoinsertion l u)
(a b : α)
:
theorem
GaloisCoinsertion.u_iInf_l
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[CompleteLattice α]
[CompleteLattice β]
(gi : GaloisCoinsertion l u)
{ι : Sort x}
(f : ι → α)
:
u (⨅ (i : ι), l (f i)) = ⨅ (i : ι), f i
theorem
GaloisCoinsertion.u_sInf_l_image
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[CompleteLattice α]
[CompleteLattice β]
(gi : GaloisCoinsertion l u)
(s : Set α)
:
theorem
GaloisCoinsertion.u_sup_l
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[SemilatticeSup α]
[SemilatticeSup β]
(gi : GaloisCoinsertion l u)
(a b : α)
:
theorem
GaloisCoinsertion.u_iSup_l
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[CompleteLattice α]
[CompleteLattice β]
(gi : GaloisCoinsertion l u)
{ι : Sort x}
(f : ι → α)
:
u (⨆ (i : ι), l (f i)) = ⨆ (i : ι), f i
theorem
GaloisCoinsertion.u_biSup_l
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[CompleteLattice α]
[CompleteLattice β]
(gi : GaloisCoinsertion 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
GaloisCoinsertion.u_sSup_l_image
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[CompleteLattice α]
[CompleteLattice β]
(gi : GaloisCoinsertion l u)
(s : Set α)
:
theorem
GaloisCoinsertion.u_iSup_of_lu_eq_self
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[CompleteLattice α]
[CompleteLattice β]
(gi : GaloisCoinsertion l u)
{ι : Sort x}
(f : ι → β)
(hf : ∀ (i : ι), l (u (f i)) = f i)
:
u (⨆ (i : ι), f i) = ⨆ (i : ι), u (f i)
theorem
GaloisCoinsertion.u_biSup_of_lu_eq_self
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[CompleteLattice α]
[CompleteLattice β]
(gi : GaloisCoinsertion 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)
@[reducible, inline]
abbrev
GaloisCoinsertion.liftSemilatticeInf
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[PartialOrder α]
[SemilatticeInf β]
(gi : GaloisCoinsertion l u)
:
Lift the infima along a Galois coinsertion
Equations
- gi.liftSemilatticeInf = SemilatticeInf.mk (fun (a b : α) => u (l a ⊓ l b)) ⋯ ⋯ ⋯
Instances For
@[reducible, inline]
abbrev
GaloisCoinsertion.liftSemilatticeSup
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[PartialOrder α]
[SemilatticeSup β]
(gi : GaloisCoinsertion l u)
:
Lift the suprema along a Galois coinsertion
Equations
- gi.liftSemilatticeSup = SemilatticeSup.mk (fun (a b : α) => gi.choice (l a ⊔ l b) ⋯) ⋯ ⋯ ⋯
Instances For
@[reducible, inline]
abbrev
GaloisCoinsertion.liftLattice
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[PartialOrder α]
[Lattice β]
(gi : GaloisCoinsertion l u)
:
Lattice α
Lift the suprema and infima along a Galois coinsertion
Equations
- gi.liftLattice = Lattice.mk SemilatticeInf.inf ⋯ ⋯ ⋯
Instances For
@[reducible, inline]
abbrev
GaloisCoinsertion.liftOrderBot
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[PartialOrder α]
[Preorder β]
[OrderBot β]
(gi : GaloisCoinsertion l u)
:
OrderBot α
Lift the bot along a Galois coinsertion
Equations
- gi.liftOrderBot = OrderBot.mk ⋯
Instances For
@[reducible, inline]
abbrev
GaloisCoinsertion.liftBoundedOrder
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[PartialOrder α]
[Preorder β]
[BoundedOrder β]
(gi : GaloisCoinsertion l u)
:
Lift the top, bottom, suprema, and infima along a Galois coinsertion
Equations
- gi.liftBoundedOrder = BoundedOrder.mk
Instances For
@[reducible, inline]
abbrev
GaloisCoinsertion.liftCompleteLattice
{α : Type u}
{β : Type v}
{l : α → β}
{u : β → α}
[PartialOrder α]
[CompleteLattice β]
(gi : GaloisCoinsertion l u)
:
Lift all suprema and infima along a Galois coinsertion
Equations
- gi.liftCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Instances For
toDual ∘ Ici and sInf ∘ ofDual form a Galois coinsertion.
Equations
- gci_Ici_sInf = ⋯.toGaloisCoinsertion ⋯
Instances For
If α is a partial order with bottom element (e.g., ℕ, ℝ≥0), then WithBot.unbot' ⊥ and
coercion form a Galois insertion.
Equations
- WithBot.giUnbot'Bot = { choice := fun (o : WithBot α) (x : ↑(WithBot.unbot' ⊥ o) ≤ o) => WithBot.unbot' ⊥ o, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }