Top elements in large posets
Content created by Egbert Rijke, Fredrik Bakke and Maša Žaucer.
Created on 2023-05-12.
Last modified on 2023-06-08.
module order-theory.top-elements-large-posets where
Imports
open import foundation.universe-levels open import order-theory.dependent-products-large-posets open import order-theory.large-posets
Idea
We say that a large poset P
has a largest
element if it comes equipped with an element t : type-Large-Poset P lzero
such that x ≤ t
holds for every x : P
Definition
The predicate on elements of posets of being a top element
module _ {α : Level → Level} {β : Level → Level → Level} (P : Large-Poset α β) where is-top-element-Large-Poset : {l1 : Level} → type-Large-Poset P l1 → UUω is-top-element-Large-Poset x = {l : Level} (y : type-Large-Poset P l) → leq-Large-Poset P y x
The predicate on posets of having a top element
module _ {α : Level → Level} {β : Level → Level → Level} (P : Large-Poset α β) where record has-top-element-Large-Poset : UUω where field top-has-top-element-Large-Poset : type-Large-Poset P lzero is-top-element-top-has-top-element-Large-Poset : is-top-element-Large-Poset P top-has-top-element-Large-Poset open has-top-element-Large-Poset public
Properties
If P
is a family of large posets, then Π-Large-Poset P
has a largest element
module _ {α : Level → Level} {β : Level → Level → Level} {l1 : Level} {I : UU l1} (P : I → Large-Poset α β) where has-top-element-Π-Large-Poset : ((i : I) → has-top-element-Large-Poset (P i)) → has-top-element-Large-Poset (Π-Large-Poset P) top-has-top-element-Large-Poset ( has-top-element-Π-Large-Poset H) i = top-has-top-element-Large-Poset (H i) is-top-element-top-has-top-element-Large-Poset ( has-top-element-Π-Large-Poset H) x i = is-top-element-top-has-top-element-Large-Poset (H i) (x i)
Recent changes
- 2023-06-08. Egbert Rijke, Maša Žaucer and Fredrik Bakke. The Zariski locale of a commutative ring (#619).
- 2023-05-12. Egbert Rijke. Subframes and quotient locales via nuclei (#613).