Commit 2023-04-19 13:55 b1e0bf77

View on Github →

feat: port Algebra.Homology.Additive (#3517)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Homology/Additive.lean

added def CategoryTheory.Equivalence.mapHomologicalComplex

added def CategoryTheory.Functor.mapHomologicalComplex

added def CategoryTheory.Functor.mapHomologicalComplexIdIso

added def CategoryTheory.NatIso.mapHomologicalComplex

added def CategoryTheory.NatTrans.mapHomologicalComplex

added theorem CategoryTheory.NatTrans.mapHomologicalComplex_comp

added theorem CategoryTheory.NatTrans.mapHomologicalComplex_id

added theorem CategoryTheory.NatTrans.mapHomologicalComplex_naturality

added theorem ChainComplex.map_chain_complex_of

added def ChainComplex.single₀MapHomologicalComplex

added theorem ChainComplex.single₀MapHomologicalComplex_hom_app_succ

added theorem ChainComplex.single₀MapHomologicalComplex_hom_app_zero

added theorem ChainComplex.single₀MapHomologicalComplex_inv_app_succ

added theorem ChainComplex.single₀MapHomologicalComplex_inv_app_zero

added def CochainComplex.single₀MapHomologicalComplex

added theorem CochainComplex.single₀MapHomologicalComplex_hom_app_succ

added theorem CochainComplex.single₀MapHomologicalComplex_hom_app_zero

added theorem CochainComplex.single₀MapHomologicalComplex_inv_app_succ

added theorem CochainComplex.single₀MapHomologicalComplex_inv_app_zero

added def HomologicalComplex.Hom.fAddMonoidHom

added theorem HomologicalComplex.add_f_apply

added theorem HomologicalComplex.neg_f_apply

added theorem HomologicalComplex.nsmul_f_apply

added def HomologicalComplex.singleMapHomologicalComplex

added theorem HomologicalComplex.singleMapHomologicalComplex_hom_app_ne

added theorem HomologicalComplex.singleMapHomologicalComplex_hom_app_self

added theorem HomologicalComplex.singleMapHomologicalComplex_inv_app_ne

added theorem HomologicalComplex.singleMapHomologicalComplex_inv_app_self

added theorem HomologicalComplex.sub_f_apply

added theorem HomologicalComplex.zero_f_apply

added theorem HomologicalComplex.zsmul_f_apply