Mathlib Map

Theorems · Definition · category theory

CategoryTheory.Limits.biprod.inr

{C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} → [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] → Y ⟶ X ⊞ Y

The inclusion into the second summand of a binary biproduct.

Defined in
Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Cited by
109 results in Mathlib
Foundations
Depth 7 from the axioms, rests on 18 definitions · uses Classical.choice
Assumes
CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsCategoryTheory.Limits.HasBinaryBiproduct
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

HomologicalComplex.homotopyCofiber.inrX · cited by 33homotopyCofiber.inrXCategoryTheory.Limits.biprod.hom_ext' · cited by 30biprod.hom_ext'CategoryTheory.Limits.biprod.inr_desc · cited by 18biprod.inr_descCategoryTheory.Biprod.ofComponents · cited by 10Biprod.ofComponentsHomologicalComplex.cylinder.ι₁ · cited by 9cylinder.ι₁CategoryTheory.Limits.pointwiseBinaryBicone · cited by 9Limits.pointwiseBinaryBic…CategoryTheory.Functor.biprodComparison' · cited by 9Functor.biprodComparison'HomologicalComplex.homotopyCofiber.inrX_sndX · cited by 8homotopyCofiber.inrX_sndXCategoryTheory.Limits.biprod.inr_desc_assoc · cited by 7biprod.inr_desc_assocCategoryTheory.Limits.biprod.lift_desc · cited by 7biprod.lift_descHomologicalComplex.homotopyCofiber.inrX_fstX · cited by 7homotopyCofiber.inrX_fstXCategoryTheory.Abelian.Ext.biprodAddEquiv · cited by 5Ext.biprodAddEquivHomologicalComplex.cylinder.ι₁_desc · cited by 4cylinder.ι₁_descCategoryTheory.Limits.biprod.inr_fst · cited by 4biprod.inr_fstCategoryTheory.Limits.biprod.inr_snd · cited by 4biprod.inr_sndCategoryTheory.Category · cited by 32673CategoryTheory.CategoryQuiver.Hom · cited by 32603Quiver.HomCategoryTheory.Limits.HasZeroMorphisms · cited by 3275Limits.HasZeroMorphismsCategoryTheory.Limits.biprod · cited by 312Limits.biprodCategoryTheory.Limits.HasBinaryBiproduct · cited by 251Limits.HasBinaryBiproductCategoryTheory.Limits.BinaryBiproduct.bicone · cited by 68BinaryBiproduct.biconeCategoryTheory.Limits.BinaryBicone.inr · cited by 47BinaryBicone.inrbiprod.inrCITED BYCITES

Cites7

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

Cited by130

Results whose statement or proof uses this declaration.