Structures · Algebra
CochainComplex.IsKProjective
A cochain complex K is K-projective if any morphism K ⟶ L
with L acyclic is homotopic to zero.
- Shape
- One type argument · adds nonempty_homotopy_zero
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by13
- CochainComplex.IsKProjective.homotopyZero
- CochainComplex.IsKProjective.Qh_map_bijective
- CochainComplex.isKProjective_of_iso
- CochainComplex.HomComplex.CohomologyClass.equivOfIsKProjective
- HomotopyEquiv.isKProjective
- CochainComplex.IsKProjective.leftOrthogonal
- CochainComplex.IsKProjective.nonempty_homotopy_zero
- CochainComplex.HomComplex.CohomologyClass.bijective_toSmallShiftedHom_of_isKProjective
- CochainComplex.IsKProjective.quasiIso_iff
- CochainComplex.instIsKProjectiveObjIntShiftFunctor
- CochainComplex.IsKProjective.homotopyZero_def
- CochainComplex.HomComplex.CohomologyClass.equivOfIsKProjective_symm_apply
- CochainComplex.HomComplex.CohomologyClass.equivOfIsKProjective_apply
Ancestors0
No ancestors.