Similarity of elements in large preorders
Content created by Egbert Rijke, Fredrik Bakke, Julian KG, Maša Žaucer, fernabnor, Gregor Perčič and louismntnu.
Created on 2023-06-08.
Last modified on 2023-09-21.
module order-theory.similarity-of-elements-large-preorders where
Imports
open import foundation.dependent-pair-types open import foundation.large-binary-relations open import foundation.propositions open import foundation.universe-levels open import order-theory.large-preorders
Idea
Two elements x
and y
of a large preorder
P
are said to be similar if both x ≤ y
and y ≤ x
hold.
Definition
module _ {α : Level → Level} {β : Level → Level → Level} (P : Large-Preorder α β) where sim-prop-Large-Preorder : {l1 l2 : Level} (x : type-Large-Preorder P l1) (y : type-Large-Preorder P l2) → Prop (β l1 l2 ⊔ β l2 l1) sim-prop-Large-Preorder x y = prod-Prop ( leq-prop-Large-Preorder P x y) ( leq-prop-Large-Preorder P y x) sim-Large-Preorder : {l1 l2 : Level} (x : type-Large-Preorder P l1) (y : type-Large-Preorder P l2) → UU (β l1 l2 ⊔ β l2 l1) sim-Large-Preorder x y = type-Prop (sim-prop-Large-Preorder x y) is-prop-sim-Large-Preorder : {l1 l2 : Level} (x : type-Large-Preorder P l1) (y : type-Large-Preorder P l2) → is-prop (sim-Large-Preorder x y) is-prop-sim-Large-Preorder x y = is-prop-type-Prop (sim-prop-Large-Preorder x y)
Properties
The similarity relation is reflexive
module _ {α : Level → Level} {β : Level → Level → Level} (P : Large-Preorder α β) where refl-sim-Large-Preorder : is-reflexive-Large-Relation (type-Large-Preorder P) (sim-Large-Preorder P) pr1 (refl-sim-Large-Preorder x) = refl-leq-Large-Preorder P x pr2 (refl-sim-Large-Preorder x) = refl-leq-Large-Preorder P x
The similarity relation is transitive
module _ {α : Level → Level} {β : Level → Level → Level} (P : Large-Preorder α β) where transitive-sim-Large-Preorder : is-transitive-Large-Relation (type-Large-Preorder P) (sim-Large-Preorder P) pr1 (transitive-sim-Large-Preorder x y z H K) = transitive-leq-Large-Preorder P x y z (pr1 H) (pr1 K) pr2 (transitive-sim-Large-Preorder x y z H K) = transitive-leq-Large-Preorder P z y x (pr2 K) (pr2 H)
The similarity relation is symmetric
module _ {α : Level → Level} {β : Level → Level → Level} (P : Large-Preorder α β) where symmetric-sim-Large-Preorder : is-symmetric-Large-Relation (type-Large-Preorder P) (sim-Large-Preorder P) pr1 (symmetric-sim-Large-Preorder _ _ H) = pr2 H pr2 (symmetric-sim-Large-Preorder _ _ H) = pr1 H
Recent changes
- 2023-09-21. Egbert Rijke and Gregor Perčič. The classification of cyclic rings (#757).
- 2023-06-25. Fredrik Bakke, louismntnu, fernabnor, Egbert Rijke and Julian KG. Posets are categories, and refactor binary relations (#665).
- 2023-06-08. Egbert Rijke, Maša Žaucer and Fredrik Bakke. The Zariski locale of a commutative ring (#619).