The pullback-hom

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

Created on 2023-02-18.
Last modified on 2023-09-12.

module orthogonal-factorization-systems.pullback-hom where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.cones-over-cospans
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.fibered-maps
open import foundation.fibers-of-maps
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.morphisms-cospans
open import foundation.pullbacks
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universal-property-pullbacks
open import foundation.universe-levels
open import foundation.whiskering-homotopies

open import orthogonal-factorization-systems.lifting-squares

Idea

Given a pair of maps f : A → B and g : X → Y, there is a commuting square

          - ∘ f
    B → X ----> A → X
      |           |
g ∘ - |           | g ∘ -
      V           V
    B → Y ----> A → Y.
          - ∘ f

The pullback-hom of f and g, f ⋔ g, is the comparison map from B → X to the pullback of the cospan:

      ∙ ------> A → X
      |  ⌟        |
      |           | g ∘ -
      V           V
    B → Y ----> A → Y.
          - ∘ f

This pullback type can be understood as the type of fibered maps from f to g, i.e. commuting squares where the vertical maps are f and g.

Definitions

The codomain of the pullback-hom

type-canonical-pullback-hom :
  {l1 l2 l3 l4 : Level}
  {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
  (f : A → B) (g : X → Y) →
  UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
type-canonical-pullback-hom {A = A} {Y = Y} f g =
  canonical-pullback (precomp f Y) (postcomp A g)

The canonical pullback-hom type is equivalent to the type of fibered maps

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

  equiv-fibered-map-type-canonical-pullback-hom :
    type-canonical-pullback-hom f g ≃ fibered-map f g
  equiv-fibered-map-type-canonical-pullback-hom =
    equiv-tot (λ _ → equiv-tot (λ _ → equiv-funext))

  equiv-type-canonical-pullback-hom-fibered-map :
    fibered-map f g ≃ type-canonical-pullback-hom f g
  equiv-type-canonical-pullback-hom-fibered-map =
    inv-equiv equiv-fibered-map-type-canonical-pullback-hom

  map-fibered-map-type-canonical-pullback-hom :
    type-canonical-pullback-hom f g → fibered-map f g
  map-fibered-map-type-canonical-pullback-hom =
    map-equiv equiv-fibered-map-type-canonical-pullback-hom

  map-type-canonical-pullback-hom-fibered-map :
    fibered-map f g → type-canonical-pullback-hom f g
  map-type-canonical-pullback-hom-fibered-map =
    map-equiv equiv-type-canonical-pullback-hom-fibered-map

Below are basic definitions related to the pullback property of the type of fibered maps.

  cone-canonical-pullback-hom :
    cone (precomp f Y) (postcomp A g) (type-canonical-pullback-hom f g)
  cone-canonical-pullback-hom =
    cone-canonical-pullback (precomp f Y) (postcomp A g)

  cone-pullback-hom :
    cone (precomp f Y) (postcomp A g) (fibered-map f g)
  cone-pullback-hom =
    cone-map
      ( precomp f Y)
      ( postcomp A g)
      ( cone-canonical-pullback (precomp f Y) (postcomp A g))
      ( map-type-canonical-pullback-hom-fibered-map)

  gap-canonical-pullback-hom :
    {l : Level} {C : UU l} →
    cone (precomp f Y) (postcomp A g) C → C → type-canonical-pullback-hom f g
  gap-canonical-pullback-hom = gap (precomp f Y) (postcomp A g)

  gap-pullback-hom :
    {l : Level} {C : UU l} →
    cone (precomp f Y) (postcomp A g) C → C → fibered-map f g
  gap-pullback-hom c x =
    map-fibered-map-type-canonical-pullback-hom (gap-canonical-pullback-hom c x)

  is-pullback-fibered-map :
    is-pullback (precomp f Y) (postcomp A g) (cone-pullback-hom)
  is-pullback-fibered-map =
    is-equiv-map-equiv equiv-type-canonical-pullback-hom-fibered-map

  universal-property-pullback-fibered-map :
    {l : Level} →
    universal-property-pullback l
      ( precomp f Y) (postcomp A g) (cone-pullback-hom)
  universal-property-pullback-fibered-map =
    universal-property-pullback-is-pullback
      ( precomp f Y)
      ( postcomp A g)
      ( cone-pullback-hom)
      ( is-pullback-fibered-map)

The pullback-hom map

The pullback-hom f ⋔ g is the map (B → X) → fibered-map f g, that takes a diagonal map j from the codomain of f to the domain of g to the fibered map (g ∘ j , j ∘ f , refl-htpy).

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

  pullback-hom : (B → X) → fibered-map f g
  pullback-hom = gap-pullback-hom f g (postcomp B g , precomp f X , refl-htpy)

  infix 30 _⋔_
  _⋔_ = pullback-hom

The symbol ⋔ is the pitchfork (agda-input: \pitchfork).

Properties

Functoriality of the pullback-hom

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

  map-pullback-hom :
    hom-cospan
      ( precomp f' Y')
      ( postcomp A' g')
      ( precomp f Y)
      ( postcomp A g) →
    fibered-map f' g' → fibered-map f g
  map-pullback-hom =
    map-is-pullback
      ( precomp f Y)
      ( postcomp A g)
      ( precomp f' Y')
      ( postcomp A' g')
      ( cone-pullback-hom f g)
      ( cone-pullback-hom f' g')
      ( is-pullback-fibered-map f g)
      ( is-pullback-fibered-map f' g')

The fibers of the pullback-hom

module _
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
  (f : A → B) (g : X → Y) (h : fibered-map f g)
  where

  inv-compute-fiber-pullback-hom :
    (fiber (pullback-hom f g) h) ≃ (lifting-square-fibered-map f g h)
  inv-compute-fiber-pullback-hom =
    equiv-tot
      ( λ j →
        ( equiv-Σ _
          ( equiv-inv-htpy (j ∘ f) (map-total-fibered-map f g h))
          ( λ E →
            equiv-Σ _
              ( equiv-inv-htpy (g ∘ j) (map-base-fibered-map f g h))
              ( λ L →
                ( equiv-concat-htpy'
                  ( inv-htpy L ·r f)
                  ( λ x →
                    ap
                      ( is-map-over-map-total-fibered-map f g h x ∙_)
                      ( inv-htpy-left-whisk-inv-htpy g E x))) ∘e
                ( ( equiv-right-transpose-htpy-concat
                    ( inv-htpy (L ·r f))
                    ( g ·l E)
                    ( is-map-over-map-total-fibered-map f g h)) ∘e
                  ( equiv-left-transpose-htpy-concat'
                    ( g ·l E)
                    ( L ·r f)
                    ( is-map-over-map-total-fibered-map f g h)))))) ∘e
        ( ( equiv-left-swap-Σ) ∘e
          ( extensionality-fibered-map f g (pullback-hom f g j) h)))

  compute-fiber-pullback-hom :
    (lifting-square-fibered-map f g h) ≃ (fiber (pullback-hom f g) h)
  compute-fiber-pullback-hom = inv-equiv inv-compute-fiber-pullback-hom

Recent changes