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 #
Structure containing the minimal axioms required to check that an order is a frame. Do NOT use,
except for implementing Order.Frame
via Order.Frame.ofMinimalAxioms
.
This structure omits the himp
, compl
fields, which can be recovered using
Order.Frame.ofMinimalAxioms
.
Instances
Structure containing the minimal axioms required to check that an order is a coframe. Do NOT
use, except for implementing Order.Coframe
via Order.Coframe.ofMinimalAxioms
.
This structure omits the sdiff
, hnot
fields, which can be recovered using
Order.Coframe.ofMinimalAxioms
.
Instances
A frame, aka complete Heyting algebra, is a complete lattice whose ⊓
distributes over ⨆
.
Instances
⊓
distributes over ⨆
.
A coframe, aka complete Brouwer algebra or complete co-Heyting algebra, is a complete lattice
whose ⊔
distributes over ⨅
.
Instances
⊔
distributes over ⨅
.
Structure containing the minimal axioms required to check that an order is a complete
distributive lattice. Do NOT use, except for implementing CompleteDistribLattice
via
CompleteDistribLattice.ofMinimalAxioms
.
This structure omits the himp
, compl
, sdiff
, hnot
fields, which can be recovered using
CompleteDistribLattice.ofMinimalAxioms
.
Instances For
A complete distributive lattice is a complete lattice whose ⊔
and ⊓
respectively
distribute over ⨅
and ⨆
.
Instances
In a complete distributive lattice, ⊔
distributes over ⨅
.
Structure containing the minimal axioms required to check that an order is a completely
distributive. Do NOT use, except for implementing CompletelyDistribLattice
via
CompletelyDistribLattice.ofMinimalAxioms
.
This structure omits the himp
, compl
, sdiff
, hnot
fields, which can be recovered using
CompletelyDistribLattice.ofMinimalAxioms
.
Instances For
A completely distributive lattice is a complete lattice whose ⨅
and ⨆
distribute over each other.
Instances
The Order.Frame.MinimalAxioms
element corresponding to a frame.
Equations
- Order.Frame.MinimalAxioms.of = Order.Frame.MinimalAxioms.mk ⋯
Instances For
Construct a frame instance using the minimal amount of work needed.
This sets a ⇨ b := sSup {c | c ⊓ a ≤ b}
and aᶜ := a ⇨ ⊥
.
Equations
- Order.Frame.ofMinimalAxioms minAx = Order.Frame.mk ⋯ ⋯ ⋯
Instances For
The Order.Coframe.MinimalAxioms
element corresponding to a frame.
Equations
- Order.Coframe.MinimalAxioms.of = Order.Coframe.MinimalAxioms.mk ⋯
Instances For
Construct a coframe instance using the minimal amount of work needed.
This sets a \ b := sInf {c | a ≤ b ⊔ c}
and ¬a := ⊤ \ a
.
Equations
- Order.Coframe.ofMinimalAxioms minAx = Order.Coframe.mk ⋯ ⋯ ⋯
Instances For
The CompleteDistribLattice.MinimalAxioms
element corresponding to a complete distrib lattice.
Equations
- CompleteDistribLattice.MinimalAxioms.of = { toCompleteLattice := Order.Frame.toCompleteLattice, inf_sSup_le_iSup_inf := ⋯, iInf_sup_le_sup_sInf := ⋯ }
Instances For
Turn minimal axioms for CompleteDistribLattice
into minimal axioms for Order.Frame
.
Equations
- minAx.toFrame = minAx.toMinimalAxioms
Instances For
Turn minimal axioms for CompleteDistribLattice
into minimal axioms for Order.Coframe
.
Equations
- minAx.toCoframe = Order.Coframe.MinimalAxioms.mk ⋯
Instances For
Construct a complete distrib lattice instance using the minimal amount of work needed.
This sets a ⇨ b := sSup {c | c ⊓ a ≤ b}
, aᶜ := a ⇨ ⊥
, a \ b := sInf {c | a ≤ b ⊔ c}
and
¬a := ⊤ \ a
.
Equations
Instances For
Turn minimal axioms for CompletelyDistribLattice
into minimal axioms for
CompleteDistribLattice
.
Equations
- minAx.toCompleteDistribLattice = { toCompleteLattice := minAx.toCompleteLattice, inf_sSup_le_iSup_inf := ⋯, iInf_sup_le_sup_sInf := ⋯ }
Instances For
The CompletelyDistribLattice.MinimalAxioms
element corresponding to a frame.
Equations
- CompletelyDistribLattice.MinimalAxioms.of = { toCompleteLattice := CompletelyDistribLattice.toCompleteLattice, iInf_iSup_eq := ⋯ }
Instances For
Construct a completely distributive lattice instance using the minimal amount of work needed.
This sets a ⇨ b := sSup {c | c ⊓ a ≤ b}
, aᶜ := a ⇨ ⊥
, a \ b := sInf {c | a ≤ b ⊔ c}
and
¬a := ⊤ \ a
.
Equations
- CompletelyDistribLattice.ofMinimalAxioms minAx = CompletelyDistribLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯
Instances For
Equations
- CompletelyDistribLattice.toCompleteDistribLattice = CompleteDistribLattice.mk ⋯ ⋯ ⋯
Equations
- CompleteLinearOrder.toCompletelyDistribLattice = CompletelyDistribLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- OrderDual.instCoframe = Order.Coframe.mk ⋯ ⋯ ⋯
Equations
- Frame.toDistribLattice = DistribLattice.ofInfSupLe ⋯
Equations
- Prod.instFrame = Order.Frame.mk ⋯ ⋯ ⋯
Equations
- Pi.instFrame = Order.Frame.mk ⋯ ⋯ ⋯
Equations
- OrderDual.instFrame = Order.Frame.mk ⋯ ⋯ ⋯
Equations
- Coframe.toDistribLattice = DistribLattice.mk ⋯
Equations
- Prod.instCoframe = Order.Coframe.mk ⋯ ⋯ ⋯
Equations
- Pi.instCoframe = Order.Coframe.mk ⋯ ⋯ ⋯
Equations
- OrderDual.instCompleteDistribLattice = CompleteDistribLattice.mk ⋯ ⋯ ⋯
Equations
- Prod.instCompleteDistribLattice = CompleteDistribLattice.mk ⋯ ⋯ ⋯
Equations
- Pi.instCompleteDistribLattice = CompleteDistribLattice.mk ⋯ ⋯ ⋯
Equations
- OrderDual.instCompletelyDistribLattice = CompletelyDistribLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- Prod.instCompletelyDistribLattice = CompletelyDistribLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- Pi.instCompletelyDistribLattice = CompletelyDistribLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯
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
⊓
distributes over ⨆
.
⊔
distributes over ⨅
.
Equations
- CompleteBooleanAlgebra.toCompleteDistribLattice = CompleteDistribLattice.mk ⋯ ⋯ ⋯
Equations
- Prod.instCompleteBooleanAlgebra = CompleteBooleanAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- Pi.instCompleteBooleanAlgebra = CompleteBooleanAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- OrderDual.instCompleteBooleanAlgebra = CompleteBooleanAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
The symmetric difference of two iSup
s is at most the iSup
of the symmetric differences.
A biSup
version of iSup_symmDiff_iSup_le
.
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
Equations
- CompleteAtomicBooleanAlgebra.toCompletelyDistribLattice = CompletelyDistribLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra = CompleteBooleanAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- Prod.instCompleteAtomicBooleanAlgebra = CompleteAtomicBooleanAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- Pi.instCompleteAtomicBooleanAlgebra = CompleteAtomicBooleanAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- OrderDual.instCompleteAtomicBooleanAlgebra = CompleteAtomicBooleanAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- «Prop».instCompleteBooleanAlgebra = inferInstance
Pullback an Order.Frame.MinimalAxioms
along an injection.
Equations
- Function.Injective.frameMinimalAxioms minAx f hf map_sup map_inf map_sSup map_sInf map_top map_bot = Order.Frame.MinimalAxioms.mk ⋯
Instances For
Pullback an Order.Coframe.MinimalAxioms
along an injection.
Equations
- Function.Injective.coframeMinimalAxioms minAx f hf map_sup map_inf map_sSup map_sInf map_top map_bot = Order.Coframe.MinimalAxioms.mk ⋯
Instances For
Pullback an Order.Frame
along an injection.
Equations
- Function.Injective.frame f hf map_sup map_inf map_sSup map_sInf map_top map_bot map_compl map_himp = Order.Frame.mk ⋯ ⋯ ⋯
Instances For
Pullback an Order.Coframe
along an injection.
Equations
- Function.Injective.coframe f hf map_sup map_inf map_sSup map_sInf map_top map_bot map_hnot map_sdiff = Order.Coframe.mk ⋯ ⋯ ⋯
Instances For
Pullback a CompleteDistribLattice.MinimalAxioms
along an injection.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pullback a CompleteDistribLattice
along an injection.
Equations
- Function.Injective.completeDistribLattice f hf map_sup map_inf map_sSup map_sInf map_top map_bot map_compl map_himp map_hnot map_sdiff = CompleteDistribLattice.mk ⋯ ⋯ ⋯
Instances For
Pullback a CompletelyDistribLattice.MinimalAxioms
along an injection.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pullback a CompletelyDistribLattice
along an injection.
Equations
- Function.Injective.completelyDistribLattice f hf map_sup map_inf map_sSup map_sInf map_top map_bot map_compl map_himp map_hnot map_sdiff = CompletelyDistribLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯
Instances For
Pullback a CompleteBooleanAlgebra
along an injection.
Equations
- Function.Injective.completeBooleanAlgebra f hf map_sup map_inf map_sSup map_sInf map_top map_bot map_compl map_himp map_sdiff = CompleteBooleanAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Instances For
Pullback a CompleteAtomicBooleanAlgebra
along an injection.
Equations
- Function.Injective.completeAtomicBooleanAlgebra f hf map_sup map_inf map_sSup map_sInf map_top map_bot map_compl map_himp map_hnot map_sdiff = CompleteAtomicBooleanAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Instances For
Equations
- PUnit.instCompleteBooleanAlgebra = inferInstance