PreservesHomology

📁 Source: Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean

Statistics

Metric	Count
Definitions PreservesHomology, PreservesLeftHomologyOf, PreservesRightHomologyOf, map, map, natTransApp, IsPreservedBy, map, map, natTransApp, IsPreservedBy, map, map, natTransApp, cyclesFunctorIso, homologyFunctorIso, leftHomologyFunctorIso, mapCyclesIso, mapHomologyIso, mapHomologyIso', mapLeftHomologyIso, mapOpcyclesIso, mapRightHomologyIso, opcyclesFunctorIso, rightHomologyFunctorIso	25
Theorems preservesCokernel, preservesCokernels, preservesKernel, preservesKernels, preservesLeftHomologyOf, preservesRightHomologyOf, isPreservedBy, mk', isPreservedBy, mk', preservesHomologyOfExact, preservesLeftHomology_of_zero_f, preservesLeftHomology_of_zero_g, preservesRightHomology_of_zero_f, preservesRightHomology_of_zero_g, app_homology, map_homologyMap', map_iso, map_left, map_right, map_left, map_right, natTransApp_left, natTransApp_right, f', g, hf', hg, isPreservedBy_of_preserves, isPreservedBy_of_preservesHomology, mapCyclesIso_eq, mapHomologyIso_eq, mapLeftHomologyIso_eq, map_H, map_K, map_cyclesMap', map_f', map_i, map_leftHomologyMap', map_π, map_φH, map_φK, natTransApp_φH, natTransApp_φK, quasiIso_map_iff, f, g', hf, hg', isPreservedBy_of_preserves, isPreservedBy_of_preservesHomology, mapHomologyIso'_eq, mapOpcyclesIso_eq, mapRightHomologyIso_eq, map_H, map_Q, map_g', map_opcyclesMap', map_p, map_rightHomologyMap', map_ι, map_φH, map_φQ, natTransApp_φH, natTransApp_φQ, quasiIso_map_iff, hasHomology_of_preserves, hasHomology_of_preserves', hasLeftHomology_of_preserves, hasLeftHomology_of_preserves', hasRightHomology_of_preserves, hasRightHomology_of_preserves', homologyMap_mapNatTrans, mapCyclesIso_hom_iCycles, mapCyclesIso_hom_iCycles_assoc, mapCyclesIso_hom_naturality, mapCyclesIso_hom_naturality_assoc, mapCyclesIso_inv_naturality, mapCyclesIso_inv_naturality_assoc, mapHomologyIso'_eq_mapHomologyIso, mapHomologyIso'_hom_naturality, mapHomologyIso'_hom_naturality_assoc, mapHomologyIso'_inv_naturality, mapHomologyIso'_inv_naturality_assoc, mapHomologyIso_hom_naturality, mapHomologyIso_hom_naturality_assoc, mapHomologyIso_inv_naturality, mapHomologyIso_inv_naturality_assoc, mapLeftHomologyIso_hom_naturality, mapLeftHomologyIso_hom_naturality_assoc, mapLeftHomologyIso_inv_naturality, mapLeftHomologyIso_inv_naturality_assoc, mapOpcyclesIso_hom_naturality, mapOpcyclesIso_hom_naturality_assoc, mapOpcyclesIso_inv_naturality, mapOpcyclesIso_inv_naturality_assoc, mapRightHomologyIso_hom_naturality, mapRightHomologyIso_hom_naturality_assoc, mapRightHomologyIso_inv_naturality, mapRightHomologyIso_inv_naturality_assoc, map_leftRightHomologyComparison', quasiIso_map_iff_of_preservesLeftHomology, quasiIso_map_iff_of_preservesRightHomology, quasiIso_map_of_preservesLeftHomology, quasiIso_map_of_preservesRightHomology	105
Total	130

CategoryTheory.Functor

Definitions

Name	Category	Theorems
PreservesHomology 📖	CompData	9 math math: preservesHomology_of_map_exact, preservesHomology_of_preservesMonos_and_cokernels, preservesHomology_of_preservesEpis_and_kernels, CategoryTheory.preservesHomology_preadditiveCoyonedaObj_of_projective, CategoryTheory.preservesHomology_preadditiveYonedaObj_of_injective, preservesHomologyOfExact, instPreservesHomologyFunctorAddCommGrpCatColim, exact_tfae, CategoryTheory.ShortComplex.instPreservesHomologyModuleCatAbForget₂LinearMapIdCarrierAddMonoidHomCarrier
PreservesLeftHomologyOf 📖	CompData	4 math math: preservesLeftHomology_of_zero_g, preservesLeftHomology_of_zero_f, PreservesHomology.preservesLeftHomologyOf, PreservesLeftHomologyOf.mk'
PreservesRightHomologyOf 📖	CompData	4 math math: PreservesHomology.preservesRightHomologyOf, preservesRightHomology_of_zero_f, PreservesRightHomologyOf.mk', preservesRightHomology_of_zero_g

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservesHomologyOfExact 📖	mathematical	—	PreservesHomology	—	CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits
preservesLeftHomology_of_zero_f 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	PreservesLeftHomologyOf	—	CategoryTheory.Limits.preservesCokernel_zero' CategoryTheory.cancel_mono CategoryTheory.ShortComplex.LeftHomologyData.instMonoI CategoryTheory.ShortComplex.LeftHomologyData.f'_i CategoryTheory.Limits.zero_comp
preservesLeftHomology_of_zero_g 📖	mathematical	CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	PreservesLeftHomologyOf	—	CategoryTheory.Limits.preservesKernel_zero CategoryTheory.ShortComplex.LeftHomologyData.isIso_i CategoryTheory.ShortComplex.LeftHomologyData.f'_i CategoryTheory.Category.id_comp CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero CategoryTheory.Limits.preservesColimit_of_iso_diagram
preservesRightHomology_of_zero_f 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	PreservesRightHomologyOf	—	CategoryTheory.Limits.preservesCokernel_zero CategoryTheory.ShortComplex.RightHomologyData.isIso_p CategoryTheory.Category.comp_id CategoryTheory.ShortComplex.RightHomologyData.p_g' CategoryTheory.Limits.comp_zero CategoryTheory.Limits.preservesLimit_of_iso_diagram
preservesRightHomology_of_zero_g 📖	mathematical	CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	PreservesRightHomologyOf	—	CategoryTheory.Limits.preservesKernel_zero' CategoryTheory.cancel_epi CategoryTheory.ShortComplex.RightHomologyData.instEpiP CategoryTheory.ShortComplex.RightHomologyData.p_g' CategoryTheory.Limits.comp_zero

CategoryTheory.Functor.PreservesHomology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservesCokernel 📖	mathematical	—	CategoryTheory.Limits.PreservesColimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero	—	preservesCokernels
preservesCokernels 📖	mathematical	—	CategoryTheory.Limits.PreservesColimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
preservesKernel 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero	—	preservesKernels
preservesKernels 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
preservesLeftHomologyOf 📖	mathematical	—	CategoryTheory.Functor.PreservesLeftHomologyOf	—	CategoryTheory.ShortComplex.LeftHomologyData.isPreservedBy_of_preservesHomology
preservesRightHomologyOf 📖	mathematical	—	CategoryTheory.Functor.PreservesRightHomologyOf	—	CategoryTheory.ShortComplex.RightHomologyData.isPreservedBy_of_preservesHomology

CategoryTheory.Functor.PreservesLeftHomologyOf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPreservedBy 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy	—	—
mk' 📖	mathematical	—	CategoryTheory.Functor.PreservesLeftHomologyOf	—	CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.hg CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.hf' CategoryTheory.ShortComplex.f'_cyclesMap' CategoryTheory.Category.id_comp CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero CategoryTheory.Limits.preservesColimit_of_iso_diagram

CategoryTheory.Functor.PreservesRightHomologyOf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPreservedBy 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy	—	—
mk' 📖	mathematical	—	CategoryTheory.Functor.PreservesRightHomologyOf	—	CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.hf CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.hg' CategoryTheory.Category.comp_id CategoryTheory.ShortComplex.opcyclesMap'_g' CategoryTheory.Limits.comp_zero CategoryTheory.Limits.preservesLimit_of_iso_diagram

CategoryTheory.NatTrans

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
app_homology 📖	mathematical	—	app CategoryTheory.ShortComplex.homology CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ShortComplex.map CategoryTheory.ShortComplex.hasHomology_of_preserves CategoryTheory.Iso.inv CategoryTheory.ShortComplex.mapHomologyIso CategoryTheory.ShortComplex.homologyMap CategoryTheory.ShortComplex.mapNatTrans CategoryTheory.Iso.hom	—	CategoryTheory.ShortComplex.hasHomology_of_preserves CategoryTheory.ShortComplex.homologyMap_mapNatTrans CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id CategoryTheory.Iso.inv_hom_id_assoc

CategoryTheory.ShortComplex

Definitions

Name	Category	Theorems
cyclesFunctorIso 📖	CompOp	—
homologyFunctorIso 📖	CompOp	—
leftHomologyFunctorIso 📖	CompOp	—
mapCyclesIso 📖	CompOp	7 math math: mapCyclesIso_hom_iCycles_assoc, mapCyclesIso_hom_naturality_assoc, mapCyclesIso_inv_naturality_assoc, LeftHomologyData.mapCyclesIso_eq, mapCyclesIso_hom_iCycles, mapCyclesIso_inv_naturality, mapCyclesIso_hom_naturality
mapHomologyIso 📖	CompOp	8 math math: mapHomologyIso_hom_naturality, mapHomologyIso_hom_naturality_assoc, CategoryTheory.NatTrans.app_homology, homologyMap_mapNatTrans, mapHomologyIso'_eq_mapHomologyIso, LeftHomologyData.mapHomologyIso_eq, mapHomologyIso_inv_naturality, mapHomologyIso_inv_naturality_assoc
mapHomologyIso' 📖	CompOp	6 math math: mapHomologyIso'_hom_naturality, mapHomologyIso'_eq_mapHomologyIso, mapHomologyIso'_hom_naturality_assoc, RightHomologyData.mapHomologyIso'_eq, mapHomologyIso'_inv_naturality_assoc, mapHomologyIso'_inv_naturality
mapLeftHomologyIso 📖	CompOp	5 math math: mapLeftHomologyIso_hom_naturality, LeftHomologyData.mapLeftHomologyIso_eq, mapLeftHomologyIso_hom_naturality_assoc, mapLeftHomologyIso_inv_naturality, mapLeftHomologyIso_inv_naturality_assoc
mapOpcyclesIso 📖	CompOp	5 math math: mapOpcyclesIso_hom_naturality_assoc, mapOpcyclesIso_inv_naturality, RightHomologyData.mapOpcyclesIso_eq, mapOpcyclesIso_inv_naturality_assoc, mapOpcyclesIso_hom_naturality
mapRightHomologyIso 📖	CompOp	5 math math: mapRightHomologyIso_inv_naturality, mapRightHomologyIso_hom_naturality, mapRightHomologyIso_inv_naturality_assoc, RightHomologyData.mapRightHomologyIso_eq, mapRightHomologyIso_hom_naturality_assoc
opcyclesFunctorIso 📖	CompOp	—
rightHomologyFunctorIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasHomology_of_preserves 📖	mathematical	—	HasHomology map	—	HasHomology.mk' LeftHomologyData.isPreservedBy_of_preserves RightHomologyData.isPreservedBy_of_preserves
hasHomology_of_preserves' 📖	mathematical	—	HasHomology CategoryTheory.Functor.obj CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex	—	hasHomology_of_preserves
hasLeftHomology_of_preserves 📖	mathematical	—	HasLeftHomology map	—	HasLeftHomology.mk' LeftHomologyData.isPreservedBy_of_preserves
hasLeftHomology_of_preserves' 📖	mathematical	—	HasLeftHomology CategoryTheory.Functor.obj CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex	—	hasLeftHomology_of_preserves
hasRightHomology_of_preserves 📖	mathematical	—	HasRightHomology map	—	HasRightHomology.mk' RightHomologyData.isPreservedBy_of_preserves
hasRightHomology_of_preserves' 📖	mathematical	—	HasRightHomology CategoryTheory.Functor.obj CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex	—	hasRightHomology_of_preserves
homologyMap_mapNatTrans 📖	mathematical	—	homologyMap map mapNatTrans hasHomology_of_preserves CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology CategoryTheory.Functor.obj CategoryTheory.Iso.hom mapHomologyIso CategoryTheory.NatTrans.app CategoryTheory.Iso.inv	—	LeftHomologyMapData.homologyMap_eq LeftHomologyData.isPreservedBy_of_preserves hasHomology_of_preserves
mapCyclesIso_hom_iCycles 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles map hasLeftHomology_of_preserves CategoryTheory.Functor.obj X₂ CategoryTheory.Iso.hom mapCyclesIso CategoryTheory.Functor.map iCycles	—	LeftHomologyData.cyclesIso_hom_comp_i hasLeftHomology_of_preserves
mapCyclesIso_hom_iCycles_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles map hasLeftHomology_of_preserves CategoryTheory.Functor.obj CategoryTheory.Iso.hom mapCyclesIso X₂ CategoryTheory.Functor.map iCycles	—	hasLeftHomology_of_preserves CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapCyclesIso_hom_iCycles
mapCyclesIso_hom_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Functor.obj CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex hasLeftHomology_of_preserves' cyclesMap CategoryTheory.Functor.map CategoryTheory.Iso.hom map hasLeftHomology_of_preserves mapCyclesIso	—	hasLeftHomology_of_preserves' hasLeftHomology_of_preserves LeftHomologyData.isPreservedBy_of_preserves CategoryTheory.Category.comp_id LeftHomologyData.map_cyclesMap' CategoryTheory.Category.id_comp
mapCyclesIso_hom_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Functor.obj CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex hasLeftHomology_of_preserves' cyclesMap CategoryTheory.Functor.map CategoryTheory.Iso.hom map hasLeftHomology_of_preserves mapCyclesIso	—	hasLeftHomology_of_preserves' hasLeftHomology_of_preserves CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapCyclesIso_hom_naturality
mapCyclesIso_inv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj cycles map hasLeftHomology_of_preserves CategoryTheory.Functor.map cyclesMap CategoryTheory.Iso.inv mapCyclesIso CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex hasLeftHomology_of_preserves'	—	hasLeftHomology_of_preserves hasLeftHomology_of_preserves' CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Iso.isIso_hom mapCyclesIso_hom_naturality_assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id CategoryTheory.Iso.hom_inv_id_assoc
mapCyclesIso_inv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj cycles CategoryTheory.Functor.map cyclesMap map hasLeftHomology_of_preserves CategoryTheory.Iso.inv mapCyclesIso CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex hasLeftHomology_of_preserves'	—	hasLeftHomology_of_preserves hasLeftHomology_of_preserves' CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapCyclesIso_inv_naturality
mapHomologyIso'_eq_mapHomologyIso 📖	mathematical	—	mapHomologyIso' hasHomology_of_preserves mapHomologyIso	—	CategoryTheory.Iso.ext hasHomology_of_preserves LeftHomologyData.isPreservedBy_of_preserves LeftHomologyData.mapHomologyIso_eq RightHomologyData.isPreservedBy_of_preserves RightHomologyData.mapHomologyIso'_eq hasRightHomology_of_hasHomology hasLeftHomology_of_hasHomology CategoryTheory.Category.assoc CategoryTheory.Category.id_comp CategoryTheory.Functor.map_comp RightHomologyData.map_rightHomologyMap' CategoryTheory.Functor.map_id LeftHomologyData.map_leftHomologyMap' HomologyMapData.comm Mathlib.Tactic.Reassoc.eq_whisker' RightHomologyMapData.rightHomologyMap'_eq LeftHomologyMapData.leftHomologyMap'_eq CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
mapHomologyIso'_hom_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology map CategoryTheory.Functor.obj homologyMap CategoryTheory.Functor.map CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex CategoryTheory.Iso.hom mapHomologyIso'	—	RightHomologyData.isPreservedBy_of_preserves RightHomologyData.rightHomologyIso_hom_naturality_assoc CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc RightHomologyData.rightHomologyIso_inv_naturality
mapHomologyIso'_hom_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology map homologyMap CategoryTheory.Functor.map CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex CategoryTheory.Functor.obj CategoryTheory.Iso.hom mapHomologyIso'	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapHomologyIso'_hom_naturality
mapHomologyIso'_inv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj homology map CategoryTheory.Functor.map homologyMap CategoryTheory.Iso.inv mapHomologyIso' CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Iso.isIso_hom mapHomologyIso'_hom_naturality_assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id CategoryTheory.Iso.hom_inv_id_assoc
mapHomologyIso'_inv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj homology CategoryTheory.Functor.map homologyMap map CategoryTheory.Iso.inv mapHomologyIso' CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapHomologyIso'_inv_naturality
mapHomologyIso_hom_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology map CategoryTheory.Functor.obj homologyMap CategoryTheory.Functor.map CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex CategoryTheory.Iso.hom mapHomologyIso	—	hasLeftHomology_of_hasHomology LeftHomologyData.isPreservedBy_of_preserves CategoryTheory.Category.comp_id LeftHomologyData.map_leftHomologyMap' CategoryTheory.Category.id_comp
mapHomologyIso_hom_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology map homologyMap CategoryTheory.Functor.map CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex CategoryTheory.Functor.obj CategoryTheory.Iso.hom mapHomologyIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapHomologyIso_hom_naturality
mapHomologyIso_inv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj homology map CategoryTheory.Functor.map homologyMap CategoryTheory.Iso.inv mapHomologyIso CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Iso.isIso_hom mapHomologyIso_hom_naturality_assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id CategoryTheory.Iso.hom_inv_id_assoc
mapHomologyIso_inv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj homology CategoryTheory.Functor.map homologyMap map CategoryTheory.Iso.inv mapHomologyIso CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapHomologyIso_inv_naturality
mapLeftHomologyIso_hom_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct leftHomology CategoryTheory.Functor.obj CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex hasLeftHomology_of_preserves' leftHomologyMap CategoryTheory.Functor.map CategoryTheory.Iso.hom map hasLeftHomology_of_preserves mapLeftHomologyIso	—	hasLeftHomology_of_preserves' hasLeftHomology_of_preserves LeftHomologyData.isPreservedBy_of_preserves CategoryTheory.Category.comp_id LeftHomologyData.map_leftHomologyMap' CategoryTheory.Category.id_comp
mapLeftHomologyIso_hom_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct leftHomology CategoryTheory.Functor.obj CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex hasLeftHomology_of_preserves' leftHomologyMap CategoryTheory.Functor.map CategoryTheory.Iso.hom map hasLeftHomology_of_preserves mapLeftHomologyIso	—	hasLeftHomology_of_preserves' hasLeftHomology_of_preserves CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapLeftHomologyIso_hom_naturality
mapLeftHomologyIso_inv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj leftHomology map hasLeftHomology_of_preserves CategoryTheory.Functor.map leftHomologyMap CategoryTheory.Iso.inv mapLeftHomologyIso CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex hasLeftHomology_of_preserves'	—	hasLeftHomology_of_preserves hasLeftHomology_of_preserves' CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Iso.isIso_hom mapLeftHomologyIso_hom_naturality_assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id CategoryTheory.Iso.hom_inv_id_assoc
mapLeftHomologyIso_inv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj leftHomology CategoryTheory.Functor.map leftHomologyMap map hasLeftHomology_of_preserves CategoryTheory.Iso.inv mapLeftHomologyIso CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex hasLeftHomology_of_preserves'	—	hasLeftHomology_of_preserves hasLeftHomology_of_preserves' CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapLeftHomologyIso_inv_naturality
mapOpcyclesIso_hom_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles CategoryTheory.Functor.obj CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex hasRightHomology_of_preserves' opcyclesMap CategoryTheory.Functor.map CategoryTheory.Iso.hom map hasRightHomology_of_preserves mapOpcyclesIso	—	hasRightHomology_of_preserves' hasRightHomology_of_preserves RightHomologyData.isPreservedBy_of_preserves CategoryTheory.Category.comp_id RightHomologyData.map_opcyclesMap' CategoryTheory.Category.id_comp
mapOpcyclesIso_hom_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles CategoryTheory.Functor.obj CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex hasRightHomology_of_preserves' opcyclesMap CategoryTheory.Functor.map CategoryTheory.Iso.hom map hasRightHomology_of_preserves mapOpcyclesIso	—	hasRightHomology_of_preserves' hasRightHomology_of_preserves CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapOpcyclesIso_hom_naturality
mapOpcyclesIso_inv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj opcycles map hasRightHomology_of_preserves CategoryTheory.Functor.map opcyclesMap CategoryTheory.Iso.inv mapOpcyclesIso CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex hasRightHomology_of_preserves'	—	hasRightHomology_of_preserves hasRightHomology_of_preserves' CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Iso.isIso_hom mapOpcyclesIso_hom_naturality_assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id CategoryTheory.Iso.hom_inv_id_assoc
mapOpcyclesIso_inv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj opcycles CategoryTheory.Functor.map opcyclesMap map hasRightHomology_of_preserves CategoryTheory.Iso.inv mapOpcyclesIso CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex hasRightHomology_of_preserves'	—	hasRightHomology_of_preserves hasRightHomology_of_preserves' CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapOpcyclesIso_inv_naturality
mapRightHomologyIso_hom_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct rightHomology CategoryTheory.Functor.obj CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex hasRightHomology_of_preserves' rightHomologyMap CategoryTheory.Functor.map CategoryTheory.Iso.hom map hasRightHomology_of_preserves mapRightHomologyIso	—	hasRightHomology_of_preserves' hasRightHomology_of_preserves RightHomologyData.isPreservedBy_of_preserves CategoryTheory.Category.comp_id RightHomologyData.map_rightHomologyMap' CategoryTheory.Category.id_comp
mapRightHomologyIso_hom_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct rightHomology CategoryTheory.Functor.obj CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex hasRightHomology_of_preserves' rightHomologyMap CategoryTheory.Functor.map CategoryTheory.Iso.hom map hasRightHomology_of_preserves mapRightHomologyIso	—	hasRightHomology_of_preserves' hasRightHomology_of_preserves CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapRightHomologyIso_hom_naturality
mapRightHomologyIso_inv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj rightHomology map hasRightHomology_of_preserves CategoryTheory.Functor.map rightHomologyMap CategoryTheory.Iso.inv mapRightHomologyIso CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex hasRightHomology_of_preserves'	—	hasRightHomology_of_preserves hasRightHomology_of_preserves' CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Iso.isIso_hom mapRightHomologyIso_hom_naturality_assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id CategoryTheory.Iso.hom_inv_id_assoc
mapRightHomologyIso_inv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj rightHomology CategoryTheory.Functor.map rightHomologyMap map hasRightHomology_of_preserves CategoryTheory.Iso.inv mapRightHomologyIso CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex hasRightHomology_of_preserves'	—	hasRightHomology_of_preserves hasRightHomology_of_preserves' CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapRightHomologyIso_inv_naturality
map_leftRightHomologyComparison' 📖	mathematical	—	CategoryTheory.Functor.map LeftHomologyData.H RightHomologyData.H leftRightHomologyComparison' map LeftHomologyData.map RightHomologyData.map	—	CategoryTheory.Limits.Cofork.IsColimit.hom_ext zero LeftHomologyData.wi LeftHomologyData.wπ CategoryTheory.Limits.Fork.IsLimit.hom_ext RightHomologyData.wp RightHomologyData.wι CategoryTheory.Category.assoc π_leftRightHomologyComparison'_ι CategoryTheory.Functor.map_comp
quasiIso_map_iff_of_preservesLeftHomology 📖	mathematical	—	QuasiIso CategoryTheory.Functor.obj CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex CategoryTheory.Functor.map	—	hasLeftHomology_of_hasHomology LeftHomologyMapData.quasiIso_iff LeftHomologyData.isPreservedBy_of_preserves LeftHomologyMapData.map_φH CategoryTheory.isIso_of_reflects_iso CategoryTheory.Functor.map_isIso
quasiIso_map_iff_of_preservesRightHomology 📖	mathematical	—	QuasiIso CategoryTheory.Functor.obj CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex CategoryTheory.Functor.map	—	hasRightHomology_of_hasHomology RightHomologyMapData.quasiIso_iff RightHomologyData.isPreservedBy_of_preserves RightHomologyMapData.map_φH CategoryTheory.isIso_of_reflects_iso CategoryTheory.Functor.map_isIso
quasiIso_map_of_preservesLeftHomology 📖	mathematical	—	QuasiIso CategoryTheory.Functor.obj CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex CategoryTheory.Functor.map	—	hasLeftHomology_of_hasHomology LeftHomologyMapData.quasiIso_iff LeftHomologyData.isPreservedBy_of_preserves LeftHomologyMapData.map_φH CategoryTheory.Functor.map_isIso
quasiIso_map_of_preservesRightHomology 📖	mathematical	—	QuasiIso CategoryTheory.Functor.obj CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex CategoryTheory.Functor.map	—	hasRightHomology_of_hasHomology RightHomologyMapData.quasiIso_iff RightHomologyData.isPreservedBy_of_preserves RightHomologyMapData.map_φH CategoryTheory.Functor.map_isIso

CategoryTheory.ShortComplex.HomologyData

Definitions

Name	Category	Theorems
map 📖	CompOp	8 math math: CategoryTheory.ShortComplex.HomologyMapData.map_left, CategoryTheory.ShortComplex.HomologyMapData.natTransApp_left, map_homologyMap', CategoryTheory.ShortComplex.HomologyMapData.map_right, map_left, map_right, map_iso, CategoryTheory.ShortComplex.HomologyMapData.natTransApp_right

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_homologyMap' 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.ShortComplex.LeftHomologyData.H left CategoryTheory.ShortComplex.homologyMap' CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.mapShortComplex map	—	CategoryTheory.ShortComplex.LeftHomologyData.map_leftHomologyMap'
map_iso 📖	mathematical	—	iso CategoryTheory.ShortComplex.map map CategoryTheory.Functor.mapIso CategoryTheory.ShortComplex.LeftHomologyData.H left CategoryTheory.ShortComplex.RightHomologyData.H right	—	—
map_left 📖	mathematical	—	left CategoryTheory.ShortComplex.map map CategoryTheory.ShortComplex.LeftHomologyData.map	—	—
map_right 📖	mathematical	—	right CategoryTheory.ShortComplex.map map CategoryTheory.ShortComplex.RightHomologyData.map	—	—

CategoryTheory.ShortComplex.HomologyMapData

Definitions

Name	Category	Theorems
map 📖	CompOp	2 math math: map_left, map_right
natTransApp 📖	CompOp	2 math math: natTransApp_left, natTransApp_right

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_left 📖	mathematical	—	left CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.mapShortComplex CategoryTheory.Functor.map CategoryTheory.ShortComplex.HomologyData.map map CategoryTheory.ShortComplex.LeftHomologyMapData.map CategoryTheory.ShortComplex.HomologyData.left	—	—
map_right 📖	mathematical	—	right CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.mapShortComplex CategoryTheory.Functor.map CategoryTheory.ShortComplex.HomologyData.map map CategoryTheory.ShortComplex.RightHomologyMapData.map CategoryTheory.ShortComplex.HomologyData.right	—	—
natTransApp_left 📖	mathematical	—	left CategoryTheory.ShortComplex.map CategoryTheory.ShortComplex.mapNatTrans CategoryTheory.ShortComplex.HomologyData.map CategoryTheory.ShortComplex.LeftHomologyData.isPreservedBy_of_preserves CategoryTheory.ShortComplex.HomologyData.left CategoryTheory.ShortComplex.RightHomologyData.isPreservedBy_of_preserves CategoryTheory.ShortComplex.HomologyData.right natTransApp CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp	—	CategoryTheory.ShortComplex.LeftHomologyData.isPreservedBy_of_preserves CategoryTheory.ShortComplex.RightHomologyData.isPreservedBy_of_preserves
natTransApp_right 📖	mathematical	—	right CategoryTheory.ShortComplex.map CategoryTheory.ShortComplex.mapNatTrans CategoryTheory.ShortComplex.HomologyData.map CategoryTheory.ShortComplex.LeftHomologyData.isPreservedBy_of_preserves CategoryTheory.ShortComplex.HomologyData.left CategoryTheory.ShortComplex.RightHomologyData.isPreservedBy_of_preserves CategoryTheory.ShortComplex.HomologyData.right natTransApp CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp	—	CategoryTheory.ShortComplex.RightHomologyData.isPreservedBy_of_preserves CategoryTheory.ShortComplex.LeftHomologyData.isPreservedBy_of_preserves

CategoryTheory.ShortComplex.LeftHomologyData

Definitions

Name	Category	Theorems
IsPreservedBy 📖	CompData	3 math math: isPreservedBy_of_preservesHomology, isPreservedBy_of_preserves, CategoryTheory.Functor.PreservesLeftHomologyOf.isPreservedBy
map 📖	CompOp	16 math math: map_leftHomologyMap', CategoryTheory.ShortComplex.LeftHomologyMapData.map_φH, map_π, map_i, map_cyclesMap', map_K, CategoryTheory.ShortComplex.HomologyData.map_left, CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp_φK, mapLeftHomologyIso_eq, mapCyclesIso_eq, CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp_φH, mapHomologyIso_eq, CategoryTheory.ShortComplex.map_leftRightHomologyComparison', map_f', map_H, CategoryTheory.ShortComplex.LeftHomologyMapData.map_φK

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPreservedBy_of_preserves 📖	mathematical	—	IsPreservedBy	—	CategoryTheory.Functor.PreservesLeftHomologyOf.isPreservedBy
isPreservedBy_of_preservesHomology 📖	mathematical	—	IsPreservedBy	—	CategoryTheory.Functor.PreservesHomology.preservesKernel CategoryTheory.Functor.PreservesHomology.preservesCokernel
mapCyclesIso_eq 📖	mathematical	—	CategoryTheory.ShortComplex.mapCyclesIso CategoryTheory.Iso.trans CategoryTheory.ShortComplex.cycles CategoryTheory.ShortComplex.map CategoryTheory.ShortComplex.hasLeftHomology_of_preserves K map isPreservedBy_of_preserves CategoryTheory.Functor.obj cyclesIso CategoryTheory.Functor.mapIso CategoryTheory.Iso.symm	—	CategoryTheory.Iso.ext CategoryTheory.ShortComplex.hasLeftHomology_of_preserves isPreservedBy_of_preserves map_cyclesMap' CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
mapHomologyIso_eq 📖	mathematical	—	CategoryTheory.ShortComplex.mapHomologyIso CategoryTheory.Iso.trans CategoryTheory.ShortComplex.homology CategoryTheory.ShortComplex.map H map isPreservedBy_of_preserves CategoryTheory.Functor.obj homologyIso CategoryTheory.Functor.mapIso CategoryTheory.Iso.symm	—	CategoryTheory.Iso.ext isPreservedBy_of_preserves CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.Category.comp_id map_leftHomologyMap' CategoryTheory.Functor.map_id
mapLeftHomologyIso_eq 📖	mathematical	—	CategoryTheory.ShortComplex.mapLeftHomologyIso CategoryTheory.Iso.trans CategoryTheory.ShortComplex.leftHomology CategoryTheory.ShortComplex.map CategoryTheory.ShortComplex.hasLeftHomology_of_preserves H map isPreservedBy_of_preserves CategoryTheory.Functor.obj leftHomologyIso CategoryTheory.Functor.mapIso CategoryTheory.Iso.symm	—	CategoryTheory.Iso.ext CategoryTheory.ShortComplex.hasLeftHomology_of_preserves isPreservedBy_of_preserves CategoryTheory.ShortComplex.leftHomology_ext map_leftHomologyMap' CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
map_H 📖	mathematical	—	H CategoryTheory.ShortComplex.map map CategoryTheory.Functor.obj	—	—
map_K 📖	mathematical	—	K CategoryTheory.ShortComplex.map map CategoryTheory.Functor.obj	—	—
map_cyclesMap' 📖	mathematical	—	CategoryTheory.Functor.map K CategoryTheory.ShortComplex.cyclesMap' CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.mapShortComplex map	—	CategoryTheory.ShortComplex.LeftHomologyMapData.cyclesMap'_eq CategoryTheory.ShortComplex.LeftHomologyMapData.map_φK
map_f' 📖	mathematical	—	f' CategoryTheory.ShortComplex.map map CategoryTheory.Functor.map CategoryTheory.ShortComplex.X₁ K	—	CategoryTheory.cancel_mono instMonoI f'_i CategoryTheory.ShortComplex.map_f map_i CategoryTheory.Functor.map_comp
map_i 📖	mathematical	—	i CategoryTheory.ShortComplex.map map CategoryTheory.Functor.map K CategoryTheory.ShortComplex.X₂	—	—
map_leftHomologyMap' 📖	mathematical	—	CategoryTheory.Functor.map H CategoryTheory.ShortComplex.leftHomologyMap' CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.mapShortComplex map	—	CategoryTheory.ShortComplex.LeftHomologyMapData.leftHomologyMap'_eq CategoryTheory.ShortComplex.LeftHomologyMapData.map_φH
map_π 📖	mathematical	—	π CategoryTheory.ShortComplex.map map CategoryTheory.Functor.map K H	—	—

CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
f' 📖	mathematical	—	CategoryTheory.Limits.PreservesColimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.LeftHomologyData.K CategoryTheory.ShortComplex.LeftHomologyData.f' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
g 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit 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	—	—
hf' 📖	mathematical	—	CategoryTheory.Limits.PreservesColimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.LeftHomologyData.K CategoryTheory.ShortComplex.LeftHomologyData.f' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero	—	f'
hg 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit 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	—	g

CategoryTheory.ShortComplex.LeftHomologyMapData

Definitions

Name	Category	Theorems
map 📖	CompOp	3 math math: map_φH, CategoryTheory.ShortComplex.HomologyMapData.map_left, map_φK
natTransApp 📖	CompOp	3 math math: CategoryTheory.ShortComplex.HomologyMapData.natTransApp_left, natTransApp_φK, natTransApp_φH

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_φH 📖	mathematical	—	φH CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.mapShortComplex CategoryTheory.Functor.map CategoryTheory.ShortComplex.LeftHomologyData.map map CategoryTheory.ShortComplex.LeftHomologyData.H	—	—
map_φK 📖	mathematical	—	φK CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.mapShortComplex CategoryTheory.Functor.map CategoryTheory.ShortComplex.LeftHomologyData.map map CategoryTheory.ShortComplex.LeftHomologyData.K	—	—
natTransApp_φH 📖	mathematical	—	φH CategoryTheory.ShortComplex.map CategoryTheory.ShortComplex.mapNatTrans CategoryTheory.ShortComplex.LeftHomologyData.map CategoryTheory.ShortComplex.LeftHomologyData.isPreservedBy_of_preserves natTransApp CategoryTheory.NatTrans.app CategoryTheory.ShortComplex.LeftHomologyData.H	—	CategoryTheory.ShortComplex.LeftHomologyData.isPreservedBy_of_preserves
natTransApp_φK 📖	mathematical	—	φK CategoryTheory.ShortComplex.map CategoryTheory.ShortComplex.mapNatTrans CategoryTheory.ShortComplex.LeftHomologyData.map CategoryTheory.ShortComplex.LeftHomologyData.isPreservedBy_of_preserves natTransApp CategoryTheory.NatTrans.app CategoryTheory.ShortComplex.LeftHomologyData.K	—	CategoryTheory.ShortComplex.LeftHomologyData.isPreservedBy_of_preserves
quasiIso_map_iff 📖	mathematical	—	CategoryTheory.ShortComplex.QuasiIso CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.mapShortComplex CategoryTheory.Functor.map CategoryTheory.IsIso CategoryTheory.ShortComplex.LeftHomologyData.H φH	—	quasiIso_iff

CategoryTheory.ShortComplex.RightHomologyData

Definitions

Name	Category	Theorems
IsPreservedBy 📖	CompData	3 math math: CategoryTheory.Functor.PreservesRightHomologyOf.isPreservedBy, isPreservedBy_of_preserves, isPreservedBy_of_preservesHomology
map 📖	CompOp	16 math math: map_ι, CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp_φQ, map_g', map_H, mapOpcyclesIso_eq, map_rightHomologyMap', CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp_φH, map_Q, map_p, mapRightHomologyIso_eq, CategoryTheory.ShortComplex.HomologyData.map_right, CategoryTheory.ShortComplex.map_leftRightHomologyComparison', CategoryTheory.ShortComplex.RightHomologyMapData.map_φH, map_opcyclesMap', CategoryTheory.ShortComplex.RightHomologyMapData.map_φQ, mapHomologyIso'_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPreservedBy_of_preserves 📖	mathematical	—	IsPreservedBy	—	CategoryTheory.Functor.PreservesRightHomologyOf.isPreservedBy
isPreservedBy_of_preservesHomology 📖	mathematical	—	IsPreservedBy	—	CategoryTheory.Functor.PreservesHomology.preservesCokernel CategoryTheory.Functor.PreservesHomology.preservesKernel
mapHomologyIso'_eq 📖	mathematical	—	CategoryTheory.ShortComplex.mapHomologyIso' CategoryTheory.Iso.trans CategoryTheory.ShortComplex.homology CategoryTheory.ShortComplex.map H map isPreservedBy_of_preserves CategoryTheory.Functor.obj homologyIso CategoryTheory.Functor.mapIso CategoryTheory.Iso.symm	—	CategoryTheory.Iso.ext isPreservedBy_of_preserves CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp map_rightHomologyMap'
mapOpcyclesIso_eq 📖	mathematical	—	CategoryTheory.ShortComplex.mapOpcyclesIso CategoryTheory.Iso.trans CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.map CategoryTheory.ShortComplex.hasRightHomology_of_preserves Q map isPreservedBy_of_preserves CategoryTheory.Functor.obj opcyclesIso CategoryTheory.Functor.mapIso CategoryTheory.Iso.symm	—	CategoryTheory.Iso.ext CategoryTheory.ShortComplex.hasRightHomology_of_preserves isPreservedBy_of_preserves CategoryTheory.ShortComplex.opcycles_ext map_opcyclesMap' CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
mapRightHomologyIso_eq 📖	mathematical	—	CategoryTheory.ShortComplex.mapRightHomologyIso CategoryTheory.Iso.trans CategoryTheory.ShortComplex.rightHomology CategoryTheory.ShortComplex.map CategoryTheory.ShortComplex.hasRightHomology_of_preserves H map isPreservedBy_of_preserves CategoryTheory.Functor.obj rightHomologyIso CategoryTheory.Functor.mapIso CategoryTheory.Iso.symm	—	CategoryTheory.Iso.ext CategoryTheory.ShortComplex.hasRightHomology_of_preserves isPreservedBy_of_preserves map_rightHomologyMap' CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
map_H 📖	mathematical	—	H CategoryTheory.ShortComplex.map map CategoryTheory.Functor.obj	—	—
map_Q 📖	mathematical	—	Q CategoryTheory.ShortComplex.map map CategoryTheory.Functor.obj	—	—
map_g' 📖	mathematical	—	g' CategoryTheory.ShortComplex.map map CategoryTheory.Functor.map Q CategoryTheory.ShortComplex.X₃	—	CategoryTheory.cancel_epi instEpiP p_g' CategoryTheory.ShortComplex.map_g map_p CategoryTheory.Functor.map_comp
map_opcyclesMap' 📖	mathematical	—	CategoryTheory.Functor.map Q CategoryTheory.ShortComplex.opcyclesMap' CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.mapShortComplex map	—	CategoryTheory.ShortComplex.RightHomologyMapData.opcyclesMap'_eq CategoryTheory.ShortComplex.RightHomologyMapData.map_φQ
map_p 📖	mathematical	—	p CategoryTheory.ShortComplex.map map CategoryTheory.Functor.map CategoryTheory.ShortComplex.X₂ Q	—	—
map_rightHomologyMap' 📖	mathematical	—	CategoryTheory.Functor.map H CategoryTheory.ShortComplex.rightHomologyMap' CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.mapShortComplex map	—	CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap'_eq CategoryTheory.ShortComplex.RightHomologyMapData.map_φH
map_ι 📖	mathematical	—	ι CategoryTheory.ShortComplex.map map CategoryTheory.Functor.map H Q	—	—

CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
f 📖	mathematical	—	CategoryTheory.Limits.PreservesColimit 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	—	—
g' 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.RightHomologyData.Q CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.RightHomologyData.g' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
hf 📖	mathematical	—	CategoryTheory.Limits.PreservesColimit 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	—	f
hg' 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.RightHomologyData.Q CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.RightHomologyData.g' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero	—	g'

CategoryTheory.ShortComplex.RightHomologyMapData

Definitions

Name	Category	Theorems
map 📖	CompOp	3 math math: CategoryTheory.ShortComplex.HomologyMapData.map_right, map_φH, map_φQ
natTransApp 📖	CompOp	3 math math: natTransApp_φQ, natTransApp_φH, CategoryTheory.ShortComplex.HomologyMapData.natTransApp_right

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_φH 📖	mathematical	—	φH CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.mapShortComplex CategoryTheory.Functor.map CategoryTheory.ShortComplex.RightHomologyData.map map CategoryTheory.ShortComplex.RightHomologyData.H	—	—
map_φQ 📖	mathematical	—	φQ CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.mapShortComplex CategoryTheory.Functor.map CategoryTheory.ShortComplex.RightHomologyData.map map CategoryTheory.ShortComplex.RightHomologyData.Q	—	—
natTransApp_φH 📖	mathematical	—	φH CategoryTheory.ShortComplex.map CategoryTheory.ShortComplex.mapNatTrans CategoryTheory.ShortComplex.RightHomologyData.map CategoryTheory.ShortComplex.RightHomologyData.isPreservedBy_of_preserves natTransApp CategoryTheory.NatTrans.app CategoryTheory.ShortComplex.RightHomologyData.H	—	CategoryTheory.ShortComplex.RightHomologyData.isPreservedBy_of_preserves
natTransApp_φQ 📖	mathematical	—	φQ CategoryTheory.ShortComplex.map CategoryTheory.ShortComplex.mapNatTrans CategoryTheory.ShortComplex.RightHomologyData.map CategoryTheory.ShortComplex.RightHomologyData.isPreservedBy_of_preserves natTransApp CategoryTheory.NatTrans.app CategoryTheory.ShortComplex.RightHomologyData.Q	—	CategoryTheory.ShortComplex.RightHomologyData.isPreservedBy_of_preserves
quasiIso_map_iff 📖	mathematical	—	CategoryTheory.ShortComplex.QuasiIso CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.mapShortComplex CategoryTheory.Functor.map CategoryTheory.IsIso CategoryTheory.ShortComplex.RightHomologyData.H φH	—	quasiIso_iff

---

← Back to Index