AbelianSubcategory

📁 Source: Mathlib/CategoryTheory/Triangulated/TStructure/AbelianSubcategory.lean

Statistics

Metric	Count
Definitions abelian, admissibleMorphism, isColimitCokernelCofork, isColimitCokernelCoforkOfDistTriang, isLimitKernelFork, isLimitKernelForkOfDistTriang, ιK, πQ	8
Theorems epi_πQ, eq_zero_of_hom_shift_pos, exists_desc_πQ, exists_distinguished_triangle_of_epi, exists_lift_ιK, hasCokernel, hasCokernel_of_admissibleMorphism, hasKernel, hasKernel_of_admissibleMorphism, mono_ιK, mor₁_πQ, mor₁_πQ_assoc, shift_ι_map_ιK, shift_ι_map_ιK_assoc, ιK_mor₁, ιK_mor₁_assoc, ι_map_πQ, ι_map_πQ_assoc	18
Total	26

CategoryTheory.Triangulated.AbelianSubcategory

Definitions

Name	Category	Theorems
abelian 📖	CompOp	—
admissibleMorphism 📖	CompOp	—
isColimitCokernelCofork 📖	CompOp	—
isColimitCokernelCoforkOfDistTriang 📖	CompOp	—
isLimitKernelFork 📖	CompOp	—
isLimitKernelForkOfDistTriang 📖	CompOp	—
ιK 📖	CompOp	6 math math: ιK_mor₁_assoc, exists_lift_ιK, ιK_mor₁, shift_ι_map_ιK_assoc, mono_ιK, shift_ι_map_ιK
πQ 📖	CompOp	6 math math: epi_πQ, mor₁_πQ, ι_map_πQ_assoc, exists_desc_πQ, mor₁_πQ_assoc, ι_map_πQ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi_πQ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Functor.map	CategoryTheory.Epi πQ	—	CategoryTheory.Preadditive.epi_iff_cancel_zero CategoryTheory.Functor.congr_map CategoryTheory.Pretriangulated.Triangle.yoneda_exact₃ CategoryTheory.Functor.map_comp ι_map_πQ CategoryTheory.Category.assoc CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_full CategoryTheory.Limits.comp_zero eq_zero_of_hom_shift_pos CategoryTheory.Functor.map_injective CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.NatIso.hom_app_isIso
eq_zero_of_hom_shift_pos 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	CategoryTheory.Functor.map_injective CategoryTheory.Functor.IsEquivalence.faithful CategoryTheory.instIsEquivalenceShiftFunctor CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.NatIso.hom_app_isIso CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Limits.comp_zero
exists_desc_πQ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Functor.map CategoryTheory.CategoryStruct.comp	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp πQ	—	CategoryTheory.Pretriangulated.Triangle.yoneda_exact₂ CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_full eq_zero_of_hom_shift_pos CategoryTheory.Functor.map_injective ι_map_πQ CategoryTheory.Functor.map_preimage CategoryTheory.Category.assoc
exists_distinguished_triangle_of_epi 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms admissibleMorphism Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Functor.map	—	CategoryTheory.Pretriangulated.distinguished_cocone_triangle CategoryTheory.Limits.Cofork.IsColimit.hom_ext mor₁_πQ CategoryTheory.Category.comp_id CategoryTheory.Limits.comp_zero CategoryTheory.cancel_epi CategoryTheory.Pretriangulated.Triangle.isZero₃_iff_isIso₁ CategoryTheory.Limits.IsZero.iff_id_eq_zero CategoryTheory.Functor.map_id CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Pretriangulated.rotate_distinguished_triangle CategoryTheory.Pretriangulated.isomorphic_distinguished CategoryTheory.Category.id_comp CategoryTheory.Category.assoc CategoryTheory.IsIso.inv_hom_id CategoryTheory.Functor.map_neg shift_ι_map_ιK neg_neg
exists_lift_ιK 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Functor.map CategoryTheory.CategoryStruct.comp	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp ιK	—	CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₁ CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_full CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂ eq_zero_of_hom_shift_pos CategoryTheory.Category.assoc CategoryTheory.Functor.Full.comp CategoryTheory.Functor.IsEquivalence.full CategoryTheory.instIsEquivalenceShiftFunctor CategoryTheory.Functor.map_injective CategoryTheory.Functor.Faithful.comp CategoryTheory.Functor.IsEquivalence.faithful CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_preimage CategoryTheory.Functor.comp_map shift_ι_map_ιK
hasCokernel 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Functor.map	CategoryTheory.Limits.HasCokernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	mor₁_πQ
hasCokernel_of_admissibleMorphism 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms admissibleMorphism	CategoryTheory.Limits.HasCokernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	CategoryTheory.Pretriangulated.distinguished_cocone_triangle hasCokernel
hasKernel 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Functor.map	CategoryTheory.Limits.HasKernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	ιK_mor₁
hasKernel_of_admissibleMorphism 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms admissibleMorphism	CategoryTheory.Limits.HasKernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	CategoryTheory.Pretriangulated.distinguished_cocone_triangle hasKernel
mono_ιK 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Functor.map	CategoryTheory.Mono ιK	—	CategoryTheory.Preadditive.mono_iff_cancel_zero CategoryTheory.Functor.congr_map CategoryTheory.Functor.map_injective CategoryTheory.Functor.Faithful.comp CategoryTheory.Functor.IsEquivalence.faithful CategoryTheory.instIsEquivalenceShiftFunctor CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_full CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₃ CategoryTheory.Functor.map_comp shift_ι_map_ιK CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₁ CategoryTheory.Limits.zero_comp eq_zero_of_hom_shift_pos CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.NatIso.hom_app_isIso CategoryTheory.Limits.comp_zero
mor₁_πQ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Functor.obj CategoryTheory.Functor.map	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct πQ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	CategoryTheory.Functor.map_injective CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂ CategoryTheory.Functor.map_comp ι_map_πQ CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Limits.zero_comp CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_full
mor₁_πQ_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Functor.obj CategoryTheory.Functor.map	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct πQ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mor₁_πQ
shift_ι_map_ιK 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Functor.obj ιK CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Functor.map_preimage CategoryTheory.Functor.Full.comp CategoryTheory.Functor.IsEquivalence.full CategoryTheory.instIsEquivalenceShiftFunctor
shift_ι_map_ιK_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Functor.map ιK	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' shift_ι_map_ιK
ιK_mor₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Functor.obj CategoryTheory.Functor.map	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct ιK Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	CategoryTheory.Functor.map_injective CategoryTheory.Functor.Faithful.comp CategoryTheory.Functor.IsEquivalence.faithful CategoryTheory.instIsEquivalenceShiftFunctor CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₃₁ CategoryTheory.Functor.map_comp shift_ι_map_ιK CategoryTheory.Category.assoc CategoryTheory.Limits.comp_zero CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_full CategoryTheory.Functor.preservesZeroMorphisms_of_additive
ιK_mor₁_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Functor.obj CategoryTheory.Functor.map	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct ιK Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ιK_mor₁
ι_map_πQ 📖	mathematical	—	CategoryTheory.Functor.map πQ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	CategoryTheory.Functor.map_preimage
ι_map_πQ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map πQ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_map_πQ

---

← Back to Index