Documentation Verification Report

HomologySequenceLemmas

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

Statistics

Metric	Count
Definitions `composableArrows₂`, `composableArrows₅`, `mapComposableArrows₂`, `mapComposableArrows₅`, `mapSnakeInput`	5
Theorems `composableArrows₂_exact`, `composableArrows₅_exact`, `epi_homologyMap_τ₃`, `isIso_homologyMap_τ₃`, `mapSnakeInput_f₀`, `mapSnakeInput_f₁`, `mapSnakeInput_f₂`, `mapSnakeInput_f₃`, `mono_homologyMap_τ₃`, `quasiIso_τ₃`, `δ_naturality`, `δ_naturality_assoc`	12
Total	17

HomologicalComplex.HomologySequence

Definitions

Name	Category	Theorems
`composableArrows₂` 📖	CompOp	1 math math: `composableArrows₂_exact`
`composableArrows₅` 📖	CompOp	1 math math: `composableArrows₅_exact`
`mapComposableArrows₂` 📖	CompOp	—
`mapComposableArrows₅` 📖	CompOp	—
`mapSnakeInput` 📖	CompOp	4 math math: `mapSnakeInput_f₃`, `mapSnakeInput_f₁`, `mapSnakeInput_f₂`, `mapSnakeInput_f₀`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`composableArrows₂_exact` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `HomologicalComplex.instCategory` `HomologicalComplex.instHasZeroMorphisms`	`CategoryTheory.ComposableArrows.Exact` `composableArrows₂`	—	`CategoryTheory.ShortComplex.Exact.exact_toComposableArrows` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.ShortComplex.ShortExact.homology_exact₂`
`composableArrows₅_exact` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `HomologicalComplex.instCategory` `HomologicalComplex.instHasZeroMorphisms` `ComplexShape.Rel`	`CategoryTheory.ComposableArrows.Exact` `composableArrows₅`	—	`CategoryTheory.ComposableArrows.exact_of_δ₀` `CategoryTheory.ShortComplex.Exact.exact_toComposableArrows` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.ShortComplex.ShortExact.homology_exact₂` `CategoryTheory.ShortComplex.ShortExact.comp_δ` `CategoryTheory.ShortComplex.ShortExact.homology_exact₃` `CategoryTheory.ShortComplex.ShortExact.δ_comp` `CategoryTheory.ShortComplex.ShortExact.homology_exact₁`
`epi_homologyMap_τ₃` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `HomologicalComplex.instCategory` `HomologicalComplex.instHasZeroMorphisms` `CategoryTheory.Epi` `HomologicalComplex.homology` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `HomologicalComplex.sc` `HomologicalComplex.homologyMap` `CategoryTheory.ShortComplex.Hom.τ₁` `CategoryTheory.Mono` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.ShortComplex.Hom.τ₂`	`CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.Hom.τ₃`	—	`CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.Abelian.epi_of_epi_of_epi_of_mono` `CategoryTheory.ComposableArrows.Exact.δlast` `CategoryTheory.ComposableArrows.Exact.δ₀` `composableArrows₅_exact` `CategoryTheory.ShortComplex.ShortExact.epi_g` `CategoryTheory.Functor.congr_map` `CategoryTheory.ShortComplex.Hom.comm₂₃` `HomologicalComplex.epi_homologyMap_of_epi_of_not_rel` `HomologicalComplex.instEpiFOfHasFiniteColimits` `CategoryTheory.Abelian.hasFiniteColimits` `CategoryTheory.epi_of_epi_fac` `CategoryTheory.epi_comp` `HomologicalComplex.homologyMap_comp`
`isIso_homologyMap_τ₃` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `HomologicalComplex.instCategory` `HomologicalComplex.instHasZeroMorphisms` `CategoryTheory.IsIso` `HomologicalComplex.homology` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `HomologicalComplex.sc` `HomologicalComplex.homologyMap` `CategoryTheory.ShortComplex.Hom.τ₁` `CategoryTheory.Mono` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.ShortComplex.Hom.τ₂`	`CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.Hom.τ₃`	—	`CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `mono_homologyMap_τ₃` `CategoryTheory.IsIso.mono_of_iso` `CategoryTheory.mono_of_strongMono` `CategoryTheory.instStrongMonoOfIsRegularMono` `CategoryTheory.instIsRegularMonoOfIsSplitMono` `CategoryTheory.IsSplitMono.of_iso` `epi_homologyMap_τ₃` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.isIso_of_mono_of_epi` `CategoryTheory.balanced_of_strongMonoCategory` `CategoryTheory.strongMonoCategory_of_regularMonoCategory` `CategoryTheory.regularMonoCategoryOfNormalMonoCategory` `CategoryTheory.Abelian.toIsNormalMonoCategory`
`mapSnakeInput_f₀` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `HomologicalComplex.instCategory` `HomologicalComplex.instHasZeroMorphisms` `ComplexShape.Rel`	`CategoryTheory.ShortComplex.SnakeInput.Hom.f₀` `snakeInput` `mapSnakeInput` `CategoryTheory.Functor.map` `CategoryTheory.ShortComplex` `CategoryTheory.ShortComplex.instCategory` `CategoryTheory.Functor.mapShortComplex` `HomologicalComplex.homologyFunctor` `CategoryTheory.categoryWithHomology_of_abelian`	—	`CategoryTheory.categoryWithHomology_of_abelian`
`mapSnakeInput_f₁` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `HomologicalComplex.instCategory` `HomologicalComplex.instHasZeroMorphisms` `ComplexShape.Rel`	`CategoryTheory.ShortComplex.SnakeInput.Hom.f₁` `snakeInput` `mapSnakeInput` `CategoryTheory.Functor.map` `CategoryTheory.ShortComplex` `CategoryTheory.ShortComplex.instCategory` `CategoryTheory.Functor.mapShortComplex` `HomologicalComplex.opcyclesFunctor` `CategoryTheory.categoryWithHomology_of_abelian`	—	`CategoryTheory.categoryWithHomology_of_abelian`
`mapSnakeInput_f₂` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `HomologicalComplex.instCategory` `HomologicalComplex.instHasZeroMorphisms` `ComplexShape.Rel`	`CategoryTheory.ShortComplex.SnakeInput.Hom.f₂` `snakeInput` `mapSnakeInput` `CategoryTheory.Functor.map` `CategoryTheory.ShortComplex` `CategoryTheory.ShortComplex.instCategory` `CategoryTheory.Functor.mapShortComplex` `HomologicalComplex.cyclesFunctor` `CategoryTheory.categoryWithHomology_of_abelian`	—	`CategoryTheory.categoryWithHomology_of_abelian`
`mapSnakeInput_f₃` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `HomologicalComplex.instCategory` `HomologicalComplex.instHasZeroMorphisms` `ComplexShape.Rel`	`CategoryTheory.ShortComplex.SnakeInput.Hom.f₃` `snakeInput` `mapSnakeInput` `CategoryTheory.Functor.map` `CategoryTheory.ShortComplex` `CategoryTheory.ShortComplex.instCategory` `CategoryTheory.Functor.mapShortComplex` `HomologicalComplex.homologyFunctor` `CategoryTheory.categoryWithHomology_of_abelian`	—	`CategoryTheory.categoryWithHomology_of_abelian`
`mono_homologyMap_τ₃` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `HomologicalComplex.instCategory` `HomologicalComplex.instHasZeroMorphisms` `CategoryTheory.Mono` `HomologicalComplex.homology` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `HomologicalComplex.sc` `HomologicalComplex.homologyMap` `CategoryTheory.ShortComplex.Hom.τ₁`	`CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.Hom.τ₃`	—	`CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono` `CategoryTheory.ComposableArrows.Exact.δlast` `composableArrows₅_exact` `CategoryTheory.Abelian.mono_of_epi_of_epi_of_mono` `composableArrows₂_exact` `CategoryTheory.ShortComplex.ShortExact.epi_g` `HomologicalComplex.epi_homologyMap_of_epi_of_not_rel` `HomologicalComplex.instEpiFOfHasFiniteColimits` `CategoryTheory.Abelian.hasFiniteColimits`
`quasiIso_τ₃` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `HomologicalComplex.instCategory` `HomologicalComplex.instHasZeroMorphisms`	`QuasiIso` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.Hom.τ₃` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `HomologicalComplex.sc`	—	`CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `quasiIso_iff` `quasiIsoAt_iff_isIso_homologyMap` `isIso_homologyMap_τ₃` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `instIsIsoHomologyMapOfQuasiIsoAt` `QuasiIso.quasiIsoAt` `CategoryTheory.mono_of_strongMono` `CategoryTheory.instStrongMonoOfIsRegularMono` `CategoryTheory.instIsRegularMonoOfIsSplitMono` `CategoryTheory.IsSplitMono.of_iso`
`δ_naturality` 📖	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.ShortExact.δ` `HomologicalComplex.homologyMap` `CategoryTheory.ShortComplex.Hom.τ₁` `CategoryTheory.ShortComplex.Hom.τ₃`	—	`CategoryTheory.ShortComplex.SnakeInput.naturality_δ`
`δ_naturality_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.ShortExact.δ` `HomologicalComplex.homologyMap` `CategoryTheory.ShortComplex.Hom.τ₁` `CategoryTheory.ShortComplex.Hom.τ₃`	—	`CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `δ_naturality`

---

← Back to Index