Mathlib Changelog
Changelog
About
Github
Commit
2021-05-19 02:36
918dcc0a
View on Github →
chore(algebra/homology): further dualization (
#7657
)
Estimated changes
Modified
src/algebra/homology/augment.lean
added
theorem
chain_complex.chain_complex_d_succ_succ_zero
deleted
theorem
chain_complex.cochain_complex_d_succ_succ_zero
added
def
cochain_complex.augment
added
theorem
cochain_complex.augment_X_succ
added
theorem
cochain_complex.augment_X_zero
added
theorem
cochain_complex.augment_d_succ_succ
added
theorem
cochain_complex.augment_d_zero_one
added
def
cochain_complex.augment_truncate
added
theorem
cochain_complex.augment_truncate_hom_f_succ
added
theorem
cochain_complex.augment_truncate_hom_f_zero
added
theorem
cochain_complex.augment_truncate_inv_f_succ
added
theorem
cochain_complex.augment_truncate_inv_f_zero
added
theorem
cochain_complex.cochain_complex_d_succ_succ_zero
added
def
cochain_complex.from_single₀_as_complex
added
def
cochain_complex.to_truncate
added
def
cochain_complex.truncate
added
def
cochain_complex.truncate_augment
added
theorem
cochain_complex.truncate_augment_hom_f
added
theorem
cochain_complex.truncate_augment_inv_f
Modified
src/algebra/homology/homological_complex.lean
added
def
cochain_complex.mk'
added
theorem
cochain_complex.mk'_X_0
added
theorem
cochain_complex.mk'_X_1
added
theorem
cochain_complex.mk'_d_1_0
added
def
cochain_complex.mk
added
theorem
cochain_complex.mk_X_0
added
theorem
cochain_complex.mk_X_1
added
theorem
cochain_complex.mk_X_2
added
def
cochain_complex.mk_aux
added
theorem
cochain_complex.mk_d_1_0
added
theorem
cochain_complex.mk_d_2_0
added
def
cochain_complex.mk_hom
added
def
cochain_complex.mk_hom_aux
added
theorem
cochain_complex.mk_hom_f_0
added
theorem
cochain_complex.mk_hom_f_1
added
theorem
cochain_complex.mk_hom_f_succ_succ
added
def
cochain_complex.mk_struct.flat
added
structure
cochain_complex.mk_struct
Modified
src/algebra/homology/single.lean
added
def
cochain_complex.from_single₀_equiv
added
def
cochain_complex.homology_functor_0_single₀
added
def
cochain_complex.homology_functor_succ_single₀
added
def
cochain_complex.single₀
added
def
cochain_complex.single₀_iso_single
added
theorem
cochain_complex.single₀_map_f_0
added
theorem
cochain_complex.single₀_map_f_succ
added
theorem
cochain_complex.single₀_obj_X_0
added
theorem
cochain_complex.single₀_obj_X_d
added
theorem
cochain_complex.single₀_obj_X_d_from
added
theorem
cochain_complex.single₀_obj_X_d_to
added
theorem
cochain_complex.single₀_obj_X_succ