Similarity of elements in large posets

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-11-24.

module order-theory.similarity-of-elements-large-posets where
Imports 
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.fundamental-theorem-of-identity-types
open import foundation.identity-types
open import foundation.large-binary-relations
open import foundation.propositions
open import foundation.subtypes
open import foundation.torsorial-type-families
open import foundation.universe-levels

open import order-theory.large-posets
open import order-theory.similarity-of-elements-large-preorders

Idea

Two elements x and y of a large poset P are said to be similar if both x ≤ y and y ≤ x hold. Note that the similarity relation is defined across universe levels, and that only similar elements of the same universe level are equal.

In informal writing we will use the notation x ≈ y to assert that x and y are similar elements in a poset P.

Definition

module _
  {α : Level → Level} {β : Level → Level → Level} (P : Large-Poset α β)
  where

  sim-prop-Large-Poset :
    {l1 l2 : Level}
    (x : type-Large-Poset P l1) (y : type-Large-Poset P l2) →
    Prop (β l1 l2 ⊔ β l2 l1)
  sim-prop-Large-Poset = sim-prop-Large-Preorder (large-preorder-Large-Poset P)

  sim-Large-Poset :
    {l1 l2 : Level}
    (x : type-Large-Poset P l1)
    (y : type-Large-Poset P l2) →
    UU (β l1 l2 ⊔ β l2 l1)
  sim-Large-Poset = sim-Large-Preorder (large-preorder-Large-Poset P)

  is-prop-sim-Large-Poset :
    {l1 l2 : Level}
    (x : type-Large-Poset P l1) (y : type-Large-Poset P l2) →
    is-prop (sim-Large-Poset x y)
  is-prop-sim-Large-Poset =
    is-prop-sim-Large-Preorder (large-preorder-Large-Poset P)

Properties

The similarity relation is reflexive

module _
  {α : Level → Level} {β : Level → Level → Level} (P : Large-Poset α β)
  where

  refl-sim-Large-Poset :
    is-reflexive-Large-Relation (type-Large-Poset P) (sim-Large-Poset P)
  refl-sim-Large-Poset = refl-sim-Large-Preorder (large-preorder-Large-Poset P)

The similarity relation is transitive

module _
  {α : Level → Level} {β : Level → Level → Level} (P : Large-Poset α β)
  where

  transitive-sim-Large-Poset :
    is-transitive-Large-Relation (type-Large-Poset P) (sim-Large-Poset P)
  transitive-sim-Large-Poset =
    transitive-sim-Large-Preorder (large-preorder-Large-Poset P)

The similarity relation is symmetric

module _
  {α : Level → Level} {β : Level → Level → Level} (P : Large-Poset α β)
  where

  symmetric-sim-Large-Poset :
    is-symmetric-Large-Relation (type-Large-Poset P) (sim-Large-Poset P)
  symmetric-sim-Large-Poset =
    symmetric-sim-Large-Preorder (large-preorder-Large-Poset P)

For any universe level l, any element x is similar to at most one element of universe level l

module _
  {α : Level → Level} {β : Level → Level → Level} (P : Large-Poset α β)
  where

  all-elements-equal-total-sim-Large-Poset :
    {l1 l2 : Level} (x : type-Large-Poset P l1) →
    all-elements-equal (Σ (type-Large-Poset P l2) (sim-Large-Poset P x))
  all-elements-equal-total-sim-Large-Poset x (y , H) (z , K) =
    eq-type-subtype
      ( sim-prop-Large-Poset P x)
      ( antisymmetric-leq-Large-Poset P
        ( y)
        ( z)
        ( transitive-leq-Large-Poset P _ _ _ (pr1 K) (pr2 H))
        ( transitive-leq-Large-Poset P _ _ _ (pr1 H) (pr2 K)))

  is-prop-total-sim-Large-Poset :
    {l1 l2 : Level} (x : type-Large-Poset P l1) →
    is-prop (Σ (type-Large-Poset P l2) (sim-Large-Poset P x))
  is-prop-total-sim-Large-Poset x =
    is-prop-all-elements-equal
      ( all-elements-equal-total-sim-Large-Poset x)

  is-torsorial-sim-Large-Poset :
    {l1 : Level} (x : type-Large-Poset P l1) →
    is-torsorial (sim-Large-Poset P x)
  is-torsorial-sim-Large-Poset x =
    is-proof-irrelevant-is-prop
      ( is-prop-total-sim-Large-Poset x)
      ( x , refl-sim-Large-Poset P x)

Similarity characterizes the identity type of elements in a large poset of the same universe level

module _
  {α : Level → Level} {β : Level → Level → Level} (P : Large-Poset α β)
  where

  sim-eq-Large-Poset :
    {l1 : Level} {x y : type-Large-Poset P l1} →
    x ＝ y → sim-Large-Poset P x y
  sim-eq-Large-Poset refl = refl-sim-Large-Poset P _

  is-equiv-sim-eq-Large-Poset :
    {l1 : Level} (x y : type-Large-Poset P l1) →
    is-equiv (sim-eq-Large-Poset {l1} {x} {y})
  is-equiv-sim-eq-Large-Poset x =
    fundamental-theorem-id
      ( is-torsorial-sim-Large-Poset P x)
      ( λ y → sim-eq-Large-Poset {_} {x} {y})

  extensionality-Large-Poset :
    {l1 : Level} (x y : type-Large-Poset P l1) →
    (x ＝ y) ≃ sim-Large-Poset P x y
  pr1 (extensionality-Large-Poset x y) = sim-eq-Large-Poset
  pr2 (extensionality-Large-Poset x y) = is-equiv-sim-eq-Large-Poset x y

  eq-sim-Large-Poset :
    {l1 : Level} (x y : type-Large-Poset P l1) →
    sim-Large-Poset P x y → x ＝ y
  eq-sim-Large-Poset x y = map-inv-is-equiv (is-equiv-sim-eq-Large-Poset x y)

Recent changes