Isolated elements

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-10-09.
Last modified on 2024-04-11.

module foundation.isolated-elements where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.constant-maps
open import foundation.decidable-embeddings
open import foundation.decidable-equality
open import foundation.decidable-maps
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.fundamental-theorem-of-identity-types
open import foundation.identity-types
open import foundation.injective-maps
open import foundation.maybe
open import foundation.negated-equality
open import foundation.negation
open import foundation.sets
open import foundation.type-arithmetic-unit-type
open import foundation.unit-type
open import foundation.universe-levels

open import foundation-core.contractible-types
open import foundation-core.coproduct-types
open import foundation-core.decidable-propositions
open import foundation-core.empty-types
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.homotopies
open import foundation-core.propositions
open import foundation-core.subtypes
open import foundation-core.torsorial-type-families
open import foundation-core.transport-along-identifications

Idea

An element a : A is considered to be isolated if a ＝ x is decidable for any x.

Definitions

Isolated elements

is-isolated :
  {l1 : Level} {X : UU l1} (a : X) → UU l1
is-isolated {l1} {X} a = (x : X) → is-decidable (a ＝ x)

isolated-element :
  {l1 : Level} (X : UU l1) → UU l1
isolated-element X = Σ X is-isolated

module _
  {l : Level} {X : UU l} (x : isolated-element X)
  where

  element-isolated-element : X
  element-isolated-element = pr1 x

  is-isolated-isolated-element : is-isolated element-isolated-element
  is-isolated-isolated-element = pr2 x

Complements of isolated elements

complement-isolated-element :
  {l1 : Level} (X : UU l1) → isolated-element X → UU l1
complement-isolated-element X x =
  Σ X (λ y → element-isolated-element x ≠ y)

Properties

An element is isolated if and only if the constant map pointing at it is decidable

module _
  {l1 : Level} {A : UU l1} (a : A)
  where

  is-decidable-point-is-isolated :
    is-isolated a → is-decidable-map (point a)
  is-decidable-point-is-isolated d x =
    is-decidable-equiv (compute-fiber-point a x) (d x)

  is-isolated-is-decidable-point :
    is-decidable-map (point a) → is-isolated a
  is-isolated-is-decidable-point d x =
    is-decidable-equiv' (compute-fiber-point a x) (d x)

  cases-Eq-isolated-element :
    is-isolated a → (x : A) → is-decidable (a ＝ x) → UU lzero
  cases-Eq-isolated-element H x (inl p) = unit
  cases-Eq-isolated-element H x (inr f) = empty

  abstract
    is-prop-cases-Eq-isolated-element :
      (d : is-isolated a) (x : A) (dx : is-decidable (a ＝ x)) →
      is-prop (cases-Eq-isolated-element d x dx)
    is-prop-cases-Eq-isolated-element d x (inl p) = is-prop-unit
    is-prop-cases-Eq-isolated-element d x (inr f) = is-prop-empty

  Eq-isolated-element : is-isolated a → A → UU lzero
  Eq-isolated-element d x = cases-Eq-isolated-element d x (d x)

  abstract
    is-prop-Eq-isolated-element :
      (d : is-isolated a) (x : A) → is-prop (Eq-isolated-element d x)
    is-prop-Eq-isolated-element d x =
      is-prop-cases-Eq-isolated-element d x (d x)

  Eq-isolated-element-Prop : is-isolated a → A → Prop lzero
  pr1 (Eq-isolated-element-Prop d x) = Eq-isolated-element d x
  pr2 (Eq-isolated-element-Prop d x) = is-prop-Eq-isolated-element d x

  decide-reflexivity :
    (d : is-decidable (a ＝ a)) → Σ (a ＝ a) (λ p → inl p ＝ d)
  pr1 (decide-reflexivity (inl p)) = p
  pr2 (decide-reflexivity (inl p)) = refl
  decide-reflexivity (inr f) = ex-falso (f refl)

  abstract
    refl-Eq-isolated-element : (d : is-isolated a) → Eq-isolated-element d a
    refl-Eq-isolated-element d =
      tr
        ( cases-Eq-isolated-element d a)
        ( pr2 (decide-reflexivity (d a)))
        ( star)

  abstract
    Eq-eq-isolated-element :
      (d : is-isolated a) {x : A} → a ＝ x → Eq-isolated-element d x
    Eq-eq-isolated-element d refl = refl-Eq-isolated-element d

  abstract
    center-total-Eq-isolated-element :
      (d : is-isolated a) → Σ A (Eq-isolated-element d)
    pr1 (center-total-Eq-isolated-element d) = a
    pr2 (center-total-Eq-isolated-element d) = refl-Eq-isolated-element d

    cases-contraction-total-Eq-isolated-element :
      (d : is-isolated a) (x : A) (dx : is-decidable (a ＝ x))
      (e : cases-Eq-isolated-element d x dx) → a ＝ x
    cases-contraction-total-Eq-isolated-element d x (inl p) e = p

    contraction-total-Eq-isolated-element :
      (d : is-isolated a) (t : Σ A (Eq-isolated-element d)) →
      center-total-Eq-isolated-element d ＝ t
    contraction-total-Eq-isolated-element d (x , e) =
      eq-type-subtype
        ( Eq-isolated-element-Prop d)
        ( cases-contraction-total-Eq-isolated-element d x (d x) e)

    is-torsorial-Eq-isolated-element :
      (d : is-isolated a) → is-torsorial (Eq-isolated-element d)
    pr1 (is-torsorial-Eq-isolated-element d) =
      center-total-Eq-isolated-element d
    pr2 (is-torsorial-Eq-isolated-element d) =
      contraction-total-Eq-isolated-element d

  abstract
    is-equiv-Eq-eq-isolated-element :
      (d : is-isolated a) (x : A) → is-equiv (Eq-eq-isolated-element d {x})
    is-equiv-Eq-eq-isolated-element d =
      fundamental-theorem-id
        ( is-torsorial-Eq-isolated-element d)
        ( λ x → Eq-eq-isolated-element d {x})

  abstract
    equiv-Eq-eq-isolated-element :
      (d : is-isolated a) (x : A) → (a ＝ x) ≃ Eq-isolated-element d x
    pr1 (equiv-Eq-eq-isolated-element d x) = Eq-eq-isolated-element d
    pr2 (equiv-Eq-eq-isolated-element d x) = is-equiv-Eq-eq-isolated-element d x

  abstract
    is-prop-eq-isolated-element : (d : is-isolated a) (x : A) → is-prop (a ＝ x)
    is-prop-eq-isolated-element d x =
      is-prop-equiv
        ( equiv-Eq-eq-isolated-element d x)
        ( is-prop-Eq-isolated-element d x)

  is-contr-loop-space-isolated-element :
    (d : is-isolated a) → is-contr (a ＝ a)
  is-contr-loop-space-isolated-element d =
    is-proof-irrelevant-is-prop (is-prop-eq-isolated-element d a) refl

  abstract
    is-emb-point-is-isolated : is-isolated a → is-emb (point a)
    is-emb-point-is-isolated d star =
      fundamental-theorem-id
        ( is-contr-equiv
          ( a ＝ a)
          ( left-unit-law-product)
          ( is-proof-irrelevant-is-prop
            ( is-prop-eq-isolated-element d a)
            ( refl)))
        ( λ x → ap (λ y → a))

Being an isolated element is a property

is-prop-is-isolated :
  {l1 : Level} {A : UU l1} (a : A) → is-prop (is-isolated a)
is-prop-is-isolated a =
  is-prop-has-element
    ( λ H → is-prop-Π (is-prop-is-decidable ∘ is-prop-eq-isolated-element a H))

is-isolated-Prop :
  {l1 : Level} {A : UU l1} (a : A) → Prop l1
pr1 (is-isolated-Prop a) = is-isolated a
pr2 (is-isolated-Prop a) = is-prop-is-isolated a

inclusion-isolated-element :
  {l1 : Level} (A : UU l1) → isolated-element A → A
inclusion-isolated-element A = pr1

is-emb-inclusion-isolated-element :
  {l1 : Level} (A : UU l1) → is-emb (inclusion-isolated-element A)
is-emb-inclusion-isolated-element A = is-emb-inclusion-subtype is-isolated-Prop

has-decidable-equality-isolated-element :
  {l1 : Level} (A : UU l1) → has-decidable-equality (isolated-element A)
has-decidable-equality-isolated-element A (x , dx) (y , dy) =
  is-decidable-equiv
    ( equiv-ap-inclusion-subtype is-isolated-Prop)
    ( dx y)

is-set-isolated-element :
  {l1 : Level} (A : UU l1) → is-set (isolated-element A)
is-set-isolated-element A =
  is-set-has-decidable-equality (has-decidable-equality-isolated-element A)

module _
  {l1 : Level} {A : UU l1} (a : isolated-element A)
  where

  point-isolated-element : unit → A
  point-isolated-element = point (element-isolated-element a)

  is-emb-point-isolated-element : is-emb point-isolated-element
  is-emb-point-isolated-element =
    is-emb-comp
      ( inclusion-isolated-element A)
      ( point a)
      ( is-emb-inclusion-isolated-element A)
      ( is-emb-is-injective
        ( is-set-isolated-element A)
        ( λ p → refl))

  emb-point-isolated-element : unit ↪ A
  pr1 emb-point-isolated-element = point-isolated-element
  pr2 emb-point-isolated-element = is-emb-point-isolated-element

  is-decidable-point-isolated-element :
    is-decidable-map point-isolated-element
  is-decidable-point-isolated-element x =
    is-decidable-product is-decidable-unit (is-isolated-isolated-element a x)

  is-decidable-emb-point-isolated-element :
    is-decidable-emb point-isolated-element
  pr1 is-decidable-emb-point-isolated-element =
    is-emb-point-isolated-element
  pr2 is-decidable-emb-point-isolated-element =
    is-decidable-point-isolated-element

  decidable-emb-point-isolated-element : unit ↪ᵈ A
  pr1 decidable-emb-point-isolated-element =
    point-isolated-element
  pr2 decidable-emb-point-isolated-element =
    is-decidable-emb-point-isolated-element

Types with isolated elements can be equipped with a Maybe-structure

map-maybe-structure-isolated-element :
  {l1 : Level} (X : UU l1) (x : isolated-element X) →
  Maybe (complement-isolated-element X x) → X
map-maybe-structure-isolated-element X (x , d) (inl (y , f)) = y
map-maybe-structure-isolated-element X (x , d) (inr star) = x

cases-map-inv-maybe-structure-isolated-element :
  {l1 : Level} (X : UU l1) (x : isolated-element X) →
  (y : X) → is-decidable (pr1 x ＝ y) → Maybe (complement-isolated-element X x)
cases-map-inv-maybe-structure-isolated-element X (x , dx) y (inl p) =
  inr star
cases-map-inv-maybe-structure-isolated-element X (x , dx) y (inr f) =
  inl (y , f)

map-inv-maybe-structure-isolated-element :
  {l1 : Level} (X : UU l1) (x : isolated-element X) →
  X → Maybe (complement-isolated-element X x)
map-inv-maybe-structure-isolated-element X (x , d) y =
  cases-map-inv-maybe-structure-isolated-element X (x , d) y (d y)

cases-is-section-map-inv-maybe-structure-isolated-element :
  {l1 : Level} (X : UU l1) (x : isolated-element X) →
  (y : X) (d : is-decidable (pr1 x ＝ y)) →
  ( map-maybe-structure-isolated-element X x
    ( cases-map-inv-maybe-structure-isolated-element X x y d)) ＝
  ( y)
cases-is-section-map-inv-maybe-structure-isolated-element X
  (x , dx) .x (inl refl) =
  refl
cases-is-section-map-inv-maybe-structure-isolated-element X (x , dx) y (inr f) =
  refl

is-section-map-inv-maybe-structure-isolated-element :
  {l1 : Level} (X : UU l1) (x : isolated-element X) →
  ( map-maybe-structure-isolated-element X x ∘
    map-inv-maybe-structure-isolated-element X x) ~ id
is-section-map-inv-maybe-structure-isolated-element X (x , d) y =
  cases-is-section-map-inv-maybe-structure-isolated-element X (x , d) y (d y)

is-retraction-map-inv-maybe-structure-isolated-element :
  {l1 : Level} (X : UU l1) (x : isolated-element X) →
  ( map-inv-maybe-structure-isolated-element X x ∘
    map-maybe-structure-isolated-element X x) ~ id
is-retraction-map-inv-maybe-structure-isolated-element
  X (x , dx) (inl (y , f)) =
  ap
    ( cases-map-inv-maybe-structure-isolated-element X (x , dx) y)
    ( eq-is-prop (is-prop-is-decidable (is-prop-eq-isolated-element x dx y)))
is-retraction-map-inv-maybe-structure-isolated-element X (x , dx) (inr star) =
  ap
    ( cases-map-inv-maybe-structure-isolated-element X (x , dx) x)
    { x = dx (map-maybe-structure-isolated-element X (x , dx) (inr star))}
    { y = inl refl}
    ( eq-is-prop (is-prop-is-decidable (is-prop-eq-isolated-element x dx x)))

is-equiv-map-maybe-structure-isolated-element :
  {l1 : Level} (X : UU l1) (x : isolated-element X) →
  is-equiv (map-maybe-structure-isolated-element X x)
is-equiv-map-maybe-structure-isolated-element X x =
  is-equiv-is-invertible
    ( map-inv-maybe-structure-isolated-element X x)
    ( is-section-map-inv-maybe-structure-isolated-element X x)
    ( is-retraction-map-inv-maybe-structure-isolated-element X x)

equiv-maybe-structure-isolated-element :
  {l1 : Level} (X : UU l1) (x : isolated-element X) →
  Maybe (complement-isolated-element X x) ≃ X
pr1 (equiv-maybe-structure-isolated-element X x) =
  map-maybe-structure-isolated-element X x
pr2 (equiv-maybe-structure-isolated-element X x) =
  is-equiv-map-maybe-structure-isolated-element X x

maybe-structure-isolated-element :
  {l1 : Level} {X : UU l1} → isolated-element X → maybe-structure X
pr1 (maybe-structure-isolated-element {l1} {X} x) =
  complement-isolated-element X x
pr2 (maybe-structure-isolated-element {l1} {X} x) =
  equiv-maybe-structure-isolated-element X x

equiv-complement-isolated-element :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : X ≃ Y) (x : isolated-element X)
  (y : isolated-element Y) (p : map-equiv e (pr1 x) ＝ pr1 y) →
  complement-isolated-element X x ≃ complement-isolated-element Y y
equiv-complement-isolated-element e x y p =
  equiv-Σ
    ( λ z → pr1 y ≠ z)
    ( e)
    ( λ z →
      equiv-neg
        ( equiv-concat (inv p) (map-equiv e z) ∘e (equiv-ap e (pr1 x) z)))

inclusion-complement-isolated-element :
  {l1 : Level} {X : UU l1} (x : isolated-element X) →
  complement-isolated-element X x → X
inclusion-complement-isolated-element x = pr1

natural-inclusion-equiv-complement-isolated-element :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : X ≃ Y) (x : isolated-element X)
  (y : isolated-element Y) (p : map-equiv e (pr1 x) ＝ pr1 y) →
  ( inclusion-complement-isolated-element y ∘
    map-equiv (equiv-complement-isolated-element e x y p)) ~
  ( map-equiv e ∘ inclusion-complement-isolated-element x)
natural-inclusion-equiv-complement-isolated-element e x y p (x' , f) = refl

Recent changes