Commit 2026-03-12 17:39 407d3318

View on Github →

feat(Algebra/Homology/SpectralObject): induced morphisms that are epi/mono (#36153)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Homology/SpectralObject/EpiMono.lean

added theorem CategoryTheory.Abelian.SpectralObject.d_map_fourδ₄Toδ₃

added theorem CategoryTheory.Abelian.SpectralObject.epi_map

added theorem CategoryTheory.Abelian.SpectralObject.isIso_mapFourδ₁Toδ₀'

added theorem CategoryTheory.Abelian.SpectralObject.isIso_mapFourδ₂Toδ₁'

added theorem CategoryTheory.Abelian.SpectralObject.isIso_mapFourδ₄Toδ₃'

added theorem CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₁Toδ₀

added theorem CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₁Toδ₀_of_isZero

added theorem CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₄Toδ₃

added theorem CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₄Toδ₃_of_isZero

added theorem CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_hom_inv_id

added theorem CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_inv_hom_id

added theorem CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₄'_hom_inv_id

added theorem CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₄'_inv_hom_id

added theorem CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'_comp

added theorem CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'_mapFourδ₃Toδ₃'

added theorem CategoryTheory.Abelian.SpectralObject.mapFourδ₄Toδ₃'_comp

added theorem CategoryTheory.Abelian.SpectralObject.map_fourδ₁Toδ₀_d

added theorem CategoryTheory.Abelian.SpectralObject.mono_map