Structures · Algebra
QuasiIso
A morphism of homological complexes f : K ⟶ L is a quasi-isomorphism when it
is so in every degree, i.e. when the induced maps homologyMap f i : K.homology i ⟶ L.homology i
are all isomorphisms (see quasiIso_iff and quasiIsoAt_iff_isIso_homologyMap).
- Defined in
- Mathlib.Algebra.Homology.QuasiIso
- Shape
- One type argument · adds quasiIsoAt
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Forgetful instances
Every QuasiIso is also a
Concrete types that are instances2
- Int
- Nat
How is a type an instance?
Loading the hierarchy index…
Assumed by15
- quasiIso_iff_comp_left
- quasiIso_iff_comp_right
- quasiIso_of_comp_right
- quasiIso_of_retractArrow
- HomologicalComplex.instQuasiIsoMapOppositeSymmUnopFunctorOp
- HomologicalComplex.isSupported_iff_of_quasiIso
- HomologicalComplex.instQuasiIsoOppositeMapSymmOpFunctorOp
- quasiIso_comp
- DerivedCategory.instIsIsoMapCochainComplexIntQOfQuasiIso
- quasiIso_of_comp_left
- HomologicalComplex.quasiIso_map_of_preservesHomology
- QuasiIso.quasiIsoAt
- HomologicalComplex.instQuasiIsoExtendMap
- quasiIso_of_arrow_mk_iso
- CochainComplex.instQuasiIsoIntMapHomologicalComplexUpShiftFunctor