The image of a map

module foundation.images where

open import foundation.propositional-truncations
open import foundation.slice
open import foundation.surjective-maps

open import foundation-core.1-types
open import foundation-core.contractible-types
open import foundation-core.dependent-pair-types
open import foundation-core.embeddings
open import foundation-core.equivalences
open import foundation-core.fibers-of-maps
open import foundation-core.functions
open import foundation-core.fundamental-theorem-of-identity-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.injective-maps
open import foundation-core.propositions
open import foundation-core.sets
open import foundation-core.subtype-identity-principle
open import foundation-core.subtypes
open import foundation-core.truncated-types
open import foundation-core.truncation-levels
open import foundation-core.universe-levels

Idea

The image of a map is a type that satisfies the universal property of the image of a map.

Definition

module _
  {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X)
  where

  subtype-im : subtype (l1 ⊔ l2) X
  subtype-im x = trunc-Prop (fib f x)

  im : UU (l1 ⊔ l2)
  im = type-subtype subtype-im

  inclusion-im : im → X
  inclusion-im = inclusion-subtype subtype-im

  map-unit-im : A → im
  pr1 (map-unit-im a) = f a
  pr2 (map-unit-im a) = unit-trunc-Prop (pair a refl)

  triangle-unit-im : f ~ (inclusion-im ∘ map-unit-im)
  triangle-unit-im a = refl

  unit-im : hom-slice f inclusion-im
  pr1 unit-im = map-unit-im
  pr2 unit-im = triangle-unit-im

Properties

We characterize the identity type of im f

module _
  {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X)
  where

  Eq-im : im f → im f → UU l1
  Eq-im x y = (pr1 x ＝ pr1 y)

  refl-Eq-im : (x : im f) → Eq-im x x
  refl-Eq-im x = refl

  Eq-eq-im : (x y : im f) → x ＝ y → Eq-im x y
  Eq-eq-im x .x refl = refl-Eq-im x

  abstract
    is-contr-total-Eq-im :
      (x : im f) → is-contr (Σ (im f) (Eq-im x))
    is-contr-total-Eq-im x =
      is-contr-total-Eq-subtype
        ( is-contr-total-path (pr1 x))
        ( λ x → is-prop-type-trunc-Prop)
        ( pr1 x)
        ( refl)
        ( pr2 x)

  abstract
    is-equiv-Eq-eq-im : (x y : im f) → is-equiv (Eq-eq-im x y)
    is-equiv-Eq-eq-im x =
      fundamental-theorem-id
        ( is-contr-total-Eq-im x)
        ( Eq-eq-im x)

  equiv-Eq-eq-im : (x y : im f) → (x ＝ y) ≃ Eq-im x y
  pr1 (equiv-Eq-eq-im x y) = Eq-eq-im x y
  pr2 (equiv-Eq-eq-im x y) = is-equiv-Eq-eq-im x y

  eq-Eq-im : (x y : im f) → Eq-im x y → x ＝ y
  eq-Eq-im x y = map-inv-is-equiv (is-equiv-Eq-eq-im x y)

The image inclusion is an embedding

abstract
  is-emb-inclusion-im :
    {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) →
    is-emb (inclusion-im f)
  is-emb-inclusion-im f =
    is-emb-inclusion-subtype (λ x → trunc-Prop (fib f x))

emb-im :
  {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) → im f ↪ X
pr1 (emb-im f) = inclusion-im f
pr2 (emb-im f) = is-emb-inclusion-im f

The image inclusion is injective

abstract
  is-injective-inclusion-im :
    {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) →
    is-injective (inclusion-im f)
  is-injective-inclusion-im f =
    is-injective-is-emb (is-emb-inclusion-im f)

The unit map of the image is surjective

abstract
  is-surjective-map-unit-im :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
    is-surjective (map-unit-im f)
  is-surjective-map-unit-im f (pair y z) =
    apply-universal-property-trunc-Prop z
      ( trunc-Prop (fib (map-unit-im f) (pair y z)))
      ( α)
    where
    α : fib f y → type-Prop (trunc-Prop (fib (map-unit-im f) (pair y z)))
    α (pair x p) =
      unit-trunc-Prop (pair x (eq-type-subtype (λ z → trunc-Prop (fib f z)) p))

The image of a map into a truncated type is truncated

abstract
  is-trunc-im :
    {l1 l2 : Level} (k : 𝕋) {X : UU l1} {A : UU l2} (f : A → X) →
    is-trunc (succ-𝕋 k) X → is-trunc (succ-𝕋 k) (im f)
  is-trunc-im k f = is-trunc-emb k (emb-im f)

The image of a map into a proposition is a proposition

abstract
  is-prop-im :
    {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) →
    is-prop X → is-prop (im f)
  is-prop-im = is-trunc-im neg-two-𝕋

The image of a map into a set is a set

abstract
  is-set-im :
    {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) →
    is-set X → is-set (im f)
  is-set-im = is-trunc-im neg-one-𝕋

im-Set :
  {l1 l2 : Level} {A : UU l2} (X : Set l1) (f : A → type-Set X) →
  Set (l1 ⊔ l2)
pr1 (im-Set X f) = im f
pr2 (im-Set X f) = is-set-im f (is-set-type-Set X)

The image of a map into a 1-type is a 1-type

abstract
  is-1-type-im :
    {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) →
    is-1-type X → is-1-type (im f)
  is-1-type-im = is-trunc-im zero-𝕋

im-1-Type :
  {l1 l2 : Level} {A : UU l2} (X : 1-Type l1)
  (f : A → type-1-Type X) → 1-Type (l1 ⊔ l2)
pr1 (im-1-Type X f) = im f
pr2 (im-1-Type X f) = is-1-type-im f (is-1-type-type-1-Type X)