Theorems · Definition · category theory

CategoryTheory.Limits.MulticospanIndex.map

{C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {J : CategoryTheory.Limits.MulticospanShape} →
          CategoryTheory.Limits.MulticospanIndex J C →
            CategoryTheory.Functor C D → CategoryTheory.Limits.MulticospanIndex J D

The multicospan index obtained by applying a functor.

Defined in: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
Cited by: 8 results in Mathlib
Foundations: Depth 4 from the axioms · uses no axioms
Assumes: CategoryTheory.Category CategoryTheory.Category

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites12

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
CategoryTheory.Functor.objproof · cited by 19,642
CategoryTheory.Functorstatement and proof · cited by 16,252
CategoryTheory.Functor.mapproof · cited by 8,698
CategoryTheory.Limits.MulticospanShapestatement and proof · cited by 160
CategoryTheory.Limits.MulticospanShape.Lproof · cited by 135
CategoryTheory.Limits.MulticospanShape.Rproof · cited by 124
CategoryTheory.Limits.MulticospanIndex.leftproof · cited by 119
CategoryTheory.Limits.MulticospanIndexstatement and proof · cited by 101
CategoryTheory.Limits.MulticospanIndex.rightproof · cited by 77
CategoryTheory.Limits.MulticospanIndex.fstproof · cited by 39
CategoryTheory.Limits.MulticospanIndex.sndproof · cited by 35

Cited by12

Results whose statement or proof uses this declaration.

CategoryTheory.Limits.Multifork.mapstatement and proof · cited by 2
CategoryTheory.Limits.MulticospanIndex.multicospanMapIsostatement and proof · cited by 2
CategoryTheory.Limits.Multifork.isLimitMapEquivstatement · cited by 0
CategoryTheory.Limits.Multifork.isLimitMapOfPreservesstatement · cited by 0
CategoryTheory.Limits.Multifork.map_ptstatement · cited by 0
CategoryTheory.Limits.Multifork.map_π_appstatement · cited by 0
CategoryTheory.Limits.MulticospanIndex.map_fststatement and proof · cited by 0
CategoryTheory.Limits.MulticospanIndex.map_leftstatement and proof · cited by 0
CategoryTheory.Limits.MulticospanIndex.map_rightstatement and proof · cited by 0
CategoryTheory.Limits.MulticospanIndex.map_sndstatement and proof · cited by 0
CategoryTheory.Limits.MulticospanIndex.multicospanMapIso_hom_appstatement · cited by 0
CategoryTheory.Limits.MulticospanIndex.multicospanMapIso_inv_appstatement · cited by 0