Cycles

📁 Source: Mathlib/Algebra/Homology/SpectralObject/Cycles.lean

Statistics

Metric	Count
Definitions cokernelIsoCycles, cokernelSequenceCycles, cokernelSequenceOpcycles, cycles, cyclesMap, descCycles, descOpcycles, fromOpcycles, iCycles, kernelSequenceCycles, kernelSequenceOpcycles, liftCycles, liftOpcycles, opcycles, opcyclesIsoKernel, opcyclesMap, pOpcycles, toCycles, δFromOpcycles, δToCycles	20
Theorems H_map_twoδ₂Toδ₁_toCycles, H_map_twoδ₂Toδ₁_toCycles_assoc, cokernelIsoCycles_hom_fac, cokernelIsoCycles_hom_fac_assoc, cokernelSequenceCycles_X₁, cokernelSequenceCycles_X₂, cokernelSequenceCycles_X₃, cokernelSequenceCycles_exact, cokernelSequenceCycles_f, cokernelSequenceCycles_g, cokernelSequenceOpcycles_X₁, cokernelSequenceOpcycles_X₂, cokernelSequenceOpcycles_X₃, cokernelSequenceOpcycles_exact, cokernelSequenceOpcycles_f, cokernelSequenceOpcycles_g, cyclesMap_comp, cyclesMap_comp_assoc, cyclesMap_i, cyclesMap_i_assoc, cyclesMap_id, fromOpcycles_H_map_twoδ₁Toδ₀, fromOpcycles_H_map_twoδ₁Toδ₀_assoc, fromOpcyles_δ, fromOpcyles_δ_assoc, iCycles_δ, iCycles_δ_assoc, instEpiGCokernelSequenceCycles, instEpiGCokernelSequenceOpcycles, instEpiPOpcycles, instEpiToCycles, instMonoFKernelSequenceCycles, instMonoFKernelSequenceOpcycles, instMonoFromOpcycles, instMonoICycles, isIso_fromOpcycles, isIso_toCycles, isZero_cycles, isZero_opcycles, kernelSequenceCycles_X₁, kernelSequenceCycles_X₂, kernelSequenceCycles_X₃, kernelSequenceCycles_exact, kernelSequenceCycles_f, kernelSequenceCycles_g, kernelSequenceOpcycles_X₁, kernelSequenceOpcycles_X₂, kernelSequenceOpcycles_X₃, kernelSequenceOpcycles_exact, kernelSequenceOpcycles_f, kernelSequenceOpcycles_g, liftCycles_i, liftCycles_i_assoc, liftOpcycles_fromOpcycles, liftOpcycles_fromOpcycles_assoc, opcyclesIsoKernel_hom_fac, opcyclesIsoKernel_hom_fac_assoc, opcyclesMap_comp, opcyclesMap_fromOpcycles, opcyclesMap_fromOpcycles_assoc, opcyclesMap_id, pOpcycles_δFromOpcycles, pOpcycles_δFromOpcycles_assoc, p_descOpcycles, p_descOpcycles_assoc, p_fromOpcycles, p_fromOpcycles_assoc, p_opcyclesMap, p_opcyclesMap_assoc, toCycles_cyclesMap, toCycles_cyclesMap_assoc, toCycles_descCycles, toCycles_descCycles_assoc, toCycles_i, toCycles_i_assoc, δToCycles_iCycles, δToCycles_iCycles_assoc, δ_pOpcycles, δ_pOpcycles_assoc, δ_toCycles, δ_toCycles_assoc	81
Total	101

CategoryTheory.Abelian.SpectralObject

Definitions

Name	Category	Theorems
cokernelIsoCycles 📖	CompOp	2 math math: cokernelIsoCycles_hom_fac_assoc, cokernelIsoCycles_hom_fac
cokernelSequenceCycles 📖	CompOp	7 math math: cokernelSequenceCycles_X₁, cokernelSequenceCycles_exact, cokernelSequenceCycles_X₂, cokernelSequenceCycles_f, cokernelSequenceCycles_X₃, cokernelSequenceCycles_g, instEpiGCokernelSequenceCycles
cokernelSequenceOpcycles 📖	CompOp	7 math math: cokernelSequenceOpcycles_X₂, cokernelSequenceOpcycles_exact, cokernelSequenceOpcycles_X₃, instEpiGCokernelSequenceOpcycles, cokernelSequenceOpcycles_g, cokernelSequenceOpcycles_X₁, cokernelSequenceOpcycles_f
cycles 📖	CompOp	83 math math: H_map_twoδ₂Toδ₁_toCycles_assoc, δToCycles_iCycles, instMonoEToCycles, leftHomologyDataShortComplex_H, cyclesIso_inv_i_assoc, toCycles_πE_d, δToCycles_πE, πE_EToCycles, toCycles_πE_d_assoc, δ_toCycles, Ψ_opcyclesMap, cyclesIsoH_hom_EIsoH_inv, δToCycles_cyclesIso_inv_assoc, cyclesMap_id, cyclesIso_hom_i, cyclesMap_Ψ_exact, cyclesMap_i, cyclesIso_hom_i_assoc, toCycles_descCycles, EToCycles_i_assoc, cyclesIso_inv_cyclesMap_assoc, cyclesMap_comp, toCycles_cyclesMap, πE_ιE, πE_EIsoH_hom_assoc, πE_map_assoc, cyclesMap_Ψ_assoc, Ψ_opcyclesMap_exact, cokernelSequenceE_g, toCycles_cyclesMap_assoc, p_opcyclesToE, cyclesIsoH_inv_hom_id, isIso_toCycles, kernelSequenceCyclesE_g, cyclesIsoH_inv_hom_id_assoc, toCycles_Ψ_assoc, H_map_twoδ₂Toδ₁_toCycles, δToCycles_πE_assoc, toCycles_πE_descE_assoc, cyclesIsoH_hom_EIsoH_inv_assoc, instEpiToCycles, Ψ_fromOpcycles_assoc, πE_EIsoH_hom, cokernelSequenceCycles_X₃, cokernelSequenceCyclesEIso_hom_τ₂, cokernelIsoCycles_hom_fac_assoc, iCycles_δ, πE_d_ιE_assoc, cokernelSequenceCyclesE_X₂, leftHomologyDataShortComplex_π, cokernelIsoCycles_hom_fac, δToCycles_cyclesIso_inv, πE_ιE_assoc, δ_toCycles_assoc, πE_EToCycles_assoc, Ψ_fromOpcycles, δToCycles_iCycles_assoc, liftCycles_i, cyclesIsoH_hom_inv_id_assoc, EToCycles_i, kernelSequenceCyclesE_X₂, cyclesMap_Ψ, p_opcyclesToE_assoc, cyclesIso_inv_i, toCycles_Ψ, cokernelSequenceCyclesEIso_inv_τ₂, liftCycles_i_assoc, isZero_cycles, cyclesIsoH_hom_inv_id, toCycles_πE_descE, cyclesIsoH_inv, cyclesMap_i_assoc, kernelSequenceCycles_X₁, πE_map, iCycles_δ_assoc, cyclesIso_inv_cyclesMap, instMonoICycles, leftHomologyDataShortComplex_K, toCycles_descCycles_assoc, cyclesMap_comp_assoc, toCycles_i, toCycles_i_assoc, πE_d_ιE
cyclesMap 📖	CompOp	16 math math: πE_EToCycles, cyclesMap_id, cyclesMap_Ψ_exact, cyclesMap_i, cyclesIso_inv_cyclesMap_assoc, cyclesMap_comp, toCycles_cyclesMap, πE_map_assoc, cyclesMap_Ψ_assoc, toCycles_cyclesMap_assoc, πE_EToCycles_assoc, cyclesMap_Ψ, cyclesMap_i_assoc, πE_map, cyclesIso_inv_cyclesMap, cyclesMap_comp_assoc
descCycles 📖	CompOp	2 math math: toCycles_descCycles, toCycles_descCycles_assoc
descOpcycles 📖	CompOp	2 math math: p_descOpcycles, p_descOpcycles_assoc
fromOpcycles 📖	CompOp	27 math math: liftOpcycles_fromOpcycles_assoc, instMonoFromOpcycles, d_ιE_fromOpcycles, kernelSequenceOpcycles_f, fromOpcycles_H_map_twoδ₁Toδ₀, EToCycles_i_assoc, fromOpcycles_H_map_twoδ₁Toδ₀_assoc, isIso_fromOpcycles, liftE_ιE_fromOpcycles, fromOpcyles_δ_assoc, opcyclesIsoH_hom, opcyclesMap_fromOpcycles, Ψ_fromOpcycles_assoc, p_fromOpcycles_assoc, liftOpcycles_fromOpcycles, kernelSequenceE_f, d_ιE_fromOpcycles_assoc, opcyclesIsoH_inv_hom_id_assoc, opcyclesIsoH_inv_hom_id, p_fromOpcycles, Ψ_fromOpcycles, EToCycles_i, opcyclesIsoH_hom_inv_id, opcyclesIsoH_hom_inv_id_assoc, liftE_ιE_fromOpcycles_assoc, opcyclesMap_fromOpcycles_assoc, fromOpcyles_δ
iCycles 📖	CompOp	26 math math: δToCycles_iCycles, cyclesIso_inv_i_assoc, cyclesIso_hom_i, cyclesMap_i, cyclesIso_hom_i_assoc, EToCycles_i_assoc, πE_ιE, kernelSequenceCyclesE_g, Ψ_fromOpcycles_assoc, cokernelIsoCycles_hom_fac_assoc, iCycles_δ, leftHomologyDataShortComplex_i, cokernelIsoCycles_hom_fac, πE_ιE_assoc, Ψ_fromOpcycles, δToCycles_iCycles_assoc, liftCycles_i, EToCycles_i, kernelSequenceCycles_f, cyclesIso_inv_i, liftCycles_i_assoc, cyclesMap_i_assoc, iCycles_δ_assoc, instMonoICycles, toCycles_i, toCycles_i_assoc
kernelSequenceCycles 📖	CompOp	7 math math: kernelSequenceCycles_g, instMonoFKernelSequenceCycles, kernelSequenceCycles_X₂, kernelSequenceCycles_f, kernelSequenceCycles_X₃, kernelSequenceCycles_exact, kernelSequenceCycles_X₁
kernelSequenceOpcycles 📖	CompOp	7 math math: instMonoFKernelSequenceOpcycles, kernelSequenceOpcycles_f, kernelSequenceOpcycles_X₂, kernelSequenceOpcycles_g, kernelSequenceOpcycles_X₁, kernelSequenceOpcycles_exact, kernelSequenceOpcycles_X₃
liftCycles 📖	CompOp	2 math math: liftCycles_i, liftCycles_i_assoc
liftOpcycles 📖	CompOp	2 math math: liftOpcycles_fromOpcycles_assoc, liftOpcycles_fromOpcycles
opcycles 📖	CompOp	86 math math: EIsoH_hom_opcyclesIsoH_inv_assoc, opcyclesMap_threeδ₂Toδ₁_opcyclesToE_assoc, opcyclesToE_map, liftOpcycles_fromOpcycles_assoc, instMonoFromOpcycles, d_ιE_fromOpcycles, opcyclesIso_hom_δFromOpcycles, Ψ_opcyclesMap, pOpcycles_δFromOpcycles, cyclesMap_Ψ_exact, fromOpcycles_H_map_twoδ₁Toδ₀, opcyclesMap_comp, EToCycles_i_assoc, πE_ιE, fromOpcycles_H_map_twoδ₁Toδ₀_assoc, cokernelSequenceOpcycles_X₃, p_opcyclesIso_inv, kernelSequenceOpcyclesEIso_inv_τ₂, isIso_fromOpcycles, rightHomologyDataShortComplex_ι, cyclesMap_Ψ_assoc, Ψ_opcyclesMap_exact, p_opcyclesToE, rightHomologyDataShortComplex_H, ιE_δFromOpcycles_assoc, liftE_ιE_fromOpcycles, fromOpcyles_δ_assoc, map_ιE_assoc, toCycles_Ψ_assoc, cokernelSequenceOpcyclesE_X₂, p_opcyclesIso_hom, opcyclesIsoH_hom, opcyclesMap_fromOpcycles, p_opcyclesIso_hom_assoc, Ψ_fromOpcycles_assoc, p_fromOpcycles_assoc, liftOpcycles_fromOpcycles, πE_d_ιE_assoc, kernelSequenceE_f, kernelSequenceOpcyclesEIso_hom_τ₂, p_opcyclesMap_assoc, d_ιE_fromOpcycles_assoc, opcyclesIsoH_inv_hom_id_assoc, p_opcyclesIso_inv_assoc, opcyclesToE_map_assoc, δ_pOpcycles_assoc, p_descOpcycles, πE_ιE_assoc, opcyclesIsoKernel_hom_fac, isZero_opcycles, kernelSequenceOpcyclesE_X₂, opcyclesIsoH_inv_hom_id, p_descOpcycles_assoc, p_fromOpcycles, Ψ_fromOpcycles, p_opcyclesMap, opcyclesIso_hom_δFromOpcycles_assoc, instEpiPOpcycles, opcyclesIsoKernel_hom_fac_assoc, ιE_δFromOpcycles, opcyclesToE_ιE, opcyclesMap_id, EToCycles_i, map_ιE, rightHomologyDataShortComplex_Q, opcyclesIsoH_hom_inv_id, opcyclesMap_opcyclesIso_hom_assoc, cyclesMap_Ψ, kernelSequenceOpcycles_X₁, opcyclesToE_ιE_assoc, instEpiOpcyclesToE, p_opcyclesToE_assoc, δ_pOpcycles, EIsoH_hom_opcyclesIsoH_inv, toCycles_Ψ, opcyclesIsoH_hom_inv_id_assoc, cokernelSequenceOpcyclesE_f, liftE_ιE_fromOpcycles_assoc, opcyclesMap_fromOpcycles_assoc, pOpcycles_δFromOpcycles_assoc, fromOpcyles_δ, shortComplexOpcyclesThreeδ₂Toδ₁_X₁, shortComplexOpcyclesThreeδ₂Toδ₁_X₂, opcyclesMap_opcyclesIso_hom, opcyclesMap_threeδ₂Toδ₁_opcyclesToE, πE_d_ιE
opcyclesIsoKernel 📖	CompOp	2 math math: opcyclesIsoKernel_hom_fac, opcyclesIsoKernel_hom_fac_assoc
opcyclesMap 📖	CompOp	19 math math: opcyclesMap_threeδ₂Toδ₁_opcyclesToE_assoc, opcyclesToE_map, Ψ_opcyclesMap, opcyclesMap_comp, Ψ_opcyclesMap_exact, map_ιE_assoc, opcyclesMap_fromOpcycles, p_opcyclesMap_assoc, opcyclesToE_map_assoc, p_opcyclesMap, opcyclesToE_ιE, opcyclesMap_id, map_ιE, opcyclesMap_opcyclesIso_hom_assoc, opcyclesToE_ιE_assoc, shortComplexOpcyclesThreeδ₂Toδ₁_f, opcyclesMap_fromOpcycles_assoc, opcyclesMap_opcyclesIso_hom, opcyclesMap_threeδ₂Toδ₁_opcyclesToE
pOpcycles 📖	CompOp	26 math math: pOpcycles_δFromOpcycles, πE_ιE, p_opcyclesIso_inv, p_opcyclesToE, toCycles_Ψ_assoc, p_opcyclesIso_hom, p_opcyclesIso_hom_assoc, p_fromOpcycles_assoc, p_opcyclesMap_assoc, p_opcyclesIso_inv_assoc, δ_pOpcycles_assoc, p_descOpcycles, πE_ιE_assoc, opcyclesIsoKernel_hom_fac, p_descOpcycles_assoc, p_fromOpcycles, p_opcyclesMap, instEpiPOpcycles, opcyclesIsoKernel_hom_fac_assoc, cokernelSequenceOpcycles_g, rightHomologyDataShortComplex_p, p_opcyclesToE_assoc, δ_pOpcycles, toCycles_Ψ, cokernelSequenceOpcyclesE_f, pOpcycles_δFromOpcycles_assoc
toCycles 📖	CompOp	27 math math: H_map_twoδ₂Toδ₁_toCycles_assoc, toCycles_πE_d, toCycles_πE_d_assoc, δ_toCycles, toCycles_descCycles, toCycles_cyclesMap, cokernelSequenceE_g, toCycles_cyclesMap_assoc, p_opcyclesToE, cyclesIsoH_inv_hom_id, isIso_toCycles, cyclesIsoH_inv_hom_id_assoc, toCycles_Ψ_assoc, H_map_twoδ₂Toδ₁_toCycles, toCycles_πE_descE_assoc, instEpiToCycles, cokernelSequenceCycles_g, δ_toCycles_assoc, cyclesIsoH_hom_inv_id_assoc, p_opcyclesToE_assoc, toCycles_Ψ, cyclesIsoH_hom_inv_id, toCycles_πE_descE, cyclesIsoH_inv, toCycles_descCycles_assoc, toCycles_i, toCycles_i_assoc
δFromOpcycles 📖	CompOp	12 math math: opcyclesIso_hom_δFromOpcycles, pOpcycles_δFromOpcycles, rightHomologyDataShortComplex_ι, rightHomologyDataShortComplex_H, ιE_δFromOpcycles_assoc, fromOpcyles_δ_assoc, rightHomologyDataShortComplex_g', opcyclesIso_hom_δFromOpcycles_assoc, ιE_δFromOpcycles, pOpcycles_δFromOpcycles_assoc, fromOpcyles_δ, kernelSequenceOpcyclesE_g
δToCycles 📖	CompOp	12 math math: δToCycles_iCycles, leftHomologyDataShortComplex_H, δToCycles_πE, δ_toCycles, δToCycles_cyclesIso_inv_assoc, leftHomologyDataShortComplex_f', δToCycles_πE_assoc, cokernelSequenceCyclesE_f, leftHomologyDataShortComplex_π, δToCycles_cyclesIso_inv, δ_toCycles_assoc, δToCycles_iCycles_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
H_map_twoδ₂Toδ₁_toCycles 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ cycles CategoryTheory.Functor.map CategoryTheory.ComposableArrows.twoδ₂Toδ₁ toCycles Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.cancel_mono instMonoICycles CategoryTheory.Category.assoc toCycles_i zero₂ CategoryTheory.Limits.zero_comp
H_map_twoδ₂Toδ₁_toCycles_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Functor.map CategoryTheory.ComposableArrows.twoδ₂Toδ₁ cycles toCycles Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' H_map_twoδ₂Toδ₁_toCycles
cokernelIsoCycles_hom_fac 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Limits.cokernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Functor.map CategoryTheory.ComposableArrows.twoδ₂Toδ₁ CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.cokernel.π cycles CategoryTheory.Iso.hom cokernelIsoCycles iCycles CategoryTheory.ComposableArrows.twoδ₁Toδ₀	—	CategoryTheory.ComposableArrows.Exact.cokerIsoKer_hom_fac CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory composableArrows₅_exact CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels
cokernelIsoCycles_hom_fac_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Limits.cokernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Functor.map CategoryTheory.ComposableArrows.twoδ₂Toδ₁ CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.cokernel.π cycles CategoryTheory.Iso.hom cokernelIsoCycles iCycles CategoryTheory.ComposableArrows.twoδ₁Toδ₀	—	CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cokernelIsoCycles_hom_fac
cokernelSequenceCycles_X₁ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceCycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	—
cokernelSequenceCycles_X₂ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceCycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	—
cokernelSequenceCycles_X₃ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceCycles cycles	—	—
cokernelSequenceCycles_exact 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceCycles	—	CategoryTheory.ShortComplex.exact_of_g_is_cokernel CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.cokernel.condition CategoryTheory.Limits.zero_comp CategoryTheory.ShortComplex.zero CategoryTheory.cancel_mono instMonoICycles CategoryTheory.Category.assoc cokernelIsoCycles_hom_fac toCycles_i CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian
cokernelSequenceCycles_f 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceCycles CategoryTheory.Functor.map CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.ComposableArrows.twoδ₂Toδ₁	—	—
cokernelSequenceCycles_g 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.g CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceCycles toCycles	—	—
cokernelSequenceOpcycles_X₁ 📖	mathematical	—	CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceOpcycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	—
cokernelSequenceOpcycles_X₂ 📖	mathematical	—	CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceOpcycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	—
cokernelSequenceOpcycles_X₃ 📖	mathematical	—	CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceOpcycles opcycles	—	—
cokernelSequenceOpcycles_exact 📖	mathematical	—	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceOpcycles	—	CategoryTheory.ShortComplex.exact_cokernel
cokernelSequenceOpcycles_f 📖	mathematical	—	CategoryTheory.ShortComplex.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceOpcycles δ	—	—
cokernelSequenceOpcycles_g 📖	mathematical	—	CategoryTheory.ShortComplex.g CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceOpcycles pOpcycles	—	—
cyclesMap_comp 📖	mathematical	Quiver.Hom CategoryTheory.ComposableArrows CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₂ CategoryTheory.CategoryStruct.comp	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles cyclesMap	—	CategoryTheory.cancel_mono instMonoICycles CategoryTheory.Category.assoc CategoryTheory.ComposableArrows.naturality' cyclesMap_i cyclesMap_i_assoc CategoryTheory.Functor.map_comp CategoryTheory.ComposableArrows.hom_ext₁
cyclesMap_comp_assoc 📖	mathematical	Quiver.Hom CategoryTheory.ComposableArrows CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₂ CategoryTheory.CategoryStruct.comp	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles cyclesMap	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cyclesMap_comp
cyclesMap_i 📖	mathematical	Quiver.Hom CategoryTheory.ComposableArrows CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₁ CategoryTheory.ComposableArrows.homMk₁ CategoryTheory.NatTrans.app CategoryTheory.ComposableArrows.mk₂ CategoryTheory.ComposableArrows.naturality'	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ cyclesMap iCycles CategoryTheory.Functor.map	—	CategoryTheory.ComposableArrows.naturality' liftCycles_i
cyclesMap_i_assoc 📖	mathematical	Quiver.Hom CategoryTheory.ComposableArrows CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₁ CategoryTheory.ComposableArrows.homMk₁ CategoryTheory.NatTrans.app CategoryTheory.ComposableArrows.mk₂ CategoryTheory.ComposableArrows.naturality'	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles cyclesMap CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ iCycles CategoryTheory.Functor.map	—	CategoryTheory.ComposableArrows.naturality' CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cyclesMap_i
cyclesMap_id 📖	mathematical	—	cyclesMap CategoryTheory.CategoryStruct.id CategoryTheory.ComposableArrows CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₂ cycles	—	CategoryTheory.cancel_mono instMonoICycles cyclesMap_i CategoryTheory.ComposableArrows.naturality' CategoryTheory.ComposableArrows.hom_ext₁ CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
fromOpcycles_H_map_twoδ₁Toδ₀ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ fromOpcycles CategoryTheory.Functor.map CategoryTheory.ComposableArrows.twoδ₁Toδ₀ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.cancel_epi instEpiPOpcycles p_fromOpcycles_assoc zero₂ CategoryTheory.Limits.comp_zero
fromOpcycles_H_map_twoδ₁Toδ₀_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ fromOpcycles CategoryTheory.Functor.map CategoryTheory.ComposableArrows.twoδ₁Toδ₀ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fromOpcycles_H_map_twoδ₁Toδ₀
fromOpcyles_δ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ fromOpcycles δ δFromOpcycles	—	CategoryTheory.cancel_epi instEpiPOpcycles p_fromOpcycles_assoc pOpcycles_δFromOpcycles δ_naturality CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
fromOpcyles_δ_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ fromOpcycles δ δFromOpcycles	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fromOpcyles_δ
iCycles_δ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ iCycles δ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.Limits.kernel.condition
iCycles_δ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ iCycles δ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' iCycles_δ
instEpiGCokernelSequenceCycles 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Epi CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceCycles CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	—	instEpiToCycles
instEpiGCokernelSequenceOpcycles 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceOpcycles CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	—	instEpiPOpcycles
instEpiPOpcycles 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ opcycles pOpcycles	—	CategoryTheory.Limits.coequalizer.π_epi
instEpiToCycles 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Epi CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ cycles toCycles	—	CategoryTheory.ShortComplex.zero CategoryTheory.ShortComplex.exact_iff_epi_kernel_lift CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian exact₃
instMonoFKernelSequenceCycles 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceCycles CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f	—	instMonoICycles
instMonoFKernelSequenceOpcycles 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Mono CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceOpcycles CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f	—	instMonoFromOpcycles
instMonoFromOpcycles 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Mono opcycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ fromOpcycles	—	CategoryTheory.ShortComplex.zero CategoryTheory.ShortComplex.exact_iff_mono_cokernel_desc CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian exact₁
instMonoICycles 📖	mathematical	—	CategoryTheory.Mono cycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ iCycles	—	CategoryTheory.Limits.equalizer.ι_mono
isIso_fromOpcycles 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	CategoryTheory.IsIso opcycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ fromOpcycles	—	CategoryTheory.ShortComplex.Exact.epi_f kernelSequenceOpcycles_exact CategoryTheory.Limits.IsZero.eq_of_tgt CategoryTheory.Balanced.isIso_of_mono_of_epi CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory instMonoFromOpcycles
isIso_toCycles 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ cycles toCycles	—	CategoryTheory.ShortComplex.Exact.mono_g cokernelSequenceCycles_exact CategoryTheory.Limits.IsZero.eq_of_src CategoryTheory.Balanced.isIso_of_mono_of_epi CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory instEpiToCycles
isZero_cycles 📖	mathematical	CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	CategoryTheory.Limits.IsZero cycles	—	CategoryTheory.Limits.IsZero.iff_id_eq_zero CategoryTheory.cancel_mono instMonoICycles CategoryTheory.Limits.IsZero.eq_of_tgt
isZero_opcycles 📖	mathematical	CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	CategoryTheory.Limits.IsZero opcycles	—	CategoryTheory.Limits.IsZero.iff_id_eq_zero CategoryTheory.cancel_epi instEpiPOpcycles CategoryTheory.Limits.IsZero.eq_of_src
kernelSequenceCycles_X₁ 📖	mathematical	—	CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceCycles cycles	—	—
kernelSequenceCycles_X₂ 📖	mathematical	—	CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceCycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	—
kernelSequenceCycles_X₃ 📖	mathematical	—	CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceCycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	—
kernelSequenceCycles_exact 📖	mathematical	—	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceCycles	—	CategoryTheory.ShortComplex.exact_kernel
kernelSequenceCycles_f 📖	mathematical	—	CategoryTheory.ShortComplex.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceCycles iCycles	—	—
kernelSequenceCycles_g 📖	mathematical	—	CategoryTheory.ShortComplex.g CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceCycles δ	—	—
kernelSequenceOpcycles_X₁ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceOpcycles opcycles	—	—
kernelSequenceOpcycles_X₂ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceOpcycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	—
kernelSequenceOpcycles_X₃ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceOpcycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	—
kernelSequenceOpcycles_exact 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceOpcycles	—	CategoryTheory.ShortComplex.exact_of_f_is_kernel CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.kernel.condition CategoryTheory.Limits.comp_zero CategoryTheory.ShortComplex.zero CategoryTheory.cancel_epi instEpiPOpcycles opcyclesIsoKernel_hom_fac p_fromOpcycles CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian
kernelSequenceOpcycles_f 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceOpcycles fromOpcycles	—	—
kernelSequenceOpcycles_g 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.g CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceOpcycles CategoryTheory.Functor.map CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.ComposableArrows.twoδ₁Toδ₀	—	—
liftCycles_i 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ δ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ liftCycles iCycles	—	CategoryTheory.Limits.kernel.lift_ι
liftCycles_i_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ δ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles liftCycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ iCycles	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' liftCycles_i
liftOpcycles_fromOpcycles 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Functor.map CategoryTheory.ComposableArrows.twoδ₁Toδ₀ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ liftOpcycles fromOpcycles	—	CategoryTheory.ShortComplex.Exact.lift_f CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory kernelSequenceOpcycles_exact instMonoFKernelSequenceOpcycles
liftOpcycles_fromOpcycles_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Functor.map CategoryTheory.ComposableArrows.twoδ₁Toδ₀ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles liftOpcycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ fromOpcycles	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' liftOpcycles_fromOpcycles
opcyclesIsoKernel_hom_fac 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ opcycles pOpcycles CategoryTheory.Limits.kernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Functor.map CategoryTheory.ComposableArrows.twoδ₁Toδ₀ CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Iso.hom opcyclesIsoKernel CategoryTheory.Limits.kernel.ι CategoryTheory.ComposableArrows.twoδ₂Toδ₁	—	CategoryTheory.ComposableArrows.Exact.cokerIsoKer_hom_fac CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory composableArrows₅_exact CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels
opcyclesIsoKernel_hom_fac_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ opcycles pOpcycles CategoryTheory.Limits.kernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Functor.map CategoryTheory.ComposableArrows.twoδ₁Toδ₀ CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Iso.hom opcyclesIsoKernel CategoryTheory.Limits.kernel.ι CategoryTheory.ComposableArrows.twoδ₂Toδ₁	—	CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opcyclesIsoKernel_hom_fac
opcyclesMap_comp 📖	mathematical	Quiver.Hom CategoryTheory.ComposableArrows CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₂ CategoryTheory.CategoryStruct.comp	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles opcyclesMap	—	CategoryTheory.cancel_epi instEpiPOpcycles CategoryTheory.ComposableArrows.naturality' p_opcyclesMap_assoc p_opcyclesMap CategoryTheory.Functor.map_comp_assoc CategoryTheory.ComposableArrows.hom_ext₁
opcyclesMap_fromOpcycles 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₁ CategoryTheory.NatTrans.app CategoryTheory.ComposableArrows.mk₂	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ opcyclesMap fromOpcycles CategoryTheory.Functor.map	—	CategoryTheory.cancel_epi instEpiPOpcycles p_fromOpcycles_assoc CategoryTheory.ComposableArrows.naturality' p_opcyclesMap_assoc p_fromOpcycles CategoryTheory.Functor.map_comp CategoryTheory.ComposableArrows.hom_ext₁ CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp le_rfl
opcyclesMap_fromOpcycles_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₁ CategoryTheory.NatTrans.app CategoryTheory.ComposableArrows.mk₂	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles opcyclesMap CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ fromOpcycles CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opcyclesMap_fromOpcycles
opcyclesMap_id 📖	mathematical	—	opcyclesMap CategoryTheory.CategoryStruct.id CategoryTheory.ComposableArrows CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₂ opcycles	—	CategoryTheory.cancel_epi instEpiPOpcycles p_opcyclesMap CategoryTheory.ComposableArrows.naturality' CategoryTheory.ComposableArrows.hom_ext₁ CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
pOpcycles_δFromOpcycles 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ opcycles pOpcycles δFromOpcycles δ	—	p_descOpcycles
pOpcycles_δFromOpcycles_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ opcycles pOpcycles δFromOpcycles δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pOpcycles_δFromOpcycles
p_descOpcycles 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ δ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ opcycles pOpcycles descOpcycles	—	CategoryTheory.Limits.cokernel.π_desc
p_descOpcycles_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ δ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ opcycles pOpcycles descOpcycles	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' p_descOpcycles
p_fromOpcycles 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ opcycles pOpcycles fromOpcycles CategoryTheory.Functor.map CategoryTheory.ComposableArrows.twoδ₂Toδ₁	—	CategoryTheory.Limits.cokernel.π_desc
p_fromOpcycles_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ opcycles pOpcycles fromOpcycles CategoryTheory.Functor.map CategoryTheory.ComposableArrows.twoδ₂Toδ₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' p_fromOpcycles
p_opcyclesMap 📖	mathematical	Quiver.Hom CategoryTheory.ComposableArrows CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₁ CategoryTheory.ComposableArrows.homMk₁ CategoryTheory.NatTrans.app CategoryTheory.ComposableArrows.mk₂ CategoryTheory.ComposableArrows.naturality'	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ opcycles pOpcycles opcyclesMap CategoryTheory.Functor.map	—	CategoryTheory.ComposableArrows.naturality' p_descOpcycles
p_opcyclesMap_assoc 📖	mathematical	Quiver.Hom CategoryTheory.ComposableArrows CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₁ CategoryTheory.ComposableArrows.homMk₁ CategoryTheory.NatTrans.app CategoryTheory.ComposableArrows.mk₂ CategoryTheory.ComposableArrows.naturality'	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ opcycles pOpcycles opcyclesMap CategoryTheory.Functor.map	—	CategoryTheory.ComposableArrows.naturality' CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' p_opcyclesMap
toCycles_cyclesMap 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₁ CategoryTheory.NatTrans.app CategoryTheory.ComposableArrows.mk₂	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ cycles toCycles cyclesMap CategoryTheory.Functor.map	—	CategoryTheory.cancel_mono instMonoICycles CategoryTheory.Category.assoc toCycles_i CategoryTheory.ComposableArrows.naturality' le_rfl cyclesMap_i toCycles_i_assoc CategoryTheory.Functor.map_comp CategoryTheory.ComposableArrows.hom_ext₁ CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
toCycles_cyclesMap_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₁ CategoryTheory.NatTrans.app CategoryTheory.ComposableArrows.mk₂	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ cycles toCycles cyclesMap CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toCycles_cyclesMap
toCycles_descCycles 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Functor.map CategoryTheory.ComposableArrows.twoδ₂Toδ₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ cycles toCycles descCycles	—	CategoryTheory.ShortComplex.Exact.g_desc CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory cokernelSequenceCycles_exact instEpiGCokernelSequenceCycles
toCycles_descCycles_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Functor.map CategoryTheory.ComposableArrows.twoδ₂Toδ₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ cycles toCycles descCycles	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toCycles_descCycles
toCycles_i 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ cycles toCycles iCycles CategoryTheory.Functor.map CategoryTheory.ComposableArrows.twoδ₁Toδ₀	—	CategoryTheory.Limits.kernel.lift_ι
toCycles_i_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ cycles toCycles iCycles CategoryTheory.Functor.map CategoryTheory.ComposableArrows.twoδ₁Toδ₀	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toCycles_i
δToCycles_iCycles 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ cycles δToCycles iCycles δ	—	liftCycles_i
δToCycles_iCycles_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ cycles δToCycles iCycles δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δToCycles_iCycles
δ_pOpcycles 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ opcycles δ pOpcycles Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.Limits.cokernel.condition
δ_pOpcycles_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ δ opcycles pOpcycles Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_pOpcycles
δ_toCycles 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ cycles δ toCycles δToCycles	—	CategoryTheory.cancel_mono instMonoICycles CategoryTheory.Category.assoc toCycles_i δToCycles_iCycles δ_naturality CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp
δ_toCycles_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ δ cycles toCycles δToCycles	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_toCycles

---

← Back to Index