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).

def CategoryTheory.Limits.MulticospanIndex.map {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {J : MulticospanShape} (d : MulticospanIndex J C) (F : Functor C D) : MulticospanIndex J D

The multicospan 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.R) => F.map (d.fst i), snd := fun (i : J.R) => F.map (d.snd i) }

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.map_fst {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {J : MulticospanShape} (d : MulticospanIndex J C) (F : Functor C D) (i : J.R) : (d.map F).fst i = F.map (d.fst i)

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.map_left {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {J : MulticospanShape} (d : MulticospanIndex J C) (F : Functor C D) (i : J.L) : (d.map F).left i = F.obj (d.left i)

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.map_right {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {J : MulticospanShape} (d : MulticospanIndex J C) (F : Functor C D) (i : J.R) : (d.map F).right i = F.obj (d.right i)

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.map_snd {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {J : MulticospanShape} (d : MulticospanIndex J C) (F : Functor C D) (i : J.R) : (d.map F).snd i = F.map (d.snd i)

def CategoryTheory.Limits.MulticospanIndex.multicospanMapIso {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {J : MulticospanShape} (d : MulticospanIndex J C) (F : Functor C D) : (d.map F).multicospan ≅ d.multicospan.comp F

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

Equations

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

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multicospanMapIso_inv_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {J : MulticospanShape} (d : MulticospanIndex J C) (F : Functor C D) (X : WalkingMulticospan J) : (d.multicospanMapIso F).inv.app X = (match X with | WalkingMulticospan.left a => Iso.refl (F.obj (d.left a)) | WalkingMulticospan.right a => Iso.refl (F.obj (d.right a))).inv

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multicospanMapIso_hom_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {J : MulticospanShape} (d : MulticospanIndex J C) (F : Functor C D) (X : WalkingMulticospan J) : (d.multicospanMapIso F).hom.app X = (match X with | WalkingMulticospan.left a => Iso.refl (F.obj (d.left a)) | WalkingMulticospan.right a => Iso.refl (F.obj (d.right a))).hom

def CategoryTheory.Limits.Multifork.map {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {J : MulticospanShape} {d : MulticospanIndex J C} (c : Multifork d) (F : Functor C D) : Multifork (d.map F)

If d : MulticospanIndex J C, c : Multifork d and F : C ⥤ D, this is the induced multifork of d.map F.

Equations

• c.map F = CategoryTheory.Limits.Multifork.ofι (d.map F) (F.obj c.pt) (fun (i : J.L) => F.map (c.ι i)) ⋯

@[simp]

theorem CategoryTheory.Limits.Multifork.map_π_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {J : MulticospanShape} {d : MulticospanIndex J C} (c : Multifork d) (F : Functor C D) (x : WalkingMulticospan J) : (c.map F).π.app x = match x with | WalkingMulticospan.left a => F.map (c.ι a) | WalkingMulticospan.right b => CategoryStruct.comp (F.map (c.ι (J.fst b))) (F.map (d.fst b))

@[simp]

theorem CategoryTheory.Limits.Multifork.map_pt {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {J : MulticospanShape} {d : MulticospanIndex J C} (c : Multifork d) (F : Functor C D) : (c.map F).pt = F.obj c.pt

def CategoryTheory.Limits.Multifork.isLimitMapEquiv {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {J : MulticospanShape} {d : MulticospanIndex J C} (c : Multifork d) (F : Functor C D) : IsLimit (F.mapCone c) ≃ IsLimit (c.map F)

If d : MulticospanIndex J C, c : Multifork d and F : C ⥤ D, the cone F.mapCone c is limiting iff the multifork c.map F is.

Equations

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

noncomputable def CategoryTheory.Limits.Multifork.isLimitMapOfPreserves {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {J : MulticospanShape} {d : MulticospanIndex J C} (c : Multifork d) (F : Functor C D) [PreservesLimit d.multicospan F] (hc : IsLimit c) : IsLimit (c.map F)

If d : MulticospanIndex J C, c : Multifork d is a limit multifork, and F : C ⥤ D is a functor which preserves the limit of d.multicospan, then the multifork c.map F is limiting.

Equations

• c.isLimitMapOfPreserves F hc = (c.isLimitMapEquiv F) (CategoryTheory.Limits.isLimitOfPreserves F hc)

def CategoryTheory.Limits.MultispanIndex.map {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {J : MultispanShape} (d : MultispanIndex J C) (F : Functor C D) : MultispanIndex J D

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) }

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.map_snd {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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)

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.map_left {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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_right {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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_fst {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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)

def CategoryTheory.Limits.MultispanIndex.multispanMapIso {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {J : MultispanShape} (d : MultispanIndex J C) (F : Functor C D) : (d.map F).multispan ≅ d.multispan.comp F

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.

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multispanMapIso_inv_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {J : MultispanShape} (d : MultispanIndex J C) (F : Functor C D) (X : WalkingMultispan J) : (d.multispanMapIso F).inv.app X = (match X with | WalkingMultispan.left a => Iso.refl (F.obj (d.left a)) | WalkingMultispan.right a => Iso.refl (F.obj (d.right a))).inv

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multispanMapIso_hom_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {J : MultispanShape} (d : MultispanIndex J C) (F : Functor C D) (X : WalkingMultispan J) : (d.multispanMapIso F).hom.app X = (match X with | WalkingMultispan.left a => Iso.refl (F.obj (d.left a)) | WalkingMultispan.right a => Iso.refl (F.obj (d.right a))).hom

def CategoryTheory.Limits.Multicofork.map {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {J : MultispanShape} {d : MultispanIndex J C} (c : Multicofork d) (F : Functor C D) : Multicofork (d.map F)

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

Equations

• c.map F = CategoryTheory.Limits.Multicofork.ofπ (d.map F) (F.obj c.pt) (fun (i : J.R) => F.map (c.π i)) ⋯

@[simp]

theorem CategoryTheory.Limits.Multicofork.map_ι_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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)

@[simp]

theorem CategoryTheory.Limits.Multicofork.map_pt {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {J : MultispanShape} {d : MultispanIndex J C} (c : Multicofork d) (F : Functor C D) : (c.map F).pt = F.obj c.pt

def CategoryTheory.Limits.Multicofork.isColimitMapEquiv {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {J : MultispanShape} {d : MultispanIndex J C} (c : Multicofork d) (F : Functor C D) : IsColimit (F.mapCocone c) ≃ IsColimit (c.map F)

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.

noncomputable def CategoryTheory.Limits.Multicofork.isColimitMapOfPreserves {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {J : MultispanShape} {d : MultispanIndex J C} (c : Multicofork d) (F : Functor C D) [PreservesColimit d.multispan F] (hc : IsColimit c) : IsColimit (c.map F)

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

• c.isColimitMapOfPreserves F hc = (c.isColimitMapEquiv F) (CategoryTheory.Limits.isColimitOfPreserves F hc)