Complemented inequality on cardinals

Content created by Fredrik Bakke.

Created on 2026-01-10.
Last modified on 2026-01-10.

module set-theory.complemented-inequality-cardinals where

Imports

open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.identity-types
open import foundation.large-binary-relations
open import foundation.mere-decidable-embeddings
open import foundation.propositional-extensionality
open import foundation.propositions
open import foundation.set-truncations
open import foundation.sets
open import foundation.univalence
open import foundation.universe-levels
open import foundation.weak-limited-principle-of-omniscience

open import order-theory.large-posets
open import order-theory.large-preorders

open import set-theory.cardinals
open import set-theory.equality-cardinals

Idea

We may say a cardinal X is (complemented) less than or equal to^¶ a cardinal Y if any set in the isomorphism class of X embeds as a decidable subtype into any set in the isomorphism class of Y. In other words, if there is a decidable embedding from the first to the second. This defines the complemented ordering^¶ on cardinals.

Under the assumption of the weak limited principle of omniscience this relation is antisymmetric and hence defines a partial order on cardinals due to the Cantor–Schröder–Bernstein theorem for decidable embeddings.

Terminology. The term “complemented” as it is used here is borrowed from topology. A subspace X of a space Y is complemented if it is closed and there is another closed subspace X̅ of Y such that X ∩ X̅ = ∅ and X ∪ X̅ = Y. Analogously, a cardinal X is complemented less than a cardinal Y if there is such a decomposition of any set in the isomorphism class of X identified as a subset of any set in the isomorphism class of Y.

Definition

Complemented boundedness of the cardinality of a set

module _
  {l1 l2 : Level} (X : Set l1)
  where

  leq-complemented-prop-Cardinal' : Cardinal l2 → Prop (l1 ⊔ l2)
  leq-complemented-prop-Cardinal' =
    map-universal-property-trunc-Set
      ( Prop-Set (l1 ⊔ l2))
      ( λ Y' → mere-decidable-emb-Prop (type-Set X) (type-Set Y'))

  compute-leq-complemented-prop-Cardinal' :
    (Y : Set l2) →
    leq-complemented-prop-Cardinal' (cardinality Y) ＝
    mere-decidable-emb-Prop (type-Set X) (type-Set Y)
  compute-leq-complemented-prop-Cardinal' =
    triangle-universal-property-trunc-Set
      ( Prop-Set (l1 ⊔ l2))
      ( λ Y' → mere-decidable-emb-Prop (type-Set X) (type-Set Y'))

Complemented inequality of cardinals

module _
  {l1 l2 : Level}
  where

  leq-complemented-prop-Cardinal :
    Cardinal l1 → Cardinal l2 → Prop (l1 ⊔ l2)
  leq-complemented-prop-Cardinal =
    map-universal-property-trunc-Set
      ( hom-set-Set (Cardinal-Set l2) (Prop-Set (l1 ⊔ l2)))
      ( leq-complemented-prop-Cardinal')

  leq-complemented-Cardinal :
    Cardinal l1 → Cardinal l2 → UU (l1 ⊔ l2)
  leq-complemented-Cardinal X Y =
    type-Prop (leq-complemented-prop-Cardinal X Y)

  is-prop-leq-complemented-Cardinal :
    {X : Cardinal l1} {Y : Cardinal l2} →
    is-prop (leq-complemented-Cardinal X Y)
  is-prop-leq-complemented-Cardinal {X} {Y} =
    is-prop-type-Prop (leq-complemented-prop-Cardinal X Y)

Complemented inequality of cardinalities

module _
  {l1 l2 : Level} (X : Set l1) (Y : Set l2)
  where

  leq-complemented-prop-cardinality : Prop (l1 ⊔ l2)
  leq-complemented-prop-cardinality =
    leq-complemented-prop-Cardinal (cardinality X) (cardinality Y)

  leq-complemented-cardinality : UU (l1 ⊔ l2)
  leq-complemented-cardinality =
    leq-complemented-Cardinal (cardinality X) (cardinality Y)

  is-prop-leq-complemented-cardinality :
    is-prop leq-complemented-cardinality
  is-prop-leq-complemented-cardinality =
    is-prop-leq-complemented-Cardinal

  compute-leq-complemented-prop-cardinality' :
    leq-complemented-prop-cardinality ＝
    mere-decidable-emb-Prop (type-Set X) (type-Set Y)
  compute-leq-complemented-prop-cardinality' =
    ( htpy-eq
      ( triangle-universal-property-trunc-Set
        ( hom-set-Set (Cardinal-Set l2) (Prop-Set (l1 ⊔ l2)))
        ( leq-complemented-prop-Cardinal') X) (cardinality Y)) ∙
    ( compute-leq-complemented-prop-Cardinal' X Y)

  compute-leq-complemented-cardinality' :
    leq-complemented-cardinality ＝
    mere-decidable-emb (type-Set X) (type-Set Y)
  compute-leq-complemented-cardinality' =
    ap type-Prop compute-leq-complemented-prop-cardinality'

  compute-leq-complemented-cardinality :
    leq-complemented-cardinality ≃
    mere-decidable-emb (type-Set X) (type-Set Y)
  compute-leq-complemented-cardinality =
    equiv-eq compute-leq-complemented-cardinality'

  unit-leq-complemented-cardinality :
    mere-decidable-emb (type-Set X) (type-Set Y) →
    leq-complemented-cardinality
  unit-leq-complemented-cardinality =
    map-inv-equiv compute-leq-complemented-cardinality

  inv-unit-leq-complemented-cardinality :
    leq-complemented-cardinality →
    mere-decidable-emb (type-Set X) (type-Set Y)
  inv-unit-leq-complemented-cardinality =
    pr1 compute-leq-complemented-cardinality