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