Structures · Algebra
CategoryTheory.ShortComplex.HasLeftHomology
A short complex S has left homology when there exists a S.LeftHomologyData
- Shape
- One type argument · adds condition
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by163
- CategoryTheory.ShortComplex.cycles
- CategoryTheory.ShortComplex.iCycles
- CategoryTheory.ShortComplex.leftHomologyData
- CategoryTheory.ShortComplex.leftHomology
- CategoryTheory.ShortComplex.toCycles
- CategoryTheory.ShortComplex.cyclesMap
- CategoryTheory.ShortComplex.liftCycles
- CategoryTheory.ShortComplex.leftHomologyπ
- CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso
- CategoryTheory.ShortComplex.leftHomologyMap
- CategoryTheory.ShortComplex.liftCycles_i
- CategoryTheory.ShortComplex.toCycles_i
- CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso
- CategoryTheory.ShortComplex.iCycles_g
- CategoryTheory.ShortComplex.isoCyclesOfIsLimit
- CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_hom_comp_i
- CategoryTheory.ShortComplex.cyclesMap_i
- CategoryTheory.ShortComplex.opcyclesOpIso
- CategoryTheory.ShortComplex.mapCyclesIso
- CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_inv_comp_iCycles
- CategoryTheory.ShortComplex.leftRightHomologyComparison
- CategoryTheory.ShortComplex.cyclesIsoLeftHomology
- CategoryTheory.ShortComplex.cyclesIsoX₂
- CategoryTheory.ShortComplex.mapLeftHomologyIso
- CategoryTheory.ShortComplex.cyclesIsKernel
- CategoryTheory.ShortComplex.liftCycles_comp_cyclesMap_assoc
- CategoryTheory.ShortComplex.cyclesMapIso
- CategoryTheory.ShortComplex.rightHomologyOpIso
- CategoryTheory.ComposableArrows.Exact.opcyclesIsoCycles
- CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyπ_comp_leftHomologyIso_hom
- CategoryTheory.ShortComplex.cyclesIsoKernel
- CategoryTheory.ShortComplex.π_leftRightHomologyComparison_ι
- CategoryTheory.ShortComplex.isoCyclesOfIsLimit_hom_iCycles_assoc
- CategoryTheory.ShortComplex.cyclesMap_comp
- CategoryTheory.ShortComplex.isoCyclesOfIsLimit_inv_ι
- CategoryTheory.ComposableArrows.IsComplex.opcyclesToCycles_fac
- CategoryTheory.ShortComplex.leftHomologyπ_naturality
- CategoryTheory.ShortComplex.opcyclesOpIso_inv_naturality
- CategoryTheory.ShortComplex.mapCyclesIso_hom_iCycles
- CategoryTheory.ShortComplex.opcyclesOpIso_hom_naturality
- CategoryTheory.ShortComplex.leftHomologyMapIso
- CategoryTheory.ShortComplex.cycles_ext
- CategoryTheory.ShortComplex.cyclesMap_i_assoc
- CategoryTheory.ShortComplex.opcyclesOpIso_hom_toCycles_op
- CategoryTheory.ShortComplex.liftCycles_leftHomologyπ_eq_zero_of_boundary
- CategoryTheory.ShortComplex.LeftHomologyData.liftCycles_comp_cyclesIso_hom
- CategoryTheory.ShortComplex.liftCycles.congr_simp
- CategoryTheory.ShortComplex.op_pOpcycles_opcyclesOpIso_hom
- CategoryTheory.ShortComplex.isIso_iCycles
- CategoryTheory.ComposableArrows.IsComplex.opcyclesToCycles
Ancestors0
No ancestors.