Theorems · Definition · category theory

CategoryTheory.Limits.Bicone.toCone

{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.Cone (CategoryTheory.Discrete.functor F)

A shorthand for toConeFunctor.obj

Defined in: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Cited by: 17 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.Conestatement · cited by 710
CategoryTheory.Discrete.functorstatement · cited by 633
CategoryTheory.Limits.Biconestatement and proof · cited by 75
CategoryTheory.Limits.Bicone.toConeFunctorproof · cited by 0

Cited by31

Results whose statement or proof uses this declaration.

CategoryTheory.Limits.biproduct.mapproof · cited by 24
CategoryTheory.Limits.Bicone.IsBilimit.isLimitstatement · cited by 9
CategoryTheory.Limits.biproduct.isLimitstatement · cited by 9
CategoryTheory.Limits.biproduct.map_πproof · cited by 5
CategoryTheory.Limits.Bicone.whiskerIsBilimitIffproof · cited by 2
CategoryTheory.Limits.preservesBiproduct_of_preservesProductproof · 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.isBilimitOfIsLimitstatement and proof · cited by 1
CategoryTheory.Limits.isBilimitOfTotalproof · cited by 1
CategoryTheory.Limits.biproduct.map_eq_map'proof · cited by 1