Theorems · Definition · category theory

CategoryTheory.Limits.Bicone.toCocone

{J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {F : J → C} → CategoryTheory.Limits.Bicone F → CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor F)

A shorthand for toCoconeFunctor.obj

Defined in: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Cited by: 15 results in Mathlib
Foundations: Depth 29 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category CategoryTheory.Limits.HasZeroMorphisms

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites8

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.Limits.HasZeroMorphismsstatement and proof · cited by 3,275
CategoryTheory.Discretestatement · cited by 2,447
CategoryTheory.Limits.Coconestatement · cited by 746
CategoryTheory.Discrete.functorstatement · cited by 633
CategoryTheory.Limits.Biconestatement and proof · cited by 75
CategoryTheory.Limits.Bicone.toCoconeFunctorproof · cited by 0

Cited by29

Results whose statement or proof uses this declaration.

CategoryTheory.Limits.Bicone.IsBilimit.isColimitstatement · cited by 6
CategoryTheory.Limits.biproduct.isColimitstatement · cited by 5
CategoryTheory.Limits.biproduct.ι_mapproof · cited by 4
CategoryTheory.Limits.Bicone.whiskerIsBilimitIffproof · cited by 2
CategoryTheory.Limits.Bicone.IsBilimit.mk.injstatement and proof · cited by 1
CategoryTheory.Limits.Bicone.IsBilimit.mk.noConfusionstatement and proof · cited by 1
CategoryTheory.Limits.Bicone.IsBilimit.extstatement and proof · cited by 1
CategoryTheory.Limits.biproduct.map'proof · cited by 1
CategoryTheory.Limits.isBilimitOfIsColimitstatement and proof · cited by 1
CategoryTheory.Limits.isBilimitOfTotalproof · cited by 1
CategoryTheory.Limits.biproduct.map_eq_map'proof · cited by 1
CategoryTheory.Limits.preservesBinaryBiproduct_of_preservesBiproductproof · cited by 1