Structures · Algebra
CategoryTheory.ShortComplex.HasHomology
A short complex S has homology when there exists a S.HomologyData
- Shape
- One type argument · adds condition
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances1
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by279
- CategoryTheory.ShortComplex.homology
- CategoryTheory.ShortComplex.homologyMap
- CategoryTheory.ShortComplex.homologyπ
- CategoryTheory.ShortComplex.homologyι
- CategoryTheory.ShortComplex.LeftHomologyData.homologyIso
- CategoryTheory.ShortComplex.homologyData
- CategoryTheory.ShortComplex.RightHomologyData.homologyIso
- CategoryTheory.ShortComplex.leftHomologyIso
- CategoryTheory.ShortComplex.exact_of_g_is_cokernel
- CategoryTheory.ShortComplex.exact_of_f_is_kernel
- CategoryTheory.ShortComplex.rightHomologyIso
- CategoryTheory.ShortComplex.toCycles_comp_homologyπ
- CategoryTheory.ShortComplex.mapHomologyIso
- HomologicalComplex.cyclesIsoSc'
- CategoryTheory.ShortComplex.homologyι_comp_fromOpcycles
- HomologicalComplex.opcyclesIsoSc'
- HomologicalComplex.homologyIsoSc'
- CategoryTheory.ShortComplex.HomologyData.canonical
- CategoryTheory.ShortComplex.homologyπ_naturality
- CategoryTheory.ShortComplex.LeftHomologyData.exact_iff
- CategoryTheory.ShortComplex.quasiIso_iff
- CategoryTheory.ShortComplex.mapHomologyIso'
- CategoryTheory.ShortComplex.LeftHomologyData.canonical
- CategoryTheory.ShortComplex.RightHomologyData.canonical
- CategoryTheory.ShortComplex.homologyι_naturality
- CategoryTheory.ShortComplex.LeftHomologyMapData.quasiIso_iff
- CategoryTheory.ShortComplex.RightHomologyMapData.quasiIso_iff
- CategoryTheory.ShortComplex.RightHomologyData.exact_iff
- CategoryTheory.ShortComplex.exact_iff_isZero_homology
- CategoryTheory.ShortComplex.asIsoHomologyι
- CategoryTheory.ShortComplex.asIsoHomologyπ
- CategoryTheory.ShortComplex.LeftHomologyData.homologyπ_comp_homologyIso_hom
- CategoryTheory.ShortComplex.homologyOpIso
- CategoryTheory.ShortComplex.homologyIsCokernel
- CategoryTheory.ShortComplex.homology_π_ι
- CategoryTheory.ShortComplex.leftRightHomologyComparison'_fac
- CategoryTheory.ShortComplex.homologyMap_comp
- quasiIsoAt_iff'
- CategoryTheory.ShortComplex.quasiIso_opMap_iff
- CategoryTheory.ShortComplex.LeftHomologyData.exact_iff_epi_f'
- CategoryTheory.ShortComplex.homologyπ_comp_leftHomologyIso_inv_assoc
- CategoryTheory.ShortComplex.homologyMap_id
- CategoryTheory.ShortComplex.homologyIsKernel
- CategoryTheory.ShortComplex.homology_π_ι_assoc
- CategoryTheory.ShortComplex.RightHomologyData.homologyIso_rightHomologyData
- CategoryTheory.ShortComplex.liftHomology
- CategoryTheory.ShortComplex.LeftHomologyData.π_comp_homologyIso_inv
- CategoryTheory.ShortComplex.descHomology
- CategoryTheory.ShortComplex.quasiIso_of_epi_of_isIso_of_mono
- CategoryTheory.ShortComplex.exact_iff_epi_kernel_lift
Ancestors0
No ancestors.