TruncLEHomology

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

Statistics

Metric	Count
Definitions shortComplexTruncLE	1
Theorems acyclic_truncLE_iff_isSupportedOutside, epi_homologyMap_shortComplexTruncLE_g, instEpiGShortComplexTruncLE, instHasHomologyTruncLE, instMonoFShortComplexTruncLE, instQuasiIsoAtιTruncLEF, isIso_homologyMap_shortComplexTruncLE_g, mono_homologyMap_shortComplexTruncLE_g, quasiIsoAt_shortComplexTruncLE_g, quasiIsoAt_ιTruncLE, quasiIso_truncLEMap_iff, quasiIso_ιTruncLE_iff_isSupported, shortComplexTruncLE_X₁, shortComplexTruncLE_X₂, shortComplexTruncLE_X₃_isSupportedOutside, shortComplexTruncLE_f, shortComplexTruncLE_shortExact, shortComplexTruncLE_shortExact_δ_eq_zero, quasiIsoAt_truncLE'ToRestriction, truncLE'_hasHomology	20
Total	21

HomologicalComplex

Definitions

Name	Category	Theorems
shortComplexTruncLE 📖	CompOp	15 math math: instEpiGShortComplexTruncLE, instMonoFShortComplexTruncLE, isIso_homologyMap_shortComplexTruncLE_g, g_shortComplexTruncLEX₃ToTruncGE, mono_homologyMap_shortComplexTruncLE_g, quasiIsoAt_shortComplexTruncLE_g, shortComplexTruncLE_f, shortComplexTruncLE_shortExact, shortComplexTruncLE_X₂, epi_homologyMap_shortComplexTruncLE_g, shortComplexTruncLE_X₁, instQuasiIsoShortComplexTruncLEX₃ToTruncGE, shortComplexTruncLE_shortExact_δ_eq_zero, g_shortComplexTruncLEX₃ToTruncGE_assoc, shortComplexTruncLE_X₃_isSupportedOutside

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
acyclic_truncLE_iff_isSupportedOutside 📖	mathematical	HasHomology	Acyclic truncLE IsSupportedOutside	—	acyclic_op_iff isSupportedOutside_op_iff acyclic_truncGE_iff_isSupportedOutside ComplexShape.Embedding.instIsTruncGEOpOfIsTruncLE instHasHomologyOppositeOp CategoryTheory.Limits.hasZeroObject_op
epi_homologyMap_shortComplexTruncLE_g 📖	mathematical	—	CategoryTheory.Epi homology CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₂ HomologicalComplex instCategory instHasZeroMorphisms shortComplexTruncLE CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian sc CategoryTheory.ShortComplex.X₃ homologyMap CategoryTheory.ShortComplex.g	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.Exact.epi_f shortComplexTruncLE_shortExact CategoryTheory.ShortComplex.ShortExact.comp_δ CategoryTheory.ShortComplex.ShortExact.homology_exact₃ CategoryTheory.Abelian.hasZeroObject shortComplexTruncLE_shortExact_δ_eq_zero epi_homologyMap_of_epi_of_not_rel instEpiFOfHasFiniteColimits CategoryTheory.Abelian.hasFiniteColimits instEpiGShortComplexTruncLE
instEpiGShortComplexTruncLE 📖	mathematical	—	CategoryTheory.Epi HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive instCategory CategoryTheory.ShortComplex.X₂ instHasZeroMorphisms shortComplexTruncLE CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.Limits.coequalizer.π_epi
instHasHomologyTruncLE 📖	mathematical	HasHomology	truncLE	—	ComplexShape.Embedding.instIsTruncGEOpOfIsTruncLE instHasHomologyOppositeOp CategoryTheory.Limits.hasZeroObject_op instHasHomologyUnopOfOpposite truncGE.instHasHomology
instMonoFShortComplexTruncLE 📖	mathematical	—	CategoryTheory.Mono HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive instCategory CategoryTheory.ShortComplex.X₁ instHasZeroMorphisms shortComplexTruncLE CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f	—	CategoryTheory.Abelian.hasZeroObject instMonoιTruncLE
instQuasiIsoAtιTruncLEF 📖	mathematical	HasHomology	QuasiIsoAt truncLE ιTruncLE ComplexShape.Embedding.f instHasHomologyTruncLE	—	quasiIsoAt_ιTruncLE
isIso_homologyMap_shortComplexTruncLE_g 📖	mathematical	—	CategoryTheory.IsIso homology CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₂ HomologicalComplex instCategory instHasZeroMorphisms shortComplexTruncLE CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian sc CategoryTheory.ShortComplex.X₃ homologyMap CategoryTheory.ShortComplex.g	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian mono_homologyMap_shortComplexTruncLE_g CategoryTheory.isIso_of_mono_of_epi CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory epi_homologyMap_shortComplexTruncLE_g
mono_homologyMap_shortComplexTruncLE_g 📖	mathematical	—	CategoryTheory.Mono homology CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₂ HomologicalComplex instCategory instHasZeroMorphisms shortComplexTruncLE CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian sc CategoryTheory.ShortComplex.X₃ homologyMap CategoryTheory.ShortComplex.g	—	CategoryTheory.ShortComplex.Exact.mono_g CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.ShortExact.homology_exact₂ shortComplexTruncLE_shortExact CategoryTheory.Limits.IsZero.eq_of_src CategoryTheory.Abelian.hasZeroObject instHasHomologyTruncLE ExactAt.isZero_homology exactAt_of_isSupported instIsSupportedOfIsStrictlySupported instIsStrictlySupportedTruncLE
quasiIsoAt_shortComplexTruncLE_g 📖	mathematical	—	QuasiIsoAt CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₂ HomologicalComplex instCategory instHasZeroMorphisms shortComplexTruncLE CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian sc	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian quasiIsoAt_iff_isIso_homologyMap isIso_homologyMap_shortComplexTruncLE_g
quasiIsoAt_ιTruncLE 📖	mathematical	HasHomology ComplexShape.Embedding.f	QuasiIsoAt truncLE ιTruncLE instHasHomologyTruncLE	—	ComplexShape.Embedding.instIsTruncGEOpOfIsTruncLE instHasHomologyOppositeOp CategoryTheory.Limits.hasZeroObject_op truncGE.instHasHomology quasiIsoAt_πTruncGE instHasHomologyObjOppositeSymmUnopFunctorOp instQuasiIsoAtMapOppositeSymmUnopFunctorOp
quasiIso_truncLEMap_iff 📖	mathematical	HasHomology	QuasiIso truncLE truncLEMap instHasHomologyTruncLE QuasiIsoAt	—	instHasHomologyTruncLE instHasHomologyOppositeObjSymmOpFunctorOp quasiIso_opFunctor_map_iff quasiIsoAt_opFunctor_map_iff quasiIso_truncGEMap_iff ComplexShape.Embedding.instIsTruncGEOpOfIsTruncLE CategoryTheory.Limits.hasZeroObject_op
quasiIso_ιTruncLE_iff_isSupported 📖	mathematical	HasHomology	QuasiIso truncLE ιTruncLE instHasHomologyTruncLE IsSupported	—	instHasHomologyTruncLE instHasHomologyOppositeObjSymmOpFunctorOp quasiIso_opFunctor_map_iff isSupported_op_iff quasiIso_πTruncGE_iff_isSupported ComplexShape.Embedding.instIsTruncGEOpOfIsTruncLE instHasHomologyOppositeOp CategoryTheory.Limits.hasZeroObject_op
shortComplexTruncLE_X₁ 📖	mathematical	—	CategoryTheory.ShortComplex.X₁ HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive instCategory instHasZeroMorphisms shortComplexTruncLE truncLE CategoryTheory.Abelian.hasZeroObject	—	—
shortComplexTruncLE_X₂ 📖	mathematical	—	CategoryTheory.ShortComplex.X₂ HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive instCategory instHasZeroMorphisms shortComplexTruncLE	—	—
shortComplexTruncLE_X₃_isSupportedOutside 📖	mathematical	—	IsSupportedOutside CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₃ HomologicalComplex instCategory instHasZeroMorphisms shortComplexTruncLE	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian exactAt_iff_isZero_homology CategoryTheory.ShortComplex.Exact.isZero_X₂ shortComplexTruncLE_shortExact CategoryTheory.ShortComplex.ShortExact.comp_δ CategoryTheory.ShortComplex.ShortExact.homology_exact₃ CategoryTheory.Abelian.hasZeroObject instHasHomologyTruncLE CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso instIsIsoHomologyMapOfQuasiIsoAt instQuasiIsoAtιTruncLEF CategoryTheory.Limits.comp_zero homologyMap_comp CategoryTheory.Limits.cokernel.condition homologyMap_zero shortComplexTruncLE_shortExact_δ_eq_zero CategoryTheory.Limits.IsZero.iff_id_eq_zero epi_homologyMap_shortComplexTruncLE_g CategoryTheory.Category.comp_id CategoryTheory.ShortComplex.zero
shortComplexTruncLE_f 📖	mathematical	—	CategoryTheory.ShortComplex.f HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive instCategory instHasZeroMorphisms shortComplexTruncLE ιTruncLE CategoryTheory.Abelian.hasZeroObject	—	CategoryTheory.Abelian.hasZeroObject
shortComplexTruncLE_shortExact 📖	mathematical	—	CategoryTheory.ShortComplex.ShortExact HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive instCategory instHasZeroMorphisms shortComplexTruncLE	—	CategoryTheory.ShortComplex.exact_of_g_is_cokernel CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian instMonoFShortComplexTruncLE instEpiGShortComplexTruncLE
shortComplexTruncLE_shortExact_δ_eq_zero 📖	mathematical	ComplexShape.Rel	CategoryTheory.ShortComplex.ShortExact.δ shortComplexTruncLE shortComplexTruncLE_shortExact Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct homology CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₃ HomologicalComplex instCategory instHasZeroMorphisms CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian sc CategoryTheory.ShortComplex.X₁ CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian shortComplexTruncLE_shortExact CategoryTheory.Abelian.hasZeroObject instHasHomologyTruncLE CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso instIsIsoHomologyMapOfQuasiIsoAt instQuasiIsoAtιTruncLEF CategoryTheory.Limits.zero_comp CategoryTheory.ShortComplex.ShortExact.δ_comp CategoryTheory.Limits.IsZero.eq_of_tgt ExactAt.isZero_homology exactAt_of_isSupported instIsSupportedOfIsStrictlySupported instIsStrictlySupportedTruncLE

HomologicalComplex.truncLE'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quasiIsoAt_truncLE'ToRestriction 📖	mathematical	HomologicalComplex.HasHomology ComplexShape.Embedding.BoundaryLE	QuasiIsoAt HomologicalComplex.truncLE' HomologicalComplex.restriction ComplexShape.Embedding.IsTruncLE.toIsRelIff HomologicalComplex.truncLE'ToRestriction	—	ComplexShape.Embedding.IsTruncLE.toIsRelIff ComplexShape.Embedding.instIsRelIffOp HomologicalComplex.instHasHomologyOppositeOp ComplexShape.Embedding.instIsTruncGEOpOfIsTruncLE HomologicalComplex.truncGE'.truncGE'_hasHomology HomologicalComplex.instHasHomologyObjOppositeSymmUnopFunctorOp HomologicalComplex.quasiIsoAt_unopFunctor_map_iff HomologicalComplex.truncGE'.quasiIsoAt_restrictionToTruncGE'
truncLE'_hasHomology 📖	mathematical	HomologicalComplex.HasHomology	HomologicalComplex.truncLE'	—	ComplexShape.Embedding.instIsTruncGEOpOfIsTruncLE HomologicalComplex.instHasHomologyOppositeOp HomologicalComplex.instHasHomologyUnopOfOpposite HomologicalComplex.truncGE'.truncGE'_hasHomology

---

← Back to Index