Documentation Verification Report

Exact

๐Ÿ“ Source: Mathlib/Algebra/Homology/ShortComplex/Exact.lean

Statistics

MetricCount
Definitionsdesc, descToInjective, fIsKernel, gIsCokernel, leftHomologyDataOfIsLimitKernelFork, liftFromProjective, rightHomologyDataOfIsColimitCokernelCofork, Splitting, fIsKernel, gIsCokernel, homologyData, isoBinaryBiproduct, leftHomologyData, map, ofExactOfRetraction, ofExactOfSection, ofHasBinaryBiproduct, ofIsIsoOfIsZero, ofIsZeroOfIsIso, ofIso, op, r, rightHomologyData, s, splitEpi_g, splitMono_f, unop, cokernelSequence, kernelSequence
29
TheoremsinstPreservesEpimorphisms, instPreservesMonomorphisms, comp_descToInjective, comp_descToInjective_assoc, comp_eq_zero, comp_eq_zero_assoc, condition, desc', epi_f, epi_f', epi_f_iff, epi_kernelLift, epi_toCycles, g_desc, g_desc_assoc, hasHomology, hasZeroObject, isIso_f', isIso_fromOpcycles, isIso_g', isIso_toCycles, isZero_Xโ‚‚, isZero_Xโ‚‚_iff, isZero_of_both_zeros, leftHomologyDataOfIsLimitKernelFork_H, leftHomologyDataOfIsLimitKernelFork_K, leftHomologyDataOfIsLimitKernelFork_i, leftHomologyDataOfIsLimitKernelFork_ฯ€, lift', liftFromProjective_comp, liftFromProjective_comp_assoc, lift_f, lift_f_assoc, map, map_of_epi_of_preservesCokernel, map_of_mono_of_preservesKernel, map_of_preservesLeftHomologyOf, map_of_preservesRightHomologyOf, mono_cokernelDesc, mono_fromOpcycles, mono_g, mono_g', mono_g_iff, op, rightHomologyDataOfIsColimitCokernelCofork_H, rightHomologyDataOfIsColimitCokernelCofork_Q, rightHomologyDataOfIsColimitCokernelCofork_p, rightHomologyDataOfIsColimitCokernelCofork_ฮน, unop, exact_iff, exact_iff', exact_iff_i_p_zero, exact_iff, exact_iff_epi_f', exact_map_iff, exact_iff, exact_iff, exact_iff_mono_g', exact_map_iff, epi_g, exact, ext_r, ext_s, f_r, f_r_assoc, g_s, g_s_assoc, homologyData_iso, homologyData_left, homologyData_right, id, isSplitEpi_g, isSplitMono_f, isoBinaryBiproduct_hom, isoBinaryBiproduct_inv, leftHomologyData_H, leftHomologyData_K, leftHomologyData_i, leftHomologyData_ฯ€, map_r, map_s, mono_f, ofIso_r, ofIso_s, op_r, op_s, r_f, r_f_assoc, rightHomologyData_H, rightHomologyData_Q, rightHomologyData_p, rightHomologyData_ฮน, s_g, s_g_assoc, s_r, s_r_assoc, splitEpi_g_section_, splitMono_f_retraction, unop_r, unop_s, cokernelSequence_Xโ‚, cokernelSequence_Xโ‚‚, cokernelSequence_Xโ‚ƒ, cokernelSequence_exact, cokernelSequence_f, cokernelSequence_g, epi_ฯ„โ‚‚_of_exact_of_epi, exact_and_epi_g_iff_g_is_cokernel, exact_and_epi_g_iff_of_iso, exact_and_mono_f_iff_f_is_kernel, exact_and_mono_f_iff_of_iso, exact_iff_epi, exact_iff_epi_kernel_lift, exact_iff_epi_toCycles, exact_iff_homology_iso_zero, exact_iff_iCycles_pOpcycles_zero, exact_iff_i_p_zero, exact_iff_isZero_homology, exact_iff_isZero_leftHomology, exact_iff_isZero_rightHomology, exact_iff_kernel_ฮน_comp_cokernel_ฯ€_zero, exact_iff_mono, exact_iff_mono_cokernel_desc, exact_iff_mono_fromOpcycles, exact_iff_of_epi_of_isIso_of_mono, exact_iff_of_iso, exact_map_iff_of_faithful, exact_of_f_is_kernel, exact_of_g_is_cokernel, exact_of_isZero_Xโ‚‚, exact_of_iso, exact_op_iff, exact_unop_iff, instEpiGCokernelSequence, instMonoFKernelSequence, kernelSequence_Xโ‚, kernelSequence_Xโ‚‚, kernelSequence_Xโ‚ƒ, kernelSequence_exact, kernelSequence_f, kernelSequence_g, mono_ฯ„โ‚‚_of_exact_of_mono, quasiIso_iff_of_zeros, quasiIso_iff_of_zeros'
144
Total173

CategoryTheory.Functor

Theorems

NameKindAssumesProvesValidatesDepends On
instPreservesEpimorphisms ๐Ÿ“–mathematicalโ€”PreservesEpimorphismsโ€”CategoryTheory.Limits.comp_zero
CategoryTheory.ShortComplex.exact_iff_epi
map_zero
CategoryTheory.ShortComplex.Exact.map
PreservesHomology.preservesLeftHomologyOf
PreservesHomology.preservesRightHomologyOf
instPreservesMonomorphisms ๐Ÿ“–mathematicalโ€”PreservesMonomorphismsโ€”CategoryTheory.Limits.zero_comp
CategoryTheory.ShortComplex.exact_iff_mono
map_zero
CategoryTheory.ShortComplex.Exact.map
PreservesHomology.preservesLeftHomologyOf
PreservesHomology.preservesRightHomologyOf

CategoryTheory.ShortComplex

Definitions

NameCategoryTheorems
Splitting ๐Ÿ“–CompData
1 mathmath: CategoryTheory.Abelian.epiWithInjectiveKernel_iff
cokernelSequence ๐Ÿ“–CompOp
7 mathmath: cokernelSequence_f, cokernelSequence_g, cokernelSequence_exact, cokernelSequence_Xโ‚, cokernelSequence_Xโ‚ƒ, cokernelSequence_Xโ‚‚, instEpiGCokernelSequence
kernelSequence ๐Ÿ“–CompOp
7 mathmath: kernelSequence_exact, kernelSequence_Xโ‚, kernelSequence_f, kernelSequence_g, kernelSequence_Xโ‚ƒ, instMonoFKernelSequence, kernelSequence_Xโ‚‚

Theorems

NameKindAssumesProvesValidatesDepends On
cokernelSequence_Xโ‚ ๐Ÿ“–mathematicalโ€”Xโ‚
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
cokernelSequence
โ€”โ€”
cokernelSequence_Xโ‚‚ ๐Ÿ“–mathematicalโ€”Xโ‚‚
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
cokernelSequence
โ€”โ€”
cokernelSequence_Xโ‚ƒ ๐Ÿ“–mathematicalโ€”Xโ‚ƒ
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
cokernelSequence
CategoryTheory.Limits.cokernel
โ€”โ€”
cokernelSequence_exact ๐Ÿ“–mathematicalโ€”Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
cokernelSequence
โ€”exact_of_g_is_cokernel
CategoryTheory.Limits.HasCokernels.has_colimit
CategoryTheory.Abelian.has_cokernels
CategoryTheory.CategoryWithHomology.hasHomology
CategoryTheory.categoryWithHomology_of_abelian
cokernelSequence_f ๐Ÿ“–mathematicalโ€”f
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
cokernelSequence
โ€”โ€”
cokernelSequence_g ๐Ÿ“–mathematicalโ€”g
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
cokernelSequence
CategoryTheory.Limits.cokernel.ฯ€
โ€”โ€”
epi_ฯ„โ‚‚_of_exact_of_epi ๐Ÿ“–mathematicalExact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Epi
Xโ‚‚
Hom.ฯ„โ‚‚
โ€”CategoryTheory.op_mono_of_epi
mono_ฯ„โ‚‚_of_exact_of_mono
CategoryTheory.balanced_opposite
Exact.op
CategoryTheory.unop_epi_of_mono
exact_and_epi_g_iff_g_is_cokernel ๐Ÿ“–mathematicalโ€”Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Epi
Xโ‚‚
Xโ‚ƒ
g
CategoryTheory.Limits.IsColimit
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
Xโ‚
f
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.HasZeroMorphisms.zero
CategoryTheory.Limits.CokernelCofork.ofฯ€
zero
โ€”zero
exact_of_g_is_cokernel
CategoryTheory.Limits.epi_of_isColimit_cofork
exact_and_epi_g_iff_of_iso ๐Ÿ“–mathematicalโ€”Exact
CategoryTheory.Epi
Xโ‚‚
Xโ‚ƒ
g
โ€”CategoryTheory.MorphismProperty.arrow_mk_iso_iff
CategoryTheory.MorphismProperty.RespectsIso.epimorphisms
Hom.commโ‚‚โ‚ƒ
exact_iff_of_iso
exact_and_mono_f_iff_f_is_kernel ๐Ÿ“–mathematicalโ€”Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Mono
Xโ‚
Xโ‚‚
f
CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
Xโ‚ƒ
g
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.HasZeroMorphisms.zero
CategoryTheory.Limits.KernelFork.ofฮน
zero
โ€”zero
exact_of_f_is_kernel
CategoryTheory.Limits.mono_of_isLimit_fork
exact_and_mono_f_iff_of_iso ๐Ÿ“–mathematicalโ€”Exact
CategoryTheory.Mono
Xโ‚
Xโ‚‚
f
โ€”CategoryTheory.MorphismProperty.arrow_mk_iso_iff
CategoryTheory.MorphismProperty.RespectsIso.monomorphisms
Hom.commโ‚โ‚‚
exact_iff_of_iso
exact_iff_epi ๐Ÿ“–mathematicalg
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
Xโ‚‚
Xโ‚ƒ
CategoryTheory.Limits.HasZeroMorphisms.zero
Exact
CategoryTheory.Epi
Xโ‚
f
โ€”Exact.hasHomology
hasLeftHomology_of_hasHomology
toCycles_i
CategoryTheory.epi_comp
CategoryTheory.Preadditive.epi_of_isZero_cokernel'
toCycles_comp_homologyฯ€
CategoryTheory.epi_of_effectiveEpi
CategoryTheory.instEffectiveEpiOfIsIso
isIso_iCycles
CategoryTheory.Limits.comp_zero
CategoryTheory.Limits.isZero_zero
HomologyData.exact_iff
exact_iff_epi_kernel_lift ๐Ÿ“–mathematicalโ€”Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Epi
Xโ‚
CategoryTheory.Limits.kernel
Xโ‚‚
Xโ‚ƒ
g
CategoryTheory.Limits.kernel.lift
f
zero
โ€”zero
hasLeftHomology_of_hasHomology
exact_iff_epi_toCycles
CategoryTheory.MorphismProperty.arrow_mk_iso_iff
CategoryTheory.MorphismProperty.RespectsIso.epimorphisms
CategoryTheory.Category.id_comp
CategoryTheory.Limits.equalizer.hom_ext
CategoryTheory.Limits.kernel.lift_ฮน
CategoryTheory.Category.assoc
toCycles_i
exact_iff_epi_toCycles ๐Ÿ“–mathematicalโ€”Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Epi
Xโ‚
cycles
hasLeftHomology_of_hasHomology
toCycles
โ€”LeftHomologyData.exact_iff_epi_f'
hasLeftHomology_of_hasHomology
exact_iff_homology_iso_zero ๐Ÿ“–mathematicalโ€”Exact
CategoryTheory.Iso
homology
CategoryTheory.Limits.HasZeroObject.zero'
โ€”exact_iff_isZero_homology
CategoryTheory.Limits.IsZero.of_iso
CategoryTheory.Limits.isZero_zero
exact_iff_iCycles_pOpcycles_zero ๐Ÿ“–mathematicalโ€”Exact
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
cycles
hasLeftHomology_of_hasHomology
Xโ‚‚
opcycles
hasRightHomology_of_hasHomology
iCycles
pOpcycles
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.HasZeroMorphisms.zero
โ€”exact_iff_i_p_zero
hasLeftHomology_of_hasHomology
hasRightHomology_of_hasHomology
exact_iff_i_p_zero ๐Ÿ“–mathematicalโ€”Exact
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
LeftHomologyData.K
Xโ‚‚
RightHomologyData.Q
LeftHomologyData.i
RightHomologyData.p
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.HasZeroMorphisms.zero
โ€”HomologyData.exact_iff_i_p_zero
isIso_leftRightHomologyComparison'
exact_iff_isZero_homology ๐Ÿ“–mathematicalโ€”Exact
CategoryTheory.Limits.IsZero
homology
โ€”CategoryTheory.Limits.IsZero.of_iso
exact_iff_isZero_leftHomology ๐Ÿ“–mathematicalโ€”Exact
CategoryTheory.Limits.IsZero
leftHomology
hasLeftHomology_of_hasHomology
โ€”LeftHomologyData.exact_iff
hasLeftHomology_of_hasHomology
exact_iff_isZero_rightHomology ๐Ÿ“–mathematicalโ€”Exact
CategoryTheory.Limits.IsZero
rightHomology
hasRightHomology_of_hasHomology
โ€”RightHomologyData.exact_iff
hasRightHomology_of_hasHomology
exact_iff_kernel_ฮน_comp_cokernel_ฯ€_zero ๐Ÿ“–mathematicalโ€”Exact
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.kernel
Xโ‚‚
Xโ‚ƒ
g
CategoryTheory.Limits.cokernel
Xโ‚
f
CategoryTheory.Limits.kernel.ฮน
CategoryTheory.Limits.cokernel.ฯ€
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.HasZeroMorphisms.zero
โ€”exact_iff_i_p_zero
HasLeftHomology.hasCokernel
hasLeftHomology_of_hasHomology
HasRightHomology.hasKernel
hasRightHomology_of_hasHomology
exact_iff_mono ๐Ÿ“–mathematicalf
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
Xโ‚
Xโ‚‚
CategoryTheory.Limits.HasZeroMorphisms.zero
Exact
CategoryTheory.Mono
Xโ‚ƒ
g
โ€”Exact.hasHomology
hasRightHomology_of_hasHomology
isIso_pOpcycles
CategoryTheory.Preadditive.mono_of_isZero_kernel'
homologyฮน_comp_fromOpcycles
p_fromOpcycles
CategoryTheory.mono_comp
CategoryTheory.mono_of_strongMono
CategoryTheory.instStrongMonoOfIsRegularMono
CategoryTheory.instIsRegularMonoOfIsSplitMono
CategoryTheory.IsSplitMono.of_iso
CategoryTheory.Limits.zero_comp
CategoryTheory.Limits.isZero_zero
HomologyData.exact_iff
exact_iff_mono_cokernel_desc ๐Ÿ“–mathematicalโ€”Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Mono
CategoryTheory.Limits.cokernel
Xโ‚
Xโ‚‚
f
Xโ‚ƒ
CategoryTheory.Limits.cokernel.desc
g
zero
โ€”zero
hasRightHomology_of_hasHomology
exact_iff_mono_fromOpcycles
CategoryTheory.MorphismProperty.arrow_mk_iso_iff
CategoryTheory.MorphismProperty.RespectsIso.monomorphisms
CategoryTheory.Category.comp_id
CategoryTheory.Limits.coequalizer.hom_ext
CategoryTheory.Limits.cokernel.ฯ€_desc_assoc
p_fromOpcycles
CategoryTheory.Limits.cokernel.ฯ€_desc
exact_iff_mono_fromOpcycles ๐Ÿ“–mathematicalโ€”Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Mono
opcycles
hasRightHomology_of_hasHomology
Xโ‚ƒ
fromOpcycles
โ€”RightHomologyData.exact_iff_mono_g'
hasRightHomology_of_hasHomology
exact_iff_of_epi_of_isIso_of_mono ๐Ÿ“–mathematicalโ€”Exactโ€”โ€”
exact_iff_of_iso ๐Ÿ“–mathematicalโ€”Exactโ€”exact_of_iso
exact_map_iff_of_faithful ๐Ÿ“–mathematicalโ€”Exact
map
โ€”hasLeftHomology_of_hasHomology
LeftHomologyData.exact_iff
CategoryTheory.Limits.IsZero.iff_id_eq_zero
CategoryTheory.Functor.map_injective
CategoryTheory.Functor.map_id
CategoryTheory.Functor.map_zero
LeftHomologyData.isPreservedBy_of_preserves
LeftHomologyData.map_H
hasHomology_of_preserves
Exact.map
exact_of_f_is_kernel ๐Ÿ“–mathematicalโ€”Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
โ€”zero
hasLeftHomology_of_hasHomology
exact_iff_epi_toCycles
iCycles_g
CategoryTheory.cancel_mono
instMonoICycles
CategoryTheory.Category.assoc
toCycles_i
CategoryTheory.Category.id_comp
CategoryTheory.Limits.Fork.IsLimit.lift_ฮน
CategoryTheory.epi_of_effectiveEpi
CategoryTheory.instEffectiveEpiOfIsRegularEpi
CategoryTheory.instIsRegularEpiOfIsSplitEpi
exact_of_g_is_cokernel ๐Ÿ“–mathematicalโ€”Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
โ€”zero
hasRightHomology_of_hasHomology
exact_iff_mono_fromOpcycles
f_pOpcycles
CategoryTheory.cancel_epi
instEpiPOpcycles
p_fromOpcycles_assoc
CategoryTheory.Category.comp_id
CategoryTheory.Limits.Cofork.IsColimit.ฯ€_desc
CategoryTheory.mono_of_strongMono
CategoryTheory.instStrongMonoOfIsRegularMono
CategoryTheory.instIsRegularMonoOfIsSplitMono
exact_of_isZero_Xโ‚‚ ๐Ÿ“–mathematicalCategoryTheory.Limits.IsZero
Xโ‚‚
Exactโ€”CategoryTheory.Limits.IsZero.eq_of_tgt
CategoryTheory.Limits.IsZero.eq_of_src
HomologyData.exact_iff
exact_of_iso ๐Ÿ“–โ€”Exactโ€”โ€”โ€”
exact_op_iff ๐Ÿ“–mathematicalโ€”Exact
Opposite
CategoryTheory.Category.opposite
CategoryTheory.Limits.hasZeroMorphismsOpposite
op
โ€”Exact.unop
Exact.op
exact_unop_iff ๐Ÿ“–mathematicalโ€”Exact
unop
Opposite
CategoryTheory.Category.opposite
CategoryTheory.Limits.hasZeroMorphismsOpposite
โ€”exact_op_iff
instEpiGCokernelSequence ๐Ÿ“–mathematicalโ€”CategoryTheory.Epi
Xโ‚‚
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
cokernelSequence
Xโ‚ƒ
g
โ€”CategoryTheory.Limits.coequalizer.ฯ€_epi
instMonoFKernelSequence ๐Ÿ“–mathematicalโ€”CategoryTheory.Mono
Xโ‚
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
kernelSequence
Xโ‚‚
f
โ€”CategoryTheory.Limits.equalizer.ฮน_mono
kernelSequence_Xโ‚ ๐Ÿ“–mathematicalโ€”Xโ‚
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
kernelSequence
CategoryTheory.Limits.kernel
โ€”โ€”
kernelSequence_Xโ‚‚ ๐Ÿ“–mathematicalโ€”Xโ‚‚
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
kernelSequence
โ€”โ€”
kernelSequence_Xโ‚ƒ ๐Ÿ“–mathematicalโ€”Xโ‚ƒ
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
kernelSequence
โ€”โ€”
kernelSequence_exact ๐Ÿ“–mathematicalโ€”Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
kernelSequence
โ€”exact_of_f_is_kernel
CategoryTheory.Limits.HasKernels.has_limit
CategoryTheory.Abelian.has_kernels
CategoryTheory.CategoryWithHomology.hasHomology
CategoryTheory.categoryWithHomology_of_abelian
kernelSequence_f ๐Ÿ“–mathematicalโ€”f
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
kernelSequence
CategoryTheory.Limits.kernel.ฮน
โ€”โ€”
kernelSequence_g ๐Ÿ“–mathematicalโ€”g
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
kernelSequence
โ€”โ€”
mono_ฯ„โ‚‚_of_exact_of_mono ๐Ÿ“–mathematicalExact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Mono
Xโ‚‚
Hom.ฯ„โ‚‚
โ€”CategoryTheory.Preadditive.mono_iff_cancel_zero
CategoryTheory.cancel_mono
CategoryTheory.Category.assoc
Hom.commโ‚‚โ‚ƒ
Mathlib.Tactic.Reassoc.eq_whisker'
CategoryTheory.Limits.zero_comp
Exact.lift_f
Hom.commโ‚โ‚‚
quasiIso_iff_of_zeros ๐Ÿ“–mathematicalf
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
Xโ‚
Xโ‚‚
CategoryTheory.Limits.HasZeroMorphisms.zero
g
Xโ‚ƒ
QuasiIso
CategoryTheory.CategoryWithHomology.hasHomology
CategoryTheory.categoryWithHomology_of_abelian
Exact
Hom.ฯ„โ‚‚
CategoryTheory.Mono
โ€”Hom.commโ‚‚โ‚ƒ
CategoryTheory.Limits.zero_comp
CategoryTheory.CategoryWithHomology.hasHomology
CategoryTheory.categoryWithHomology_of_abelian
hasLeftHomology_of_hasHomology
quasiIso_iff_isIso_liftCycles
liftCycles_i
CategoryTheory.mono_comp
CategoryTheory.mono_of_strongMono
CategoryTheory.instStrongMonoOfIsRegularMono
CategoryTheory.instIsRegularMonoOfIsSplitMono
CategoryTheory.IsSplitMono.of_iso
instMonoICycles
exact_of_f_is_kernel
iCycles_g
zero
CategoryTheory.balanced_of_strongMonoCategory
CategoryTheory.strongMonoCategory_of_regularMonoCategory
CategoryTheory.regularMonoCategoryOfNormalMonoCategory
CategoryTheory.Abelian.toIsNormalMonoCategory
CategoryTheory.cancel_mono
CategoryTheory.Category.assoc
Exact.lift_f
CategoryTheory.Category.id_comp
quasiIso_iff_of_zeros' ๐Ÿ“–mathematicalg
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
Xโ‚‚
Xโ‚ƒ
CategoryTheory.Limits.HasZeroMorphisms.zero
f
Xโ‚
QuasiIso
CategoryTheory.CategoryWithHomology.hasHomology
CategoryTheory.categoryWithHomology_of_abelian
Exact
Hom.ฯ„โ‚‚
CategoryTheory.Epi
โ€”CategoryTheory.CategoryWithHomology.hasHomology
CategoryTheory.categoryWithHomology_of_abelian
instHasHomologyOppositeOp
quasiIso_opMap_iff
CategoryTheory.Limits.op_zero
quasiIso_iff_of_zeros
exact_unop_iff
CategoryTheory.unop_epi_of_mono
CategoryTheory.op_mono_of_epi

CategoryTheory.ShortComplex.Exact

Definitions

NameCategoryTheorems
desc ๐Ÿ“–CompOp
2 mathmath: g_desc_assoc, g_desc
descToInjective ๐Ÿ“–CompOp
2 mathmath: comp_descToInjective, comp_descToInjective_assoc
fIsKernel ๐Ÿ“–CompOpโ€”
gIsCokernel ๐Ÿ“–CompOpโ€”
leftHomologyDataOfIsLimitKernelFork ๐Ÿ“–CompOp
4 mathmath: leftHomologyDataOfIsLimitKernelFork_K, leftHomologyDataOfIsLimitKernelFork_ฯ€, leftHomologyDataOfIsLimitKernelFork_i, leftHomologyDataOfIsLimitKernelFork_H
liftFromProjective ๐Ÿ“–CompOp
2 mathmath: liftFromProjective_comp_assoc, liftFromProjective_comp
rightHomologyDataOfIsColimitCokernelCofork ๐Ÿ“–CompOp
4 mathmath: rightHomologyDataOfIsColimitCokernelCofork_H, rightHomologyDataOfIsColimitCokernelCofork_Q, rightHomologyDataOfIsColimitCokernelCofork_ฮน, rightHomologyDataOfIsColimitCokernelCofork_p

Theorems

NameKindAssumesProvesValidatesDepends On
comp_descToInjective ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.f
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.HasZeroMorphisms.zero
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.g
descToInjective
โ€”CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology
CategoryTheory.CategoryWithHomology.hasHomology
CategoryTheory.categoryWithHomology_of_abelian
CategoryTheory.Category.assoc
CategoryTheory.Injective.comp_factorThru
CategoryTheory.ShortComplex.p_descOpcycles
comp_descToInjective_assoc ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.f
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.HasZeroMorphisms.zero
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.g
descToInjective
โ€”CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
comp_descToInjective
comp_eq_zero ๐Ÿ“–โ€”CategoryTheory.ShortComplex.Exact
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.g
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.HasZeroMorphisms.zero
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.ShortComplex.f
โ€”โ€”hasHomology
CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology
CategoryTheory.ShortComplex.liftCycles_i
CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology
CategoryTheory.ShortComplex.p_descOpcycles
CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
CategoryTheory.ShortComplex.exact_iff_iCycles_pOpcycles_zero
CategoryTheory.Limits.zero_comp
CategoryTheory.Limits.comp_zero
comp_eq_zero_assoc ๐Ÿ“–โ€”CategoryTheory.ShortComplex.Exact
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.g
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.HasZeroMorphisms.zero
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.ShortComplex.f
โ€”โ€”CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
comp_eq_zero
condition ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.ExactCategoryTheory.Limits.IsZero
CategoryTheory.ShortComplex.LeftHomologyData.H
CategoryTheory.ShortComplex.HomologyData.left
โ€”โ€”
desc' ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.f
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.HasZeroMorphisms.zero
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.g
โ€”g_desc
epi_f ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.g
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.Limits.HasZeroMorphisms.zero
CategoryTheory.Epi
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.ShortComplex.f
โ€”hasHomology
CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology
mono_fromOpcycles
CategoryTheory.cancel_mono
CategoryTheory.Limits.zero_comp
CategoryTheory.ShortComplex.p_fromOpcycles
CategoryTheory.Preadditive.epi_of_cancel_zero
CategoryTheory.ShortComplex.p_descOpcycles
epi_f' ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Epi
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.ShortComplex.LeftHomologyData.K
CategoryTheory.ShortComplex.LeftHomologyData.f'
โ€”CategoryTheory.Preadditive.epi_of_isZero_cokernel'
CategoryTheory.ShortComplex.zero
CategoryTheory.ShortComplex.LeftHomologyData.wi
CategoryTheory.ShortComplex.LeftHomologyData.wฯ€
CategoryTheory.ShortComplex.LeftHomologyData.exact_iff
hasHomology
epi_f_iff ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Epi
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.f
CategoryTheory.ShortComplex.g
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.Limits.HasZeroMorphisms.zero
โ€”CategoryTheory.cancel_epi
CategoryTheory.ShortComplex.zero
CategoryTheory.Limits.comp_zero
epi_f
epi_kernelLift ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Epi
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.Limits.kernel
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.g
CategoryTheory.Limits.kernel.lift
CategoryTheory.ShortComplex.f
CategoryTheory.ShortComplex.zero
โ€”CategoryTheory.ShortComplex.zero
CategoryTheory.ShortComplex.exact_iff_epi_kernel_lift
epi_toCycles ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Epi
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.ShortComplex.cycles
CategoryTheory.ShortComplex.toCycles
โ€”epi_f'
g_desc ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.f
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.HasZeroMorphisms.zero
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.g
desc
โ€”CategoryTheory.Limits.Cofork.IsColimit.ฯ€_desc
CategoryTheory.ShortComplex.zero
g_desc_assoc ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.f
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.HasZeroMorphisms.zero
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.g
desc
โ€”CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
g_desc
hasHomology ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.ExactCategoryTheory.ShortComplex.HasHomologyโ€”CategoryTheory.ShortComplex.HasHomology.mk'
condition
hasZeroObject ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.ExactCategoryTheory.Limits.HasZeroObjectโ€”condition
isIso_f' ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.IsIso
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.ShortComplex.LeftHomologyData.K
CategoryTheory.ShortComplex.LeftHomologyData.f'
โ€”epi_f'
CategoryTheory.mono_of_mono_fac
CategoryTheory.ShortComplex.LeftHomologyData.f'_i
CategoryTheory.isIso_of_mono_of_epi
isIso_fromOpcycles ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.IsIso
CategoryTheory.ShortComplex.opcycles
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.fromOpcycles
โ€”isIso_g'
isIso_g' ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.IsIso
CategoryTheory.ShortComplex.RightHomologyData.Q
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.RightHomologyData.g'
โ€”mono_g'
CategoryTheory.epi_of_epi_fac
CategoryTheory.ShortComplex.RightHomologyData.p_g'
CategoryTheory.isIso_of_mono_of_epi
isIso_toCycles ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.IsIso
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.ShortComplex.cycles
CategoryTheory.ShortComplex.toCycles
โ€”isIso_f'
isZero_Xโ‚‚ ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.f
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.Limits.HasZeroMorphisms.zero
CategoryTheory.ShortComplex.g
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.Limits.IsZeroโ€”mono_g
CategoryTheory.Limits.IsZero.iff_id_eq_zero
CategoryTheory.cancel_mono
CategoryTheory.Limits.comp_zero
isZero_Xโ‚‚_iff ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Limits.IsZero
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.f
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.Limits.HasZeroMorphisms.zero
CategoryTheory.ShortComplex.g
CategoryTheory.ShortComplex.Xโ‚ƒ
โ€”CategoryTheory.Limits.IsZero.eq_of_tgt
CategoryTheory.Limits.IsZero.eq_of_src
isZero_Xโ‚‚
isZero_of_both_zeros ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.ShortComplex.f
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.Limits.HasZeroMorphisms.zero
CategoryTheory.ShortComplex.g
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.Limits.IsZeroโ€”CategoryTheory.ShortComplex.HomologyData.exact_iff
leftHomologyDataOfIsLimitKernelFork_H ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.LeftHomologyData.H
leftHomologyDataOfIsLimitKernelFork
CategoryTheory.Limits.HasZeroObject.zero'
โ€”โ€”
leftHomologyDataOfIsLimitKernelFork_K ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.LeftHomologyData.K
leftHomologyDataOfIsLimitKernelFork
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.g
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.HasZeroMorphisms.zero
โ€”โ€”
leftHomologyDataOfIsLimitKernelFork_i ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.LeftHomologyData.i
leftHomologyDataOfIsLimitKernelFork
CategoryTheory.Limits.Fork.ฮน
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.g
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.HasZeroMorphisms.zero
โ€”โ€”
leftHomologyDataOfIsLimitKernelFork_ฯ€ ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.LeftHomologyData.ฯ€
leftHomologyDataOfIsLimitKernelFork
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.Cone.pt
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.g
CategoryTheory.Limits.HasZeroMorphisms.zero
CategoryTheory.Limits.HasZeroObject.zero'
โ€”โ€”
lift' ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.g
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.HasZeroMorphisms.zero
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.ShortComplex.f
โ€”lift_f
liftFromProjective_comp ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.g
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.HasZeroMorphisms.zero
CategoryTheory.ShortComplex.Xโ‚
liftFromProjective
CategoryTheory.ShortComplex.f
โ€”CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology
CategoryTheory.CategoryWithHomology.hasHomology
CategoryTheory.categoryWithHomology_of_abelian
CategoryTheory.ShortComplex.toCycles_i
CategoryTheory.Projective.factorThru_comp_assoc
CategoryTheory.ShortComplex.liftCycles_i
liftFromProjective_comp_assoc ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Abelian.toPreadditive
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.g
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.HasZeroMorphisms.zero
CategoryTheory.ShortComplex.Xโ‚
liftFromProjective
CategoryTheory.ShortComplex.f
โ€”CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
liftFromProjective_comp
lift_f ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.g
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.HasZeroMorphisms.zero
CategoryTheory.ShortComplex.Xโ‚
lift
CategoryTheory.ShortComplex.f
โ€”CategoryTheory.Limits.Fork.IsLimit.lift_ฮน
lift_f_assoc ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.g
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.HasZeroMorphisms.zero
CategoryTheory.ShortComplex.Xโ‚
lift
CategoryTheory.ShortComplex.f
โ€”CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
lift_f
map ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.ExactCategoryTheory.ShortComplex.mapโ€”hasHomology
map_of_preservesLeftHomologyOf
CategoryTheory.ShortComplex.hasHomology_of_preserves
map_of_epi_of_preservesCokernel ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.mapโ€”CategoryTheory.ShortComplex.exact_of_g_is_cokernel
CategoryTheory.ShortComplex.zero
map_of_mono_of_preservesKernel ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.mapโ€”CategoryTheory.ShortComplex.exact_of_f_is_kernel
CategoryTheory.ShortComplex.zero
map_of_preservesLeftHomologyOf ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.ExactCategoryTheory.ShortComplex.mapโ€”hasHomology
CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology
CategoryTheory.ShortComplex.LeftHomologyData.exact_map_iff
CategoryTheory.ShortComplex.LeftHomologyData.isPreservedBy_of_preserves
CategoryTheory.Limits.IsZero.iff_id_eq_zero
CategoryTheory.Functor.map_id
CategoryTheory.ShortComplex.LeftHomologyData.exact_iff
CategoryTheory.Functor.map_zero
map_of_preservesRightHomologyOf ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.ExactCategoryTheory.ShortComplex.mapโ€”hasHomology
CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology
CategoryTheory.ShortComplex.RightHomologyData.exact_map_iff
CategoryTheory.ShortComplex.RightHomologyData.isPreservedBy_of_preserves
CategoryTheory.Limits.IsZero.iff_id_eq_zero
CategoryTheory.Functor.map_id
CategoryTheory.ShortComplex.RightHomologyData.exact_iff
CategoryTheory.Functor.map_zero
mono_cokernelDesc ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Mono
CategoryTheory.Limits.cokernel
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.f
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.Limits.cokernel.desc
CategoryTheory.ShortComplex.g
CategoryTheory.ShortComplex.zero
โ€”CategoryTheory.ShortComplex.zero
CategoryTheory.ShortComplex.exact_iff_mono_cokernel_desc
mono_fromOpcycles ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Mono
CategoryTheory.ShortComplex.opcycles
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.fromOpcycles
โ€”mono_g'
mono_g ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.f
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.Limits.HasZeroMorphisms.zero
CategoryTheory.Mono
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.g
โ€”hasHomology
CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology
epi_toCycles
CategoryTheory.cancel_epi
CategoryTheory.Limits.comp_zero
CategoryTheory.ShortComplex.toCycles_i
CategoryTheory.Preadditive.mono_of_cancel_zero
CategoryTheory.ShortComplex.liftCycles_i
mono_g' ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Mono
CategoryTheory.ShortComplex.RightHomologyData.Q
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.RightHomologyData.g'
โ€”CategoryTheory.Preadditive.mono_of_isZero_kernel'
CategoryTheory.ShortComplex.zero
CategoryTheory.ShortComplex.RightHomologyData.wp
CategoryTheory.ShortComplex.RightHomologyData.wฮน
CategoryTheory.ShortComplex.RightHomologyData.exact_iff
hasHomology
mono_g_iff ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Mono
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.g
CategoryTheory.ShortComplex.f
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.Limits.HasZeroMorphisms.zero
โ€”CategoryTheory.cancel_mono
CategoryTheory.ShortComplex.zero
CategoryTheory.Limits.zero_comp
mono_g
op ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.ExactOpposite
CategoryTheory.Category.opposite
CategoryTheory.Limits.hasZeroMorphismsOpposite
CategoryTheory.ShortComplex.op
โ€”CategoryTheory.Limits.IsZero.op
CategoryTheory.Limits.IsZero.of_iso
rightHomologyDataOfIsColimitCokernelCofork_H ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.RightHomologyData.H
rightHomologyDataOfIsColimitCokernelCofork
CategoryTheory.Limits.HasZeroObject.zero'
โ€”โ€”
rightHomologyDataOfIsColimitCokernelCofork_Q ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.RightHomologyData.Q
rightHomologyDataOfIsColimitCokernelCofork
CategoryTheory.Limits.Cocone.pt
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.f
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.HasZeroMorphisms.zero
โ€”โ€”
rightHomologyDataOfIsColimitCokernelCofork_p ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.RightHomologyData.p
rightHomologyDataOfIsColimitCokernelCofork
CategoryTheory.Limits.Cofork.ฯ€
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.f
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.HasZeroMorphisms.zero
โ€”โ€”
rightHomologyDataOfIsColimitCokernelCofork_ฮน ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.RightHomologyData.ฮน
rightHomologyDataOfIsColimitCokernelCofork
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.HasZeroObject.zero'
CategoryTheory.Limits.Cocone.pt
CategoryTheory.Limits.WalkingParallelPair
CategoryTheory.Limits.walkingParallelPairHomCategory
CategoryTheory.Limits.parallelPair
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.f
CategoryTheory.Limits.HasZeroMorphisms.zero
โ€”โ€”
unop ๐Ÿ“–mathematicalCategoryTheory.ShortComplex.Exact
Opposite
CategoryTheory.Category.opposite
CategoryTheory.Limits.hasZeroMorphismsOpposite
CategoryTheory.ShortComplex.unopโ€”CategoryTheory.Limits.IsZero.unop
CategoryTheory.Limits.IsZero.of_iso

CategoryTheory.ShortComplex.HomologyData

Theorems

NameKindAssumesProvesValidatesDepends On
exact_iff ๐Ÿ“–mathematicalโ€”CategoryTheory.ShortComplex.Exact
CategoryTheory.Limits.IsZero
CategoryTheory.ShortComplex.LeftHomologyData.H
left
โ€”CategoryTheory.ShortComplex.LeftHomologyData.exact_iff
CategoryTheory.ShortComplex.HasHomology.mk'
exact_iff' ๐Ÿ“–mathematicalโ€”CategoryTheory.ShortComplex.Exact
CategoryTheory.Limits.IsZero
CategoryTheory.ShortComplex.RightHomologyData.H
right
โ€”CategoryTheory.ShortComplex.RightHomologyData.exact_iff
CategoryTheory.ShortComplex.HasHomology.mk'
exact_iff_i_p_zero ๐Ÿ“–mathematicalโ€”CategoryTheory.ShortComplex.Exact
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.LeftHomologyData.K
left
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.RightHomologyData.Q
right
CategoryTheory.ShortComplex.LeftHomologyData.i
CategoryTheory.ShortComplex.RightHomologyData.p
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.HasZeroMorphisms.zero
โ€”CategoryTheory.ShortComplex.LeftHomologyData.exact_iff
CategoryTheory.ShortComplex.HasHomology.mk'
comm
CategoryTheory.Limits.IsZero.eq_of_src
CategoryTheory.Limits.zero_comp
CategoryTheory.Limits.comp_zero
CategoryTheory.cancel_mono
CategoryTheory.mono_of_strongMono
CategoryTheory.instStrongMonoOfIsRegularMono
CategoryTheory.instIsRegularMonoOfIsSplitMono
CategoryTheory.IsSplitMono.of_iso
CategoryTheory.Iso.isIso_hom
CategoryTheory.Category.id_comp
CategoryTheory.ShortComplex.RightHomologyData.instMonoฮน
CategoryTheory.cancel_epi
CategoryTheory.ShortComplex.LeftHomologyData.instEpiฯ€

CategoryTheory.ShortComplex.LeftHomologyData

Theorems

NameKindAssumesProvesValidatesDepends On
exact_iff ๐Ÿ“–mathematicalโ€”CategoryTheory.ShortComplex.Exact
CategoryTheory.Limits.IsZero
H
โ€”CategoryTheory.ShortComplex.exact_iff_isZero_homology
CategoryTheory.Iso.isZero_iff
exact_iff_epi_f' ๐Ÿ“–mathematicalโ€”CategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Epi
CategoryTheory.ShortComplex.Xโ‚
K
f'
โ€”CategoryTheory.ShortComplex.Exact.epi_f'
exact_iff
CategoryTheory.cancel_epi
instEpiฯ€
CategoryTheory.Category.comp_id
CategoryTheory.Limits.comp_zero
f'_ฯ€
exact_map_iff ๐Ÿ“–mathematicalโ€”CategoryTheory.ShortComplex.Exact
CategoryTheory.ShortComplex.map
CategoryTheory.Limits.IsZero
CategoryTheory.Functor.obj
H
โ€”exact_iff

CategoryTheory.ShortComplex.QuasiIso

Theorems

NameKindAssumesProvesValidatesDepends On
exact_iff ๐Ÿ“–mathematicalโ€”CategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
โ€”CategoryTheory.Iso.isZero_iff
isIso

CategoryTheory.ShortComplex.RightHomologyData

Theorems

NameKindAssumesProvesValidatesDepends On
exact_iff ๐Ÿ“–mathematicalโ€”CategoryTheory.ShortComplex.Exact
CategoryTheory.Limits.IsZero
H
โ€”CategoryTheory.ShortComplex.exact_iff_isZero_homology
CategoryTheory.Iso.isZero_iff
exact_iff_mono_g' ๐Ÿ“–mathematicalโ€”CategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Mono
Q
CategoryTheory.ShortComplex.Xโ‚ƒ
g'
โ€”CategoryTheory.ShortComplex.Exact.mono_g'
exact_iff
CategoryTheory.cancel_mono
instMonoฮน
CategoryTheory.Category.id_comp
CategoryTheory.Limits.zero_comp
ฮน_g'
exact_map_iff ๐Ÿ“–mathematicalโ€”CategoryTheory.ShortComplex.Exact
CategoryTheory.ShortComplex.map
CategoryTheory.Limits.IsZero
CategoryTheory.Functor.obj
H
โ€”exact_iff

CategoryTheory.ShortComplex.Splitting

Definitions

NameCategoryTheorems
fIsKernel ๐Ÿ“–CompOpโ€”
gIsCokernel ๐Ÿ“–CompOpโ€”
homologyData ๐Ÿ“–CompOp
3 mathmath: homologyData_right, homologyData_left, homologyData_iso
isoBinaryBiproduct ๐Ÿ“–CompOp
2 mathmath: isoBinaryBiproduct_hom, isoBinaryBiproduct_inv
leftHomologyData ๐Ÿ“–CompOp
5 mathmath: leftHomologyData_K, leftHomologyData_H, leftHomologyData_ฯ€, leftHomologyData_i, homologyData_left
map ๐Ÿ“–CompOp
2 mathmath: map_s, map_r
ofExactOfRetraction ๐Ÿ“–CompOpโ€”
ofExactOfSection ๐Ÿ“–CompOpโ€”
ofHasBinaryBiproduct ๐Ÿ“–CompOpโ€”
ofIsIsoOfIsZero ๐Ÿ“–CompOpโ€”
ofIsZeroOfIsIso ๐Ÿ“–CompOpโ€”
ofIso ๐Ÿ“–CompOp
2 mathmath: ofIso_s, ofIso_r
op ๐Ÿ“–CompOp
2 mathmath: op_r, op_s
r ๐Ÿ“–CompOp
18 mathmath: op_r, id, map_r, g_s, splitMono_f_retraction, unop_r, g_s_assoc, f_r_assoc, CochainComplex.mappingCone.triangleRotateShortComplexSplitting_r, op_s, r_f, s_r, r_f_assoc, ofIso_r, f_r, unop_s, isoBinaryBiproduct_hom, s_r_assoc
rightHomologyData ๐Ÿ“–CompOp
5 mathmath: homologyData_right, rightHomologyData_ฮน, rightHomologyData_p, rightHomologyData_Q, rightHomologyData_H
s ๐Ÿ“–CompOp
18 mathmath: op_r, map_s, s_g, id, s_g_assoc, g_s, unop_r, ofIso_s, splitEpi_g_section_, g_s_assoc, op_s, r_f, s_r, r_f_assoc, CochainComplex.mappingCone.triangleRotateShortComplexSplitting_s, unop_s, s_r_assoc, isoBinaryBiproduct_inv
splitEpi_g ๐Ÿ“–CompOp
1 mathmath: splitEpi_g_section_
splitMono_f ๐Ÿ“–CompOp
1 mathmath: splitMono_f_retraction
unop ๐Ÿ“–CompOp
2 mathmath: unop_r, unop_s

Theorems

NameKindAssumesProvesValidatesDepends On
epi_g ๐Ÿ“–mathematicalโ€”CategoryTheory.Epi
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.g
โ€”isSplitEpi_g
CategoryTheory.epi_of_effectiveEpi
CategoryTheory.instEffectiveEpiOfIsRegularEpi
CategoryTheory.instIsRegularEpiOfIsSplitEpi
exact ๐Ÿ“–mathematicalโ€”CategoryTheory.ShortComplex.Exact
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
โ€”CategoryTheory.Limits.isZero_zero
ext_r ๐Ÿ“–โ€”rโ€”โ€”epi_g
id
CategoryTheory.cancel_epi
AddLeftCancelSemigroup.toIsLeftCancelAdd
ext_s ๐Ÿ“–โ€”sโ€”โ€”mono_f
id
CategoryTheory.cancel_mono
AddRightCancelSemigroup.toIsRightCancelAdd
f_r ๐Ÿ“–mathematicalโ€”CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.f
r
CategoryTheory.CategoryStruct.id
โ€”โ€”
f_r_assoc ๐Ÿ“–mathematicalโ€”CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.f
r
โ€”CategoryTheory.Category.assoc
CategoryTheory.Category.id_comp
Mathlib.Tactic.Reassoc.eq_whisker'
f_r
g_s ๐Ÿ“–mathematicalโ€”CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.g
s
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
SubNegMonoid.toSub
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
CategoryTheory.Preadditive.homGroup
CategoryTheory.CategoryStruct.id
CategoryTheory.ShortComplex.Xโ‚
r
CategoryTheory.ShortComplex.f
โ€”id
add_sub_cancel_left
g_s_assoc ๐Ÿ“–mathematicalโ€”CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.g
s
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
SubNegMonoid.toSub
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
CategoryTheory.Preadditive.homGroup
CategoryTheory.CategoryStruct.id
CategoryTheory.ShortComplex.Xโ‚
r
CategoryTheory.ShortComplex.f
โ€”CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
g_s
homologyData_iso ๐Ÿ“–mathematicalโ€”CategoryTheory.ShortComplex.HomologyData.iso
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
homologyData
CategoryTheory.Iso.refl
CategoryTheory.Limits.HasZeroObject.zero'
โ€”โ€”
homologyData_left ๐Ÿ“–mathematicalโ€”CategoryTheory.ShortComplex.HomologyData.left
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
homologyData
leftHomologyData
โ€”โ€”
homologyData_right ๐Ÿ“–mathematicalโ€”CategoryTheory.ShortComplex.HomologyData.right
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
homologyData
rightHomologyData
โ€”โ€”
id ๐Ÿ“–mathematicalโ€”Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
AddCommGroup.toAddCommMonoid
CategoryTheory.Preadditive.homGroup
CategoryTheory.CategoryStruct.comp
CategoryTheory.ShortComplex.Xโ‚
r
CategoryTheory.ShortComplex.f
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.g
s
CategoryTheory.CategoryStruct.id
โ€”โ€”
isSplitEpi_g ๐Ÿ“–mathematicalโ€”CategoryTheory.IsSplitEpi
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.g
โ€”โ€”
isSplitMono_f ๐Ÿ“–mathematicalโ€”CategoryTheory.IsSplitMono
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.f
โ€”โ€”
isoBinaryBiproduct_hom ๐Ÿ“–mathematicalโ€”CategoryTheory.Iso.hom
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Limits.biprod
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.ShortComplex.Xโ‚ƒ
isoBinaryBiproduct
CategoryTheory.Limits.biprod.lift
r
CategoryTheory.ShortComplex.g
โ€”โ€”
isoBinaryBiproduct_inv ๐Ÿ“–mathematicalโ€”CategoryTheory.Iso.inv
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Limits.biprod
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.ShortComplex.Xโ‚ƒ
isoBinaryBiproduct
CategoryTheory.Limits.biprod.desc
CategoryTheory.ShortComplex.f
s
โ€”โ€”
leftHomologyData_H ๐Ÿ“–mathematicalโ€”CategoryTheory.ShortComplex.LeftHomologyData.H
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
leftHomologyData
CategoryTheory.Limits.HasZeroObject.zero'
โ€”โ€”
leftHomologyData_K ๐Ÿ“–mathematicalโ€”CategoryTheory.ShortComplex.LeftHomologyData.K
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
leftHomologyData
CategoryTheory.ShortComplex.Xโ‚
โ€”โ€”
leftHomologyData_i ๐Ÿ“–mathematicalโ€”CategoryTheory.ShortComplex.LeftHomologyData.i
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
leftHomologyData
CategoryTheory.ShortComplex.f
โ€”โ€”
leftHomologyData_ฯ€ ๐Ÿ“–mathematicalโ€”CategoryTheory.ShortComplex.LeftHomologyData.ฯ€
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
leftHomologyData
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.Limits.HasZeroObject.zero'
CategoryTheory.Limits.HasZeroMorphisms.zero
โ€”โ€”
map_r ๐Ÿ“–mathematicalโ€”r
CategoryTheory.ShortComplex.map
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Functor.preservesZeroMorphisms_of_additive
map
CategoryTheory.Functor.map
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.Xโ‚
โ€”CategoryTheory.Functor.preservesZeroMorphisms_of_additive
map_s ๐Ÿ“–mathematicalโ€”s
CategoryTheory.ShortComplex.map
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.Functor.preservesZeroMorphisms_of_additive
map
CategoryTheory.Functor.map
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.Xโ‚‚
โ€”CategoryTheory.Functor.preservesZeroMorphisms_of_additive
mono_f ๐Ÿ“–mathematicalโ€”CategoryTheory.Mono
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.f
โ€”isSplitMono_f
CategoryTheory.mono_of_strongMono
CategoryTheory.instStrongMonoOfIsRegularMono
CategoryTheory.instIsRegularMonoOfIsSplitMono
ofIso_r ๐Ÿ“–mathematicalโ€”r
ofIso
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.ShortComplex.Hom.ฯ„โ‚‚
CategoryTheory.Iso.inv
CategoryTheory.ShortComplex
CategoryTheory.ShortComplex.instCategory
CategoryTheory.ShortComplex.Hom.ฯ„โ‚
CategoryTheory.Iso.hom
โ€”โ€”
ofIso_s ๐Ÿ“–mathematicalโ€”s
ofIso
CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.Hom.ฯ„โ‚ƒ
CategoryTheory.Iso.inv
CategoryTheory.ShortComplex
CategoryTheory.ShortComplex.instCategory
CategoryTheory.ShortComplex.Hom.ฯ„โ‚‚
CategoryTheory.Iso.hom
โ€”โ€”
op_r ๐Ÿ“–mathematicalโ€”r
Opposite
CategoryTheory.Category.opposite
CategoryTheory.instPreadditiveOpposite
CategoryTheory.ShortComplex.op
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
op
Quiver.Hom.op
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.Xโ‚‚
s
โ€”โ€”
op_s ๐Ÿ“–mathematicalโ€”s
Opposite
CategoryTheory.Category.opposite
CategoryTheory.instPreadditiveOpposite
CategoryTheory.ShortComplex.op
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
op
Quiver.Hom.op
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.Xโ‚
r
โ€”โ€”
r_f ๐Ÿ“–mathematicalโ€”CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.Xโ‚
r
CategoryTheory.ShortComplex.f
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
SubNegMonoid.toSub
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
CategoryTheory.Preadditive.homGroup
CategoryTheory.CategoryStruct.id
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.g
s
โ€”id
add_sub_cancel_right
r_f_assoc ๐Ÿ“–mathematicalโ€”CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.Xโ‚
r
CategoryTheory.ShortComplex.f
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
SubNegMonoid.toSub
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
CategoryTheory.Preadditive.homGroup
CategoryTheory.CategoryStruct.id
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.g
s
โ€”CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
r_f
rightHomologyData_H ๐Ÿ“–mathematicalโ€”CategoryTheory.ShortComplex.RightHomologyData.H
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
rightHomologyData
CategoryTheory.Limits.HasZeroObject.zero'
โ€”โ€”
rightHomologyData_Q ๐Ÿ“–mathematicalโ€”CategoryTheory.ShortComplex.RightHomologyData.Q
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
rightHomologyData
CategoryTheory.ShortComplex.Xโ‚ƒ
โ€”โ€”
rightHomologyData_p ๐Ÿ“–mathematicalโ€”CategoryTheory.ShortComplex.RightHomologyData.p
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
rightHomologyData
CategoryTheory.ShortComplex.g
โ€”โ€”
rightHomologyData_ฮน ๐Ÿ“–mathematicalโ€”CategoryTheory.ShortComplex.RightHomologyData.ฮน
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
rightHomologyData
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.Limits.HasZeroObject.zero'
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.Limits.HasZeroMorphisms.zero
โ€”โ€”
s_g ๐Ÿ“–mathematicalโ€”CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.Xโ‚‚
s
CategoryTheory.ShortComplex.g
CategoryTheory.CategoryStruct.id
โ€”โ€”
s_g_assoc ๐Ÿ“–mathematicalโ€”CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.Xโ‚‚
s
CategoryTheory.ShortComplex.g
โ€”CategoryTheory.Category.assoc
CategoryTheory.Category.id_comp
Mathlib.Tactic.Reassoc.eq_whisker'
s_g
s_r ๐Ÿ“–mathematicalโ€”CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.Xโ‚
s
r
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.HasZeroMorphisms.zero
โ€”epi_g
CategoryTheory.cancel_epi
g_s_assoc
CategoryTheory.Preadditive.sub_comp
CategoryTheory.Category.id_comp
CategoryTheory.Category.assoc
f_r
CategoryTheory.Category.comp_id
sub_self
CategoryTheory.Limits.comp_zero
s_r_assoc ๐Ÿ“–mathematicalโ€”CategoryTheory.CategoryStruct.comp
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.Xโ‚‚
s
CategoryTheory.ShortComplex.Xโ‚
r
Quiver.Hom
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Limits.HasZeroMorphisms.zero
โ€”CategoryTheory.Category.assoc
Mathlib.Tactic.Reassoc.eq_whisker'
s_r
splitEpi_g_section_ ๐Ÿ“–mathematicalโ€”CategoryTheory.SplitEpi.section_
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.Xโ‚ƒ
CategoryTheory.ShortComplex.g
splitEpi_g
s
โ€”โ€”
splitMono_f_retraction ๐Ÿ“–mathematicalโ€”CategoryTheory.SplitMono.retraction
CategoryTheory.ShortComplex.Xโ‚
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
CategoryTheory.ShortComplex.Xโ‚‚
CategoryTheory.ShortComplex.f
splitMono_f
r
โ€”โ€”
unop_r ๐Ÿ“–mathematicalโ€”r
CategoryTheory.ShortComplex.unop
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
unop
Quiver.Hom.unop
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚ƒ
Opposite
CategoryTheory.Category.opposite
CategoryTheory.instPreadditiveOpposite
CategoryTheory.ShortComplex.Xโ‚‚
s
โ€”โ€”
unop_s ๐Ÿ“–mathematicalโ€”s
CategoryTheory.ShortComplex.unop
CategoryTheory.Preadditive.preadditiveHasZeroMorphisms
unop
Quiver.Hom.unop
CategoryTheory.CategoryStruct.toQuiver
CategoryTheory.Category.toCategoryStruct
CategoryTheory.ShortComplex.Xโ‚‚
Opposite
CategoryTheory.Category.opposite
CategoryTheory.instPreadditiveOpposite
CategoryTheory.ShortComplex.Xโ‚
r
โ€”โ€”

---

โ† Back to Index