SingleHomology

📁 Source: Mathlib/Algebra/Homology/SingleHomology.lean

Statistics

Metric	Count
Definitions homologyFunctorSingleIso, singleObjCyclesSelfIso, singleObjHomologySelfIso, singleObjOpcyclesSelfIso	4
Theorems exactAt_succ_single_obj, exactAt_succ_single_obj, exactAt_single_obj, homologyFunctorSingleIso_hom_app, homologyFunctorSingleIso_inv_app, homologyι_singleObjOpcyclesSelfIso_inv, homologyι_singleObjOpcyclesSelfIso_inv_assoc, homologyπ_singleObjHomologySelfIso_hom, homologyπ_singleObjHomologySelfIso_hom_assoc, instHasHomologyObjSingle, isZero_single_obj_homology, pOpcycles_singleObjOpcyclesSelfIso_inv, pOpcycles_singleObjOpcyclesSelfIso_inv_assoc, singleObjCyclesSelfIso_hom, singleObjCyclesSelfIso_hom_assoc, singleObjCyclesSelfIso_hom_naturality, singleObjCyclesSelfIso_hom_naturality_assoc, singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom, singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc, singleObjCyclesSelfIso_inv_homologyπ, singleObjCyclesSelfIso_inv_homologyπ_assoc, singleObjCyclesSelfIso_inv_iCycles, singleObjCyclesSelfIso_inv_iCycles_assoc, singleObjCyclesSelfIso_inv_naturality, singleObjCyclesSelfIso_inv_naturality_assoc, singleObjHomologySelfIso_hom_naturality, singleObjHomologySelfIso_hom_naturality_assoc, singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv, singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv_assoc, singleObjHomologySelfIso_hom_singleObjOpcyclesSelfIso_hom, singleObjHomologySelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc, singleObjHomologySelfIso_inv_homologyι, singleObjHomologySelfIso_inv_homologyι_assoc, singleObjHomologySelfIso_inv_naturality, singleObjHomologySelfIso_inv_naturality_assoc, singleObjOpcyclesSelfIso_hom, singleObjOpcyclesSelfIso_hom_assoc, singleObjOpcyclesSelfIso_hom_naturality, singleObjOpcyclesSelfIso_hom_naturality_assoc, singleObjOpcyclesSelfIso_inv_naturality, singleObjOpcyclesSelfIso_inv_naturality_assoc	41
Total	45

ChainComplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exactAt_succ_single_obj 📖	mathematical	—	HomologicalComplex.ExactAt ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj ChainComplex HomologicalComplex.instCategory single₀	—	HomologicalComplex.exactAt_single_obj AddRightCancelSemigroup.toIsRightCancelAdd

CochainComplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exactAt_succ_single_obj 📖	mathematical	—	HomologicalComplex.ExactAt ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory single₀	—	HomologicalComplex.exactAt_single_obj AddRightCancelSemigroup.toIsRightCancelAdd

HomologicalComplex

Definitions

Name	Category	Theorems
homologyFunctorSingleIso 📖	CompOp	2 math math: homologyFunctorSingleIso_inv_app, homologyFunctorSingleIso_hom_app
singleObjCyclesSelfIso 📖	CompOp	16 math math: singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc, singleObjCyclesSelfIso_inv_iCycles, singleObjCyclesSelfIso_inv_homologyπ, singleObjCyclesSelfIso_hom_naturality, singleObjCyclesSelfIso_inv_naturality_assoc, singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv_assoc, homologyπ_singleObjHomologySelfIso_hom_assoc, singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom, singleObjCyclesSelfIso_inv_homologyπ_assoc, homologyπ_singleObjHomologySelfIso_hom, singleObjCyclesSelfIso_inv_iCycles_assoc, singleObjCyclesSelfIso_hom_assoc, singleObjCyclesSelfIso_inv_naturality, singleObjCyclesSelfIso_hom_naturality_assoc, singleObjCyclesSelfIso_hom, singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv
singleObjHomologySelfIso 📖	CompOp	18 math math: singleObjHomologySelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc, homologyι_singleObjOpcyclesSelfIso_inv_assoc, singleObjCyclesSelfIso_inv_homologyπ, homologyι_singleObjOpcyclesSelfIso_inv, singleObjHomologySelfIso_hom_singleObjOpcyclesSelfIso_hom, singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv_assoc, homologyπ_singleObjHomologySelfIso_hom_assoc, singleObjHomologySelfIso_inv_homologyι_assoc, singleObjCyclesSelfIso_inv_homologyπ_assoc, homologyπ_singleObjHomologySelfIso_hom, homologyFunctorSingleIso_inv_app, singleObjHomologySelfIso_hom_naturality, singleObjHomologySelfIso_hom_naturality_assoc, singleObjHomologySelfIso_inv_naturality_assoc, singleObjHomologySelfIso_inv_naturality, singleObjHomologySelfIso_inv_homologyι, homologyFunctorSingleIso_hom_app, singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv
singleObjOpcyclesSelfIso 📖	CompOp	16 math math: singleObjHomologySelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc, singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc, pOpcycles_singleObjOpcyclesSelfIso_inv, singleObjOpcyclesSelfIso_hom, homologyι_singleObjOpcyclesSelfIso_inv_assoc, homologyι_singleObjOpcyclesSelfIso_inv, singleObjHomologySelfIso_hom_singleObjOpcyclesSelfIso_hom, singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom, singleObjHomologySelfIso_inv_homologyι_assoc, singleObjOpcyclesSelfIso_inv_naturality, singleObjOpcyclesSelfIso_hom_naturality_assoc, pOpcycles_singleObjOpcyclesSelfIso_inv_assoc, singleObjOpcyclesSelfIso_inv_naturality_assoc, singleObjHomologySelfIso_inv_homologyι, singleObjOpcyclesSelfIso_hom_assoc, singleObjOpcyclesSelfIso_hom_naturality

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exactAt_single_obj 📖	mathematical	—	ExactAt CategoryTheory.Functor.obj HomologicalComplex instCategory single	—	CategoryTheory.ShortComplex.exact_of_isZero_X₂ isZero_single_obj_X
homologyFunctorSingleIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp HomologicalComplex instCategory single homologyFunctor CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category homologyFunctorSingleIso homology CategoryTheory.Functor.obj singleObjHomologySelfIso	—	—
homologyFunctorSingleIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp HomologicalComplex instCategory single homologyFunctor CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category homologyFunctorSingleIso homology CategoryTheory.Functor.obj singleObjHomologySelfIso	—	—
homologyι_singleObjOpcyclesSelfIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle opcycles homologyι CategoryTheory.Iso.inv singleObjOpcyclesSelfIso CategoryTheory.Iso.hom singleObjHomologySelfIso	—	instHasHomologyObjSingle CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_inv singleObjHomologySelfIso_inv_homologyι_assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Iso.inv_hom_id
homologyι_singleObjOpcyclesSelfIso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle opcycles homologyι CategoryTheory.Iso.inv singleObjOpcyclesSelfIso CategoryTheory.Iso.hom singleObjHomologySelfIso	—	instHasHomologyObjSingle CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homologyι_singleObjOpcyclesSelfIso_inv
homologyπ_singleObjHomologySelfIso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle homology homologyπ CategoryTheory.Iso.hom singleObjHomologySelfIso singleObjCyclesSelfIso	—	instHasHomologyObjSingle isoHomologyπ_hom_inv_id_assoc
homologyπ_singleObjHomologySelfIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle homology homologyπ CategoryTheory.Iso.hom singleObjHomologySelfIso singleObjCyclesSelfIso	—	instHasHomologyObjSingle CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homologyπ_singleObjHomologySelfIso_hom
instHasHomologyObjSingle 📖	mathematical	—	HasHomology CategoryTheory.Functor.obj HomologicalComplex instCategory single	—	CategoryTheory.ShortComplex.hasHomology_of_zeros
isZero_single_obj_homology 📖	mathematical	—	CategoryTheory.Limits.IsZero homology CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle	—	instHasHomologyObjSingle exactAt_single_obj
pOpcycles_singleObjOpcyclesSelfIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Functor.obj HomologicalComplex instCategory single opcycles instHasHomologyObjSingle pOpcycles CategoryTheory.Iso.inv singleObjOpcyclesSelfIso CategoryTheory.Iso.hom singleObjXSelf	—	instHasHomologyObjSingle isIso_iCycles CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso homology_π_ι_assoc homologyι_singleObjOpcyclesSelfIso_inv homologyπ_singleObjHomologySelfIso_hom singleObjCyclesSelfIso_hom
pOpcycles_singleObjOpcyclesSelfIso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Functor.obj HomologicalComplex instCategory single opcycles instHasHomologyObjSingle pOpcycles CategoryTheory.Iso.inv singleObjOpcyclesSelfIso CategoryTheory.Iso.hom singleObjXSelf	—	instHasHomologyObjSingle CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pOpcycles_singleObjOpcyclesSelfIso_inv
singleObjCyclesSelfIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom cycles CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle singleObjCyclesSelfIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X iCycles singleObjXSelf	—	instHasHomologyObjSingle
singleObjCyclesSelfIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle CategoryTheory.Iso.hom singleObjCyclesSelfIso X iCycles singleObjXSelf	—	instHasHomologyObjSingle CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' singleObjCyclesSelfIso_hom
singleObjCyclesSelfIso_hom_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle cyclesMap CategoryTheory.Functor.map CategoryTheory.Iso.hom singleObjCyclesSelfIso	—	instHasHomologyObjSingle 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 instMonoICycles cyclesMap_i single_map_f_self iCyclesIso_inv_hom_id
singleObjCyclesSelfIso_hom_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle cyclesMap CategoryTheory.Functor.map CategoryTheory.Iso.hom singleObjCyclesSelfIso	—	instHasHomologyObjSingle CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' singleObjCyclesSelfIso_hom_naturality
singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle opcycles CategoryTheory.Iso.hom singleObjCyclesSelfIso singleObjOpcyclesSelfIso X iCycles pOpcycles	—	instHasHomologyObjSingle CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id_assoc
singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle CategoryTheory.Iso.hom singleObjCyclesSelfIso opcycles singleObjOpcyclesSelfIso X iCycles pOpcycles	—	instHasHomologyObjSingle CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom
singleObjCyclesSelfIso_inv_homologyπ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle homology CategoryTheory.Iso.inv singleObjCyclesSelfIso homologyπ singleObjHomologySelfIso	—	instHasHomologyObjSingle CategoryTheory.Category.assoc
singleObjCyclesSelfIso_inv_homologyπ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle CategoryTheory.Iso.inv singleObjCyclesSelfIso homology homologyπ singleObjHomologySelfIso	—	instHasHomologyObjSingle CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' singleObjCyclesSelfIso_inv_homologyπ
singleObjCyclesSelfIso_inv_iCycles 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle X CategoryTheory.Iso.inv singleObjCyclesSelfIso iCycles singleObjXSelf	—	instHasHomologyObjSingle CategoryTheory.Category.assoc iCyclesIso_inv_hom_id CategoryTheory.Category.comp_id
singleObjCyclesSelfIso_inv_iCycles_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle CategoryTheory.Iso.inv singleObjCyclesSelfIso X iCycles singleObjXSelf	—	instHasHomologyObjSingle CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' singleObjCyclesSelfIso_inv_iCycles
singleObjCyclesSelfIso_inv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle CategoryTheory.Iso.inv singleObjCyclesSelfIso cyclesMap CategoryTheory.Functor.map	—	instHasHomologyObjSingle CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom CategoryTheory.Iso.hom_inv_id_assoc singleObjCyclesSelfIso_hom_naturality_assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
singleObjCyclesSelfIso_inv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle CategoryTheory.Iso.inv singleObjCyclesSelfIso cyclesMap CategoryTheory.Functor.map	—	instHasHomologyObjSingle CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' singleObjCyclesSelfIso_inv_naturality
singleObjHomologySelfIso_hom_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle homologyMap CategoryTheory.Functor.map CategoryTheory.Iso.hom singleObjHomologySelfIso	—	instHasHomologyObjSingle CategoryTheory.cancel_epi instEpiHomologyπ homologyπ_naturality_assoc homologyπ_singleObjHomologySelfIso_hom singleObjCyclesSelfIso_hom_naturality homologyπ_singleObjHomologySelfIso_hom_assoc
singleObjHomologySelfIso_hom_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle homologyMap CategoryTheory.Functor.map CategoryTheory.Iso.hom singleObjHomologySelfIso	—	instHasHomologyObjSingle CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' singleObjHomologySelfIso_hom_naturality
singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle homology CategoryTheory.Iso.hom singleObjCyclesSelfIso CategoryTheory.Iso.inv singleObjHomologySelfIso homologyπ	—	instHasHomologyObjSingle 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π_singleObjHomologySelfIso_hom
singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle CategoryTheory.Iso.hom singleObjCyclesSelfIso homology CategoryTheory.Iso.inv singleObjHomologySelfIso homologyπ	—	instHasHomologyObjSingle CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv
singleObjHomologySelfIso_hom_singleObjOpcyclesSelfIso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle opcycles CategoryTheory.Iso.hom singleObjHomologySelfIso singleObjOpcyclesSelfIso homologyι	—	instHasHomologyObjSingle CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_inv CategoryTheory.Iso.inv_hom_id_assoc singleObjHomologySelfIso_inv_homologyι
singleObjHomologySelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle CategoryTheory.Iso.hom singleObjHomologySelfIso opcycles singleObjOpcyclesSelfIso homologyι	—	instHasHomologyObjSingle CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' singleObjHomologySelfIso_hom_singleObjOpcyclesSelfIso_hom
singleObjHomologySelfIso_inv_homologyι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle opcycles CategoryTheory.Iso.inv singleObjHomologySelfIso homologyι CategoryTheory.Iso.hom singleObjOpcyclesSelfIso	—	instHasHomologyObjSingle CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv_assoc homology_π_ι singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom
singleObjHomologySelfIso_inv_homologyι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle CategoryTheory.Iso.inv singleObjHomologySelfIso opcycles homologyι CategoryTheory.Iso.hom singleObjOpcyclesSelfIso	—	instHasHomologyObjSingle CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' singleObjHomologySelfIso_inv_homologyι
singleObjHomologySelfIso_inv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle CategoryTheory.Iso.inv singleObjHomologySelfIso homologyMap CategoryTheory.Functor.map	—	instHasHomologyObjSingle CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Category.assoc singleObjHomologySelfIso_hom_naturality CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
singleObjHomologySelfIso_inv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle CategoryTheory.Iso.inv singleObjHomologySelfIso homologyMap CategoryTheory.Functor.map	—	instHasHomologyObjSingle CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' singleObjHomologySelfIso_inv_naturality
singleObjOpcyclesSelfIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom opcycles CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle singleObjOpcyclesSelfIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.inv singleObjXSelf pOpcycles	—	instHasHomologyObjSingle
singleObjOpcyclesSelfIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle CategoryTheory.Iso.hom singleObjOpcyclesSelfIso X CategoryTheory.Iso.inv singleObjXSelf pOpcycles	—	instHasHomologyObjSingle CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' singleObjOpcyclesSelfIso_hom
singleObjOpcyclesSelfIso_hom_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle CategoryTheory.Iso.hom singleObjOpcyclesSelfIso opcyclesMap CategoryTheory.Functor.map	—	instHasHomologyObjSingle CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc p_opcyclesMap single_map_f_self CategoryTheory.Category.assoc singleObjCyclesSelfIso_hom singleObjOpcyclesSelfIso_hom
singleObjOpcyclesSelfIso_hom_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle CategoryTheory.Iso.hom singleObjOpcyclesSelfIso opcyclesMap CategoryTheory.Functor.map	—	instHasHomologyObjSingle CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' singleObjOpcyclesSelfIso_hom_naturality
singleObjOpcyclesSelfIso_inv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle opcyclesMap CategoryTheory.Functor.map CategoryTheory.Iso.inv singleObjOpcyclesSelfIso	—	instHasHomologyObjSingle 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 singleObjOpcyclesSelfIso_hom_naturality CategoryTheory.Iso.inv_hom_id_assoc
singleObjOpcyclesSelfIso_inv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles CategoryTheory.Functor.obj HomologicalComplex instCategory single instHasHomologyObjSingle opcyclesMap CategoryTheory.Functor.map CategoryTheory.Iso.inv singleObjOpcyclesSelfIso	—	instHasHomologyObjSingle CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' singleObjOpcyclesSelfIso_inv_naturality

---

← Back to Index