Structures · Algebra
QuasiIsoAt
A morphism of homological complexes f : K ⟶ L is a quasi-isomorphism in degree i
when it induces a quasi-isomorphism of short complexes K.sc i ⟶ L.sc i.
- Defined in
- Mathlib.Algebra.Homology.QuasiIso
- Shape
- 2 explicit arguments · adds quasiIso
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances1
- Int
How is a type an instance?
Loading the hierarchy index…
Assumed by21
- isoOfQuasiIsoAt
- exactAt_iff_of_quasiIsoAt
- quasiIsoAt_iff_comp_left
- quasiIsoAt_iff_comp_right
- CochainComplex.isSplitMono_from_singleFunctor_obj_of_injective
- CochainComplex.isSplitEpi_to_singleFunctor_obj_of_projective
- isoOfQuasiIsoAt_inv_hom_id
- isoOfQuasiIsoAt_hom_inv_id
- quasiIsoAt_of_retract
- QuasiIsoAt.quasiIso
- quasiIsoAt_of_comp_right
- quasiIsoAt_of_comp_left
- quasiIsoAt_comp
- isoOfQuasiIsoAt.congr_simp
- HomologicalComplex.instQuasiIsoAtMapOppositeSymmUnopFunctorOp
- HomologicalComplex.quasiIsoAt_map_of_preservesHomology
- HomologicalComplex.instQuasiIsoAtOppositeMapSymmOpFunctorOp
- instIsIsoHomologyMapOfQuasiIsoAt
- isoOfQuasiIsoAt_inv_hom_id_assoc
- isoOfQuasiIsoAt_hom_inv_id_assoc
- isoOfQuasiIsoAt_hom
Ancestors0
No ancestors.