feat(algebra/homology): chain complexes

src/algebra/homology/chain_complex.lean

@@ -50,9 +50,11 @@ variables {V}
 A convenience lemma for morphisms of differential graded objects,
 picking out one component of the commutation relation.
 -/
--- Could this be a simp lemma? Which way?
-lemma category_theory.differential_object.hom.comm_at {X Y : differential_object.{v} (graded_object ℤ V)}
-  (f : X ⟶ Y) (i : ℤ) : f.f i ≫ Y.d i = X.d i ≫ f.f (i+1) := congr_fun f.comm i
+@[simp]
+lemma category_theory.differential_object.hom.comm_at
+  {X Y : differential_object.{v} (graded_object ℤ V)} (f : X ⟶ Y) (i : ℤ) :
+    X.d i ≫ f.f (i+1) = f.f i ≫ Y.d i :=
+congr_fun f.comm i
 end
 
 namespace chain_complex
@@ -73,8 +75,8 @@ by { dsimp [chain_complex], apply_instance }.
 
 -- The components of a chain map `f : C ⟶ D` are accessed as `f.f i`.
 example {C D : chain_complex V} (f : C ⟶ D) : C.X 5 ⟶ D.X 5 := f.f 5
-example {C D : chain_complex V} (f : C ⟶ D) : f.f ≫ D.d = C.d ≫ f.f[[1]] := f.comm
-example {C D : chain_complex V} (f : C ⟶ D) : f.f 5 ≫ D.d 5 = C.d 5 ≫ f.f 6 := congr_fun f.comm 5
+example {C D : chain_complex V} (f : C ⟶ D) : C.d ≫ f.f⟦1⟧' = f.f ≫ D.d := by simp
+example {C D : chain_complex V} (f : C ⟶ D) : C.d 5 ≫ f.f 6 = f.f 5 ≫ D.d 5 := congr_fun f.comm 5
 
 /-- The forgetful functor from chain complexes to graded objects, forgetting the differential. -/
 def forget : (chain_complex V) ⥤ (graded_object ℤ V) :=

src/algebra/homology/homology.lean

@@ -37,7 +37,7 @@ def induced_map_on_cycles {C C' : chain_complex.{v} V} (f : C ⟶ C') (i : ℤ)
   kernel (C.d i) ⟶ kernel (C'.d i) :=
 kernel.lift _ (kernel.ι _ ≫ f.f i)
 begin
-  rw [category.assoc, f.comm_at, ←category.assoc, kernel.condition, has_zero_morphisms.zero_comp],
+  rw [category.assoc, ←f.comm_at, ←category.assoc, kernel.condition, has_zero_morphisms.zero_comp],
 end
 end
 

src/category_theory/differential_object.lean

@@ -11,7 +11,7 @@ import category_theory.shift
 
 A differential object in a category with zero morphisms and a shift is
 an object `X` equipped with
-a morphism `d : X ⟶ X[1]`, such that `d^2 = 0`.
+a morphism `d : X ⟶ X⟦1⟧`, such that `d^2 = 0`.
 
 We build the category of differential objects, and some basic constructions
 such as the forgetful functor, and zero morphisms and zero objects.
@@ -31,13 +31,13 @@ variables [has_zero_morphisms.{v} C] [has_shift.{v} C]
 /--
 A differential object in a category with zero morphisms and a shift is
 an object `X` equipped with
-a morphism `d : X ⟶ X[1]`, such that `d^2 = 0`.
+a morphism `d : X ⟶ X⟦1⟧`, such that `d^2 = 0`.
 -/
 @[nolint has_inhabited_instance]
 structure differential_object :=
 (X : C)
-(d : X ⟶ X[1])
-(d_squared' : d ≫ d[[1]] = 0 . obviously)
+(d : X ⟶ X⟦1⟧)
+(d_squared' : d ≫ d⟦1⟧' = 0 . obviously)
 
 restate_axiom differential_object.d_squared'
 attribute [simp] differential_object.d_squared
@@ -52,9 +52,10 @@ A morphism of differential objects is a morphism commuting with the differential
 @[ext, nolint has_inhabited_instance]
 structure hom (X Y : differential_object.{v} C) :=
 (f : X.X ⟶ Y.X)
-(comm' : f ≫ Y.d = X.d ≫ f[[1]] . obviously)
+(comm' : X.d ≫ f⟦1⟧' = f ≫ Y.d . obviously)
 
 restate_axiom hom.comm'
+attribute [simp, reassoc] hom.comm
 
 namespace hom
 
@@ -66,8 +67,7 @@ def id (X : differential_object.{v} C) : hom X X :=
 /-- The composition of morphisms of differential objects. -/
 @[simps]
 def comp {X Y Z : differential_object.{v} C} (f : hom X Y) (g : hom Y Z) : hom X Z :=
-{ f := f.f ≫ g.f,
-  comm' := by rw [category.assoc, g.comm, ←category.assoc, f.comm, category.assoc, functor.map_comp], }
+{ f := f.f ≫ g.f, }
 
 end hom
 

src/category_theory/equivalence.lean

@@ -196,20 +196,14 @@ omit 𝒟 ℰ
 -- The power structure is nevertheless useful
 
 /-- Powers of an auto-equivalence. -/
-def nat_pow (e : C ≌ C) : ℕ → (C ≌ C)
-| 0 := equivalence.refl
-| 1 := e
-| (n+2) := e.trans (nat_pow (n+1))
-
-instance has_pow_nat : has_pow (C ≌ C) ℕ := ⟨nat_pow⟩
-
-/-- Integer powers of an auto-equivalence. -/
-def int_pow (e : C ≌ C) : ℤ → (C ≌ C)
-| (int.of_nat n) := e^n
+def pow (e : C ≌ C) : ℤ → (C ≌ C)
+| (int.of_nat 0) := equivalence.refl
+| (int.of_nat 1) := e
+| (int.of_nat (n+2)) := e.trans (pow (int.of_nat (n+1)))
 | (int.neg_succ_of_nat 0) := e.symm
-| (int.neg_succ_of_nat (n+1)) := e.symm.trans (int_pow (int.neg_succ_of_nat n))
+| (int.neg_succ_of_nat (n+1)) := e.symm.trans (pow (int.neg_succ_of_nat n))
 
-instance has_pow_int : has_pow (C ≌ C) ℤ := ⟨int_pow⟩
+instance : has_pow (C ≌ C) ℤ := ⟨pow⟩
 
 end
 

src/category_theory/shift.lean

@@ -5,10 +5,10 @@ Authors: Scott Morrison
 -/
 import category_theory.limits.shapes.zero
 
-/-! #Shift 
+/-! #Shift
 
 A `shift` on a category is nothing more than an automorphism of the category. An example to
-keep in mind might be the category of complexes ⋯ → C_{n-1} → C_n → C_{n+1} → ⋯with the shift
+keep in mind might be the category of complexes ⋯ → C_{n-1} → C_n → C_{n+1} → ⋯ with the shift
 operator re-indexing the terms, so the degree `n` term of `shift C` would be the degree `n+1`
 term of `C`.
 
@@ -26,20 +26,21 @@ class has_shift :=
 
 variables [has_shift.{v} C]
 
-/-- The shift functor, moving objects and morphisms 'up'. -/
-def shift : C ⥤ C := (has_shift.shift.{v} C).functor
+/-- The shift autoequivalence, moving objects and morphisms 'up'. -/
+def shift : C ≌ C := has_shift.shift.{v} C
 
 -- Any better notational suggestions?
-notation X`[1]`:20 := (shift _).obj X
-notation f`[[1]]`:80 := (shift _).map f
+notation X`⟦`n`⟧`:20 := ((shift _)^(n : ℤ)).functor.obj X
+notation f`⟦`n`⟧'`:80 := ((shift _)^(n : ℤ)).functor.map f
 
-example {X Y : C} (f : X ⟶ Y) : X[1] ⟶ Y[1] := f[[1]]
+example {X Y : C} (f : X ⟶ Y) : X⟦1⟧ ⟶ Y⟦1⟧ := f⟦1⟧'
+example {X Y : C} (f : X ⟶ Y) : X⟦-2⟧ ⟶ Y⟦-2⟧ := f⟦-2⟧'
 
 open category_theory.limits
 variables [has_zero_morphisms.{v} C]
 
 @[simp]
-lemma shift_zero (X Y : C) : (0 : X ⟶ Y)[[1]] = (0 : X[1] ⟶ Y[1]) :=
+lemma shift_zero (X Y : C) (n : ℤ) : (0 : X ⟶ Y)⟦n⟧' = (0 : X⟦n⟧ ⟶ Y⟦n⟧) :=
 by apply equivalence_preserves_zero_morphisms
 
 end category_theory