Documentation

Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer

Preservation of multicoequalizers #

Let J : MultispanShape and d : MultispanIndex J C. If F : C ⥤ D, we define d.map F : MultispanIndex J D and an isomorphism of functors (d.map F).multispan ≅ d.multispan ⋙ F (see MultispanIndex.multispanMapIso). If c : Multicofork d, we define c.map F : Multicofork (d.map F) and obtain a bijection IsColimit (F.mapCocone c) ≃ IsColimit (c.map F) (see Multicofork.isColimitMapEquiv). As a result, if F preserves the colimit of d.multispan, we deduce that if c is a colimit, then c.map F also is (see Multicofork.isColimitMapOfPreserves).

The multispan index obtained by applying a functor.

Equations
  • d.map F = { left := fun (i : J.L) => F.obj (d.left i), right := fun (i : J.R) => F.obj (d.right i), fst := fun (i : J.L) => F.map (d.fst i), snd := fun (i : J.L) => F.map (d.snd i) }
Instances For
    @[simp]
    theorem CategoryTheory.Limits.MultispanIndex.map_left {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {J : MultispanShape} (d : MultispanIndex J C) (F : Functor C D) (i : J.L) :
    (d.map F).left i = F.obj (d.left i)
    @[simp]
    theorem CategoryTheory.Limits.MultispanIndex.map_fst {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {J : MultispanShape} (d : MultispanIndex J C) (F : Functor C D) (i : J.L) :
    (d.map F).fst i = F.map (d.fst i)
    @[simp]
    theorem CategoryTheory.Limits.MultispanIndex.map_right {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {J : MultispanShape} (d : MultispanIndex J C) (F : Functor C D) (i : J.R) :
    (d.map F).right i = F.obj (d.right i)
    @[simp]
    theorem CategoryTheory.Limits.MultispanIndex.map_snd {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {J : MultispanShape} (d : MultispanIndex J C) (F : Functor C D) (i : J.L) :
    (d.map F).snd i = F.map (d.snd i)

    If d : MultispanIndex J C and F : C ⥤ D, this is the obvious isomorphism (d.map F).multispan ≅ d.multispan ⋙ F.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      If d : MultispanIndex J C, c : Multicofork d and F : C ⥤ D, this is the induced multicofork of d.map F.

      Equations
      Instances For
        @[simp]
        @[simp]
        theorem CategoryTheory.Limits.Multicofork.map_ι_app {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {J : MultispanShape} {d : MultispanIndex J C} (c : Multicofork d) (F : Functor C D) (x : WalkingMultispan J) :
        (c.map F).ι.app x = match x with | WalkingMultispan.left a => CategoryStruct.comp (F.map (d.fst a)) (F.map (c.π (J.fst a))) | WalkingMultispan.right a => F.map (c.π a)

        If d : MultispanIndex J C, c : Multicofork d and F : C ⥤ D, the cocone F.mapCocone c is colimit iff the multicofork c.map F is.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          If d : MultispanIndex J C, c : Multicofork d is a colimit multicofork, and F : C ⥤ D is a functor which preserves the colimit of d.multispan, then the multicofork c.map F is colimit.

          Equations
          Instances For