Structures · Algebra
CochainComplex.IsKInjective
A cochain complex L is K-injective if any morphism K ⟶ L
with K 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 by15
- CochainComplex.IsKInjective.homotopyZero
- CochainComplex.IsKInjective.Qh_map_bijective
- CochainComplex.IsKInjective.quasiIso_iff
- CochainComplex.isKInjective_of_iso
- CochainComplex.HomComplex.CohomologyClass.equivOfIsKInjective
- CochainComplex.IsKInjective.nonempty_homotopy_zero
- CochainComplex.HomComplex.CohomologyClass.bijective_toSmallShiftedHom_of_isKInjective
- HomotopyEquiv.isKInjective
- CochainComplex.IsKInjective.eq_δ_of_cocycle
- CochainComplex.IsKInjective.rightOrthogonal
- CochainComplex.IsKInjective.eq_δ_of_cocycle'
- CochainComplex.instIsKInjectiveObjIntShiftFunctor
- CochainComplex.HomComplex.CohomologyClass.equivOfIsKInjective_symm_apply
- CochainComplex.HomComplex.CohomologyClass.equivOfIsKInjective_apply
- CochainComplex.IsKInjective.homotopyZero_def
Ancestors0
No ancestors.