TruncGE

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

Statistics

Metric	Count
Definitions restrictionToTruncGE'NatTrans, truncGE'Functor, truncGEFunctor, πTruncGENatTrans, restrictionToTruncGE', f, truncGE, truncGE', X, XIso, XIsoOpcycles, d, truncGE'Map, truncGE'XIso, truncGE'XIsoOpcycles, truncGEMap, truncGEXIso, truncGEXIsoOpcycles, πTruncGE	19
Theorems restrictionToTruncGE'NatTrans_app, truncGE'Functor_map, truncGE'Functor_obj, truncGEFunctor_map, truncGEFunctor_obj, πTruncGENatTrans_app, instEpiFRestrictionToTruncGE', instEpiFπTruncGE, instEpiπTruncGE, instIsIsoFRestrictionToTruncGE'OfIsStrictlySupported, instIsIsoπTruncGEOfIsStrictlySupported, instIsStrictlySupportedTruncGE, instIsStrictlySupportedTruncGE_1, isIso_restrictionToTruncGE', isIso_πTruncGE_iff, comm, comm_assoc, f_eq_iso_hom_iso_inv, f_eq_iso_hom_pOpcycles_iso_inv, restrictionToTruncGE'_f_eq_iso_hom_iso_inv, restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv, restrictionToTruncGE'_hasLift, restrictionToTruncGE'_naturality, restrictionToTruncGE'_naturality_assoc, d_comp_d, d_comp_d_assoc, truncGE'Map_comp, truncGE'Map_comp_assoc, truncGE'Map_f_eq, truncGE'Map_f_eq_opcyclesMap, truncGE'Map_id, truncGE'_d_eq, truncGE'_d_eq_fromOpcycles, truncGEMap_comp, truncGEMap_comp_assoc, truncGEMap_id, πTruncGE_naturality, πTruncGE_naturality_assoc	38
Total	57

ComplexShape.Embedding

Definitions

Name	Category	Theorems
restrictionToTruncGE'NatTrans 📖	CompOp	1 math math: restrictionToTruncGE'NatTrans_app
truncGE'Functor 📖	CompOp	3 math math: truncGE'Functor_obj, truncGE'Functor_map, restrictionToTruncGE'NatTrans_app
truncGEFunctor 📖	CompOp	3 math math: πTruncGENatTrans_app, truncGEFunctor_map, truncGEFunctor_obj
πTruncGENatTrans 📖	CompOp	1 math math: πTruncGENatTrans_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrictionToTruncGE'NatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app HomologicalComplex HomologicalComplex.instCategory restrictionFunctor IsTruncGE.toIsRelIff truncGE'Functor restrictionToTruncGE'NatTrans HomologicalComplex.restrictionToTruncGE'	—	IsTruncGE.toIsRelIff
truncGE'Functor_map 📖	mathematical	—	CategoryTheory.Functor.map HomologicalComplex HomologicalComplex.instCategory truncGE'Functor HomologicalComplex.truncGE'Map	—	—
truncGE'Functor_obj 📖	mathematical	—	CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory truncGE'Functor HomologicalComplex.truncGE'	—	—
truncGEFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map HomologicalComplex HomologicalComplex.instCategory truncGEFunctor HomologicalComplex.truncGEMap	—	—
truncGEFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory truncGEFunctor HomologicalComplex.truncGE	—	—
πTruncGENatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app HomologicalComplex HomologicalComplex.instCategory CategoryTheory.Functor.id truncGEFunctor πTruncGENatTrans HomologicalComplex.πTruncGE	—	—

HomologicalComplex

Definitions

Name	Category	Theorems
restrictionToTruncGE' 📖	CompOp	10 math math: restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv, instIsIsoFRestrictionToTruncGE'OfIsStrictlySupported, truncGE'.quasiIsoAt_restrictionToTruncGE', restrictionToTruncGE'_naturality_assoc, restrictionToTruncGE'_naturality, ComplexShape.Embedding.restrictionToTruncGE'NatTrans_app, isIso_restrictionToTruncGE', restrictionToTruncGE'_f_eq_iso_hom_iso_inv, instEpiFRestrictionToTruncGE', restrictionToTruncGE'_hasLift
truncGE 📖	CompOp	23 math math: πTruncGE_naturality_assoc, truncGE.rightHomologyMapData_φQ, instIsStrictlySupportedTruncGE_1, instEpiFπTruncGE, truncGEMap_comp_assoc, quasiIso_πTruncGE_iff_isSupported, truncGE.instHasHomology, instIsIsoπTruncGEOfIsStrictlySupported, g_shortComplexTruncLEX₃ToTruncGE, quasiIsoAt_πTruncGE, isIso_πTruncGE_iff, πTruncGE_naturality, instIsStrictlySupportedTruncGE, truncGE.rightHomologyMapData_φH, acyclic_truncGE_iff_isSupportedOutside, quasiIso_truncGEMap_iff, instQuasiIsoShortComplexTruncLEX₃ToTruncGE, instEpiπTruncGE, truncGEMap_comp, g_shortComplexTruncLEX₃ToTruncGE_assoc, truncGEMap_id, instQuasiIsoAtπTruncGEF, ComplexShape.Embedding.truncGEFunctor_obj
truncGE' 📖	CompOp	28 math math: restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv, truncGE.rightHomologyMapData_φQ, truncGE'.truncGE'_hasHomology, ComplexShape.Embedding.truncGE'Functor_obj, truncGE'Map_comp, instIsIsoFRestrictionToTruncGE'OfIsStrictlySupported, restrictionToTruncGE'.comm_assoc, restrictionToTruncGE'.comm, truncGE'.hasHomology_sc'_of_not_mem_boundary, truncGE'_d_eq, truncGE'.homologyData_right_g', truncGE'_d_eq_fromOpcycles, truncGE'Map_f_eq_opcyclesMap, restrictionToTruncGE'.f_eq_iso_hom_pOpcycles_iso_inv, truncGE.rightHomologyMapData_φH, truncGE'.quasiIsoAt_restrictionToTruncGE', restrictionToTruncGE'_naturality_assoc, truncGE'Map_comp_assoc, truncGE'Map_id, truncGE'.hasHomology_of_not_mem_boundary, restrictionToTruncGE'_naturality, isIso_restrictionToTruncGE', restrictionToTruncGE'.f_eq_iso_hom_iso_inv, truncGE'.homologyι_truncGE'XIsoOpcycles_inv_d, truncGE'Map_f_eq, restrictionToTruncGE'_f_eq_iso_hom_iso_inv, instEpiFRestrictionToTruncGE', restrictionToTruncGE'_hasLift
truncGE'Map 📖	CompOp	8 math math: truncGE'Map_comp, truncGE'Map_f_eq_opcyclesMap, restrictionToTruncGE'_naturality_assoc, truncGE'Map_comp_assoc, truncGE'Map_id, ComplexShape.Embedding.truncGE'Functor_map, restrictionToTruncGE'_naturality, truncGE'Map_f_eq
truncGE'XIso 📖	CompOp	5 math math: truncGE'_d_eq, truncGE'_d_eq_fromOpcycles, restrictionToTruncGE'.f_eq_iso_hom_iso_inv, truncGE'Map_f_eq, restrictionToTruncGE'_f_eq_iso_hom_iso_inv
truncGE'XIsoOpcycles 📖	CompOp	6 math math: restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv, truncGE.rightHomologyMapData_φQ, truncGE'_d_eq_fromOpcycles, truncGE'Map_f_eq_opcyclesMap, restrictionToTruncGE'.f_eq_iso_hom_pOpcycles_iso_inv, truncGE'.homologyι_truncGE'XIsoOpcycles_inv_d
truncGEMap 📖	CompOp	7 math math: πTruncGE_naturality_assoc, truncGEMap_comp_assoc, πTruncGE_naturality, quasiIso_truncGEMap_iff, truncGEMap_comp, ComplexShape.Embedding.truncGEFunctor_map, truncGEMap_id
truncGEXIso 📖	CompOp	—
truncGEXIsoOpcycles 📖	CompOp	—
πTruncGE 📖	CompOp	14 math math: πTruncGE_naturality_assoc, truncGE.rightHomologyMapData_φQ, instEpiFπTruncGE, quasiIso_πTruncGE_iff_isSupported, instIsIsoπTruncGEOfIsStrictlySupported, g_shortComplexTruncLEX₃ToTruncGE, quasiIsoAt_πTruncGE, isIso_πTruncGE_iff, πTruncGE_naturality, ComplexShape.Embedding.πTruncGENatTrans_app, truncGE.rightHomologyMapData_φH, instEpiπTruncGE, g_shortComplexTruncLEX₃ToTruncGE_assoc, instQuasiIsoAtπTruncGEF

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instEpiFRestrictionToTruncGE' 📖	mathematical	HasHomology	CategoryTheory.Epi X restriction ComplexShape.Embedding.IsTruncGE.toIsRelIff truncGE' Hom.f restrictionToTruncGE'	—	ComplexShape.Embedding.IsTruncGE.toIsRelIff restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv CategoryTheory.epi_comp CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom instEpiPOpcycles CategoryTheory.Iso.isIso_inv isIso_restrictionToTruncGE'
instEpiFπTruncGE 📖	mathematical	HasHomology	CategoryTheory.Epi X truncGE Hom.f πTruncGE	—	ComplexShape.Embedding.IsTruncGE.toIsRelIff restrictionToTruncGE'_hasLift ComplexShape.Embedding.epi_liftExtend_f_iff instEpiFRestrictionToTruncGE' CategoryTheory.Limits.IsZero.epi isZero_extend_X
instEpiπTruncGE 📖	mathematical	HasHomology	CategoryTheory.Epi HomologicalComplex instCategory truncGE πTruncGE	—	epi_of_epi_f instEpiFπTruncGE
instIsIsoFRestrictionToTruncGE'OfIsStrictlySupported 📖	mathematical	HasHomology	CategoryTheory.IsIso X restriction ComplexShape.Embedding.IsTruncGE.toIsRelIff truncGE' Hom.f restrictionToTruncGE'	—	ComplexShape.Embedding.IsTruncGE.toIsRelIff restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv isIso_pOpcycles CategoryTheory.Limits.IsZero.eq_of_src isZero_X_of_isStrictlySupported CategoryTheory.IsIso.comp_isIso CategoryTheory.Iso.isIso_hom CategoryTheory.Iso.isIso_inv restrictionToTruncGE'_f_eq_iso_hom_iso_inv
instIsIsoπTruncGEOfIsStrictlySupported 📖	mathematical	HasHomology	CategoryTheory.IsIso HomologicalComplex instCategory truncGE πTruncGE	—	ComplexShape.Embedding.IsTruncGE.toIsRelIff restrictionToTruncGE'_hasLift ComplexShape.Embedding.isIso_liftExtend_f_iff instIsIsoFRestrictionToTruncGE'OfIsStrictlySupported CategoryTheory.Limits.IsZero.eq_of_src isZero_X_of_isStrictlySupported instIsStrictlySupportedTruncGE_1 Hom.isIso_of_components
instIsStrictlySupportedTruncGE 📖	mathematical	HasHomology	IsStrictlySupported truncGE	—	instIsStrictlySupportedExtend
instIsStrictlySupportedTruncGE_1 📖	mathematical	HasHomology	IsStrictlySupported truncGE	—	CategoryTheory.Limits.IsZero.iff_id_eq_zero CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_inv instEpiPOpcycles CategoryTheory.Limits.IsZero.eq_of_src isZero_X_of_isStrictlySupported CategoryTheory.Limits.IsZero.of_iso instIsStrictlySupportedTruncGE
isIso_restrictionToTruncGE' 📖	mathematical	HasHomology ComplexShape.Embedding.BoundaryGE	CategoryTheory.IsIso X restriction ComplexShape.Embedding.IsTruncGE.toIsRelIff truncGE' Hom.f restrictionToTruncGE'	—	ComplexShape.Embedding.IsTruncGE.toIsRelIff restrictionToTruncGE'_f_eq_iso_hom_iso_inv CategoryTheory.IsIso.comp_isIso CategoryTheory.Iso.isIso_hom CategoryTheory.Iso.isIso_inv
isIso_πTruncGE_iff 📖	mathematical	HasHomology	CategoryTheory.IsIso HomologicalComplex instCategory truncGE πTruncGE IsStrictlySupported	—	isStrictlySupported_of_iso instIsStrictlySupportedTruncGE instIsIsoπTruncGEOfIsStrictlySupported
restrictionToTruncGE'_f_eq_iso_hom_iso_inv 📖	mathematical	HasHomology ComplexShape.Embedding.f ComplexShape.Embedding.BoundaryGE	Hom.f restriction ComplexShape.Embedding.IsTruncGE.toIsRelIff truncGE' restrictionToTruncGE' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.hom restrictionXIso CategoryTheory.Iso.inv truncGE'XIso	—	restrictionToTruncGE'.f_eq_iso_hom_iso_inv
restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv 📖	mathematical	HasHomology ComplexShape.Embedding.f ComplexShape.Embedding.BoundaryGE	Hom.f restriction ComplexShape.Embedding.IsTruncGE.toIsRelIff truncGE' restrictionToTruncGE' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.hom restrictionXIso opcycles pOpcycles CategoryTheory.Iso.inv truncGE'XIsoOpcycles	—	restrictionToTruncGE'.f_eq_iso_hom_pOpcycles_iso_inv
restrictionToTruncGE'_hasLift 📖	mathematical	HasHomology	ComplexShape.Embedding.HasLift truncGE' ComplexShape.Embedding.IsTruncGE.toIsRelIff restrictionToTruncGE'	—	ComplexShape.Embedding.IsTruncGE.toIsRelIff restrictionToTruncGE'.f_eq_iso_hom_pOpcycles_iso_inv CategoryTheory.Category.id_comp d_pOpcycles_assoc CategoryTheory.Limits.zero_comp
restrictionToTruncGE'_naturality 📖	mathematical	HasHomology	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory restriction ComplexShape.Embedding.IsTruncGE.toIsRelIff truncGE' restrictionToTruncGE' truncGE'Map restrictionMap	—	hom_ext ComplexShape.Embedding.IsTruncGE.toIsRelIff restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv CategoryTheory.Category.id_comp truncGE'Map_f_eq_opcyclesMap CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc p_opcyclesMap_assoc restrictionToTruncGE'_f_eq_iso_hom_iso_inv truncGE'Map_f_eq
restrictionToTruncGE'_naturality_assoc 📖	mathematical	HasHomology	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory restriction ComplexShape.Embedding.IsTruncGE.toIsRelIff truncGE' restrictionToTruncGE' truncGE'Map restrictionMap	—	ComplexShape.Embedding.IsTruncGE.toIsRelIff CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' restrictionToTruncGE'_naturality
truncGE'Map_comp 📖	mathematical	HasHomology	truncGE'Map CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory truncGE'	—	hom_ext truncGE'Map_f_eq_opcyclesMap opcyclesMap_comp CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc truncGE'Map_f_eq
truncGE'Map_comp_assoc 📖	mathematical	HasHomology	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory truncGE' truncGE'Map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' truncGE'Map_comp
truncGE'Map_f_eq 📖	mathematical	HasHomology ComplexShape.Embedding.BoundaryGE ComplexShape.Embedding.f	Hom.f truncGE' truncGE'Map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.hom truncGE'XIso CategoryTheory.Iso.inv	—	—
truncGE'Map_f_eq_opcyclesMap 📖	mathematical	HasHomology ComplexShape.Embedding.BoundaryGE ComplexShape.Embedding.f	Hom.f truncGE' truncGE'Map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X opcycles CategoryTheory.Iso.hom truncGE'XIsoOpcycles opcyclesMap CategoryTheory.Iso.inv	—	—
truncGE'Map_id 📖	mathematical	HasHomology	truncGE'Map CategoryTheory.CategoryStruct.id HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory truncGE'	—	hom_ext truncGE'Map_f_eq_opcyclesMap opcyclesMap_id CategoryTheory.Category.id_comp CategoryTheory.Iso.hom_inv_id truncGE'Map_f_eq
truncGE'_d_eq 📖	mathematical	HasHomology ComplexShape.Rel ComplexShape.Embedding.f ComplexShape.Embedding.BoundaryGE	d truncGE' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.hom truncGE'XIso CategoryTheory.Iso.inv ComplexShape.Embedding.not_boundaryGE_next ComplexShape.Embedding.IsTruncGE.toIsRelIff	—	ComplexShape.Embedding.not_boundaryGE_next ComplexShape.Embedding.IsTruncGE.toIsRelIff CategoryTheory.Iso.trans_refl
truncGE'_d_eq_fromOpcycles 📖	mathematical	HasHomology ComplexShape.Rel ComplexShape.Embedding.f ComplexShape.Embedding.BoundaryGE	d truncGE' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X opcycles CategoryTheory.Iso.hom truncGE'XIsoOpcycles fromOpcycles CategoryTheory.Iso.inv truncGE'XIso ComplexShape.Embedding.not_boundaryGE_next ComplexShape.Embedding.IsTruncGE.toIsRelIff	—	ComplexShape.Embedding.not_boundaryGE_next ComplexShape.Embedding.IsTruncGE.toIsRelIff CategoryTheory.Iso.trans_refl
truncGEMap_comp 📖	mathematical	HasHomology	truncGEMap CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory truncGE	—	truncGE'Map_comp extendMap_comp
truncGEMap_comp_assoc 📖	mathematical	HasHomology	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory truncGE truncGEMap	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' truncGEMap_comp
truncGEMap_id 📖	mathematical	HasHomology	truncGEMap CategoryTheory.CategoryStruct.id HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory truncGE	—	truncGE'Map_id extendMap_id
πTruncGE_naturality 📖	mathematical	HasHomology	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory truncGE πTruncGE truncGEMap	—	Equiv.injective ComplexShape.Embedding.IsTruncGE.toIsRelIff restrictionToTruncGE'_hasLift ComplexShape.Embedding.homRestrict_comp_extendMap ComplexShape.Embedding.homRestrict_liftExtend ComplexShape.Embedding.homRestrict_precomp restrictionToTruncGE'_naturality
πTruncGE_naturality_assoc 📖	mathematical	HasHomology	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory truncGE πTruncGE truncGEMap	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' πTruncGE_naturality

HomologicalComplex.restrictionToTruncGE'

Definitions

Name	Category	Theorems
f 📖	CompOp	4 math math: comm_assoc, comm, f_eq_iso_hom_pOpcycles_iso_inv, f_eq_iso_hom_iso_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm 📖	mathematical	HomologicalComplex.HasHomology	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex.restriction ComplexShape.Embedding.IsTruncGE.toIsRelIff HomologicalComplex.truncGE' f HomologicalComplex.d	—	ComplexShape.Embedding.IsTruncGE.toIsRelIff f_eq_iso_hom_pOpcycles_iso_inv ComplexShape.Embedding.not_boundaryGE_next f_eq_iso_hom_iso_inv HomologicalComplex.truncGE'_d_eq_fromOpcycles CategoryTheory.Category.id_comp CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc HomologicalComplex.p_fromOpcycles_assoc HomologicalComplex.truncGE'_d_eq HomologicalComplex.shape CategoryTheory.Limits.comp_zero CategoryTheory.Limits.zero_comp
comm_assoc 📖	mathematical	HomologicalComplex.HasHomology	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex.restriction ComplexShape.Embedding.IsTruncGE.toIsRelIff HomologicalComplex.truncGE' f HomologicalComplex.d	—	ComplexShape.Embedding.IsTruncGE.toIsRelIff CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm
f_eq_iso_hom_iso_inv 📖	mathematical	HomologicalComplex.HasHomology ComplexShape.Embedding.f ComplexShape.Embedding.BoundaryGE	f CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex.restriction ComplexShape.Embedding.IsTruncGE.toIsRelIff HomologicalComplex.truncGE' CategoryTheory.Iso.hom HomologicalComplex.restrictionXIso CategoryTheory.Iso.inv HomologicalComplex.truncGE'XIso	—	ComplexShape.Embedding.IsTruncGE.toIsRelIff CategoryTheory.Category.id_comp
f_eq_iso_hom_pOpcycles_iso_inv 📖	mathematical	HomologicalComplex.HasHomology ComplexShape.Embedding.f ComplexShape.Embedding.BoundaryGE	f CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex.restriction ComplexShape.Embedding.IsTruncGE.toIsRelIff HomologicalComplex.truncGE' CategoryTheory.Iso.hom HomologicalComplex.restrictionXIso HomologicalComplex.opcycles HomologicalComplex.pOpcycles CategoryTheory.Iso.inv HomologicalComplex.truncGE'XIsoOpcycles	—	ComplexShape.Embedding.IsTruncGE.toIsRelIff CategoryTheory.Category.id_comp

HomologicalComplex.truncGE'

Definitions

Name	Category	Theorems
X 📖	CompOp	2 math math: d_comp_d, d_comp_d_assoc
XIso 📖	CompOp	—
XIsoOpcycles 📖	CompOp	—
d 📖	CompOp	2 math math: d_comp_d, d_comp_d_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
d_comp_d 📖	mathematical	HomologicalComplex.HasHomology	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	ComplexShape.Embedding.not_boundaryGE_next ComplexShape.Embedding.IsTruncGE.toIsRelIff CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc HomologicalComplex.fromOpcycles_d_assoc CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero HomologicalComplex.d_comp_d_assoc
d_comp_d_assoc 📖	mathematical	HomologicalComplex.HasHomology	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' d_comp_d

---

← Back to Index