HomologySequence

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

Statistics

Metric	Count
Definitions δ, δIso, composableArrows₃, composableArrows₃Functor, snakeInput, natTransOpCyclesToCycles, opcyclesToCycles	7
Theorems comp_δ, comp_δ_assoc, epi_δ, homology_exact₁, homology_exact₂, homology_exact₃, isIso_δ, mono_δ, δ_comp, δ_comp_assoc, δ_eq, δ_eq', composableArrows₃Functor_map, composableArrows₃Functor_obj, composableArrows₃_exact, instEpiMap'ComposableArrows₃OfNatNat, instMonoMap'ComposableArrows₃OfNatNat, snakeInput_L₀, snakeInput_L₁, snakeInput_L₂, snakeInput_L₃, snakeInput_v₀₁, snakeInput_v₁₂, snakeInput_v₂₃, cycles_left_exact, homologyι_opcyclesToCycles, homologyι_opcyclesToCycles_assoc, natTransOpCyclesToCycles_app, opcyclesToCycles_homologyπ, opcyclesToCycles_homologyπ_assoc, opcyclesToCycles_iCycles, opcyclesToCycles_iCycles_assoc, opcyclesToCycles_naturality, opcyclesToCycles_naturality_assoc, opcycles_right_exact, pOpcycles_opcyclesToCycles, pOpcycles_opcyclesToCycles_assoc, pOpcycles_opcyclesToCycles_iCycles, pOpcycles_opcyclesToCycles_iCycles_assoc	39
Total	46

CategoryTheory.ShortComplex.ShortExact

Definitions

Name	Category	Theorems
δ 📖	CompOp	17 math math: epi_δ, mono_δ, CochainComplex.mappingCone.homologySequenceδ_triangleh, comp_δ, δ_eq', δ_apply', HomologicalComplex.HomologySequence.δ_naturality_assoc, isIso_δ, δ_comp_assoc, homology_exact₃, δ_eq, δ_apply, δ_comp, HomologicalComplex.HomologySequence.δ_naturality, homology_exact₁, HomologicalComplex.shortComplexTruncLE_shortExact_δ_eq_zero, comp_δ_assoc
δIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_δ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.homology CategoryTheory.ShortComplex.X₂ CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.X₁ HomologicalComplex.homologyMap CategoryTheory.ShortComplex.g δ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.ShortComplex.SnakeInput.L₀_g_δ
comp_δ_assoc 📖	mathematical	CategoryTheory.ShortComplex.ShortExact HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.homology CategoryTheory.ShortComplex.X₂ CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc CategoryTheory.ShortComplex.X₃ HomologicalComplex.homologyMap CategoryTheory.ShortComplex.g CategoryTheory.ShortComplex.X₁ δ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_δ
epi_δ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms ComplexShape.Rel CategoryTheory.Limits.IsZero HomologicalComplex.homology CategoryTheory.ShortComplex.X₂ CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc	CategoryTheory.Epi CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.X₁ δ	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.SnakeInput.epi_δ
homology_exact₁ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms ComplexShape.Rel	CategoryTheory.ShortComplex.Exact HomologicalComplex.homology CategoryTheory.ShortComplex.X₃ CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ δ HomologicalComplex.homologyMap CategoryTheory.ShortComplex.f δ_comp	—	CategoryTheory.ShortComplex.SnakeInput.L₂'_exact
homology_exact₂ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms	CategoryTheory.ShortComplex.Exact HomologicalComplex.homology CategoryTheory.ShortComplex.X₁ CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ HomologicalComplex.homologyMap CategoryTheory.ShortComplex.f CategoryTheory.ShortComplex.g	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.SnakeInput.L₀_exact epi_g CategoryTheory.ShortComplex.isIso_homologyι HomologicalComplex.shape HomologicalComplex.instPreservesZeroMorphismsHomologyFunctor HomologicalComplex.instPreservesZeroMorphismsOpcyclesFunctor HomologicalComplex.homologyι_naturality CategoryTheory.ShortComplex.exact_of_iso HomologicalComplex.opcycles_right_exact exact
homology_exact₃ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms ComplexShape.Rel	CategoryTheory.ShortComplex.Exact HomologicalComplex.homology CategoryTheory.ShortComplex.X₂ CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.X₁ HomologicalComplex.homologyMap CategoryTheory.ShortComplex.g δ comp_δ	—	CategoryTheory.ShortComplex.SnakeInput.L₁'_exact
isIso_δ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms ComplexShape.Rel CategoryTheory.Limits.IsZero HomologicalComplex.homology CategoryTheory.ShortComplex.X₂ CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc	CategoryTheory.IsIso CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.X₁ δ	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.SnakeInput.isIso_δ
mono_δ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms ComplexShape.Rel CategoryTheory.Limits.IsZero HomologicalComplex.homology CategoryTheory.ShortComplex.X₂ CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc	CategoryTheory.Mono CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.X₁ δ	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.SnakeInput.mono_δ
δ_comp 📖	mathematical	CategoryTheory.ShortComplex.ShortExact HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.homology CategoryTheory.ShortComplex.X₃ CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ δ HomologicalComplex.homologyMap CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.ShortComplex.SnakeInput.δ_L₃_f
δ_comp_assoc 📖	mathematical	CategoryTheory.ShortComplex.ShortExact HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.homology CategoryTheory.ShortComplex.X₃ CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc CategoryTheory.ShortComplex.X₁ δ CategoryTheory.ShortComplex.X₂ HomologicalComplex.homologyMap CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_comp
δ_eq 📖	mathematical	CategoryTheory.ShortComplex.ShortExact HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms ComplexShape.Rel CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.ShortComplex.X₃ HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.ShortComplex.X₂ HomologicalComplex.Hom.f CategoryTheory.ShortComplex.g CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f ComplexShape.next	HomologicalComplex.cycles CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc HomologicalComplex.homology HomologicalComplex.liftCycles ComplexShape.next_eq' HomologicalComplex.homologyπ δ	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian ComplexShape.next_eq' CategoryTheory.Category.assoc δ_eq' HomologicalComplex.p_opcyclesMap Mathlib.Tactic.Reassoc.eq_whisker' HomologicalComplex.homology_π_ι HomologicalComplex.liftCycles_i_assoc CategoryTheory.cancel_mono HomologicalComplex.instMonoICycles HomologicalComplex.liftCycles_comp_cyclesMap HomologicalComplex.liftCycles_i HomologicalComplex.opcyclesToCycles_iCycles HomologicalComplex.p_fromOpcycles
δ_eq' 📖	mathematical	CategoryTheory.ShortComplex.ShortExact HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms ComplexShape.Rel CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.opcycles CategoryTheory.ShortComplex.X₂ CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc CategoryTheory.ShortComplex.X₃ HomologicalComplex.opcyclesMap CategoryTheory.ShortComplex.g HomologicalComplex.homology HomologicalComplex.homologyι HomologicalComplex.cycles CategoryTheory.ShortComplex.X₁ HomologicalComplex.cyclesMap CategoryTheory.ShortComplex.f HomologicalComplex.opcyclesToCycles	δ HomologicalComplex.homologyπ	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.SnakeInput.δ_eq

HomologicalComplex

Definitions

Name	Category	Theorems
natTransOpCyclesToCycles 📖	CompOp	2 math math: natTransOpCyclesToCycles_app, HomologySequence.snakeInput_v₁₂
opcyclesToCycles 📖	CompOp	13 math math: pOpcycles_opcyclesToCycles_iCycles_assoc, homologyι_opcyclesToCycles_assoc, opcyclesToCycles_iCycles_assoc, opcyclesToCycles_naturality, opcyclesToCycles_homologyπ, natTransOpCyclesToCycles_app, opcyclesToCycles_homologyπ_assoc, opcyclesToCycles_naturality_assoc, homologyι_opcyclesToCycles, pOpcycles_opcyclesToCycles_iCycles, pOpcycles_opcyclesToCycles, pOpcycles_opcyclesToCycles_assoc, opcyclesToCycles_iCycles

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cycles_left_exact 📖	mathematical	CategoryTheory.ShortComplex.Exact HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive instCategory instHasZeroMorphisms	cycles CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ cyclesMap CategoryTheory.ShortComplex.f CategoryTheory.ShortComplex.g	—	instPreservesZeroMorphismsEval instMonoFOfHasFiniteLimits CategoryTheory.Abelian.hasFiniteLimits CategoryTheory.ShortComplex.zero CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory CategoryTheory.ShortComplex.Exact.map CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf CategoryTheory.Functor.preservesHomologyOfExact instPreservesFiniteLimitsEvalOfHasFiniteLimits instPreservesFiniteColimitsEvalOfHasFiniteColimits CategoryTheory.Abelian.hasFiniteColimits CategoryTheory.Functor.PreservesHomology.preservesRightHomologyOf CategoryTheory.ShortComplex.exact_of_f_is_kernel CategoryTheory.Category.assoc cyclesMap_i Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Limits.zero_comp CategoryTheory.cancel_mono Hom.comm iCycles_d CategoryTheory.Limits.comp_zero instMonoICycles liftCycles_comp_cyclesMap liftCycles_i instMonoCyclesMapOfF CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian
homologyι_opcyclesToCycles 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology opcycles cycles homologyι opcyclesToCycles Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.cancel_mono instMonoICycles CategoryTheory.Category.assoc opcyclesToCycles_iCycles homologyι_comp_fromOpcycles CategoryTheory.Limits.zero_comp
homologyι_opcyclesToCycles_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology opcycles homologyι cycles opcyclesToCycles Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homologyι_opcyclesToCycles
natTransOpCyclesToCycles_app 📖	mathematical	—	CategoryTheory.NatTrans.app HomologicalComplex instCategory opcyclesFunctor cyclesFunctor natTransOpCyclesToCycles opcyclesToCycles	—	—
opcyclesToCycles_homologyπ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles cycles homology opcyclesToCycles homologyπ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.cancel_epi instEpiPOpcycles pOpcycles_opcyclesToCycles_assoc toCycles_comp_homologyπ CategoryTheory.Limits.comp_zero
opcyclesToCycles_homologyπ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles cycles opcyclesToCycles homology homologyπ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opcyclesToCycles_homologyπ
opcyclesToCycles_iCycles 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles cycles X opcyclesToCycles iCycles fromOpcycles	—	liftCycles_i
opcyclesToCycles_iCycles_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles cycles opcyclesToCycles X iCycles fromOpcycles	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opcyclesToCycles_iCycles
opcyclesToCycles_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles cycles opcyclesMap opcyclesToCycles cyclesMap	—	CategoryTheory.cancel_mono instMonoICycles CategoryTheory.Category.assoc cyclesMap_i CategoryTheory.cancel_epi instEpiPOpcycles p_opcyclesMap_assoc pOpcycles_opcyclesToCycles_iCycles Hom.comm pOpcycles_opcyclesToCycles_iCycles_assoc
opcyclesToCycles_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles opcyclesMap cycles opcyclesToCycles cyclesMap	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opcyclesToCycles_naturality
opcycles_right_exact 📖	mathematical	CategoryTheory.ShortComplex.Exact HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive instCategory instHasZeroMorphisms	opcycles CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ opcyclesMap CategoryTheory.ShortComplex.f CategoryTheory.ShortComplex.g	—	instPreservesZeroMorphismsEval instEpiFOfHasFiniteColimits CategoryTheory.Abelian.hasFiniteColimits CategoryTheory.ShortComplex.zero CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory CategoryTheory.ShortComplex.Exact.map CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf CategoryTheory.Functor.preservesHomologyOfExact instPreservesFiniteLimitsEvalOfHasFiniteLimits CategoryTheory.Abelian.hasFiniteLimits instPreservesFiniteColimitsEvalOfHasFiniteColimits CategoryTheory.Functor.PreservesHomology.preservesRightHomologyOf CategoryTheory.ShortComplex.exact_of_g_is_cokernel p_opcyclesMap_assoc CategoryTheory.Limits.comp_zero CategoryTheory.cancel_epi Hom.comm_assoc d_pOpcycles_assoc CategoryTheory.Limits.zero_comp instEpiPOpcycles opcyclesMap_comp_descOpcycles p_descOpcycles instEpiOpcyclesMapOfF CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian
pOpcycles_opcyclesToCycles 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X opcycles cycles pOpcycles opcyclesToCycles toCycles	—	CategoryTheory.cancel_mono instMonoICycles CategoryTheory.Category.assoc opcyclesToCycles_iCycles p_fromOpcycles toCycles_i
pOpcycles_opcyclesToCycles_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X opcycles pOpcycles cycles opcyclesToCycles toCycles	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pOpcycles_opcyclesToCycles
pOpcycles_opcyclesToCycles_iCycles 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X opcycles pOpcycles cycles opcyclesToCycles iCycles d	—	liftCycles_i p_fromOpcycles
pOpcycles_opcyclesToCycles_iCycles_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X opcycles pOpcycles cycles opcyclesToCycles iCycles d	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pOpcycles_opcyclesToCycles_iCycles

HomologicalComplex.HomologySequence

Definitions

Name	Category	Theorems
composableArrows₃ 📖	CompOp	5 math math: instEpiMap'ComposableArrows₃OfNatNat, instMonoMap'ComposableArrows₃OfNatNat, composableArrows₃_exact, composableArrows₃Functor_map, composableArrows₃Functor_obj
composableArrows₃Functor 📖	CompOp	2 math math: composableArrows₃Functor_map, composableArrows₃Functor_obj
snakeInput 📖	CompOp	11 math math: snakeInput_v₂₃, mapSnakeInput_f₃, snakeInput_L₁, snakeInput_v₀₁, mapSnakeInput_f₁, snakeInput_L₀, snakeInput_L₂, snakeInput_v₁₂, snakeInput_L₃, mapSnakeInput_f₂, mapSnakeInput_f₀

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
composableArrows₃Functor_map 📖	mathematical	—	CategoryTheory.Functor.map HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder composableArrows₃Functor CategoryTheory.ComposableArrows.homMk₃ composableArrows₃ HomologicalComplex.homologyMap HomologicalComplex.opcyclesMap HomologicalComplex.cyclesMap	—	—
composableArrows₃Functor_obj 📖	mathematical	—	CategoryTheory.Functor.obj HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder composableArrows₃Functor composableArrows₃	—	—
composableArrows₃_exact 📖	mathematical	ComplexShape.Rel	CategoryTheory.ComposableArrows.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms composableArrows₃ CategoryTheory.CategoryWithHomology.hasHomology HomologicalComplex.sc	—	CategoryTheory.CategoryWithHomology.hasHomology HomologicalComplex.homologyι_opcyclesToCycles HomologicalComplex.homologyι_comp_fromOpcycles CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id HomologicalComplex.opcyclesToCycles_iCycles CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono CategoryTheory.instEpiId CategoryTheory.IsIso.id HomologicalComplex.instMonoICycles CategoryTheory.ShortComplex.exact_of_f_is_kernel ComplexShape.next_eq' HomologicalComplex.opcyclesToCycles_homologyπ HomologicalComplex.toCycles_comp_homologyπ HomologicalComplex.pOpcycles_opcyclesToCycles HomologicalComplex.instEpiPOpcycles CategoryTheory.instMonoId CategoryTheory.ShortComplex.exact_of_g_is_cokernel ComplexShape.prev_eq' CategoryTheory.ComposableArrows.exact_of_δ₀ CategoryTheory.ShortComplex.Exact.exact_toComposableArrows
instEpiMap'ComposableArrows₃OfNatNat 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder composableArrows₃ CategoryTheory.ComposableArrows.map'	—	HomologicalComplex.instEpiHomologyπ
instMonoMap'ComposableArrows₃OfNatNat 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder composableArrows₃ CategoryTheory.ComposableArrows.map'	—	HomologicalComplex.instMonoHomologyι
snakeInput_L₀ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms ComplexShape.Rel	CategoryTheory.ShortComplex.SnakeInput.L₀ snakeInput CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.mapShortComplex HomologicalComplex.homologyFunctor CategoryTheory.categoryWithHomology_of_abelian	—	—
snakeInput_L₁ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms ComplexShape.Rel	CategoryTheory.ShortComplex.SnakeInput.L₁ snakeInput CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.mapShortComplex HomologicalComplex.opcyclesFunctor CategoryTheory.categoryWithHomology_of_abelian	—	—
snakeInput_L₂ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms ComplexShape.Rel	CategoryTheory.ShortComplex.SnakeInput.L₂ snakeInput CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.mapShortComplex HomologicalComplex.cyclesFunctor CategoryTheory.categoryWithHomology_of_abelian	—	—
snakeInput_L₃ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms ComplexShape.Rel	CategoryTheory.ShortComplex.SnakeInput.L₃ snakeInput CategoryTheory.Functor.obj CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.mapShortComplex HomologicalComplex.homologyFunctor CategoryTheory.categoryWithHomology_of_abelian	—	—
snakeInput_v₀₁ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms ComplexShape.Rel	CategoryTheory.ShortComplex.SnakeInput.v₀₁ snakeInput CategoryTheory.ShortComplex.mapNatTrans HomologicalComplex.homologyFunctor CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.opcyclesFunctor HomologicalComplex.natTransHomologyι	—	CategoryTheory.categoryWithHomology_of_abelian
snakeInput_v₁₂ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms ComplexShape.Rel	CategoryTheory.ShortComplex.SnakeInput.v₁₂ snakeInput CategoryTheory.ShortComplex.mapNatTrans HomologicalComplex.opcyclesFunctor CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.cyclesFunctor HomologicalComplex.natTransOpCyclesToCycles	—	CategoryTheory.categoryWithHomology_of_abelian
snakeInput_v₂₃ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms ComplexShape.Rel	CategoryTheory.ShortComplex.SnakeInput.v₂₃ snakeInput CategoryTheory.ShortComplex.mapNatTrans HomologicalComplex.cyclesFunctor CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.homologyFunctor HomologicalComplex.natTransHomologyπ	—	CategoryTheory.categoryWithHomology_of_abelian

---

← Back to Index