Functoriality of fibers of maps

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

Created on 2022-07-25.
Last modified on 2024-03-02.

module foundation.functoriality-fibers-of-maps where
Imports
open import foundation.action-on-higher-identifications-functions
open import foundation.action-on-identifications-functions
open import foundation.cones-over-cospan-diagrams
open import foundation.dependent-pair-types
open import foundation.homotopies-morphisms-arrows
open import foundation.morphisms-arrows
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import foundation-core.commuting-squares-of-homotopies
open import foundation-core.commuting-squares-of-maps
open import foundation-core.equality-dependent-pair-types
open import foundation-core.fibers-of-maps
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.homotopies
open import foundation-core.identity-types

Idea

Any morphism of arrows (i , j , H) from f to g

        i
    A -----> X
    |        |
  f |        | g
    v        v
    B -----> Y
        j

induces a morphism of arrows between the fiber inclusions of f and g, i.e., a commuting square

  fiber f b -----> fiber g (j b)
      |                  |
      |                  |
      V                  V
      A ---------------> X.

This operation from morphisms of arrows from f to g to morphisms of arrows between their fiber inclusions is the functorial action of fibers. The functorial action obeys the functor laws, i.e., it preserves identity morphisms and composition.

Definitions

Any commuting square induces a family of maps between the fibers of the vertical maps

Our definition of map-domain-hom-arrow-fiber is given in such a way that it always computes nicely.

module _
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
  (f : A  B) (g : X  Y) (α : hom-arrow f g) (b : B)
  where

  map-domain-hom-arrow-fiber :
    fiber f b  fiber g (map-codomain-hom-arrow f g α b)
  map-domain-hom-arrow-fiber =
    map-Σ _
      ( map-domain-hom-arrow f g α)
      ( λ a p 
        inv (coh-hom-arrow f g α a)  ap (map-codomain-hom-arrow f g α) p)

  map-fiber :
    fiber f b  fiber g (map-codomain-hom-arrow f g α b)
  map-fiber = map-domain-hom-arrow-fiber

  map-codomain-hom-arrow-fiber : A  X
  map-codomain-hom-arrow-fiber = map-domain-hom-arrow f g α

  coh-hom-arrow-fiber :
    coherence-square-maps
      ( map-domain-hom-arrow-fiber)
      ( inclusion-fiber f)
      ( inclusion-fiber g)
      ( map-domain-hom-arrow f g α)
  coh-hom-arrow-fiber = refl-htpy

  hom-arrow-fiber :
    hom-arrow
      ( inclusion-fiber f {b})
      ( inclusion-fiber g {map-codomain-hom-arrow f g α b})
  pr1 hom-arrow-fiber = map-domain-hom-arrow-fiber
  pr1 (pr2 hom-arrow-fiber) = map-codomain-hom-arrow-fiber
  pr2 (pr2 hom-arrow-fiber) = coh-hom-arrow-fiber

Any cone induces a family of maps between the fibers of the vertical maps

module _
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4}
  (f : A  X) (g : B  X) (c : cone f g C) (a : A)
  where

  map-fiber-vertical-map-cone :
    fiber (vertical-map-cone f g c) a  fiber g (f a)
  map-fiber-vertical-map-cone =
    map-domain-hom-arrow-fiber
      ( vertical-map-cone f g c)
      ( g)
      ( hom-arrow-cone f g c)
      ( a)

For any f : A → B and any identification p : b = b' in B, we obtain a morphism of arrows between the fiber inclusion at b to the fiber inclusion at b'

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

  tr-hom-arrow-inclusion-fiber :
    {b b' : B} (p : b  b') 
    hom-arrow (inclusion-fiber f {b}) (inclusion-fiber f {b'})
  pr1 (tr-hom-arrow-inclusion-fiber p) = tot  a  concat' (f a) p)
  pr1 (pr2 (tr-hom-arrow-inclusion-fiber p)) = id
  pr2 (pr2 (tr-hom-arrow-inclusion-fiber p)) = refl-htpy

Properties

The functorial action of fiber preserves the identity function

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

  preserves-id-map-fiber :
    map-domain-hom-arrow-fiber f f id-hom-arrow b ~ id
  preserves-id-map-fiber (a , refl) = refl

  coh-preserves-id-hom-arrow-fiber :
    coherence-square-homotopies
      ( refl-htpy)
      ( refl-htpy)
      ( coh-hom-arrow-fiber f f id-hom-arrow b)
      ( inclusion-fiber f ·l preserves-id-map-fiber)
  coh-preserves-id-hom-arrow-fiber (a , refl) = refl

  preserves-id-hom-arrow-fiber :
    htpy-hom-arrow
      ( inclusion-fiber f)
      ( inclusion-fiber f)
      ( hom-arrow-fiber f f id-hom-arrow b)
      ( id-hom-arrow)
  pr1 preserves-id-hom-arrow-fiber = preserves-id-map-fiber
  pr1 (pr2 preserves-id-hom-arrow-fiber) = refl-htpy
  pr2 (pr2 preserves-id-hom-arrow-fiber) = coh-preserves-id-hom-arrow-fiber

The functorial action of fiber preserves composition of morphisms of arrows

module _
  {l1 l2 l3 l4 l5 l6 : Level}
  {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {U : UU l5} {V : UU l6}
  (f : A  B) (g : X  Y) (h : U  V) (β : hom-arrow g h) (α : hom-arrow f g)
  (b : B)
  where

  preserves-comp-map-fiber :
    map-fiber f h (comp-hom-arrow f g h β α) b ~
    map-fiber g h β (map-codomain-hom-arrow f g α b)  map-fiber f g α b
  preserves-comp-map-fiber (a , refl) =
    ap
      ( pair _)
      ( ( right-unit) 
        ( distributive-inv-concat
          ( ap (map-codomain-hom-arrow g h β) (coh-hom-arrow f g α a))
          ( coh-hom-arrow g h β (map-domain-hom-arrow f g α a))) 
        ( ap
          ( concat (inv (coh-hom-arrow g h β (pr1 α a))) _)
          ( inv
            ( ( ap² (map-codomain-hom-arrow g h β) right-unit) 
              ( ap-inv
                ( map-codomain-hom-arrow g h β)
                ( coh-hom-arrow f g α a))))))

  compute-left-whisker-inclusion-fiber-preserves-comp-map-fiber :
    inclusion-fiber h ·l preserves-comp-map-fiber ~ refl-htpy
  compute-left-whisker-inclusion-fiber-preserves-comp-map-fiber (a , refl) =
    ( inv (ap-comp (inclusion-fiber h) (pair _) _)) 
    ( ap-const _ _)

  coh-preserves-comp-hom-arrow-fiber :
    coherence-square-homotopies
      ( refl-htpy)
      ( coh-hom-arrow
        ( inclusion-fiber f)
        ( inclusion-fiber h)
        ( hom-arrow-fiber f h (comp-hom-arrow f g h β α) b))
      ( coh-hom-arrow
        ( inclusion-fiber f)
        ( inclusion-fiber h)
        ( comp-hom-arrow
          ( inclusion-fiber f)
          ( inclusion-fiber g)
          ( inclusion-fiber h)
          ( hom-arrow-fiber g h β (map-codomain-hom-arrow f g α b))
          ( hom-arrow-fiber f g α b)))
      ( inclusion-fiber h ·l preserves-comp-map-fiber)
  coh-preserves-comp-hom-arrow-fiber p =
    ap
      ( concat _ _)
      ( compute-left-whisker-inclusion-fiber-preserves-comp-map-fiber p)

  preserves-comp-hom-arrow-fiber :
    htpy-hom-arrow
      ( inclusion-fiber f)
      ( inclusion-fiber h)
      ( hom-arrow-fiber f h (comp-hom-arrow f g h β α) b)
      ( comp-hom-arrow
        ( inclusion-fiber f)
        ( inclusion-fiber g)
        ( inclusion-fiber h)
        ( hom-arrow-fiber g h β (map-codomain-hom-arrow f g α b))
        ( hom-arrow-fiber f g α b))
  pr1 preserves-comp-hom-arrow-fiber = preserves-comp-map-fiber
  pr1 (pr2 preserves-comp-hom-arrow-fiber) = refl-htpy
  pr2 (pr2 preserves-comp-hom-arrow-fiber) = coh-preserves-comp-hom-arrow-fiber

The functorial action of fiber preserves homotopies of morphisms of fibers

Given two morphisms of arrows

        α₀
      ------>
    A ------> X
    |   β₀    |
    |         |
  f |  α  β   | g
    |         |
    V   α₁    V
    B ------> Y
      ------>
        β₁

with a homotopy γ : α ~ β of morphisms of arrows, we obtain a commuting diagram of the form

           fiber g (α₁ b)
            ∧     |   \
           /      |    \ (x , q) ↦ (x , q ∙ γ₁ b)
          /       |     \
         /        |      V
  fiber f b --------> fiber g (β₁ b)
        |         |     /
        |         |    /
        |         |   /
        |         |  /
        V         V V
        A -------> X

To show that we have such a commuting diagram, we have to show that the top triangle commutes, and that there is a homotopy filling the diagram:

We first show that the top triangle commutes. To see this, let (a , refl) : fiber f (f a). Then we have to show that

  ((x , q) ↦ (x , q ∙ γ₁ b)) (map-fiber f g α (a , refl)) =
  map-fiber f g β (a , refl)

Simply computing the left-hand side and the right-hand side, we're tasked with constructing an identification

  (α₀ a , ((α a)⁻¹ ∙ refl) ∙ γ₁ (f a)) = (β₀ a , (β a)⁻¹ ∙ refl)

By the characterization of equality in fibers, it suffices to construct identifications

  p : α₀ a = β₀ a
  q : ap g p ∙ ((β a)⁻¹ ∙ refl) = ((α a)⁻¹ ∙ refl) ∙ γ₁ (f a)

The first identification is γ₀ a. To obtain the second identification, we first simplify using the right unit law. I.e., it suffices to construct an identification

  ap g p ∙ (β a)⁻¹ = (α a)⁻¹ ∙ γ₁ (f a).

Now we proceed by transposing equality on both sides, i.e., it suffices to costruct an identification

  α a ∙ ap g p = γ₁ (f a) ∙ β a.

The identification γ a has exactly this type. This completes the construction of the homotopy witnessing that the upper triangle commutes. Since it is constructed as a family of identifications of the form

  eq-Eq-fiber g (γ₀ a) _,

it follows that when we left whisker this homotopy with inclusion-fiber g, we recover the homotopy γ₀ ·r inclusion-fiber f.

Now it remains to fill a coherence for the square of homotopies

                   γ₀ ·r i
                · ---------> ·
                |            |
 coh (tr ∘ α b) |            | coh-hom-arrow-fiber f g β b
    ≐ refl-htpy |            | ≐ refl-htpy
                V            V
                · ---------> ·
                   i ·r H

where H is the homotopy that we just constructed, witnessing that the upper triangle commutes, and where we have written i for all fiber inclusions.

module _
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
  (f : A  B) (g : X  Y) (α β : hom-arrow f g) (γ : htpy-hom-arrow f g α β)
  (b : B)
  where

  htpy-fiber :
    ( tot  x  concat' (g x) (htpy-codomain-htpy-hom-arrow f g α β γ b)) 
      map-fiber f g α b) ~
    ( map-fiber f g β b)
  htpy-fiber (a , refl) =
    eq-Eq-fiber g
      ( map-codomain-hom-arrow f g β (f a))
      ( htpy-domain-htpy-hom-arrow f g α β γ a)
      ( ( ap
          ( concat
            ( ap g (htpy-domain-htpy-hom-arrow f g α β γ a))
            ( map-codomain-hom-arrow f g β (f a)))
          ( right-unit)) 
        ( double-transpose-eq-concat'
          ( htpy-codomain-htpy-hom-arrow f g α β γ (f a))
          ( coh-hom-arrow f g α a)
          ( coh-hom-arrow f g β a)
          ( ap g (htpy-domain-htpy-hom-arrow f g α β γ a))
          ( coh-htpy-hom-arrow f g α β γ a)) 
        ( inv
          ( ap
            ( concat'
              ( g (map-domain-hom-arrow f g α a))
              ( htpy-codomain-htpy-hom-arrow f g α β γ (f a)))
            ( right-unit))))

  compute-left-whisker-inclusion-fiber-htpy-fiber :
    inclusion-fiber g ·l htpy-fiber ~
    htpy-domain-htpy-hom-arrow f g α β γ ·r inclusion-fiber f
  compute-left-whisker-inclusion-fiber-htpy-fiber (a , refl) =
    compute-ap-inclusion-fiber-eq-Eq-fiber g
      ( map-codomain-hom-arrow f g β (f a))
      ( htpy-domain-htpy-hom-arrow f g α β γ a)
      ( _)

  htpy-codomain-htpy-hom-arrow-fiber :
    map-codomain-hom-arrow-fiber f g α b ~
    map-codomain-hom-arrow-fiber f g β b
  htpy-codomain-htpy-hom-arrow-fiber =
    htpy-domain-htpy-hom-arrow f g α β γ

  coh-htpy-hom-arrow-fiber :
    coherence-square-homotopies
      ( htpy-domain-htpy-hom-arrow f g α β γ ·r inclusion-fiber f)
      ( refl-htpy)
      ( refl-htpy)
      ( inclusion-fiber g ·l htpy-fiber)
  coh-htpy-hom-arrow-fiber =
    compute-left-whisker-inclusion-fiber-htpy-fiber ∙h inv-htpy right-unit-htpy

  htpy-hom-arrow-fiber :
    htpy-hom-arrow
      ( inclusion-fiber f)
      ( inclusion-fiber g)
      ( comp-hom-arrow
        ( inclusion-fiber f)
        ( inclusion-fiber g)
        ( inclusion-fiber g)
        ( tr-hom-arrow-inclusion-fiber g
          ( htpy-codomain-htpy-hom-arrow f g α β γ b))
        ( hom-arrow-fiber f g α b))
      ( hom-arrow-fiber f g β b)
  pr1 htpy-hom-arrow-fiber = htpy-fiber
  pr1 (pr2 htpy-hom-arrow-fiber) = htpy-codomain-htpy-hom-arrow-fiber
  pr2 (pr2 htpy-hom-arrow-fiber) = coh-htpy-hom-arrow-fiber

Computing map-fiber-vertical-map-cone of a horizontal pasting of cones

module _
  {l1 l2 l3 l4 l5 l6 : Level}
  {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} {Y : UU l5} {Z : UU l6}
  (i : X  Y) (j : Y  Z) (h : C  Z)
  where

  preserves-pasting-horizontal-map-fiber-vertical-map-cone :
    (c : cone j h B) (d : cone i (vertical-map-cone j h c) A) (x : X) 
    ( map-fiber-vertical-map-cone (j  i) h
      ( pasting-horizontal-cone i j h c d)
      ( x)) ~
    ( map-fiber-vertical-map-cone j h c (i x) 
      map-fiber-vertical-map-cone i (vertical-map-cone j h c) d x)
  preserves-pasting-horizontal-map-fiber-vertical-map-cone c d =
    preserves-comp-map-fiber
      ( vertical-map-cone i (vertical-map-cone j h c) d)
      ( vertical-map-cone j h c)
      ( h)
      ( hom-arrow-cone j h c)
      ( hom-arrow-cone i (vertical-map-cone j h c) d)

Computing map-fiber-vertical-map-cone of a horizontal pasting of cones

Note: There should be a definition of vertical composition of morphisms of arrows, and a proof that hom-arrow-fiber preserves vertical composition.

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

  preserves-pasting-vertical-map-fiber-vertical-map-cone :
    (c : cone f g B) (d : cone (horizontal-map-cone f g c) h A) (x : C) 
    ( ( map-fiber-vertical-map-cone f (g  h)
        ( pasting-vertical-cone f g h c d)
        ( x)) 
      ( map-inv-compute-fiber-comp (pr1 c) (pr1 d) x)) ~
    ( ( map-inv-compute-fiber-comp g h (f x)) 
      ( map-Σ
        ( λ t  fiber h (pr1 t))
        ( map-fiber-vertical-map-cone f g c x)
        ( λ t 
          map-fiber-vertical-map-cone (horizontal-map-cone f g c) h d (pr1 t))))
  preserves-pasting-vertical-map-fiber-vertical-map-cone
    (p , q , H) (p' , q' , H') .(p (p' a))
    ((.(p' a) , refl) , (a , refl)) =
    eq-pair-eq-fiber
      ( ( right-unit) 
        ( distributive-inv-concat (H (p' a)) (ap g (H' a))) 
        ( ap
          ( concat (inv (ap g (H' a))) (f (p (p' a))))
          ( inv right-unit)) 
        ( ap
          ( concat' (g (h (q' a)))
            ( pr2
              ( map-fiber-vertical-map-cone f g
                ( p , q , H)
                ( p (p' a))
                ( p' a , refl))))
          ( ( inv (ap-inv g (H' a))) 
            ( ap² g (inv right-unit)))))

See also

  • In retracts of maps, we show that if g is a retract of g', then the fibers of g are retracts of the fibers of g'.

Table of files about fibers of maps

The following table lists files that are about fibers of maps as a general concept.

ConceptFile
Fibers of maps (foundation-core)foundation-core.fibers-of-maps
Fibers of maps (foundation)foundation.fibers-of-maps
Equality in the fibers of a mapfoundation.equality-fibers-of-maps
Functoriality of fibers of mapsfoundation.functoriality-fibers-of-maps
Fibers of pointed mapsstructured-types.fibers-of-pointed-maps
Fibers of maps of finite typesunivalent-combinatorics.fibers-of-maps
The universal property of the family of fibers of mapsfoundation.universal-property-family-of-fibers-of-maps

Recent changes