Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-05-13 15:18
ce455949
View on Github →
feat(algebra/homology/single): chain complexes supported in a single degree (
#7477
)
Estimated changes
Modified
src/algebra/homology/homological_complex.lean
Created
src/algebra/homology/single.lean
added
def
chain_complex.homology_functor_0_single₀
added
def
chain_complex.homology_functor_succ_single₀
added
def
chain_complex.single₀
added
def
chain_complex.single₀_iso_single
added
theorem
chain_complex.single₀_map_f_0
added
theorem
chain_complex.single₀_map_f_succ
added
theorem
chain_complex.single₀_obj_X_0
added
theorem
chain_complex.single₀_obj_X_d
added
theorem
chain_complex.single₀_obj_X_d_from
added
theorem
chain_complex.single₀_obj_X_d_to
added
theorem
chain_complex.single₀_obj_X_succ
added
def
chain_complex.to_single₀_equiv
added
def
homological_complex.single
added
theorem
homological_complex.single_map_f_self
added
def
homological_complex.single_obj_X_self
Modified
src/category_theory/fully_faithful.lean
added
def
category_theory.full.of_iso