Commit 2023-04-19 22:29 4f99e001

View on Github →

feat: port Algebra.Homology.Homotopy (#3524)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Homology/Homotopy.lean

added def CategoryTheory.Functor.mapHomotopy

added def CategoryTheory.Functor.mapHomotopyEquiv

added def Homotopy.add

added def Homotopy.comp

added def Homotopy.compLeft

added def Homotopy.compLeftId

added def Homotopy.compRight

added def Homotopy.compRightId

added theorem Homotopy.comp_nullHomotopicMap'

added theorem Homotopy.comp_nullHomotopicMap

added theorem Homotopy.dNext_cochainComplex

added theorem Homotopy.dNext_succ_chainComplex

added theorem Homotopy.dNext_zero_chainComplex

added def Homotopy.equivSubZero

added theorem Homotopy.map_nullHomotopicMap'

added theorem Homotopy.map_nullHomotopicMap

added def Homotopy.mkCoinductive

added def Homotopy.mkCoinductiveAux₁

added def Homotopy.mkCoinductiveAux₂

added theorem Homotopy.mkCoinductiveAux₃

added def Homotopy.mkInductive

added def Homotopy.mkInductiveAux₁

added def Homotopy.mkInductiveAux₂

added theorem Homotopy.mkInductiveAux₃

added def Homotopy.nullHomotopicMap'

added theorem Homotopy.nullHomotopicMap'_comp

added theorem Homotopy.nullHomotopicMap'_f

added theorem Homotopy.nullHomotopicMap'_f_eq_zero

added theorem Homotopy.nullHomotopicMap'_f_of_not_rel_left

added theorem Homotopy.nullHomotopicMap'_f_of_not_rel_right

added def Homotopy.nullHomotopicMap

added theorem Homotopy.nullHomotopicMap_comp

added theorem Homotopy.nullHomotopicMap_f

added theorem Homotopy.nullHomotopicMap_f_eq_zero

added theorem Homotopy.nullHomotopicMap_f_of_not_rel_left

added theorem Homotopy.nullHomotopicMap_f_of_not_rel_right

added def Homotopy.nullHomotopy'

added def Homotopy.nullHomotopy

added def Homotopy.ofEq

added theorem Homotopy.prevD_chainComplex

added theorem Homotopy.prevD_succ_cochainComplex

added theorem Homotopy.prevD_zero_cochainComplex

added def Homotopy.refl

added def Homotopy.symm

added def Homotopy.trans

added structure Homotopy

added def HomotopyEquiv.ofIso

added def HomotopyEquiv.refl

added def HomotopyEquiv.symm

added def HomotopyEquiv.trans

added structure HomotopyEquiv

added def dNext

added theorem dNext_comp_left

added theorem dNext_comp_right

added theorem dNext_eq

added theorem dNext_eq_dFrom_fromNext

added theorem dNext_nat

added def fromNext

added def homologyObjIsoOfHomotopyEquiv

added theorem homology_map_eq_of_homotopy

added def prevD

added theorem prevD_comp_left

added theorem prevD_comp_right

added theorem prevD_eq

added theorem prevD_eq_toPrev_dTo

added theorem prevD_nat

added def toPrev