Colon

📁 Source: Mathlib/CategoryTheory/Abelian/Preradical/Colon.lean

Statistics

Metric	Count
Definitions colon, colonπ, instEpiFunctorπ, isColimitCokernelCofork, isColimitCokernelCoforkObj, isLimitKernelFork, isLimitKernelForkObj, quotient, shortComplex, shortComplexObj, toColon, π	12
Theorems colon_ι_app_π_app, colon_ι_app_π_app_assoc, instEpiAppColonπ, instEpiFunctorColonπ, instEpiFunctorGShortComplex, instEpiGShortComplexObj, instMonoFShortComplexObj, instMonoFunctorFShortComplex, isIso_toColon_hom_left_app_iff, isIso_toColon_iff, isPullback_colon, isPullback_colon_obj, shortComplexObj_X₁, shortComplexObj_X₂, shortComplexObj_X₃, shortComplexObj_f, shortComplexObj_g, shortComplex_X₁, shortComplex_X₂, shortComplex_X₃, shortComplex_f, shortComplex_g, shortExact_shortComplex, shortExact_shortComplexObj, toColon_hom_left_app_colon_ι_app, toColon_hom_left_app_colon_ι_app_assoc, toColon_hom_left_app_colonπ_app, toColon_hom_left_app_colonπ_app_assoc, toColon_hom_left_colonπ, toColon_hom_left_colonπ_assoc, ι_π, ι_π_app, ι_π_app_assoc, ι_π_assoc	34
Total	46

CategoryTheory.Abelian.Preradical

Definitions

Name	Category	Theorems
colon 📖	CompOp	16 math math: colon_ι_app_π_app, isPullback_colon_obj, instEpiAppColonπ, toColon_hom_left_app_colon_ι_app_assoc, instEpiFunctorColonπ, toColon_hom_left_colonπ_assoc, toColon_hom_left_colonπ, isRadical_iff_isIso, isIso_toColon_hom_left_app_iff, toColon_hom_left_app_colonπ_app_assoc, CategoryTheory.Abelian.Radical.instIsIsoPreradicalToColonObjIsRadical, toColon_hom_left_app_colon_ι_app, colon_ι_app_π_app_assoc, isPullback_colon, isIso_toColon_iff, toColon_hom_left_app_colonπ_app
colonπ 📖	CompOp	10 math math: colon_ι_app_π_app, isPullback_colon_obj, instEpiAppColonπ, instEpiFunctorColonπ, toColon_hom_left_colonπ_assoc, toColon_hom_left_colonπ, toColon_hom_left_app_colonπ_app_assoc, colon_ι_app_π_app_assoc, isPullback_colon, toColon_hom_left_app_colonπ_app
instEpiFunctorπ 📖	CompOp	—
isColimitCokernelCofork 📖	CompOp	—
isColimitCokernelCoforkObj 📖	CompOp	—
isLimitKernelFork 📖	CompOp	—
isLimitKernelForkObj 📖	CompOp	—
quotient 📖	CompOp	21 math math: colon_ι_app_π_app, isPullback_colon_obj, instEpiAppColonπ, isRadical_iff_isZero, ι_π_assoc, instEpiFunctorColonπ, toColon_hom_left_colonπ_assoc, ι_π, toColon_hom_left_colonπ, isIso_toColon_hom_left_app_iff, toColon_hom_left_app_colonπ_app_assoc, shortComplexObj_g, ι_π_app, colon_ι_app_π_app_assoc, isPullback_colon, shortComplex_X₃, shortComplexObj_X₃, ι_π_app_assoc, CategoryTheory.Abelian.Radical.isZero, isIso_toColon_iff, toColon_hom_left_app_colonπ_app
shortComplex 📖	CompOp	8 math math: shortComplex_X₁, shortComplex_g, shortComplex_X₂, instEpiFunctorGShortComplex, shortComplex_f, instMonoFunctorFShortComplex, shortComplex_X₃, shortExact_shortComplex
shortComplexObj 📖	CompOp	8 math math: instEpiGShortComplexObj, instMonoFShortComplexObj, shortComplexObj_X₂, shortExact_shortComplexObj, shortComplexObj_X₁, shortComplexObj_f, shortComplexObj_g, shortComplexObj_X₃
toColon 📖	CompOp	10 math math: toColon_hom_left_app_colon_ι_app_assoc, toColon_hom_left_colonπ_assoc, toColon_hom_left_colonπ, isRadical_iff_isIso, isIso_toColon_hom_left_app_iff, toColon_hom_left_app_colonπ_app_assoc, CategoryTheory.Abelian.Radical.instIsIsoPreradicalToColonObjIsRadical, toColon_hom_left_app_colon_ι_app, isIso_toColon_iff, toColon_hom_left_app_colonπ_app
π 📖	CompOp	10 math math: shortComplex_g, colon_ι_app_π_app, isPullback_colon_obj, ι_π_assoc, ι_π, shortComplexObj_g, ι_π_app, colon_ι_app_π_app_assoc, isPullback_colon, ι_π_app_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
colon_ι_app_π_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj r colon CategoryTheory.Functor.id quotient CategoryTheory.NatTrans.app ι π CategoryTheory.Functor.comp colonπ	—	CategoryTheory.CommSq.w CategoryTheory.IsPullback.toCommSq isPullback_colon_obj
colon_ι_app_π_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj r colon CategoryTheory.NatTrans.app CategoryTheory.Functor.id ι quotient π CategoryTheory.Functor.comp colonπ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' colon_ι_app_π_app
instEpiAppColonπ 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Functor.obj r colon CategoryTheory.Functor.comp quotient CategoryTheory.NatTrans.app colonπ	—	CategoryTheory.instEpiAppOfFunctor CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Abelian.hasFiniteColimits instEpiFunctorColonπ
instEpiFunctorColonπ 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Functor CategoryTheory.Functor.category r colon CategoryTheory.Functor.comp quotient colonπ	—	CategoryTheory.Abelian.epi_pullback_of_epi_f CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.instHasFiniteLimitsFunctor CategoryTheory.Abelian.hasFiniteLimits
instEpiFunctorGShortComplex 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	—	—
instEpiGShortComplexObj 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplexObj CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	—	CategoryTheory.instEpiAppOfFunctor CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Abelian.hasFiniteColimits
instMonoFShortComplexObj 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplexObj CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f	—	CategoryTheory.instMonoAppOfFunctor CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Abelian.hasFiniteLimits CategoryTheory.MonoOver.mono
instMonoFunctorFShortComplex 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.ShortComplex.X₁ CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f	—	CategoryTheory.MonoOver.mono
isIso_toColon_hom_left_app_iff 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono colon CategoryTheory.NatTrans.app CategoryTheory.CommaMorphism.left CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory toColon CategoryTheory.Limits.IsZero r quotient	—	CategoryTheory.Limits.IsZero.of_epi_eq_zero instEpiAppColonπ CategoryTheory.Limits.zero_of_epi_comp CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso toColon_hom_left_app_colonπ_app ι_π_app colon_ι_app_π_app CategoryTheory.Limits.IsZero.eq_zero_of_tgt CategoryTheory.Limits.zero_comp CategoryTheory.cancel_mono CategoryTheory.instMonoAppOfFunctor CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Abelian.hasFiniteLimits CategoryTheory.MonoOver.mono CategoryTheory.Category.assoc toColon_hom_left_app_colon_ι_app CategoryTheory.Category.id_comp
isIso_toColon_iff 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Abelian.Preradical CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.instCategoryOver CategoryTheory.Over.isMono colon toColon CategoryTheory.Limits.IsZero CategoryTheory.Functor.comp quotient r	—	CategoryTheory.Functor.isZero_iff CategoryTheory.Abelian.hasZeroObject isIso_toColon_hom_left_app_iff
isPullback_colon 📖	mathematical	—	CategoryTheory.IsPullback CategoryTheory.Functor CategoryTheory.Functor.category r colon CategoryTheory.Functor.id CategoryTheory.Functor.comp quotient ι colonπ π CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.hom CategoryTheory.Functor.rightUnitor	—	CategoryTheory.IsPullback.of_hasPullback
isPullback_colon_obj 📖	mathematical	—	CategoryTheory.IsPullback CategoryTheory.Functor.obj r colon CategoryTheory.Functor.id CategoryTheory.Functor.comp quotient CategoryTheory.NatTrans.app ι colonπ π	—	CategoryTheory.Category.comp_id CategoryTheory.IsPullback.map CategoryTheory.Limits.evaluation_preservesLimit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Abelian.hasFiniteLimits isPullback_colon
shortComplexObj_X₁ 📖	mathematical	—	CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplexObj CategoryTheory.Functor.obj r	—	—
shortComplexObj_X₂ 📖	mathematical	—	CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplexObj CategoryTheory.Functor.obj CategoryTheory.Functor.id	—	—
shortComplexObj_X₃ 📖	mathematical	—	CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplexObj CategoryTheory.Functor.obj quotient	—	—
shortComplexObj_f 📖	mathematical	—	CategoryTheory.ShortComplex.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplexObj CategoryTheory.NatTrans.app r CategoryTheory.Functor.id ι	—	—
shortComplexObj_g 📖	mathematical	—	CategoryTheory.ShortComplex.g CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplexObj CategoryTheory.NatTrans.app CategoryTheory.Functor.id quotient π	—	—
shortComplex_X₁ 📖	mathematical	—	CategoryTheory.ShortComplex.X₁ CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex r	—	—
shortComplex_X₂ 📖	mathematical	—	CategoryTheory.ShortComplex.X₂ CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.Functor.id	—	—
shortComplex_X₃ 📖	mathematical	—	CategoryTheory.ShortComplex.X₃ CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex quotient	—	—
shortComplex_f 📖	mathematical	—	CategoryTheory.ShortComplex.f CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex ι	—	—
shortComplex_g 📖	mathematical	—	CategoryTheory.ShortComplex.g CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex π	—	—
shortExact_shortComplex 📖	mathematical	—	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex	—	CategoryTheory.ShortComplex.exact_of_g_is_cokernel CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian instMonoFunctorFShortComplex instEpiFunctorGShortComplex
shortExact_shortComplexObj 📖	mathematical	—	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplexObj	—	CategoryTheory.ShortComplex.ShortExact.exact CategoryTheory.Functor.preservesZeroMorphisms_evaluation_obj CategoryTheory.ShortComplex.ShortExact.map_of_exact shortExact_shortComplex CategoryTheory.Limits.instPreservesFiniteLimitsFunctorObjEvaluationOfHasFiniteLimits CategoryTheory.Abelian.hasFiniteLimits CategoryTheory.Limits.instPreservesFiniteColimitsFunctorObjEvaluationOfHasFiniteColimits CategoryTheory.Abelian.hasFiniteColimits instMonoFShortComplexObj instEpiGShortComplexObj
toColon_hom_left_app_colon_ι_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono colon CategoryTheory.NatTrans.app CategoryTheory.CommaMorphism.left CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory toColon r ι	—	CategoryTheory.NatTrans.comp_app CategoryTheory.Over.w
toColon_hom_left_app_colon_ι_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono colon CategoryTheory.NatTrans.app CategoryTheory.CommaMorphism.left CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory toColon r ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toColon_hom_left_app_colon_ι_app
toColon_hom_left_app_colonπ_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono colon CategoryTheory.Functor.comp quotient r CategoryTheory.NatTrans.app CategoryTheory.CommaMorphism.left CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory toColon colonπ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.NatTrans.congr_app toColon_hom_left_colonπ
toColon_hom_left_app_colonπ_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono colon CategoryTheory.NatTrans.app CategoryTheory.CommaMorphism.left CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory toColon r quotient CategoryTheory.Functor.comp colonπ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toColon_hom_left_app_colonπ_app
toColon_hom_left_colonπ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono colon CategoryTheory.Functor.comp quotient r CategoryTheory.CommaMorphism.left CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory toColon colonπ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.instZeroHomFunctor CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.IsPullback.lift_snd isPullback_colon
toColon_hom_left_colonπ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono colon CategoryTheory.CommaMorphism.left CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory toColon CategoryTheory.Functor.comp quotient r colonπ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.instZeroHomFunctor CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toColon_hom_left_colonπ
ι_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category r CategoryTheory.Functor.id quotient ι π Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.instZeroHomFunctor CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.Limits.cokernel.condition
ι_π_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj r CategoryTheory.Functor.id quotient CategoryTheory.NatTrans.app ι π Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	ι_π
ι_π_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj r CategoryTheory.NatTrans.app CategoryTheory.Functor.id ι quotient π Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_π_app
ι_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category r CategoryTheory.Functor.id ι quotient π Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.instZeroHomFunctor CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_π

---

← Back to Index