Factorizations of maps

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-03-10.
Last modified on 2024-04-25.

module orthogonal-factorization-systems.factorizations-of-maps where
Imports 
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.homotopy-algebra
open import foundation.homotopy-induction
open import foundation.identity-types
open import foundation.retracts-of-types
open import foundation.structure-identity-principle
open import foundation.torsorial-type-families
open import foundation.univalence
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

Idea

A factorization of a map f : A → B is a pair of maps g : X → B and h : A → X such that their composite g ∘ h is f.

       X
      ∧ \
   h /   \ g
    /     ∨
  A -----> B
      f

We use diagrammatic order and say the map h is the left and g the right map of the factorization.

Definitions

The predicate on triangles of maps of being a factorization

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

  is-factorization :
    {l3 : Level} {X : UU l3} →
    (g : X → B) (h : A → X) → UU (l1 ⊔ l2)
  is-factorization g h = g ∘ h ~ f

The type of factorizations of a map through a specified image/type

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2}
  where

  factorization-through : (f : A → B) (X : UU l3) → UU (l1 ⊔ l2 ⊔ l3)
  factorization-through f X =
    Σ ( X → B)
      ( λ g →
        Σ ( A → X)
          ( is-factorization f g))

  right-map-factorization-through :
    {f : A → B} {X : UU l3} → factorization-through f X → X → B
  right-map-factorization-through = pr1

  left-map-factorization-through :
    {f : A → B} {X : UU l3} → factorization-through f X → A → X
  left-map-factorization-through = pr1 ∘ pr2

  is-factorization-factorization-through :
    {f : A → B} {X : UU l3}
    (F : factorization-through f X) →
      is-factorization f
        ( right-map-factorization-through F)
        ( left-map-factorization-through F)
  is-factorization-factorization-through = pr2 ∘ pr2

The type of factorizations of a map through images in a universe

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  where

  factorization : (l3 : Level) (f : A → B) → UU (l1 ⊔ l2 ⊔ lsuc l3)
  factorization l3 f = Σ (UU l3) (factorization-through f)

  image-factorization : {l3 : Level} {f : A → B} → factorization l3 f → UU l3
  image-factorization = pr1

  factorization-through-factorization :
    {l3 : Level} {f : A → B} (F : factorization l3 f) →
    factorization-through f (image-factorization F)
  factorization-through-factorization = pr2

  right-map-factorization :
    {l3 : Level} {f : A → B} (F : factorization l3 f) →
    image-factorization F → B
  right-map-factorization F =
    right-map-factorization-through (factorization-through-factorization F)

  left-map-factorization :
    {l3 : Level} {f : A → B} (F : factorization l3 f) →
    A → image-factorization F
  left-map-factorization F =
    left-map-factorization-through (factorization-through-factorization F)

  is-factorization-factorization :
    {l3 : Level} {f : A → B} (F : factorization l3 f) →
    is-factorization f (right-map-factorization F) (left-map-factorization F)
  is-factorization-factorization F =
    is-factorization-factorization-through
      ( factorization-through-factorization F)

Properties

Whiskering of factorizations by retracts

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

  whisker-image-factorization-through :
    {l3 l4 : Level} {X : UU l3} {Y : UU l4} →
    X retract-of Y → factorization-through f X → factorization-through f Y
  pr1 (whisker-image-factorization-through (s , r , h) (fr , fl , fH)) =
    fr ∘ r
  pr1 (pr2 (whisker-image-factorization-through (s , r , h) (fr , fl , fH))) =
    s ∘ fl
  pr2 (pr2 (whisker-image-factorization-through (s , r , h) (fr , fl , fH))) =
    (fr ·l (h ·r fl)) ∙h fH

Characterization of identifications of factorizations through a type

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

  coherence-htpy-factorization-through :
    (F E : factorization-through f X) →
    right-map-factorization-through F ~ right-map-factorization-through E →
    left-map-factorization-through F ~ left-map-factorization-through E →
    UU (l1 ⊔ l2)
  coherence-htpy-factorization-through F E R L =
    ( is-factorization-factorization-through F) ~
    ( horizontal-concat-htpy R L ∙h is-factorization-factorization-through E)

  htpy-factorization-through :
    (F E : factorization-through f X) → UU (l1 ⊔ l2 ⊔ l3)
  htpy-factorization-through F E =
    Σ ( right-map-factorization-through F ~
        right-map-factorization-through E)
      ( λ R →
        Σ ( left-map-factorization-through F ~
            left-map-factorization-through E)
          ( coherence-htpy-factorization-through F E R))

  refl-htpy-factorization-through :
    (F : factorization-through f X) → htpy-factorization-through F F
  pr1 (refl-htpy-factorization-through F) = refl-htpy
  pr1 (pr2 (refl-htpy-factorization-through F)) = refl-htpy
  pr2 (pr2 (refl-htpy-factorization-through F)) = refl-htpy

  htpy-eq-factorization-through :
    (F E : factorization-through f X) →
    F ＝ E → htpy-factorization-through F E
  htpy-eq-factorization-through F .F refl = refl-htpy-factorization-through F

  is-torsorial-htpy-factorization-through :
    (F : factorization-through f X) →
    is-torsorial (htpy-factorization-through F)
  is-torsorial-htpy-factorization-through F =
    is-torsorial-Eq-structure
      ( is-torsorial-htpy (right-map-factorization-through F))
      ( right-map-factorization-through F , refl-htpy)
      ( is-torsorial-Eq-structure
        ( is-torsorial-htpy (left-map-factorization-through F))
        ( left-map-factorization-through F , refl-htpy)
        ( is-torsorial-htpy (is-factorization-factorization-through F)))

  is-equiv-htpy-eq-factorization-through :
    (F E : factorization-through f X) →
    is-equiv (htpy-eq-factorization-through F E)
  is-equiv-htpy-eq-factorization-through F =
    fundamental-theorem-id
      ( is-torsorial-htpy-factorization-through F)
      ( htpy-eq-factorization-through F)

  extensionality-factorization-through :
    (F E : factorization-through f X) →
    (F ＝ E) ≃ (htpy-factorization-through F E)
  pr1 (extensionality-factorization-through F E) =
    htpy-eq-factorization-through F E
  pr2 (extensionality-factorization-through F E) =
    is-equiv-htpy-eq-factorization-through F E

  eq-htpy-factorization-through :
    (F E : factorization-through f X) →
    htpy-factorization-through F E → F ＝ E
  eq-htpy-factorization-through F E =
    map-inv-equiv (extensionality-factorization-through F E)

Characterization of identifications of factorizations of a map in a universe level

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

  equiv-factorization :
    (F E : factorization l3 f) → UU (l1 ⊔ l2 ⊔ l3)
  equiv-factorization F E =
    Σ ( image-factorization F ≃ image-factorization E)
      ( λ e →
        htpy-factorization-through f
          ( whisker-image-factorization-through f
            ( map-equiv e , retraction-map-equiv e)
            ( factorization-through-factorization F))
          ( factorization-through-factorization E))

  id-equiv-factorization :
    (F : factorization l3 f) → equiv-factorization F F
  pr1 (id-equiv-factorization F) = id-equiv
  pr2 (id-equiv-factorization F) =
    refl-htpy-factorization-through f (factorization-through-factorization F)

  equiv-eq-factorization :
    (F E : factorization l3 f) →
    F ＝ E → equiv-factorization F E
  equiv-eq-factorization F .F refl = id-equiv-factorization F

  is-torsorial-equiv-factorization :
    (F : factorization l3 f) →
    is-torsorial (equiv-factorization F)
  is-torsorial-equiv-factorization F =
    is-torsorial-Eq-structure
      ( is-torsorial-equiv (image-factorization F))
      ( image-factorization F , id-equiv)
      ( is-torsorial-htpy-factorization-through f
        ( factorization-through-factorization F))

  is-equiv-equiv-eq-factorization :
    (F E : factorization l3 f) → is-equiv (equiv-eq-factorization F E)
  is-equiv-equiv-eq-factorization F =
    fundamental-theorem-id
      ( is-torsorial-equiv-factorization F)
      ( equiv-eq-factorization F)

  extensionality-factorization :
    (F E : factorization l3 f) → (F ＝ E) ≃ (equiv-factorization F E)
  pr1 (extensionality-factorization F E) = equiv-eq-factorization F E
  pr2 (extensionality-factorization F E) = is-equiv-equiv-eq-factorization F E

  eq-equiv-factorization :
    (F E : factorization l3 f) → equiv-factorization F E → F ＝ E
  eq-equiv-factorization F E = map-inv-equiv (extensionality-factorization F E)

See also

Recent changes