Mathlib Map

Theorems · Definition · category theory

CategoryTheory.Limits.BinaryBiconeMorphism.hom

{C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} →
        {A B : CategoryTheory.Limits.BinaryBicone P Q} → CategoryTheory.Limits.BinaryBiconeMorphism A B → (A.pt ⟶ B.pt)

A morphism between the two vertex objects of the bicones

Defined in
Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Cited by
17 results in Mathlib
Foundations
Depth 4 from the axioms · uses no axioms
Assumes
CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphisms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

CategoryTheory.Limits.BinaryBicones.functoriality · cited by 7BinaryBicones.functoriali…CategoryTheory.Limits.BinaryBicone.toBiconeFunctor · cited by 4BinaryBicone.toBiconeFunc…CategoryTheory.Limits.BinaryBiconeMorphism.ext · cited by 1BinaryBiconeMorphism.extCategoryTheory.Limits.BinaryBiconeMorphism.wfst · cited by 1BinaryBiconeMorphism.wfstCategoryTheory.Limits.BinaryBiconeMorphism.winl · cited by 1BinaryBiconeMorphism.winlCategoryTheory.Limits.BinaryBiconeMorphism.winr · cited by 1BinaryBiconeMorphism.winrCategoryTheory.Limits.BinaryBiconeMorphism.wsnd · cited by 1BinaryBiconeMorphism.wsndCategoryTheory.Limits.BinaryBiconeMorphism.ext_iff · cited by 0BinaryBiconeMorphism.ext_…CategoryTheory.Limits.BinaryBiconeMorphism.wfst_assoc · cited by 0BinaryBiconeMorphism.wfst…CategoryTheory.Limits.BinaryBiconeMorphism.winl_assoc · cited by 0BinaryBiconeMorphism.winl…CategoryTheory.Limits.BinaryBiconeMorphism.winr_assoc · cited by 0BinaryBiconeMorphism.winr…CategoryTheory.Limits.BinaryBiconeMorphism.wsnd_assoc · cited by 0BinaryBiconeMorphism.wsnd…CategoryTheory.Limits.BinaryBicones.ext_hom_hom · cited by 0BinaryBicones.ext_hom_homCategoryTheory.Limits.BinaryBicones.ext_inv_hom · cited by 0BinaryBicones.ext_inv_homCategoryTheory.Limits.BinaryBicones.functoriality_map_hom · cited by 0BinaryBicones.functoriali…CategoryTheory.Category · cited by 32673CategoryTheory.CategoryQuiver.Hom · cited by 32603Quiver.HomCategoryTheory.Limits.HasZeroMorphisms · cited by 3275Limits.HasZeroMorphismsCategoryTheory.Limits.BinaryBicone · cited by 111Limits.BinaryBiconeCategoryTheory.Limits.BinaryBicone.pt · cited by 95BinaryBicone.ptCategoryTheory.Limits.BinaryBiconeMorphism · cited by 13Limits.BinaryBiconeMorphi…BinaryBiconeMorphism.homCITED BYCITES

Cites6

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

Cited by19

Results whose statement or proof uses this declaration.