TruncLE

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

Statistics

Metric	Count
Definitions truncLE'Functor, truncLE'ToRestrictionNatTrans, truncLEFunctor, ιTruncLENatTrans, truncLE, truncLE', truncLE'Map, truncLE'ToRestriction, truncLE'XIso, truncLE'XIsoCycles, truncLEIso, truncLEMap, truncLEXIso, truncLEXIsoCycles, ιTruncLE	15
Theorems truncLE'Functor_map, truncLE'Functor_obj, truncLE'ToRestrictionNatTrans_app, truncLEFunctor_map, truncLEFunctor_obj, ιTruncLENatTrans_app, instIsIsoFTruncLE'ToRestrictionOfIsStrictlySupported, instIsIsoιTruncLEOfIsStrictlySupported, instIsStrictlySupportedTruncLE, instIsStrictlySupportedTruncLE_1, instMonoFTruncLE'ToRestriction, instMonoFιTruncLE, instMonoιTruncLE, isIso_truncLE'ToRestriction, isIso_ιTruncLE_iff, truncLE'Map_comp, truncLE'Map_comp_assoc, truncLE'Map_f_eq, truncLE'Map_f_eq_cyclesMap, truncLE'Map_id, truncLE'ToRestriction_naturality, truncLE'ToRestriction_naturality_assoc, truncLE'_d_eq, truncLE'_d_eq_toCycles, truncLEMap_comp, truncLEMap_comp_assoc, truncLEMap_id, ιTruncLE_naturality, ιTruncLE_naturality_assoc	29
Total	44

ComplexShape.Embedding

Definitions

Name	Category	Theorems
truncLE'Functor 📖	CompOp	3 math math: truncLE'Functor_map, truncLE'Functor_obj, truncLE'ToRestrictionNatTrans_app
truncLE'ToRestrictionNatTrans 📖	CompOp	1 math math: truncLE'ToRestrictionNatTrans_app
truncLEFunctor 📖	CompOp	3 math math: truncLEFunctor_obj, ιTruncLENatTrans_app, truncLEFunctor_map
ιTruncLENatTrans 📖	CompOp	1 math math: ιTruncLENatTrans_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
truncLE'Functor_map 📖	mathematical	—	CategoryTheory.Functor.map HomologicalComplex HomologicalComplex.instCategory truncLE'Functor HomologicalComplex.truncLE'Map	—	—
truncLE'Functor_obj 📖	mathematical	—	CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory truncLE'Functor HomologicalComplex.truncLE'	—	—
truncLE'ToRestrictionNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app HomologicalComplex HomologicalComplex.instCategory truncLE'Functor restrictionFunctor IsTruncLE.toIsRelIff truncLE'ToRestrictionNatTrans HomologicalComplex.truncLE'ToRestriction	—	IsTruncLE.toIsRelIff
truncLEFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map HomologicalComplex HomologicalComplex.instCategory truncLEFunctor HomologicalComplex.truncLEMap	—	—
truncLEFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory truncLEFunctor HomologicalComplex.truncLE	—	—
ιTruncLENatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app HomologicalComplex HomologicalComplex.instCategory truncLEFunctor CategoryTheory.Functor.id ιTruncLENatTrans HomologicalComplex.ιTruncLE	—	—

HomologicalComplex

Definitions

Name	Category	Theorems
truncLE 📖	CompOp	19 math math: ComplexShape.Embedding.truncLEFunctor_obj, truncLEMap_comp_assoc, ιTruncLE_naturality, instQuasiIsoAtιTruncLEF, instMonoFιTruncLE, ιTruncLE_naturality_assoc, truncLEMap_comp, isIso_ιTruncLE_iff, instHasHomologyTruncLE, instIsStrictlySupportedTruncLE_1, instMonoιTruncLE, quasiIso_ιTruncLE_iff_isSupported, truncLEMap_id, quasiIsoAt_ιTruncLE, instIsIsoιTruncLEOfIsStrictlySupported, instIsStrictlySupportedTruncLE, shortComplexTruncLE_X₁, acyclic_truncLE_iff_isSupportedOutside, quasiIso_truncLEMap_iff
truncLE' 📖	CompOp	15 math math: truncLE'_d_eq_toCycles, instMonoFTruncLE'ToRestriction, truncLE'.quasiIsoAt_truncLE'ToRestriction, truncLE'Map_f_eq_cyclesMap, truncLE'Map_id, isIso_truncLE'ToRestriction, truncLE'.truncLE'_hasHomology, truncLE'_d_eq, truncLE'ToRestriction_naturality_assoc, ComplexShape.Embedding.truncLE'Functor_obj, instIsIsoFTruncLE'ToRestrictionOfIsStrictlySupported, truncLE'Map_comp, truncLE'Map_comp_assoc, truncLE'Map_f_eq, truncLE'ToRestriction_naturality
truncLE'Map 📖	CompOp	8 math math: truncLE'Map_f_eq_cyclesMap, truncLE'Map_id, truncLE'ToRestriction_naturality_assoc, ComplexShape.Embedding.truncLE'Functor_map, truncLE'Map_comp, truncLE'Map_comp_assoc, truncLE'Map_f_eq, truncLE'ToRestriction_naturality
truncLE'ToRestriction 📖	CompOp	7 math math: instMonoFTruncLE'ToRestriction, truncLE'.quasiIsoAt_truncLE'ToRestriction, isIso_truncLE'ToRestriction, truncLE'ToRestriction_naturality_assoc, instIsIsoFTruncLE'ToRestrictionOfIsStrictlySupported, ComplexShape.Embedding.truncLE'ToRestrictionNatTrans_app, truncLE'ToRestriction_naturality
truncLE'XIso 📖	CompOp	3 math math: truncLE'_d_eq_toCycles, truncLE'_d_eq, truncLE'Map_f_eq
truncLE'XIsoCycles 📖	CompOp	2 math math: truncLE'_d_eq_toCycles, truncLE'Map_f_eq_cyclesMap
truncLEIso 📖	CompOp	—
truncLEMap 📖	CompOp	7 math math: truncLEMap_comp_assoc, ιTruncLE_naturality, ιTruncLE_naturality_assoc, truncLEMap_comp, truncLEMap_id, ComplexShape.Embedding.truncLEFunctor_map, quasiIso_truncLEMap_iff
truncLEXIso 📖	CompOp	—
truncLEXIsoCycles 📖	CompOp	—
ιTruncLE 📖	CompOp	11 math math: ιTruncLE_naturality, instQuasiIsoAtιTruncLEF, instMonoFιTruncLE, ιTruncLE_naturality_assoc, isIso_ιTruncLE_iff, shortComplexTruncLE_f, ComplexShape.Embedding.ιTruncLENatTrans_app, instMonoιTruncLE, quasiIso_ιTruncLE_iff_isSupported, quasiIsoAt_ιTruncLE, instIsIsoιTruncLEOfIsStrictlySupported

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsIsoFTruncLE'ToRestrictionOfIsStrictlySupported 📖	mathematical	HasHomology	CategoryTheory.IsIso X truncLE' restriction ComplexShape.Embedding.IsTruncLE.toIsRelIff Hom.f truncLE'ToRestriction	—	ComplexShape.Embedding.instIsTruncGEOpOfIsTruncLE instHasHomologyOppositeOp ComplexShape.Embedding.IsTruncGE.toIsRelIff CategoryTheory.isIso_unop instIsIsoFRestrictionToTruncGE'OfIsStrictlySupported instIsStrictlySupportedOppositeOpOp
instIsIsoιTruncLEOfIsStrictlySupported 📖	mathematical	HasHomology	CategoryTheory.IsIso HomologicalComplex instCategory truncLE ιTruncLE	—	ComplexShape.Embedding.instIsTruncGEOpOfIsTruncLE instHasHomologyOppositeOp CategoryTheory.Limits.hasZeroObject_op CategoryTheory.Functor.map_isIso CategoryTheory.isIso_op instIsIsoπTruncGEOfIsStrictlySupported instIsStrictlySupportedOppositeOpOp
instIsStrictlySupportedTruncLE 📖	mathematical	HasHomology	IsStrictlySupported truncLE	—	isStrictlySupported_op_iff ComplexShape.Embedding.instIsTruncGEOpOfIsTruncLE instHasHomologyOppositeOp CategoryTheory.Limits.hasZeroObject_op instIsStrictlySupportedTruncGE
instIsStrictlySupportedTruncLE_1 📖	mathematical	HasHomology	IsStrictlySupported truncLE	—	isStrictlySupported_op_iff ComplexShape.Embedding.instIsTruncGEOpOfIsTruncLE instHasHomologyOppositeOp CategoryTheory.Limits.hasZeroObject_op instIsStrictlySupportedTruncGE_1 instIsStrictlySupportedOppositeOpOp
instMonoFTruncLE'ToRestriction 📖	mathematical	HasHomology	CategoryTheory.Mono X truncLE' restriction ComplexShape.Embedding.IsTruncLE.toIsRelIff Hom.f truncLE'ToRestriction	—	ComplexShape.Embedding.instIsTruncGEOpOfIsTruncLE instHasHomologyOppositeOp ComplexShape.Embedding.IsTruncGE.toIsRelIff CategoryTheory.unop_mono_of_epi instEpiFRestrictionToTruncGE'
instMonoFιTruncLE 📖	mathematical	HasHomology	CategoryTheory.Mono X truncLE Hom.f ιTruncLE	—	ComplexShape.Embedding.instIsTruncGEOpOfIsTruncLE instHasHomologyOppositeOp CategoryTheory.Limits.hasZeroObject_op CategoryTheory.unop_mono_of_epi instEpiFπTruncGE
instMonoιTruncLE 📖	mathematical	HasHomology	CategoryTheory.Mono HomologicalComplex instCategory truncLE ιTruncLE	—	mono_of_mono_f instMonoFιTruncLE
isIso_truncLE'ToRestriction 📖	mathematical	HasHomology ComplexShape.Embedding.BoundaryLE	CategoryTheory.IsIso X truncLE' restriction ComplexShape.Embedding.IsTruncLE.toIsRelIff Hom.f truncLE'ToRestriction	—	ComplexShape.Embedding.IsTruncLE.toIsRelIff ComplexShape.Embedding.IsTruncGE.toIsRelIff ComplexShape.Embedding.instIsTruncGEOpOfIsTruncLE instHasHomologyOppositeOp isIso_restrictionToTruncGE' CategoryTheory.isIso_unop
isIso_ιTruncLE_iff 📖	mathematical	HasHomology	CategoryTheory.IsIso HomologicalComplex instCategory truncLE ιTruncLE IsStrictlySupported	—	isStrictlySupported_of_iso instIsStrictlySupportedTruncLE instIsIsoιTruncLEOfIsStrictlySupported
truncLE'Map_comp 📖	mathematical	HasHomology	truncLE'Map CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory truncLE'	—	CategoryTheory.Functor.congr_map ComplexShape.Embedding.instIsTruncGEOpOfIsTruncLE instHasHomologyOppositeObjSymmOpFunctorOp truncGE'Map_comp
truncLE'Map_comp_assoc 📖	mathematical	HasHomology	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory truncLE' truncLE'Map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' truncLE'Map_comp
truncLE'Map_f_eq 📖	mathematical	HasHomology ComplexShape.Embedding.BoundaryLE ComplexShape.Embedding.f	Hom.f truncLE' truncLE'Map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.hom truncLE'XIso CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc truncGE'Map_f_eq ComplexShape.Embedding.instIsTruncGEOpOfIsTruncLE instHasHomologyOppositeObjSymmOpFunctorOp
truncLE'Map_f_eq_cyclesMap 📖	mathematical	HasHomology ComplexShape.Embedding.BoundaryLE ComplexShape.Embedding.f	Hom.f truncLE' truncLE'Map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X cycles CategoryTheory.Iso.hom truncLE'XIsoCycles cyclesMap CategoryTheory.Iso.inv	—	ComplexShape.Embedding.instIsTruncGEOpOfIsTruncLE CategoryTheory.Category.assoc truncGE'Map_f_eq_opcyclesMap instHasHomologyOppositeOp instHasHomologyOppositeObjSymmOpFunctorOp opcyclesOpIso_inv_naturality_assoc CategoryTheory.Iso.hom_inv_id_assoc
truncLE'Map_id 📖	mathematical	HasHomology	truncLE'Map CategoryTheory.CategoryStruct.id HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory truncLE'	—	CategoryTheory.Functor.congr_map ComplexShape.Embedding.instIsTruncGEOpOfIsTruncLE instHasHomologyOppositeOp truncGE'Map_id
truncLE'ToRestriction_naturality 📖	mathematical	HasHomology	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory truncLE' restriction ComplexShape.Embedding.IsTruncLE.toIsRelIff truncLE'Map truncLE'ToRestriction restrictionMap	—	CategoryTheory.Functor.congr_map ComplexShape.Embedding.instIsTruncGEOpOfIsTruncLE instHasHomologyOppositeObjSymmOpFunctorOp ComplexShape.Embedding.IsTruncGE.toIsRelIff restrictionToTruncGE'_naturality
truncLE'ToRestriction_naturality_assoc 📖	mathematical	HasHomology	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory truncLE' truncLE'Map restriction ComplexShape.Embedding.IsTruncLE.toIsRelIff truncLE'ToRestriction restrictionMap	—	ComplexShape.Embedding.IsTruncLE.toIsRelIff CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' truncLE'ToRestriction_naturality
truncLE'_d_eq 📖	mathematical	HasHomology ComplexShape.Rel ComplexShape.Embedding.f ComplexShape.Embedding.BoundaryLE	d truncLE' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.hom truncLE'XIso ComplexShape.Embedding.not_boundaryLE_prev ComplexShape.Embedding.IsTruncLE.toIsRelIff CategoryTheory.Iso.inv	—	ComplexShape.Embedding.not_boundaryLE_prev ComplexShape.Embedding.IsTruncLE.toIsRelIff CategoryTheory.Category.assoc truncGE'_d_eq ComplexShape.Embedding.instIsTruncGEOpOfIsTruncLE instHasHomologyOppositeOp
truncLE'_d_eq_toCycles 📖	mathematical	HasHomology ComplexShape.Rel ComplexShape.Embedding.f ComplexShape.Embedding.BoundaryLE	d truncLE' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.hom truncLE'XIso ComplexShape.Embedding.not_boundaryLE_prev ComplexShape.Embedding.IsTruncLE.toIsRelIff cycles toCycles CategoryTheory.Iso.inv truncLE'XIsoCycles	—	ComplexShape.Embedding.not_boundaryLE_prev ComplexShape.Embedding.IsTruncLE.toIsRelIff ComplexShape.Embedding.instIsTruncGEOpOfIsTruncLE instHasHomologyOppositeOp CategoryTheory.Category.assoc opcyclesOpIso_hom_toCycles_op truncGE'_d_eq_fromOpcycles
truncLEMap_comp 📖	mathematical	HasHomology	truncLEMap CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory truncLE	—	CategoryTheory.Functor.congr_map ComplexShape.Embedding.instIsTruncGEOpOfIsTruncLE instHasHomologyOppositeObjSymmOpFunctorOp CategoryTheory.Limits.hasZeroObject_op truncGEMap_comp
truncLEMap_comp_assoc 📖	mathematical	HasHomology	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory truncLE truncLEMap	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' truncLEMap_comp
truncLEMap_id 📖	mathematical	HasHomology	truncLEMap CategoryTheory.CategoryStruct.id HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory truncLE	—	CategoryTheory.Functor.congr_map ComplexShape.Embedding.instIsTruncGEOpOfIsTruncLE instHasHomologyOppositeOp CategoryTheory.Limits.hasZeroObject_op truncGEMap_id
ιTruncLE_naturality 📖	mathematical	HasHomology	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory truncLE truncLEMap ιTruncLE	—	CategoryTheory.Functor.congr_map ComplexShape.Embedding.instIsTruncGEOpOfIsTruncLE instHasHomologyOppositeObjSymmOpFunctorOp CategoryTheory.Limits.hasZeroObject_op πTruncGE_naturality
ιTruncLE_naturality_assoc 📖	mathematical	HasHomology	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory truncLE truncLEMap ιTruncLE	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ιTruncLE_naturality

---

← Back to Index