Commit 2023-11-10 14:22 a189a128

View on Github →

feat: quasi-isomorphisms of homological complexes (#8206) This PR defines the typeclass QuasiIso which corresponds to quasi-isomorphisms of homological complexes for the new homology API.

Estimated changes

Modified Mathlib/Algebra/Homology/QuasiIso.lean

added theorem ChainComplex.quasiIsoAt₀_iff

added theorem CochainComplex.quasiIsoAt₀_iff

added theorem isoOfQuasiIsoAt_hom_inv_id

added theorem isoOfQuasiIsoAt_inv_hom_id

added theorem quasiIsoAt_iff'

added theorem quasiIsoAt_iff

added theorem quasiIsoAt_iff_comp_left

added theorem quasiIsoAt_iff_comp_right

added theorem quasiIsoAt_iff_exactAt'

added theorem quasiIsoAt_iff_exactAt

added theorem quasiIsoAt_iff_isIso_homologyMap

added theorem quasiIsoAt_of_comp_left

added theorem quasiIsoAt_of_comp_right

added theorem quasiIso_iff

added theorem quasiIso_iff_comp_left

added theorem quasiIso_iff_comp_right

added theorem quasiIso_iff_of_arrow_mk_iso

added theorem quasiIso_of_arrow_mk_iso

added theorem quasiIso_of_comp_left

added theorem quasiIso_of_comp_right