Isolated points

Content created by Egbert Rijke, Fredrik Bakke and Jonathan Prieto-Cubides.

Created on 2022-01-27.
Last modified on 2023-09-11.

module foundation.isolated-points where
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.maybe
open import foundation.negation
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.injective-maps
open import foundation-core.propositions
open import foundation-core.sets
open import foundation-core.subtypes
open import foundation-core.transport-along-identifications


A point a : A is considered to be isolated if Id a x is decidable for any x.


Isolated points

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

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

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

  point-isolated-point : X
  point-isolated-point = pr1 x

  is-isolated-isolated-point : is-isolated point-isolated-point
  is-isolated-isolated-point = pr2 x

Complements of isolated points

complement-isolated-point :
  {l1 : Level} (X : UU l1)  isolated-point X  UU l1
complement-isolated-point X x =
  Σ X  y  ¬ (point-isolated-point x  y))


A point is decidable if and only if the constant map pointing at it is decidable

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

  is-decidable-map-const-is-isolated :
    is-isolated a  is-decidable-map (const unit A a)
  is-decidable-map-const-is-isolated d x =
    is-decidable-equiv (fiber-const a x) (d x)

  is-isolated-is-decidable-map-const :
    is-decidable-map (const unit A a)  is-isolated a
  is-isolated-is-decidable-map-const d x =
    is-decidable-equiv' (fiber-const a x) (d x)

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

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

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

    is-prop-Eq-isolated-point :
      (d : is-isolated a) (x : A)  is-prop (Eq-isolated-point d x)
    is-prop-Eq-isolated-point d x =
      is-prop-cases-Eq-isolated-point d x (d x)

  Eq-isolated-point-Prop : is-isolated a  A  Prop lzero
  pr1 (Eq-isolated-point-Prop d x) = Eq-isolated-point d x
  pr2 (Eq-isolated-point-Prop d x) = is-prop-Eq-isolated-point 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)

    refl-Eq-isolated-point : (d : is-isolated a)  Eq-isolated-point d a
    refl-Eq-isolated-point d =
        ( cases-Eq-isolated-point d a)
        ( pr2 (decide-reflexivity (d a)))
        ( star)

    Eq-eq-isolated-point :
      (d : is-isolated a) {x : A}  a  x  Eq-isolated-point d x
    Eq-eq-isolated-point d refl = refl-Eq-isolated-point d

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

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

    contraction-total-Eq-isolated-point :
      (d : is-isolated a) (t : Σ A (Eq-isolated-point d)) 
      center-total-Eq-isolated-point d  t
    contraction-total-Eq-isolated-point d (x , e) =
        ( Eq-isolated-point-Prop d)
        ( cases-contraction-total-Eq-isolated-point d x (d x) e)

    is-contr-total-Eq-isolated-point :
      (d : is-isolated a)  is-contr (Σ A (Eq-isolated-point d))
    pr1 (is-contr-total-Eq-isolated-point d) = center-total-Eq-isolated-point d
    pr2 (is-contr-total-Eq-isolated-point d) =
      contraction-total-Eq-isolated-point d

    is-equiv-Eq-eq-isolated-point :
      (d : is-isolated a) (x : A)  is-equiv (Eq-eq-isolated-point d {x})
    is-equiv-Eq-eq-isolated-point d =
        ( is-contr-total-Eq-isolated-point d)
        ( λ x  Eq-eq-isolated-point d {x})

    equiv-Eq-eq-isolated-point :
      (d : is-isolated a) (x : A)  (a  x)  Eq-isolated-point d x
    pr1 (equiv-Eq-eq-isolated-point d x) = Eq-eq-isolated-point d
    pr2 (equiv-Eq-eq-isolated-point d x) = is-equiv-Eq-eq-isolated-point d x

    is-prop-eq-isolated-point : (d : is-isolated a) (x : A)  is-prop (a  x)
    is-prop-eq-isolated-point d x =
        ( equiv-Eq-eq-isolated-point d x)
        ( is-prop-Eq-isolated-point d x)

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

    is-emb-const-is-isolated : is-isolated a  is-emb (const unit A a)
    is-emb-const-is-isolated d star =
        ( is-contr-equiv
          ( a  a)
          ( left-unit-law-prod)
          ( is-proof-irrelevant-is-prop
            ( is-prop-eq-isolated-point d a)
            ( refl)))
        ( λ x  ap  y  a))

Being an isolated point is a property

is-prop-is-isolated :
  {l1 : Level} {A : UU l1} (a : A)  is-prop (is-isolated a)
is-prop-is-isolated a =
    ( λ H 
      is-prop-Π  x  is-prop-is-decidable (is-prop-eq-isolated-point a H x)))

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-point :
  {l1 : Level} (A : UU l1)  isolated-point A  A
inclusion-isolated-point A = pr1

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

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

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

decidable-emb-isolated-point :
  {l1 : Level} {A : UU l1} (a : isolated-point A)  unit ↪ᵈ A
pr1 (decidable-emb-isolated-point {l1} {A} a) =
  const unit A (pr1 a)
pr1 (pr2 (decidable-emb-isolated-point {l1} {A} a)) =
    ( inclusion-isolated-point A)
    ( const unit (isolated-point A) a)
    ( is-emb-inclusion-isolated-point A)
    ( is-emb-is-injective
      ( is-set-isolated-point A)
      ( λ { {star} {star} p  refl}))
pr2 (pr2 (decidable-emb-isolated-point {l1} {A} a)) x =
  is-decidable-prod is-decidable-unit (pr2 a x)

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

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

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

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

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

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

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

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

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

maybe-structure-isolated-point :
  {l1 : Level} {X : UU l1}  isolated-point X  maybe-structure X
pr1 (maybe-structure-isolated-point {l1} {X} x) =
  complement-isolated-point X x
pr2 (maybe-structure-isolated-point {l1} {X} x) =
  equiv-maybe-structure-isolated-point X x
equiv-complement-isolated-point :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : X  Y) (x : isolated-point X)
  (y : isolated-point Y) (p : map-equiv e (pr1 x)  pr1 y) 
  complement-isolated-point X x  complement-isolated-point Y y
equiv-complement-isolated-point e x y p =
    ( λ z  ¬ (pr1 y  z))
    ( e)
    ( λ z 
        ( equiv-concat (inv p) (map-equiv e z) ∘e (equiv-ap e (pr1 x) z)))
inclusion-complement-isolated-point :
  {l1 : Level} {X : UU l1} (x : isolated-point X) 
  complement-isolated-point X x  X
inclusion-complement-isolated-point x = pr1

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

Recent changes