ExtendHomology

📁 Source: Mathlib/Algebra/Homology/Embedding/ExtendHomology.lean

Statistics

Metric	Count
Definitions homologyData, homologyData', leftHomologyData, cokernelCofork, isColimitCokernelCofork, isLimitKernelFork, kernelFork, rightHomologyData, cokernelCofork, isColimitCokernelCofork, isLimitKernelFork, kernelFork, extendCyclesIso, extendHomologyIso, extendOpcyclesIso	15
Theorems comp_d_eq_zero_iff, d_comp_eq_zero_iff, hasHomology, homologyData'_iso, homologyData'_left_H, homologyData'_left_K, homologyData'_left_i, homologyData'_left_π, homologyData'_right_H, homologyData'_right_Q, homologyData'_right_p, homologyData'_right_ι, homologyData_iso, homologyData_left, homologyData_right, instHasHomology, instHasHomologyF, lift_d_comp_eq_zero_iff, lift_d_comp_eq_zero_iff', leftHomologyData_H, leftHomologyData_K, leftHomologyData_i, leftHomologyData_π, d_comp_desc_eq_zero_iff, d_comp_desc_eq_zero_iff', rightHomologyData_H, rightHomologyData_Q, rightHomologyData_g', rightHomologyData_p, rightHomologyData_ι, extendCyclesIso_hom_iCycles, extendCyclesIso_hom_iCycles_assoc, extendCyclesIso_hom_naturality, extendCyclesIso_hom_naturality_assoc, extendCyclesIso_inv_iCycles, extendCyclesIso_inv_iCycles_assoc, extendHomologyIso_hom_homologyι, extendHomologyIso_hom_homologyι_assoc, extendHomologyIso_hom_naturality, extendHomologyIso_hom_naturality_assoc, extendHomologyIso_inv_homologyι, extendHomologyIso_inv_homologyι_assoc, extend_exactAt, extend_exactAt_iff, homologyπ_extendHomologyIso_hom, homologyπ_extendHomologyIso_hom_assoc, homologyπ_extendHomologyIso_inv, homologyπ_extendHomologyIso_inv_assoc, instQuasiIsoExtendMap, pOpcycles_extendOpcyclesIso_hom, pOpcycles_extendOpcyclesIso_hom_assoc, pOpcycles_extendOpcyclesIso_inv, pOpcycles_extendOpcyclesIso_inv_assoc, quasiIsoAt_extendMap_iff, quasiIso_extendMap_iff	55
Total	70

HomologicalComplex

Definitions

Name	Category	Theorems
extendCyclesIso 📖	CompOp	10 math math: homologyπ_extendHomologyIso_hom, homologyπ_extendHomologyIso_inv, extendCyclesIso_inv_iCycles_assoc, extendCyclesIso_hom_naturality_assoc, homologyπ_extendHomologyIso_inv_assoc, extendCyclesIso_hom_iCycles, homologyπ_extendHomologyIso_hom_assoc, extendCyclesIso_hom_naturality, extendCyclesIso_inv_iCycles, extendCyclesIso_hom_iCycles_assoc
extendHomologyIso 📖	CompOp	10 math math: homologyπ_extendHomologyIso_hom, extendHomologyIso_hom_naturality, extendHomologyIso_hom_naturality_assoc, extendHomologyIso_hom_homologyι_assoc, homologyπ_extendHomologyIso_inv, homologyπ_extendHomologyIso_inv_assoc, homologyπ_extendHomologyIso_hom_assoc, extendHomologyIso_inv_homologyι, extendHomologyIso_inv_homologyι_assoc, extendHomologyIso_hom_homologyι
extendOpcyclesIso 📖	CompOp	8 math math: extendHomologyIso_hom_homologyι_assoc, pOpcycles_extendOpcyclesIso_hom_assoc, pOpcycles_extendOpcyclesIso_inv, pOpcycles_extendOpcyclesIso_hom, extendHomologyIso_inv_homologyι, extendHomologyIso_inv_homologyι_assoc, pOpcycles_extendOpcyclesIso_inv_assoc, extendHomologyIso_hom_homologyι

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
extendCyclesIso_hom_iCycles 📖	mathematical	ComplexShape.Embedding.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles extend X CategoryTheory.Iso.hom extendCyclesIso iCycles extendXIso	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_inv CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Category.assoc CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_inv_comp_iCycles_assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_hom_comp_i
extendCyclesIso_hom_iCycles_assoc 📖	mathematical	ComplexShape.Embedding.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles extend CategoryTheory.Iso.hom extendCyclesIso X iCycles extendXIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' extendCyclesIso_hom_iCycles
extendCyclesIso_hom_naturality 📖	mathematical	ComplexShape.Embedding.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles extend cyclesMap extendMap CategoryTheory.Iso.hom extendCyclesIso	—	CategoryTheory.cancel_mono instMonoICycles CategoryTheory.Category.assoc extendCyclesIso_hom_iCycles cyclesMap_i_assoc extendMap_f CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id cyclesMap_i extendCyclesIso_hom_iCycles_assoc
extendCyclesIso_hom_naturality_assoc 📖	mathematical	ComplexShape.Embedding.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles extend cyclesMap extendMap CategoryTheory.Iso.hom extendCyclesIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' extendCyclesIso_hom_naturality
extendCyclesIso_inv_iCycles 📖	mathematical	ComplexShape.Embedding.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles extend X CategoryTheory.Iso.inv extendCyclesIso iCycles extendXIso	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom CategoryTheory.Iso.hom_inv_id_assoc extendCyclesIso_hom_iCycles_assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
extendCyclesIso_inv_iCycles_assoc 📖	mathematical	ComplexShape.Embedding.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles extend CategoryTheory.Iso.inv extendCyclesIso X iCycles extendXIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' extendCyclesIso_inv_iCycles
extendHomologyIso_hom_homologyι 📖	mathematical	ComplexShape.Embedding.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology extend opcycles CategoryTheory.Iso.hom extendHomologyIso homologyι extendOpcyclesIso	—	CategoryTheory.cancel_epi instEpiHomologyπ homologyπ_extendHomologyIso_hom_assoc homology_π_ι extendCyclesIso_hom_iCycles_assoc homology_π_ι_assoc pOpcycles_extendOpcyclesIso_hom
extendHomologyIso_hom_homologyι_assoc 📖	mathematical	ComplexShape.Embedding.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology extend CategoryTheory.Iso.hom extendHomologyIso opcycles homologyι extendOpcyclesIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' extendHomologyIso_hom_homologyι
extendHomologyIso_hom_naturality 📖	mathematical	ComplexShape.Embedding.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology extend homologyMap extendMap CategoryTheory.Iso.hom extendHomologyIso	—	CategoryTheory.cancel_epi instEpiHomologyπ homologyπ_naturality_assoc homologyπ_extendHomologyIso_hom extendCyclesIso_hom_naturality_assoc homologyπ_extendHomologyIso_hom_assoc homologyπ_naturality
extendHomologyIso_hom_naturality_assoc 📖	mathematical	ComplexShape.Embedding.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology extend homologyMap extendMap CategoryTheory.Iso.hom extendHomologyIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' extendHomologyIso_hom_naturality
extendHomologyIso_inv_homologyι 📖	mathematical	ComplexShape.Embedding.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology extend opcycles CategoryTheory.Iso.inv extendHomologyIso homologyι extendOpcyclesIso	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom CategoryTheory.Iso.hom_inv_id_assoc extendHomologyIso_hom_homologyι_assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
extendHomologyIso_inv_homologyι_assoc 📖	mathematical	ComplexShape.Embedding.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology extend CategoryTheory.Iso.inv extendHomologyIso opcycles homologyι extendOpcyclesIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' extendHomologyIso_inv_homologyι
extend_exactAt 📖	mathematical	—	ExactAt extend	—	exactAt_of_isSupported instIsSupportedOfIsStrictlySupported instIsStrictlySupportedExtend
extend_exactAt_iff 📖	mathematical	ComplexShape.Embedding.f	ExactAt extend	—	CategoryTheory.Iso.isZero_iff
homologyπ_extendHomologyIso_hom 📖	mathematical	ComplexShape.Embedding.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles extend homology homologyπ CategoryTheory.Iso.hom extendHomologyIso extendCyclesIso	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.ShortComplex.LeftHomologyData.homologyπ_comp_homologyIso_hom_assoc CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id CategoryTheory.ShortComplex.LeftHomologyData.homologyπ_comp_homologyIso_hom CategoryTheory.Iso.inv_hom_id_assoc
homologyπ_extendHomologyIso_hom_assoc 📖	mathematical	ComplexShape.Embedding.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles extend homology homologyπ CategoryTheory.Iso.hom extendHomologyIso extendCyclesIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homologyπ_extendHomologyIso_hom
homologyπ_extendHomologyIso_inv 📖	mathematical	ComplexShape.Embedding.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles homology extend homologyπ CategoryTheory.Iso.inv extendHomologyIso extendCyclesIso	—	CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id homologyπ_extendHomologyIso_hom CategoryTheory.Iso.inv_hom_id_assoc
homologyπ_extendHomologyIso_inv_assoc 📖	mathematical	ComplexShape.Embedding.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles homology homologyπ extend CategoryTheory.Iso.inv extendHomologyIso extendCyclesIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homologyπ_extendHomologyIso_inv
instQuasiIsoExtendMap 📖	mathematical	HasHomology	QuasiIso extend extendMap extend.instHasHomology	—	extend.instHasHomology quasiIso_extendMap_iff
pOpcycles_extendOpcyclesIso_hom 📖	mathematical	ComplexShape.Embedding.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X extend opcycles pOpcycles CategoryTheory.Iso.hom extendOpcyclesIso extendXIso	—	CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_inv CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id pOpcycles_extendOpcyclesIso_inv CategoryTheory.Iso.hom_inv_id_assoc
pOpcycles_extendOpcyclesIso_hom_assoc 📖	mathematical	ComplexShape.Embedding.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X extend opcycles pOpcycles CategoryTheory.Iso.hom extendOpcyclesIso extendXIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pOpcycles_extendOpcyclesIso_hom
pOpcycles_extendOpcyclesIso_inv 📖	mathematical	ComplexShape.Embedding.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X opcycles extend pOpcycles CategoryTheory.Iso.inv extendOpcyclesIso extendXIso	—	CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id CategoryTheory.ShortComplex.RightHomologyData.pOpcycles_comp_opcyclesIso_hom_assoc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.ShortComplex.RightHomologyData.p_comp_opcyclesIso_inv
pOpcycles_extendOpcyclesIso_inv_assoc 📖	mathematical	ComplexShape.Embedding.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X opcycles pOpcycles extend CategoryTheory.Iso.inv extendOpcyclesIso extendXIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pOpcycles_extendOpcyclesIso_inv
quasiIsoAt_extendMap_iff 📖	mathematical	ComplexShape.Embedding.f	QuasiIsoAt extend extendMap	—	CategoryTheory.MorphismProperty.arrow_mk_iso_iff CategoryTheory.MorphismProperty.RespectsIso.isomorphisms extendHomologyIso_hom_naturality
quasiIso_extendMap_iff 📖	mathematical	HasHomology	QuasiIso extend extendMap extend.instHasHomology	—	extend.instHasHomology extend.instHasHomologyF quasiIsoAt_extendMap_iff quasiIsoAt_iff_exactAt extend_exactAt

HomologicalComplex.extend

Definitions

Name	Category	Theorems
homologyData 📖	CompOp	3 math math: homologyData_left, homologyData_iso, homologyData_right
homologyData' 📖	CompOp	9 math math: homologyData'_left_H, homologyData'_right_H, homologyData'_iso, homologyData'_right_p, homologyData'_left_i, homologyData'_right_ι, homologyData'_right_Q, homologyData'_left_π, homologyData'_left_K
leftHomologyData 📖	CompOp	5 math math: leftHomologyData_π, homologyData_left, leftHomologyData_H, leftHomologyData_i, leftHomologyData_K
rightHomologyData 📖	CompOp	8 math math: HomologicalComplex.truncGE.rightHomologyMapData_φQ, rightHomologyData_p, rightHomologyData_g', rightHomologyData_ι, rightHomologyData_H, HomologicalComplex.truncGE.rightHomologyMapData_φH, homologyData_right, rightHomologyData_Q

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_d_eq_zero_iff 📖	mathematical	ComplexShape.Embedding.f ComplexShape.next	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero HomologicalComplex.extend CategoryTheory.Iso.inv HomologicalComplex.extendXIso	—	ComplexShape.next_eq' ComplexShape.Embedding.rel HomologicalComplex.extend_d_eq CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_inv CategoryTheory.Limits.zero_comp CategoryTheory.Category.assoc HomologicalComplex.shape CategoryTheory.Limits.comp_zero HomologicalComplex.extend_d_from_eq_zero
d_comp_eq_zero_iff 📖	mathematical	ComplexShape.Embedding.f ComplexShape.prev	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero HomologicalComplex.extend CategoryTheory.Iso.hom HomologicalComplex.extendXIso	—	ComplexShape.prev_eq' ComplexShape.Embedding.rel HomologicalComplex.extend_d_eq CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom CategoryTheory.Limits.comp_zero HomologicalComplex.shape CategoryTheory.Limits.zero_comp HomologicalComplex.extend_d_to_eq_zero
hasHomology 📖	mathematical	ComplexShape.Embedding.f	HomologicalComplex.HasHomology HomologicalComplex.extend	—	CategoryTheory.ShortComplex.HasHomology.mk'
homologyData'_iso 📖	mathematical	ComplexShape.Embedding.f ComplexShape.prev ComplexShape.next	CategoryTheory.ShortComplex.HomologyData.iso HomologicalComplex.sc HomologicalComplex.extend homologyData' HomologicalComplex.sc'	—	—
homologyData'_left_H 📖	mathematical	ComplexShape.Embedding.f ComplexShape.prev ComplexShape.next	CategoryTheory.ShortComplex.LeftHomologyData.H HomologicalComplex.sc' HomologicalComplex.extend CategoryTheory.ShortComplex.HomologyData.left HomologicalComplex.sc homologyData'	—	—
homologyData'_left_K 📖	mathematical	ComplexShape.Embedding.f ComplexShape.prev ComplexShape.next	CategoryTheory.ShortComplex.LeftHomologyData.K HomologicalComplex.sc' HomologicalComplex.extend CategoryTheory.ShortComplex.HomologyData.left HomologicalComplex.sc homologyData'	—	—
homologyData'_left_i 📖	mathematical	ComplexShape.Embedding.f ComplexShape.prev ComplexShape.next	CategoryTheory.ShortComplex.LeftHomologyData.i HomologicalComplex.sc' HomologicalComplex.extend CategoryTheory.ShortComplex.HomologyData.left HomologicalComplex.sc homologyData' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.LeftHomologyData.K HomologicalComplex.X CategoryTheory.Iso.inv HomologicalComplex.extendXIso	—	—
homologyData'_left_π 📖	mathematical	ComplexShape.Embedding.f ComplexShape.prev ComplexShape.next	CategoryTheory.ShortComplex.LeftHomologyData.π HomologicalComplex.sc' HomologicalComplex.extend CategoryTheory.ShortComplex.HomologyData.left HomologicalComplex.sc homologyData'	—	—
homologyData'_right_H 📖	mathematical	ComplexShape.Embedding.f ComplexShape.prev ComplexShape.next	CategoryTheory.ShortComplex.RightHomologyData.H HomologicalComplex.sc' HomologicalComplex.extend CategoryTheory.ShortComplex.HomologyData.right HomologicalComplex.sc homologyData'	—	—
homologyData'_right_Q 📖	mathematical	ComplexShape.Embedding.f ComplexShape.prev ComplexShape.next	CategoryTheory.ShortComplex.RightHomologyData.Q HomologicalComplex.sc' HomologicalComplex.extend CategoryTheory.ShortComplex.HomologyData.right HomologicalComplex.sc homologyData'	—	—
homologyData'_right_p 📖	mathematical	ComplexShape.Embedding.f ComplexShape.prev ComplexShape.next	CategoryTheory.ShortComplex.RightHomologyData.p HomologicalComplex.sc' HomologicalComplex.extend CategoryTheory.ShortComplex.HomologyData.right HomologicalComplex.sc homologyData' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.ShortComplex.RightHomologyData.Q CategoryTheory.Iso.hom HomologicalComplex.extendXIso	—	—
homologyData'_right_ι 📖	mathematical	ComplexShape.Embedding.f ComplexShape.prev ComplexShape.next	CategoryTheory.ShortComplex.RightHomologyData.ι HomologicalComplex.sc' HomologicalComplex.extend CategoryTheory.ShortComplex.HomologyData.right HomologicalComplex.sc homologyData'	—	—
homologyData_iso 📖	mathematical	ComplexShape.Embedding.f ComplexShape.prev ComplexShape.next	CategoryTheory.ShortComplex.HomologyData.iso HomologicalComplex.sc' HomologicalComplex.extend homologyData	—	—
homologyData_left 📖	mathematical	ComplexShape.Embedding.f ComplexShape.prev ComplexShape.next	CategoryTheory.ShortComplex.HomologyData.left HomologicalComplex.sc' HomologicalComplex.extend homologyData leftHomologyData	—	—
homologyData_right 📖	mathematical	ComplexShape.Embedding.f ComplexShape.prev ComplexShape.next	CategoryTheory.ShortComplex.HomologyData.right HomologicalComplex.sc' HomologicalComplex.extend homologyData rightHomologyData	—	—
instHasHomology 📖	mathematical	HomologicalComplex.HasHomology	HomologicalComplex.extend	—	instHasHomologyF HomologicalComplex.isZero_extend_X CategoryTheory.ShortComplex.HasHomology.mk' CategoryTheory.Limits.IsZero.eq_of_tgt CategoryTheory.Limits.IsZero.eq_of_src
instHasHomologyF 📖	mathematical	—	HomologicalComplex.HasHomology HomologicalComplex.extend ComplexShape.Embedding.f	—	hasHomology
leftHomologyData_H 📖	mathematical	ComplexShape.Embedding.f ComplexShape.prev ComplexShape.next	CategoryTheory.ShortComplex.LeftHomologyData.H HomologicalComplex.sc' HomologicalComplex.extend leftHomologyData	—	—
leftHomologyData_K 📖	mathematical	ComplexShape.Embedding.f ComplexShape.prev ComplexShape.next	CategoryTheory.ShortComplex.LeftHomologyData.K HomologicalComplex.sc' HomologicalComplex.extend leftHomologyData	—	—
leftHomologyData_i 📖	mathematical	ComplexShape.Embedding.f ComplexShape.prev ComplexShape.next	CategoryTheory.ShortComplex.LeftHomologyData.i HomologicalComplex.sc' HomologicalComplex.extend leftHomologyData CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.LeftHomologyData.K CategoryTheory.ShortComplex.X₂ CategoryTheory.Iso.inv HomologicalComplex.X HomologicalComplex.extendXIso	—	—
leftHomologyData_π 📖	mathematical	ComplexShape.Embedding.f ComplexShape.prev ComplexShape.next	CategoryTheory.ShortComplex.LeftHomologyData.π HomologicalComplex.sc' HomologicalComplex.extend leftHomologyData	—	—
rightHomologyData_H 📖	mathematical	ComplexShape.Embedding.f ComplexShape.prev ComplexShape.next	CategoryTheory.ShortComplex.RightHomologyData.H HomologicalComplex.sc' HomologicalComplex.extend rightHomologyData	—	—
rightHomologyData_Q 📖	mathematical	ComplexShape.Embedding.f ComplexShape.prev ComplexShape.next	CategoryTheory.ShortComplex.RightHomologyData.Q HomologicalComplex.sc' HomologicalComplex.extend rightHomologyData	—	—
rightHomologyData_g' 📖	mathematical	ComplexShape.Embedding.f ComplexShape.prev ComplexShape.next	CategoryTheory.ShortComplex.RightHomologyData.g' HomologicalComplex.sc' HomologicalComplex.extend rightHomologyData CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.RightHomologyData.Q CategoryTheory.ShortComplex.X₃ HomologicalComplex.X CategoryTheory.Iso.inv HomologicalComplex.extendXIso	—	CategoryTheory.cancel_epi CategoryTheory.ShortComplex.RightHomologyData.instEpiP CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom CategoryTheory.ShortComplex.RightHomologyData.p_g' CategoryTheory.Category.assoc HomologicalComplex.extend_d_eq CategoryTheory.ShortComplex.RightHomologyData.p_g'_assoc HomologicalComplex.shortComplexFunctor'_obj_g
rightHomologyData_p 📖	mathematical	ComplexShape.Embedding.f ComplexShape.prev ComplexShape.next	CategoryTheory.ShortComplex.RightHomologyData.p HomologicalComplex.sc' HomologicalComplex.extend rightHomologyData CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ HomologicalComplex.X CategoryTheory.ShortComplex.RightHomologyData.Q CategoryTheory.Iso.hom HomologicalComplex.extendXIso	—	—
rightHomologyData_ι 📖	mathematical	ComplexShape.Embedding.f ComplexShape.prev ComplexShape.next	CategoryTheory.ShortComplex.RightHomologyData.ι HomologicalComplex.sc' HomologicalComplex.extend rightHomologyData	—	—

HomologicalComplex.extend.leftHomologyData

Definitions

Name	Category	Theorems
cokernelCofork 📖	CompOp	—
isColimitCokernelCofork 📖	CompOp	—
isLimitKernelFork 📖	CompOp	1 math math: lift_d_comp_eq_zero_iff
kernelFork 📖	CompOp	1 math math: lift_d_comp_eq_zero_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift_d_comp_eq_zero_iff 📖	mathematical	ComplexShape.Embedding.f ComplexShape.prev ComplexShape.next	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair HomologicalComplex.X HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.KernelFork.ofι HomologicalComplex.d_comp_d CategoryTheory.Limits.IsLimit.lift HomologicalComplex.extend kernelFork isLimitKernelFork	—	lift_d_comp_eq_zero_iff' HomologicalComplex.d_comp_d CategoryTheory.Limits.IsLimit.fac
lift_d_comp_eq_zero_iff' 📖	—	ComplexShape.Embedding.f ComplexShape.prev CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Fork.ι HomologicalComplex.extend CategoryTheory.Iso.inv HomologicalComplex.extendXIso	—	—	ComplexShape.prev_eq' ComplexShape.Embedding.rel CategoryTheory.Limits.Fork.IsLimit.hom_ext CategoryTheory.Category.assoc CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_inv HomologicalComplex.extend_d_eq CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom CategoryTheory.Limits.comp_zero HomologicalComplex.shape CategoryTheory.Limits.zero_comp HomologicalComplex.extend_d_to_eq_zero

HomologicalComplex.extend.rightHomologyData

Definitions

Name	Category	Theorems
cokernelCofork 📖	CompOp	1 math math: d_comp_desc_eq_zero_iff
isColimitCokernelCofork 📖	CompOp	1 math math: d_comp_desc_eq_zero_iff
isLimitKernelFork 📖	CompOp	—
kernelFork 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
d_comp_desc_eq_zero_iff 📖	mathematical	ComplexShape.Embedding.f ComplexShape.prev ComplexShape.next	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair HomologicalComplex.X HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.CokernelCofork.ofπ HomologicalComplex.d_comp_d CategoryTheory.Limits.IsColimit.desc HomologicalComplex.extend cokernelCofork isColimitCokernelCofork	—	d_comp_desc_eq_zero_iff' HomologicalComplex.d_comp_d CategoryTheory.Limits.IsColimit.fac CategoryTheory.Category.assoc
d_comp_desc_eq_zero_iff' 📖	—	ComplexShape.Embedding.f ComplexShape.next CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair HomologicalComplex.X HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cofork.π HomologicalComplex.extend CategoryTheory.Iso.hom HomologicalComplex.extendXIso	—	—	ComplexShape.next_eq' ComplexShape.Embedding.rel CategoryTheory.Limits.Cofork.IsColimit.hom_ext CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom HomologicalComplex.extend_d_eq CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_inv CategoryTheory.Limits.zero_comp HomologicalComplex.shape CategoryTheory.Limits.comp_zero HomologicalComplex.extend_d_from_eq_zero

---

← Back to Index