NonPreadditive

📁 Source: Mathlib/CategoryTheory/Abelian/NonPreadditive.lean

Statistics

Metric	Count
Definitions NonPreadditiveAbelian, epiIsCokernelOfKernel, hasAdd, hasNeg, hasSub, isColimitσ, monoIsKernelOfCokernel, preadditive, r, toHasZeroMorphisms, σ	11
Theorems add_assoc, add_comm, add_comp, add_def, add_neg, add_neg_cancel, add_zero, comp_add, comp_sub, diag_σ, diag_σ_assoc, epi_r, has_cokernels, has_finite_coproducts, has_finite_products, has_kernels, has_zero_object, instEpiFactorThruImage, instMonoFactorThruCoimage, isIso_factorThruCoimage, isIso_factorThruImage, isIso_r, lift_map, lift_map_assoc, lift_sub_lift, lift_σ, lift_σ_assoc, mono_r, mono_Δ, neg_add, neg_add_cancel, neg_def, neg_neg, neg_sub, neg_sub', sub_add, sub_comp, sub_def, sub_self, sub_sub_sub, sub_zero, toIsNormalEpiCategory, toIsNormalMonoCategory, σ_comp	44
Total	55

CategoryTheory

Definitions

Name	Category	Theorems
NonPreadditiveAbelian 📖	CompData	—

CategoryTheory.NonPreadditiveAbelian

Definitions

Name	Category	Theorems
epiIsCokernelOfKernel 📖	CompOp	—
hasAdd 📖	CompOp	12 math math: neg_sub', add_assoc, add_def, sub_add, add_zero, neg_add_cancel, neg_add, add_neg, add_comp, add_comm, comp_add, add_neg_cancel
hasNeg 📖	CompOp	9 math math: neg_sub', add_def, neg_add_cancel, neg_add, add_neg, neg_sub, add_neg_cancel, neg_def, neg_neg
hasSub 📖	CompOp	14 math math: neg_sub', add_def, sub_sub_sub, sub_add, sub_zero, sub_comp, lift_sub_lift, neg_add, add_neg, neg_sub, sub_def, comp_sub, neg_def, sub_self
isColimitσ 📖	CompOp	—
monoIsKernelOfCokernel 📖	CompOp	—
preadditive 📖	CompOp	—
r 📖	CompOp	5 math math: epi_r, isIso_r, mono_r, diag_σ_assoc, lift_σ_assoc
toHasZeroMorphisms 📖	CompOp	33 math math: CategoryTheory.Abelian.imageStrongEpiMonoFactorisation_e, diag_σ, isIso_factorThruCoimage, CategoryTheory.Abelian.instEpiFactorThruImage, has_cokernels, CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation_e, has_kernels, sub_zero, CategoryTheory.Abelian.instMonoFactorThruCoimage, instEpiFactorThruImage, CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation_I, epi_r, toIsNormalMonoCategory, isIso_r, add_zero, toIsNormalEpiCategory, CategoryTheory.Abelian.imageStrongEpiMonoFactorisation_m, neg_add_cancel, lift_map_assoc, mono_r, CategoryTheory.Abelian.imageStrongEpiMonoFactorisation_I, instMonoFactorThruCoimage, diag_σ_assoc, lift_map, CategoryTheory.Abelian.isIso_factorThruImage, isIso_factorThruImage, add_neg_cancel, lift_σ, lift_σ_assoc, neg_def, CategoryTheory.Abelian.isIso_factorThruCoimage, CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation_m, sub_self
σ 📖	CompOp	4 math math: diag_σ, σ_comp, sub_def, lift_σ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_assoc 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct hasAdd	—	add_def sub_add add_neg neg_sub' neg_neg
add_comm 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct hasAdd	—	add_def neg_neg neg_def sub_sub_sub neg_sub
add_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver hasAdd	—	add_def sub_comp neg_def CategoryTheory.Limits.zero_comp
add_def 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct hasAdd hasSub hasNeg	—	—
add_neg 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct hasAdd hasNeg hasSub	—	add_def neg_neg
add_neg_cancel 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct hasAdd hasNeg CategoryTheory.Limits.HasZeroMorphisms.zero toHasZeroMorphisms	—	add_neg sub_self
add_zero 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct hasAdd CategoryTheory.Limits.HasZeroMorphisms.zero toHasZeroMorphisms	—	add_def neg_def sub_self sub_zero
comp_add 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver hasAdd	—	add_def comp_sub neg_def CategoryTheory.Limits.comp_zero
comp_sub 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver hasSub	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype sub_def CategoryTheory.Category.assoc CategoryTheory.Limits.prod.comp_lift
diag_σ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair CategoryTheory.Limits.diag σ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero toHasZeroMorphisms	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype isIso_r CategoryTheory.Limits.cokernel.condition_assoc CategoryTheory.Limits.zero_comp
diag_σ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair CategoryTheory.Limits.diag CategoryTheory.Limits.cokernel toHasZeroMorphisms CategoryTheory.Limits.cokernel.π CategoryTheory.inv r isIso_r Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype isIso_r CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' diag_σ
epi_r 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Limits.cokernel toHasZeroMorphisms CategoryTheory.Limits.prod CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair CategoryTheory.Limits.diag CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels r	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype CategoryTheory.Limits.prod.lift_snd CategoryTheory.Limits.prod.hom_ext CategoryTheory.Limits.prod.comp_lift CategoryTheory.Category.comp_id CategoryTheory.Limits.comp_zero CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.KernelFork.condition CategoryTheory.cancel_mono CategoryTheory.mono_of_mono_fac CategoryTheory.instMonoId CategoryTheory.Limits.prod.lift_fst CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsRegularEpi CategoryTheory.instIsRegularEpiOfIsSplitEpi CategoryTheory.Limits.isSplitEpi_prod_snd CategoryTheory.NormalMonoCategory.epi_of_zero_cancel has_kernels toIsNormalMonoCategory has_zero_object CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels CategoryTheory.Category.assoc CategoryTheory.Category.id_comp CategoryTheory.Limits.CokernelCofork.π_ofπ CategoryTheory.Limits.cokernel.condition CategoryTheory.Limits.zero_comp CategoryTheory.cancel_epi CategoryTheory.Limits.coequalizer.π_epi
has_cokernels 📖	mathematical	—	CategoryTheory.Limits.HasCokernels toHasZeroMorphisms	—	—
has_finite_coproducts 📖	mathematical	—	CategoryTheory.Limits.HasFiniteCoproducts	—	—
has_finite_products 📖	mathematical	—	CategoryTheory.Limits.HasFiniteProducts	—	—
has_kernels 📖	mathematical	—	CategoryTheory.Limits.HasKernels toHasZeroMorphisms	—	—
has_zero_object 📖	mathematical	—	CategoryTheory.Limits.HasZeroObject	—	—
instEpiFactorThruImage 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Abelian.image toHasZeroMorphisms CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels CategoryTheory.Limits.HasKernels.has_limit has_kernels CategoryTheory.Limits.cokernel CategoryTheory.Limits.cokernel.π CategoryTheory.Abelian.factorThruImage	—	CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels CategoryTheory.Limits.HasKernels.has_limit has_kernels CategoryTheory.NormalMonoCategory.epi_of_zero_cancel has_finite_products toIsNormalMonoCategory has_zero_object CategoryTheory.mono_comp CategoryTheory.Limits.equalizer.ι_mono CategoryTheory.Abelian.image.fac CategoryTheory.Category.assoc CategoryTheory.NormalMono.w CategoryTheory.Limits.HasZeroMorphisms.comp_zero CategoryTheory.Limits.kernel.condition CategoryTheory.Limits.zero_comp CategoryTheory.Category.id_comp CategoryTheory.Limits.zero_of_epi_comp CategoryTheory.epi_of_epi_fac CategoryTheory.instEpiId CategoryTheory.cancel_mono
instMonoFactorThruCoimage 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Abelian.coimage toHasZeroMorphisms CategoryTheory.Limits.HasKernels.has_limit has_kernels CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels CategoryTheory.Limits.kernel CategoryTheory.Limits.kernel.ι CategoryTheory.Abelian.factorThruCoimage	—	CategoryTheory.Limits.HasKernels.has_limit has_kernels CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels CategoryTheory.NormalEpiCategory.mono_of_cancel_zero has_finite_coproducts toIsNormalEpiCategory has_zero_object CategoryTheory.epi_comp CategoryTheory.Limits.coequalizer.π_epi CategoryTheory.Abelian.coimage.fac CategoryTheory.Category.assoc CategoryTheory.NormalEpi.w CategoryTheory.Limits.zero_comp CategoryTheory.Limits.cokernel.condition CategoryTheory.Limits.comp_zero CategoryTheory.Category.comp_id CategoryTheory.Limits.zero_of_comp_mono CategoryTheory.mono_of_mono_fac CategoryTheory.instMonoId CategoryTheory.cancel_epi
isIso_factorThruCoimage 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Abelian.coimage toHasZeroMorphisms CategoryTheory.Limits.HasKernels.has_limit has_kernels CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels CategoryTheory.Limits.kernel CategoryTheory.Limits.kernel.ι CategoryTheory.Abelian.factorThruCoimage	—	CategoryTheory.isIso_of_mono_of_epi CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory toIsNormalMonoCategory CategoryTheory.Limits.HasKernels.has_limit has_kernels CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels instMonoFactorThruCoimage CategoryTheory.Abelian.epi_factorThruCoimage
isIso_factorThruImage 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Abelian.image toHasZeroMorphisms CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels CategoryTheory.Limits.HasKernels.has_limit has_kernels CategoryTheory.Limits.cokernel CategoryTheory.Limits.cokernel.π CategoryTheory.Abelian.factorThruImage	—	CategoryTheory.isIso_of_mono_of_epi CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory toIsNormalMonoCategory CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels CategoryTheory.Limits.HasKernels.has_limit has_kernels CategoryTheory.Abelian.mono_factorThruImage instEpiFactorThruImage
isIso_r 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Limits.cokernel toHasZeroMorphisms CategoryTheory.Limits.prod CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair CategoryTheory.Limits.diag CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels r	—	CategoryTheory.isIso_of_mono_of_epi CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory toIsNormalMonoCategory CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels mono_r epi_r
lift_map 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair CategoryTheory.Limits.prod.lift CategoryTheory.CategoryStruct.id Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero toHasZeroMorphisms CategoryTheory.Limits.prod.map	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype CategoryTheory.Limits.prod.lift_map CategoryTheory.Category.id_comp CategoryTheory.Limits.zero_comp CategoryTheory.Limits.prod.comp_lift CategoryTheory.Category.comp_id CategoryTheory.Limits.comp_zero
lift_map_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair CategoryTheory.Limits.prod.lift CategoryTheory.CategoryStruct.id Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero toHasZeroMorphisms CategoryTheory.Limits.prod.map	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_map
lift_sub_lift 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair hasSub CategoryTheory.Limits.prod.lift	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype CategoryTheory.Limits.prod.hom_ext CategoryTheory.Category.assoc σ_comp CategoryTheory.Limits.prod.lift_map_assoc CategoryTheory.Limits.prod.lift_fst CategoryTheory.Limits.prod.lift_snd
lift_σ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair CategoryTheory.Limits.prod.lift CategoryTheory.CategoryStruct.id Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero toHasZeroMorphisms σ	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype isIso_r CategoryTheory.Category.assoc CategoryTheory.IsIso.hom_inv_id
lift_σ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair CategoryTheory.Limits.prod.lift CategoryTheory.CategoryStruct.id Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero toHasZeroMorphisms CategoryTheory.Limits.cokernel CategoryTheory.Limits.diag CategoryTheory.Limits.cokernel.π CategoryTheory.inv r isIso_r	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype isIso_r CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' lift_σ
mono_r 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Limits.cokernel toHasZeroMorphisms CategoryTheory.Limits.prod CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair CategoryTheory.Limits.diag CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels r	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels CategoryTheory.Limits.cokernel.condition mono_Δ CategoryTheory.NormalEpiCategory.mono_of_cancel_zero has_finite_coproducts toIsNormalEpiCategory has_zero_object CategoryTheory.Category.assoc CategoryTheory.Category.comp_id CategoryTheory.Limits.prod.lift_snd CategoryTheory.Limits.KernelFork.ι_ofι CategoryTheory.Limits.HasZeroMorphisms.comp_zero CategoryTheory.cancel_mono CategoryTheory.mono_of_mono_fac CategoryTheory.instMonoId CategoryTheory.Limits.prod.lift_fst CategoryTheory.Limits.zero_comp
mono_Δ 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Limits.prod CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair CategoryTheory.Limits.diag	—	CategoryTheory.mono_of_mono_fac CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype CategoryTheory.instMonoId CategoryTheory.Limits.prod.lift_fst
neg_add 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct hasNeg hasAdd hasSub	—	add_def neg_sub' add_neg
neg_add_cancel 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct hasAdd hasNeg CategoryTheory.Limits.HasZeroMorphisms.zero toHasZeroMorphisms	—	add_comm add_neg_cancel
neg_def 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct hasNeg hasSub CategoryTheory.Limits.HasZeroMorphisms.zero toHasZeroMorphisms	—	—
neg_neg 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct hasNeg	—	neg_def sub_self sub_sub_sub sub_zero
neg_sub 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct hasSub hasNeg	—	neg_def sub_zero sub_sub_sub
neg_sub' 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct hasNeg hasSub hasAdd	—	neg_def sub_self sub_sub_sub add_def
sub_add 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct hasAdd hasSub	—	add_def neg_def sub_sub_sub sub_zero
sub_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver hasSub	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype sub_def CategoryTheory.Category.assoc σ_comp CategoryTheory.Limits.prod.lift_map
sub_def 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct hasSub CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair CategoryTheory.Limits.prod.lift σ	—	—
sub_self 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct hasSub CategoryTheory.Limits.HasZeroMorphisms.zero toHasZeroMorphisms	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype sub_def CategoryTheory.Category.comp_id CategoryTheory.Limits.prod.comp_lift CategoryTheory.Category.assoc diag_σ CategoryTheory.Limits.comp_zero
sub_sub_sub 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct hasSub	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype sub_def lift_sub_lift CategoryTheory.Category.assoc σ_comp CategoryTheory.Limits.prod.lift_map_assoc
sub_zero 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct hasSub CategoryTheory.Limits.HasZeroMorphisms.zero toHasZeroMorphisms	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype sub_def CategoryTheory.Category.comp_id CategoryTheory.Limits.comp_zero CategoryTheory.Limits.prod.comp_lift CategoryTheory.Category.assoc lift_σ
toIsNormalEpiCategory 📖	mathematical	—	CategoryTheory.IsNormalEpiCategory toHasZeroMorphisms	—	—
toIsNormalMonoCategory 📖	mathematical	—	CategoryTheory.IsNormalMonoCategory toHasZeroMorphisms	—	—
σ_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair σ CategoryTheory.Limits.prod.map	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype diag_σ CategoryTheory.Limits.prod.diag_map_assoc CategoryTheory.Limits.comp_zero lift_σ CategoryTheory.Category.comp_id lift_map_assoc CategoryTheory.Limits.CokernelCofork.π_ofπ CategoryTheory.Category.assoc CategoryTheory.Category.id_comp CategoryTheory.Limits.Cofork.π_ofπ

---

← Back to Index