Frames, completely distributive lattices and Boolean algebras #
In this file we define and provide API for frames, completely distributive lattices and completely distributive Boolean algebras.
Typeclasses #
Order.Frame
: Frame: A complete lattice whose⊓⊓
distributes over⨆⨆
.Order.Coframe
: Coframe: A complete lattice whose⊔⊔
distributes over⨅⨅
.CompleteDistribLattice
: Completely distributive lattices: A complete lattice whose⊓⊓
and⊔⊔
distribute over⨆⨆
and⨅⨅
respectively.CompleteBooleanAlgebra
: Completely distributive Boolean algebra: A Boolean algebra whose⊓⊓
and⊔⊔
distribute over⨆⨆
and⨅⨅
respectively.
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.
TODO #
Add instances for Prod
References #
- Wikipedia, Complete Heyting algebra
- [Francis Borceux, Handbook of Categorical Algebra III][borceux-vol3]
In a coframe,
⊔⊔
distributes over⨅⨅
.
A coframe, aka complete Brouwer algebra or complete co-Heyting algebra, is a complete lattice
whose ⊔⊔
distributes over ⨅⨅
.
Instances
In a completely distributive lattice,
⊔⊔
distributes over⨅⨅
.
A completely distributive lattice is a complete lattice whose ⊔⊔
and ⊓⊓
respectively
distribute over ⨅⨅
and ⨆⨆
.
Instances
Equations
- OrderDual.coframe = let src := OrderDual.completeLattice α; Order.Coframe.mk (_ : ∀ (a : α) (s : Set α), a ⊓ supₛ s ≤ ⨆ b, ⨆ h, a ⊓ b)
Equations
- One or more equations did not get rendered due to their size.
Equations
- OrderDual.frame = let src := OrderDual.completeLattice α; Order.Frame.mk (_ : ∀ (a : α) (s : Set α), (⨅ b, ⨅ h, a ⊔ b) ≤ a ⊔ infₛ s)
Equations
- One or more equations did not get rendered due to their size.
Any upper bound is more than the set supremum.
- toInfSet : InfSet α
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 completely distributive lattice,
⊔⊔
distributes over⨅⨅
.
A complete Boolean algebra is a completely distributive Boolean algebra.
Instances
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Pullback an Order.Frame
along an injection.
Equations
- One or more equations did not get rendered due to their size.
Pullback an Order.Coframe
along an injection.
Equations
- One or more equations did not get rendered due to their size.
Pullback a CompleteDistribLattice
along an injection.
Equations
- One or more equations did not get rendered due to their size.
Pullback a CompleteBooleanAlgebra
along an injection.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.