Documentation Verification Report

TruncGEHomology

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

Statistics

Metric	Count
Definitions `homologyData`, `isLimitKernelFork`, `rightHomologyMapData`	3
Theorems `acyclic_truncGE_iff_isSupportedOutside`, `instQuasiIsoAtπTruncGEF`, `quasiIsoAt_πTruncGE`, `quasiIso_truncGEMap_iff`, `quasiIso_πTruncGE_iff_isSupported`, `hasHomology_of_not_mem_boundary`, `hasHomology_sc'_of_not_mem_boundary`, `homologyData_right_g'`, `homologyι_truncGE'XIsoOpcycles_inv_d`, `quasiIsoAt_restrictionToTruncGE'`, `truncGE'_hasHomology`, `instHasHomology`, `rightHomologyMapData_φH`, `rightHomologyMapData_φQ`	14
Total	17

HomologicalComplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`acyclic_truncGE_iff_isSupportedOutside` 📖	mathematical	`HasHomology`	`Acyclic` `truncGE` `IsSupportedOutside`	—	`exactAt_iff_of_quasiIsoAt` `truncGE.instHasHomology` `instQuasiIsoAtπTruncGEF` `IsSupportedOutside.exactAt` `exactAt_of_isSupported` `instIsSupportedOfIsStrictlySupported` `instIsStrictlySupportedTruncGE`
`instQuasiIsoAtπTruncGEF` 📖	mathematical	`HasHomology`	`QuasiIsoAt` `truncGE` `πTruncGE` `ComplexShape.Embedding.f` `truncGE.instHasHomology`	—	`quasiIsoAt_πTruncGE`
`quasiIsoAt_πTruncGE` 📖	mathematical	`HasHomology` `ComplexShape.Embedding.f`	`QuasiIsoAt` `truncGE` `πTruncGE` `truncGE.instHasHomology`	—	`truncGE.instHasHomology` `quasiIsoAt_iff` `CategoryTheory.ShortComplex.RightHomologyMapData.quasiIso_iff` `CategoryTheory.IsIso.id` `ComplexShape.Embedding.IsTruncGE.toIsRelIff` `restrictionToTruncGE'_hasLift` `ComplexShape.Embedding.epi_liftExtend_f_iff` `instEpiFRestrictionToTruncGE'` `CategoryTheory.Limits.IsZero.epi` `isZero_extend_X` `ComplexShape.Embedding.isIso_liftExtend_f_iff` `isIso_restrictionToTruncGE'` `ComplexShape.Embedding.next_f` `ComplexShape.Embedding.not_boundaryGE_next'` `CategoryTheory.ShortComplex.quasiIso_of_epi_of_isIso_of_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.instStrongMonoOfIsRegularMono` `CategoryTheory.instIsRegularMonoOfIsSplitMono` `CategoryTheory.IsSplitMono.of_iso`
`quasiIso_truncGEMap_iff` 📖	mathematical	`HasHomology`	`QuasiIso` `truncGE` `truncGEMap` `truncGE.instHasHomology` `QuasiIsoAt`	—	`truncGE.instHasHomology` `quasiIsoAt_iff_comp_left` `instQuasiIsoAtπTruncGEF` `πTruncGE_naturality` `quasiIsoAt_iff_comp_right` `quasiIso_iff` `quasiIsoAt_iff_exactAt` `exactAt_of_isSupported` `instIsSupportedOfIsStrictlySupported` `instIsStrictlySupportedTruncGE`
`quasiIso_πTruncGE_iff_isSupported` 📖	mathematical	`HasHomology`	`QuasiIso` `truncGE` `πTruncGE` `truncGE.instHasHomology` `IsSupported`	—	`truncGE.instHasHomology` `exactAt_iff_of_quasiIsoAt` `QuasiIso.quasiIsoAt` `exactAt_of_isSupported` `instIsSupportedOfIsStrictlySupported` `instIsStrictlySupportedTruncGE` `quasiIso_iff` `instQuasiIsoAtπTruncGEF` `quasiIsoAt_iff_exactAt`

HomologicalComplex.truncGE

Definitions

Name	Category	Theorems
`rightHomologyMapData` 📖	CompOp	2 math math: `rightHomologyMapData_φQ`, `rightHomologyMapData_φH`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasHomology` 📖	mathematical	`HomologicalComplex.HasHomology`	`HomologicalComplex.truncGE`	—	`HomologicalComplex.extend.instHasHomology` `HomologicalComplex.truncGE'.truncGE'_hasHomology`
`rightHomologyMapData_φH` 📖	mathematical	`HomologicalComplex.HasHomology` `ComplexShape.Embedding.f` `ComplexShape.prev` `ComplexShape.next` `ComplexShape.Embedding.BoundaryGE`	`CategoryTheory.ShortComplex.RightHomologyMapData.φH` `CategoryTheory.Functor.obj` `HomologicalComplex` `HomologicalComplex.instCategory` `CategoryTheory.ShortComplex` `CategoryTheory.ShortComplex.instCategory` `HomologicalComplex.shortComplexFunctor` `HomologicalComplex.truncGE` `CategoryTheory.Functor.map` `HomologicalComplex.πTruncGE` `CategoryTheory.ShortComplex.RightHomologyData.canonical` `HomologicalComplex.sc` `HomologicalComplex.extend.rightHomologyData` `HomologicalComplex.truncGE'` `CategoryTheory.ShortComplex.HomologyData.right` `HomologicalComplex.sc'` `HomologicalComplex.truncGE'.homologyData` `rightHomologyMapData` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.RightHomologyData.H`	—	—
`rightHomologyMapData_φQ` 📖	mathematical	`HomologicalComplex.HasHomology` `ComplexShape.Embedding.f` `ComplexShape.prev` `ComplexShape.next` `ComplexShape.Embedding.BoundaryGE`	`CategoryTheory.ShortComplex.RightHomologyMapData.φQ` `CategoryTheory.Functor.obj` `HomologicalComplex` `HomologicalComplex.instCategory` `CategoryTheory.ShortComplex` `CategoryTheory.ShortComplex.instCategory` `HomologicalComplex.shortComplexFunctor` `HomologicalComplex.truncGE` `CategoryTheory.Functor.map` `HomologicalComplex.πTruncGE` `CategoryTheory.ShortComplex.RightHomologyData.canonical` `HomologicalComplex.sc` `HomologicalComplex.extend.rightHomologyData` `HomologicalComplex.truncGE'` `CategoryTheory.ShortComplex.HomologyData.right` `HomologicalComplex.sc'` `HomologicalComplex.truncGE'.homologyData` `rightHomologyMapData` `CategoryTheory.Iso.inv` `HomologicalComplex.X` `HomologicalComplex.opcycles` `HomologicalComplex.truncGE'XIsoOpcycles`	—	—

HomologicalComplex.truncGE'

Definitions

Name	Category	Theorems
`homologyData` 📖	CompOp	3 math math: `HomologicalComplex.truncGE.rightHomologyMapData_φQ`, `homologyData_right_g'`, `HomologicalComplex.truncGE.rightHomologyMapData_φH`
`isLimitKernelFork` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasHomology_of_not_mem_boundary` 📖	mathematical	`HomologicalComplex.HasHomology` `ComplexShape.Embedding.BoundaryGE`	`HomologicalComplex.truncGE'`	—	`hasHomology_sc'_of_not_mem_boundary`
`hasHomology_sc'_of_not_mem_boundary` 📖	mathematical	`HomologicalComplex.HasHomology` `ComplexShape.prev` `ComplexShape.next` `ComplexShape.Embedding.BoundaryGE`	`CategoryTheory.ShortComplex.HasHomology` `HomologicalComplex.sc'` `HomologicalComplex.truncGE'`	—	`ComplexShape.Embedding.IsTruncGE.toIsRelIff` `HomologicalComplex.restriction.hasHomology` `ComplexShape.Embedding.prev_f_of_not_boundaryGE` `ComplexShape.Embedding.next_f` `CategoryTheory.ShortComplex.hasHomology_of_iso` `HomologicalComplex.instEpiFRestrictionToTruncGE'` `HomologicalComplex.isIso_restrictionToTruncGE'` `ComplexShape.Embedding.not_boundaryGE_next'` `CategoryTheory.ShortComplex.hasHomology_of_epi_of_isIso_of_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.instStrongMonoOfIsRegularMono` `CategoryTheory.instIsRegularMonoOfIsSplitMono` `CategoryTheory.IsSplitMono.of_iso`
`homologyData_right_g'` 📖	mathematical	`HomologicalComplex.HasHomology` `ComplexShape.next` `ComplexShape.Embedding.f` `ComplexShape.Embedding.BoundaryGE`	`CategoryTheory.ShortComplex.RightHomologyData.g'` `HomologicalComplex.sc'` `HomologicalComplex.truncGE'` `CategoryTheory.ShortComplex.HomologyData.right` `homologyData` `HomologicalComplex.d`	—	—
`homologyι_truncGE'XIsoOpcycles_inv_d` 📖	mathematical	`HomologicalComplex.HasHomology` `ComplexShape.Embedding.f` `ComplexShape.Embedding.BoundaryGE`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.homology` `HomologicalComplex.X` `HomologicalComplex.truncGE'` `HomologicalComplex.opcycles` `HomologicalComplex.homologyι` `CategoryTheory.Iso.inv` `HomologicalComplex.truncGE'XIsoOpcycles` `HomologicalComplex.d` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`ComplexShape.Embedding.not_boundaryGE_next` `ComplexShape.Embedding.IsTruncGE.toIsRelIff` `HomologicalComplex.truncGE'_d_eq_fromOpcycles` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id_assoc` `HomologicalComplex.homologyι_comp_fromOpcycles_assoc` `CategoryTheory.Limits.zero_comp` `HomologicalComplex.shape` `CategoryTheory.Limits.comp_zero`
`quasiIsoAt_restrictionToTruncGE'` 📖	mathematical	`HomologicalComplex.HasHomology` `ComplexShape.Embedding.BoundaryGE`	`QuasiIsoAt` `HomologicalComplex.restriction` `ComplexShape.Embedding.IsTruncGE.toIsRelIff` `HomologicalComplex.truncGE'` `HomologicalComplex.restrictionToTruncGE'`	—	`ComplexShape.Embedding.IsTruncGE.toIsRelIff` `quasiIsoAt_iff` `HomologicalComplex.instEpiFRestrictionToTruncGE'` `HomologicalComplex.isIso_restrictionToTruncGE'` `ComplexShape.Embedding.not_boundaryGE_next'` `CategoryTheory.ShortComplex.quasiIso_of_epi_of_isIso_of_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.instStrongMonoOfIsRegularMono` `CategoryTheory.instIsRegularMonoOfIsSplitMono` `CategoryTheory.IsSplitMono.of_iso`
`truncGE'_hasHomology` 📖	mathematical	`HomologicalComplex.HasHomology`	`HomologicalComplex.truncGE'`	—	`CategoryTheory.ShortComplex.HasHomology.mk'` `hasHomology_of_not_mem_boundary`

---

← Back to Index