Commit 2023-05-17 12:51 13d2e52d

View on Github →

feat: port Algebra.Homology.QuasiIso (#3969)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Homology/QuasiIso.lean

added theorem CategoryTheory.Functor.quasiIso_of_map_quasiIso

added theorem HomologicalComplex.Hom.fromSingle₀KernelAtZeroIso_inv_eq

added theorem HomologicalComplex.Hom.from_single₀_exact_at_succ

added theorem HomologicalComplex.Hom.from_single₀_exact_f_d_at_zero

added theorem HomologicalComplex.Hom.from_single₀_mono_at_zero

added theorem HomologicalComplex.Hom.toSingle₀CokernelAtZeroIso_hom_eq

added theorem HomologicalComplex.Hom.to_single₀_epi_at_zero

added theorem HomologicalComplex.Hom.to_single₀_exact_at_succ

added theorem HomologicalComplex.Hom.to_single₀_exact_d_f_at_zero

added theorem HomotopyEquiv.toQuasiIso

added theorem HomotopyEquiv.toQuasiIso_inv

added theorem quasiIso_of_comp_left

added theorem quasiIso_of_comp_right