The pullback-hom

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

Created on 2023-02-18.
Last modified on 2024-10-27.

module orthogonal-factorization-systems.pullback-hom where

Imports

open import foundation.commuting-squares-of-maps
open import foundation.commuting-triangles-of-maps
open import foundation.cones-over-cospan-diagrams
open import foundation.cospan-diagrams
open import foundation.dependent-pair-types
open import foundation.equality-dependent-pair-types
open import foundation.equivalences
open import foundation.equivalences-arrows
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.functoriality-fibers-of-maps
open import foundation.functoriality-morphisms-arrows
open import foundation.higher-homotopies-morphisms-arrows
open import foundation.homotopies
open import foundation.homotopies-morphisms-arrows
open import foundation.identity-types
open import foundation.morphisms-arrows
open import foundation.postcomposition-functions
open import foundation.precomposition-dependent-functions
open import foundation.precomposition-functions
open import foundation.pullback-cones
open import foundation.pullbacks
open import foundation.retractions
open import foundation.sections
open import foundation.standard-pullbacks
open import foundation.transport-along-identifications
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.type-theoretic-principle-of-choice
open import foundation.universal-property-pullbacks
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

Idea

The pullback-hom^¶ or pullback-power^¶ of two maps f : A → B and g : X → Y, is the gap map of the commuting square:

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

More explicitly, the pullback of - ∘ f and g ∘ - is the type of morphisms of arrows from f to g, while the domain of the pullback-hom is the type B → X of diagonal fillers for morphisms of arrows from f to g. The pullback-hom can therefore be described as a map

  pullback-hom f g : (B → X) → hom-arrow f g

This map takes a map j : B → X as in the diagram

    A       X
    |     ∧ |
  f |  j/   | g
    ∨ /     ∨
    B       Y

to the morphism of arrows from f to g as in the diagram

         j ∘ f
    A ----------> X
    |             |
  f |  refl-htpy  | g
    ∨             ∨
    B ----------> Y.
         g ∘ j

The fibers of the pullback-hom are lifting squares. The pullback-hom is therefore a fundamental operation in the study of lifting conditions and orthogonality conditions: The pullback-hom of f and g is an equivalence if and only if f is left orthogonal to g, while the pullback-hom of f and g is surjective if and only if f satisfies the left lifting property to g.

Notation. There are two common ways to denote the pullback-hom: Some authors use f ⋔ g, while other authors use ⟨f , g⟩. Both notations can be used, depending on what perspective of the pullback-hom is emphasized. The pitchfork-notation f ⋔ g is used more often in settings where a lifting property of f and g is emphasized, while the hom-notation ⟨f , g⟩ is used when the pullback-hom is thought of in terms of hom-sets. The latter notation is useful for instance, if one wants to emphasize an adjoint relation between the pullback-hom and the pushout-product:

  ⟨f □ g , h⟩ ＝ ⟨f , ⟨g , h⟩⟩.

Definitions

The pullback-hom

The pullback-hom f ⋔ g is the map (B → X) → hom-arrow f g, that takes a diagonal map j from the codomain of f to the domain of g to the morphism of arrows

         j ∘ f
    A ----------> X
    |             |
  f |  refl-htpy  | g
    ∨             ∨
    B ----------> Y.
         g ∘ j

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

  map-domain-pullback-hom : (B → X) → A → X
  map-domain-pullback-hom j = j ∘ f

  map-codomain-pullback-hom : (B → X) → B → Y
  map-codomain-pullback-hom j = g ∘ j

  coh-pullback-hom :
    (j : B → X) →
    coherence-hom-arrow f g
      ( map-domain-pullback-hom j)
      ( map-codomain-pullback-hom j)
  coh-pullback-hom j = refl-htpy

  pullback-hom : (B → X) → hom-arrow f g
  pullback-hom j =
    ( map-domain-pullback-hom j ,
      map-codomain-pullback-hom j ,
      coh-pullback-hom j)

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

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

The cone structure on the codomain of the pullback-hom

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

  left-projection-hom-arrow-pullback-hom : hom-arrow f g → B → Y
  left-projection-hom-arrow-pullback-hom = map-codomain-hom-arrow f g

  right-projection-hom-arrow-pullback-hom : hom-arrow f g → A → X
  right-projection-hom-arrow-pullback-hom = map-domain-hom-arrow f g

  coherence-square-cone-hom-arrow-pullback-hom :
    coherence-square-maps
      ( right-projection-hom-arrow-pullback-hom)
      ( left-projection-hom-arrow-pullback-hom)
      ( postcomp A g)
      ( precomp f Y)
  coherence-square-cone-hom-arrow-pullback-hom h = eq-htpy (coh-hom-arrow f g h)

  cone-hom-arrow-pullback-hom :
    cone (precomp f Y) (postcomp A g) (hom-arrow f g)
  pr1 cone-hom-arrow-pullback-hom = left-projection-hom-arrow-pullback-hom
  pr1 (pr2 cone-hom-arrow-pullback-hom) =
    right-projection-hom-arrow-pullback-hom
  pr2 (pr2 cone-hom-arrow-pullback-hom) =
    coherence-square-cone-hom-arrow-pullback-hom

The standard pullback of the defining cospan 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)
  where

  type-standard-pullback-hom : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
  type-standard-pullback-hom =
    standard-pullback (precomp f Y) (postcomp A g)

  module _
    (h : type-standard-pullback-hom)
    where

    map-domain-standard-pullback-hom : A → X
    map-domain-standard-pullback-hom = pr1 (pr2 h)

    map-codomain-standard-pullback-hom : B → Y
    map-codomain-standard-pullback-hom = pr1 h

    eq-coh-standard-pullback-hom :
      precomp f Y map-codomain-standard-pullback-hom ＝
      postcomp A g map-domain-standard-pullback-hom
    eq-coh-standard-pullback-hom = pr2 (pr2 h)

    coh-standard-pullback-hom :
      precomp f Y map-codomain-standard-pullback-hom ~
      postcomp A g map-domain-standard-pullback-hom
    coh-standard-pullback-hom = htpy-eq eq-coh-standard-pullback-hom

The cone of the diagram defining 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)
  where

  cone-pullback-hom : cone (precomp f Y) (postcomp A g) (B → X)
  cone-pullback-hom = (postcomp B g , precomp f X , refl-htpy)

  gap-pullback-hom : (B → X) → type-standard-pullback-hom f g
  gap-pullback-hom = gap (precomp f Y) (postcomp A g) cone-pullback-hom

The equivalence of the codomain of the pullback-hom with the standard pullback

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

  map-compute-pullback-hom :
    hom-arrow f g → type-standard-pullback-hom f g
  map-compute-pullback-hom h =
    ( map-codomain-hom-arrow f g h ,
      map-domain-hom-arrow f g h ,
      eq-htpy (coh-hom-arrow f g h))

  map-inv-compute-pullback-hom :
    type-standard-pullback-hom f g → hom-arrow f g
  map-inv-compute-pullback-hom h =
    ( map-domain-standard-pullback-hom f g h ,
      map-codomain-standard-pullback-hom f g h ,
      coh-standard-pullback-hom f g h)

  is-section-map-inv-compute-pullback-hom :
    is-section map-compute-pullback-hom map-inv-compute-pullback-hom
  is-section-map-inv-compute-pullback-hom h =
    eq-pair-eq-fiber
      ( eq-pair-eq-fiber
        ( is-retraction-eq-htpy (eq-coh-standard-pullback-hom f g h)))

  is-retraction-map-inv-compute-pullback-hom :
    is-retraction map-compute-pullback-hom map-inv-compute-pullback-hom
  is-retraction-map-inv-compute-pullback-hom h =
    eq-pair-eq-fiber
      ( eq-pair-eq-fiber (is-section-eq-htpy (coh-hom-arrow f g h)))

  is-equiv-map-compute-pullback-hom :
    is-equiv map-compute-pullback-hom
  is-equiv-map-compute-pullback-hom =
    is-equiv-is-invertible
      ( map-inv-compute-pullback-hom)
      ( is-section-map-inv-compute-pullback-hom)
      ( is-retraction-map-inv-compute-pullback-hom)

  is-equiv-map-inv-compute-pullback-hom :
    is-equiv map-inv-compute-pullback-hom
  is-equiv-map-inv-compute-pullback-hom =
    is-equiv-is-invertible
      ( map-compute-pullback-hom)
      ( is-retraction-map-inv-compute-pullback-hom)
      ( is-section-map-inv-compute-pullback-hom)

  compute-pullback-hom : hom-arrow f g ≃ type-standard-pullback-hom f g
  pr1 compute-pullback-hom = map-compute-pullback-hom
  pr2 compute-pullback-hom = is-equiv-map-compute-pullback-hom

  inv-compute-pullback-hom : type-standard-pullback-hom f g ≃ hom-arrow f g
  pr1 inv-compute-pullback-hom = map-inv-compute-pullback-hom
  pr2 inv-compute-pullback-hom = is-equiv-map-inv-compute-pullback-hom

The commuting triangle of the pullback-hom and the gap map

We construct the homotopy witnessing that the triangle of maps

                  (B → X)
                 /       \
  pullback-hom  /         \ gap
               ∨           ∨
     hom-arrow f g -----> type-standard-pullback-hom f g

commutes. The bottom map in this triangle is the underlying map of the equivalence hom-arrow f g ≃ type-stanard-pullback-hom f g constructed above.

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

  triangle-pullback-hom :
    coherence-triangle-maps'
      ( gap-pullback-hom f g)
      ( gap (precomp f Y) (postcomp A g) (cone-hom-arrow' f g))
      ( pullback-hom f g)
  triangle-pullback-hom j =
    eq-pair-eq-fiber (eq-pair-eq-fiber (is-retraction-eq-htpy refl))

The action on homotopies of the `pullback-hom`

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

  htpy-domain-htpy-hom-arrow-htpy :
    map-domain-pullback-hom f g j ~ map-domain-pullback-hom f g k
  htpy-domain-htpy-hom-arrow-htpy = H ·r f

  htpy-codomain-htpy-hom-arrow-htpy :
    map-codomain-pullback-hom f g j ~ map-codomain-pullback-hom f g k
  htpy-codomain-htpy-hom-arrow-htpy = g ·l H

  coh-htpy-hom-arrow-htpy :
    coherence-htpy-hom-arrow f g
      ( pullback-hom f g j)
      ( pullback-hom f g k)
      ( htpy-domain-htpy-hom-arrow-htpy)
      ( htpy-codomain-htpy-hom-arrow-htpy)
  coh-htpy-hom-arrow-htpy = inv-htpy right-unit-htpy

  htpy-hom-arrow-htpy :
    htpy-hom-arrow f g (pullback-hom f g j) (pullback-hom f g k)
  pr1 htpy-hom-arrow-htpy = htpy-domain-htpy-hom-arrow-htpy
  pr1 (pr2 htpy-hom-arrow-htpy) = htpy-codomain-htpy-hom-arrow-htpy
  pr2 (pr2 htpy-hom-arrow-htpy) = coh-htpy-hom-arrow-htpy

Properties

The cone of the pullback-hom is a pullback

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

  is-pullback-cone-hom-arrow-pullback-hom :
    is-pullback
      ( precomp f Y)
      ( postcomp A g)
      ( cone-hom-arrow-pullback-hom f g)
  is-pullback-cone-hom-arrow-pullback-hom =
    is-equiv-map-compute-pullback-hom f g

  pullback-cone-hom-arrow-pullback-hom :
    pullback-cone (cospan-diagram-hom-arrow f g) (l1 ⊔ l2 ⊔ l3 ⊔ l4)
  pullback-cone-hom-arrow-pullback-hom =
    ( hom-arrow f g , cone-hom-arrow-pullback-hom f g) ,
    ( is-pullback-cone-hom-arrow-pullback-hom)

  universal-property-pullback-cone-hom-arrow-pullback-hom :
    universal-property-pullback
      ( precomp f Y)
      ( postcomp A g)
      ( cone-hom-arrow-pullback-hom f g)
  universal-property-pullback-cone-hom-arrow-pullback-hom =
    universal-property-pullback-is-pullback
      ( precomp f Y)
      ( postcomp A g)
      ( cone-hom-arrow-pullback-hom f g)
      ( is-pullback-cone-hom-arrow-pullback-hom)

The action on homotopies at `refl-htpy` is the reflexivity homotopy of morphisms of arrows

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

  htpy-domain-compute-refl-htpy-hom-arrow-htpy :
    htpy-domain-htpy-hom-arrow-htpy f g (refl-htpy' j) ~
    htpy-domain-refl-htpy-hom-arrow f g (pullback-hom f g j)
  htpy-domain-compute-refl-htpy-hom-arrow-htpy = refl-htpy

  htpy-codomain-compute-refl-htpy-hom-arrow-htpy :
    htpy-codomain-htpy-hom-arrow-htpy f g (refl-htpy' j) ~
    htpy-codomain-refl-htpy-hom-arrow f g (pullback-hom f g j)
  htpy-codomain-compute-refl-htpy-hom-arrow-htpy = refl-htpy

  coh-compute-refl-htpy-hom-arrow-htpy :
    coherence-htpy-htpy-hom-arrow f g
      ( pullback-hom f g j)
      ( pullback-hom f g j)
      ( htpy-hom-arrow-htpy f g refl-htpy)
      ( refl-htpy-hom-arrow f g (pullback-hom f g j))
      ( htpy-domain-compute-refl-htpy-hom-arrow-htpy)
      ( htpy-codomain-compute-refl-htpy-hom-arrow-htpy)
  coh-compute-refl-htpy-hom-arrow-htpy = refl-htpy

  compute-refl-htpy-hom-arrow-htpy :
    htpy-htpy-hom-arrow f g
      ( pullback-hom f g j)
      ( pullback-hom f g j)
      ( htpy-hom-arrow-htpy f g refl-htpy)
      ( refl-htpy-hom-arrow f g (pullback-hom f g j))
  pr1 compute-refl-htpy-hom-arrow-htpy =
    htpy-domain-compute-refl-htpy-hom-arrow-htpy
  pr1 (pr2 compute-refl-htpy-hom-arrow-htpy) =
    htpy-codomain-compute-refl-htpy-hom-arrow-htpy
  pr2 (pr2 compute-refl-htpy-hom-arrow-htpy) =
    coh-compute-refl-htpy-hom-arrow-htpy

Computing the pullback-hom of a composite

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

  map-domain-left-whisker-hom-arrow : hom-arrow f g → A → X
  map-domain-left-whisker-hom-arrow α = map-domain-hom-arrow f g α

  map-codomain-left-whisker-hom-arrow : hom-arrow f g → B → S
  map-codomain-left-whisker-hom-arrow α = h ∘ map-codomain-hom-arrow f g α

  coh-left-whisker-hom-arrow :
    (α : hom-arrow f g) →
    coherence-square-maps
      ( map-domain-left-whisker-hom-arrow α)
      ( f)
      ( h ∘ g)
      ( map-codomain-left-whisker-hom-arrow α)
  coh-left-whisker-hom-arrow α = h ·l (coh-hom-arrow f g α)

  left-whisker-hom-arrow :
    hom-arrow f g → hom-arrow f (h ∘ g)
  pr1 (left-whisker-hom-arrow α) = map-domain-left-whisker-hom-arrow α
  pr1 (pr2 (left-whisker-hom-arrow α)) = map-codomain-left-whisker-hom-arrow α
  pr2 (pr2 (left-whisker-hom-arrow α)) = coh-left-whisker-hom-arrow α

  compute-pullback-hom-comp-right :
    coherence-triangle-maps
      ( pullback-hom f (h ∘ g))
      ( left-whisker-hom-arrow)
      ( pullback-hom f g)
  compute-pullback-hom-comp-right = refl-htpy

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

  map-domain-right-whisker-hom-arrow : hom-arrow f g → S → X
  map-domain-right-whisker-hom-arrow α = map-domain-hom-arrow f g α ∘ h

  map-codomain-right-whisker-hom-arrow : hom-arrow f g → B → Y
  map-codomain-right-whisker-hom-arrow α = map-codomain-hom-arrow f g α

  coh-right-whisker-hom-arrow :
    (α : hom-arrow f g) →
    coherence-hom-arrow (f ∘ h) g
      ( map-domain-right-whisker-hom-arrow α)
      ( map-codomain-right-whisker-hom-arrow α)
  coh-right-whisker-hom-arrow α =
    coh-hom-arrow f g α ·r h

  right-whisker-hom-arrow :
    hom-arrow f g → hom-arrow (f ∘ h) g
  pr1 (right-whisker-hom-arrow α) = map-domain-right-whisker-hom-arrow α
  pr1 (pr2 (right-whisker-hom-arrow α)) = map-codomain-right-whisker-hom-arrow α
  pr2 (pr2 (right-whisker-hom-arrow α)) = coh-right-whisker-hom-arrow α

  compute-pullback-hom-comp-left :
    coherence-triangle-maps
      ( pullback-hom (f ∘ h) g)
      ( right-whisker-hom-arrow)
      ( pullback-hom f g)
  compute-pullback-hom-comp-left = refl-htpy

Computing the fiber map between the vertical maps in the pullback-hom square

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

  compute-map-fiber-vertical-pullback-hom :
    (h : B → Y) →
    equiv-arrow
      ( precomp-Π f (fiber g ∘ h))
      ( map-fiber-vertical-map-cone
        ( precomp f Y)
        ( postcomp A g)
        ( cone-pullback-hom f g)
        ( h))
  pr1 (compute-map-fiber-vertical-pullback-hom h) =
    compute-Π-fiber-postcomp B g h
  pr1 (pr2 (compute-map-fiber-vertical-pullback-hom h)) =
    compute-Π-fiber-postcomp A g (h ∘ f)
  pr2 (pr2 (compute-map-fiber-vertical-pullback-hom h)) H =
    eq-Eq-fiber
      ( postcomp A g)
      ( precomp f Y h)
      ( refl)
      ( compute-eq-htpy-ap-precomp f (pr2 (map-distributive-Π-Σ H)))

Table of files about pullbacks

The following table lists files that are about pullbacks as a general concept.

Concept	File
Cospan diagrams	`foundation.cospans`
Morphisms of cospan diagrams	`foundation.morphisms-cospans`
Cones over cospan diagrams	`foundation.cones-over-cospan-diagrams`
The universal property of pullbacks (foundation-core)	`foundation-core.universal-property-pullbacks`
The universal property of pullbacks (foundation)	`foundation.universal-property-pullbacks`
The universal property of fiber products	`foundation.universal-property-fiber-products`
Standard pullbacks	`foundation.standard-pullbacks`
Pullbacks (foundation-core)	`foundation-core.pullbacks`
Pullbacks (foundation)	`foundation.pullbacks`
Pullback cones	`foundation.pullback-cones`
Functoriality of pullbacks	`foundation.functoriality-pullbacks`
Cartesian morphisms of arrows	`foundation.cartesian-morphisms-arrows`
Dependent products of pullbacks	`foundation.dependent-products-pullbacks`
Dependent sums of pullbacks	`foundation.dependent-sums-pullbacks`
Products of pullbacks	`foundation.products-pullbacks`
Coroducts of pullbacks	`foundation.coproducts-pullbacks`
Postcomposition of pullbacks	`foundation.postcomposition-pullbacks`
Pullbacks of subtypes	`foundation.pullbacks-subtypes`
The pullback-hom	`orthogonal-factorization-systems.pullback-hom`
Functoriality of the pullback-hom	`orthogonal-factorization-systems.functoriality-pullback-hom`
Pullbacks in precategories	`category-theory.pullbacks-in-precategories`

External links

Pullback-power at the $n$ Lab

A wikidata identifier for this concept is unavailable.

References

[RV22]: Emily Riehl and Dominic Verity. Elements of ∞-Category Theory. Cambridge Studies in Advanced Mathematics. Cambridge University Press, 2022. ISBN 978-1-108-83798-9. URL: https://math.jhu.edu/~eriehl/elements.pdf, doi:10.1017/9781108936880.

Recent changes

2024-10-27. Fredrik Bakke. Functoriality of morphisms of arrows (#1130).
2024-04-25. Fredrik Bakke. chore: Fix arrowheads in character diagrams (#1124).
2024-03-22. Fredrik Bakke. Additions to cartesian morphisms (#1087).
2024-03-12. Fredrik Bakke. Bibliographies (#1058).
2024-03-02. Fredrik Bakke. Factor out standard pullbacks (#1042).