Frames, completely distributive lattices and complete Boolean algebras #
In this file we define and provide API for (co)frames, completely distributive lattices and complete Boolean algebras.
We distinguish two different distributivity properties:
inf_iSup_eq : (a ⊓ ⨆ i, f i) = ⨆ i, a ⊓ f i
(finite⊓
distributes over infinite⨆
). This is required byFrame
,CompleteDistribLattice
, andCompleteBooleanAlgebra
(Coframe
, etc., require the dual property).iInf_iSup_eq : (⨅ i, ⨆ j, f i j) = ⨆ s, ⨅ i, f i (s i)
(infinite⨅
distributes over infinite⨆
). This stronger property is called "completely distributive", and is required byCompletelyDistribLattice
andCompleteAtomicBooleanAlgebra
.
Typeclasses #
Order.Frame
: Frame: A complete lattice whose⊓
distributes over⨆
.Order.Coframe
: Coframe: A complete lattice whose⊔
distributes over⨅
.CompleteDistribLattice
: Complete distributive lattices: A complete lattice whose⊓
and⊔
distribute over⨆
and⨅
respectively.CompleteBooleanAlgebra
: Complete Boolean algebra: A Boolean algebra whose⊓
and⊔
distribute over⨆
and⨅
respectively.CompletelyDistribLattice
: Completely distributive lattices: A complete lattice whose⨅
and⨆
satisfyiInf_iSup_eq
.CompleteBooleanAlgebra
: Complete Boolean algebra: A Boolean algebra whose⊓
and⊔
distribute over⨆
and⨅
respectively.CompleteAtomicBooleanAlgebra
: Complete atomic Boolean algebra: A complete Boolean algebra which is additionally completely distributive. (This implies that it's (co)atom(ist)ic.)
A set of opens gives rise to a topological space precisely if it forms a frame. Such a frame is also
completely distributive, but not all frames are. Filter
is a coframe but not a completely
distributive lattice.
References #
- Wikipedia, Complete Heyting algebra
- [Francis Borceux, Handbook of Categorical Algebra III][borceux-vol3]
- sup : α → α → α
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- inf : α → α → α
- sSup : Set α → α
- sInf : Set α → α
- top : α
- bot : α
In a coframe,
⊔
distributes over⨅
.
A coframe, aka complete Brouwer algebra or complete co-Heyting algebra, is a complete lattice
whose ⊔
distributes over ⨅
.
Instances
- sup : α → α → α
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- inf : α → α → α
- sSup : Set α → α
- sInf : Set α → α
- top : α
- bot : α
In a complete distributive lattice,
⊔
distributes over⨅
.
A complete distributive lattice is a complete lattice whose ⊔
and ⊓
respectively
distribute over ⨅
and ⨆
.
Instances
- sup : α → α → α
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- inf : α → α → α
- compl : α → α
- sdiff : α → α → α
- himp : α → α → α
- top : α
- bot : α
- sSup : Set α → α
Any element of a set is less than the set supremum.
Any upper bound is more than the set supremum.
- sInf : Set α → α
Any element of a set is more than the set infimum.
Any lower bound is less than the set infimum.
In a frame,
⊓
distributes over⨆
.In a complete distributive lattice,
⊔
distributes over⨅
.
A complete Boolean algebra is a Boolean algebra that is also a complete distributive lattice.
It is only completely distributive if it is also atomic.
Instances
- sup : α → α → α
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- inf : α → α → α
- sSup : Set α → α
- sInf : Set α → α
- top : α
- bot : α
The infimum distributes over the supremum
- compl : α → α
- sdiff : α → α → α
- himp : α → α → α
The infimum of
x
andxᶜ
is at most⊥
The supremum of
x
andxᶜ
is at least⊤
x \ y
is equal tox ⊓ yᶜ
x ⇨ y
is equal toy ⊔ xᶜ
In a frame,
⊓
distributes over⨆
.In a complete distributive lattice,
⊔
distributes over⨅
.
A complete atomic Boolean algebra is a complete Boolean algebra that is also completely distributive.
We take iSup_iInf_eq as the definition here, and prove later on that this implies atomicity.
Instances
Pullback an Order.Frame
along an injection.
Instances For
Pullback an Order.Coframe
along an injection.
Instances For
Pullback a CompleteDistribLattice
along an injection.
Instances For
Pullback a CompletelyDistribLattice
along an injection.
Instances For
Pullback a CompleteBooleanAlgebra
along an injection.
Instances For
Pullback a CompleteAtomicBooleanAlgebra
along an injection.