Commit 2023-04-17 19:17 fca09560

View on Github →

feat: port Algebra.Homology.HomologicalComplex (#3451)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Homology/HomologicalComplex.lean

added def ChainComplex.MkStruct.flat

added structure ChainComplex.MkStruct

added def ChainComplex.mk'

added theorem ChainComplex.mk'_X_0

added theorem ChainComplex.mk'_X_1

added theorem ChainComplex.mk'_d_1_0

added def ChainComplex.mk

added def ChainComplex.mkAux

added def ChainComplex.mkHom

added def ChainComplex.mkHomAux

added theorem ChainComplex.mkHom_f_0

added theorem ChainComplex.mkHom_f_1

added theorem ChainComplex.mkHom_f_succ_succ

added theorem ChainComplex.mk_X_0

added theorem ChainComplex.mk_X_1

added theorem ChainComplex.mk_X_2

added theorem ChainComplex.mk_d_1_0

added theorem ChainComplex.mk_d_2_0

added theorem ChainComplex.next

added theorem ChainComplex.next_nat_succ

added theorem ChainComplex.next_nat_zero

added def ChainComplex.of

added def ChainComplex.ofHom

added theorem ChainComplex.of_d

added theorem ChainComplex.of_d_ne

added theorem ChainComplex.of_x

added theorem ChainComplex.prev

added def CochainComplex.MkStruct.flat

added structure CochainComplex.MkStruct

added def CochainComplex.mk'

added theorem CochainComplex.mk'_X_0

added theorem CochainComplex.mk'_X_1

added theorem CochainComplex.mk'_d_1_0

added def CochainComplex.mk

added def CochainComplex.mkAux

added def CochainComplex.mkHom

added def CochainComplex.mkHomAux

added theorem CochainComplex.mkHom_f_0

added theorem CochainComplex.mkHom_f_1

added theorem CochainComplex.mkHom_f_succ_succ

added theorem CochainComplex.mk_X_0

added theorem CochainComplex.mk_X_1

added theorem CochainComplex.mk_X_2

added theorem CochainComplex.mk_d_1_0

added theorem CochainComplex.mk_d_2_0

added theorem CochainComplex.next

added def CochainComplex.of

added def CochainComplex.ofHom

added theorem CochainComplex.of_d

added theorem CochainComplex.of_d_ne

added theorem CochainComplex.of_x

added theorem CochainComplex.prev

added theorem CochainComplex.prev_nat_succ

added theorem CochainComplex.prev_nat_zero

added theorem HomologicalComplex.Hom.comm

added theorem HomologicalComplex.Hom.comm_from

added theorem HomologicalComplex.Hom.comm_to

added theorem HomologicalComplex.Hom.isIso_of_components

added def HomologicalComplex.Hom.isoApp

added def HomologicalComplex.Hom.isoOfComponents

added theorem HomologicalComplex.Hom.isoOfComponents_app

added theorem HomologicalComplex.Hom.next_eq

added theorem HomologicalComplex.Hom.prev_eq

added def HomologicalComplex.Hom.sqFrom

added theorem HomologicalComplex.Hom.sqFrom_comp

added theorem HomologicalComplex.Hom.sqFrom_id

added theorem HomologicalComplex.Hom.sqFrom_left

added theorem HomologicalComplex.Hom.sqFrom_right

added def HomologicalComplex.Hom.sqTo

added theorem HomologicalComplex.Hom.sqTo_left

added theorem HomologicalComplex.Hom.sqTo_right

added structure HomologicalComplex.Hom

added def HomologicalComplex.comp

added theorem HomologicalComplex.comp_f

added theorem HomologicalComplex.congr_hom

added theorem HomologicalComplex.dFrom_comp_xNextIso

added theorem HomologicalComplex.dFrom_comp_xNextIsoSelf

added theorem HomologicalComplex.dFrom_eq

added theorem HomologicalComplex.dFrom_eq_zero

added theorem HomologicalComplex.dTo_comp_dFrom

added theorem HomologicalComplex.dTo_eq

added theorem HomologicalComplex.dTo_eq_zero

added theorem HomologicalComplex.d_comp_d

added theorem HomologicalComplex.d_comp_eqToHom

added theorem HomologicalComplex.eqToHom_comp_d

added theorem HomologicalComplex.eqToHom_f

added def HomologicalComplex.eval

added theorem HomologicalComplex.ext

added def HomologicalComplex.forget

added def HomologicalComplex.forgetEval

added theorem HomologicalComplex.hom_ext

added theorem HomologicalComplex.hom_f_injective

added def HomologicalComplex.id

added theorem HomologicalComplex.id_f

added theorem HomologicalComplex.image_eq_image

added theorem HomologicalComplex.image_to_eq_image

added theorem HomologicalComplex.isZero_zero

added theorem HomologicalComplex.kernel_eq_kernel

added theorem HomologicalComplex.kernel_from_eq_kernel

added def HomologicalComplex.xNextIso

added def HomologicalComplex.xNextIsoSelf

added def HomologicalComplex.xPrevIso

added def HomologicalComplex.xPrevIsoSelf

added theorem HomologicalComplex.xPrevIsoSelf_comp_dTo

added theorem HomologicalComplex.xPrevIso_comp_dTo

added theorem HomologicalComplex.zero_f

added structure HomologicalComplex