feat(algebra/homology/homotopy) : mk_coinductive (#12457)

`mk_coinductive` is the dual version of `mk_inductive` in the same file. `mk_inductive` is to build homotopy of chain complexes inductively and `mk_coinductive` is to build homotopy of cochain complexes inductively.

src/algebra/homology/homotopy.lean

@@ -512,7 +512,7 @@ begin
 end
 
 /-!
-`homotopy.mk_inductive` allows us to build a homotopy inductively,
+`homotopy.mk_inductive` allows us to build a homotopy of chain complexes inductively,
 so that as we construct each component, we have available the previous two components,
 and the fact that they satisfy the homotopy condition.
 
@@ -645,6 +645,140 @@ end
 
 end mk_inductive
 
+/-!
+`homotopy.mk_coinductive` allows us to build a homotopy of cochain complexes inductively,
+so that as we construct each component, we have available the previous two components,
+and the fact that they satisfy the homotopy condition.
+-/
+section mk_coinductive
+
+variables {P Q : cochain_complex V ℕ}
+
+@[simp] lemma d_next_cochain_complex (f : Π i j, P.X i ⟶ Q.X j) (j : ℕ) :
+  d_next j f = P.d _ _ ≫ f (j+1) j :=
+begin
+  dsimp [d_next],
+  simp only [cochain_complex.next],
+  refl,
+end
+
+@[simp] lemma prev_d_succ_cochain_complex (f : Π i j, P.X i ⟶ Q.X j) (i : ℕ) :
+  prev_d (i+1) f = f (i+1) _ ≫ Q.d i (i+1) :=
+begin
+  dsimp [prev_d],
+  simp [cochain_complex.prev_nat_succ],
+  refl,
+end
+
+@[simp] lemma prev_d_zero_cochain_complex (f : Π i j, P.X i ⟶ Q.X j) :
+  prev_d 0 f = 0 :=
+begin
+  dsimp [prev_d],
+  simp only [cochain_complex.prev_nat_zero],
+  refl,
+end
+
+variables (e : P ⟶ Q)
+  (zero : P.X 1 ⟶ Q.X 0)
+  (comm_zero : e.f 0 = P.d 0 1 ≫ zero)
+  (one : P.X 2 ⟶ Q.X 1)
+  (comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one)
+  (succ : ∀ (n : ℕ)
+    (p : Σ' (f : P.X (n+1) ⟶ Q.X n) (f' : P.X (n+2) ⟶ Q.X (n+1)),
+      e.f (n+1) = f ≫ Q.d n (n+1) + P.d (n+1) (n+2) ≫ f'),
+    Σ' f'' : P.X (n+3) ⟶ Q.X (n+2), e.f (n+2) = p.2.1 ≫ Q.d (n+1) (n+2) + P.d (n+2) (n+3) ≫ f'')
+
+include comm_one comm_zero succ
+
+/--
+An auxiliary construction for `mk_coinductive`.
+
+Here we build by induction a family of diagrams,
+but don't require at the type level that these successive diagrams actually agree.
+They do in fact agree, and we then capture that at the type level (i.e. by constructing a homotopy)
+in `mk_coinductive`.
+
+At this stage, we don't check the homotopy condition in degree 0,
+because it "falls off the end", and is easier to treat using `X_next` and `X_prev`,
+which we do in `mk_inductive_aux₂`.
+-/
+@[simp, nolint unused_arguments]
+def mk_coinductive_aux₁ :
+  Π n, Σ' (f : P.X (n+1) ⟶ Q.X n) (f' : P.X (n+2) ⟶ Q.X (n+1)),
+    e.f (n+1) = f ≫ Q.d n (n+1) + P.d (n+1) (n+2) ≫ f'
+| 0 := ⟨zero, one, comm_one⟩
+| 1 := ⟨one, (succ 0 ⟨zero, one, comm_one⟩).1, (succ 0 ⟨zero, one, comm_one⟩).2⟩
+| (n+2) :=
+  ⟨(mk_coinductive_aux₁ (n+1)).2.1,
+    (succ (n+1) (mk_coinductive_aux₁ (n+1))).1,
+    (succ (n+1) (mk_coinductive_aux₁ (n+1))).2⟩
+
+section
+
+variable [has_zero_object V]
+
+/--
+An auxiliary construction for `mk_inductive`.
+-/
+@[simp]
+def mk_coinductive_aux₂ :
+  Π n, Σ' (f : P.X n ⟶ Q.X_prev n) (f' : P.X_next n ⟶ Q.X n),
+    e.f n = f ≫ Q.d_to n + P.d_from n ≫ f'
+| 0 := ⟨0, (P.X_next_iso rfl).hom ≫ zero, by simpa using comm_zero⟩
+| (n+1) := let I := mk_coinductive_aux₁ e zero comm_zero one comm_one succ n in
+  ⟨I.1 ≫ (Q.X_prev_iso rfl).inv, (P.X_next_iso rfl).hom ≫ I.2.1, by simpa using I.2.2⟩
+
+lemma mk_coinductive_aux₃ (i : ℕ) :
+  (mk_coinductive_aux₂ e zero comm_zero one comm_one succ i).2.1 ≫ (Q.X_prev_iso rfl).inv
+    = (P.X_next_iso rfl).hom ≫ (mk_coinductive_aux₂ e zero comm_zero one comm_one succ (i+1)).1 :=
+by rcases i with (_|_|i); { dsimp, simp, }
+
+/--
+A constructor for a `homotopy e 0`, for `e` a chain map between `ℕ`-indexed cochain complexes,
+working by induction.
+
+You need to provide the components of the homotopy in degrees 0 and 1,
+show that these satisfy the homotopy condition,
+and then give a construction of each component,
+and the fact that it satisfies the homotopy condition,
+using as an inductive hypothesis the data and homotopy condition for the previous two components.
+-/
+def mk_coinductive : homotopy e 0 :=
+{ hom := λ i j, if h : j + 1 = i then
+    (P.X_next_iso h).inv ≫ (mk_coinductive_aux₂ e zero comm_zero one comm_one succ j).2.1
+  else
+    0,
+  zero' := λ i j w, by rwa dif_neg,
+  comm := λ i, begin
+    dsimp,
+    rw [add_zero, add_comm],
+    convert (mk_coinductive_aux₂ e zero comm_zero one comm_one succ i).2.2 using 2,
+    { rcases i with (_|_|_|i),
+      { simp only [mk_coinductive_aux₂, prev_d_zero_cochain_complex, zero_comp] },
+      all_goals
+      { simp only [prev_d_succ_cochain_complex],
+        dsimp,
+        simp only [eq_self_iff_true, iso.inv_hom_id_assoc, dite_eq_ite,
+          if_true, category.assoc, X_prev_iso_comp_d_to], }, },
+    { cases i,
+      { dsimp,
+        simp only [eq_self_iff_true, d_next_cochain_complex, dif_pos,
+          d_from_comp_X_next_iso_assoc, ←comm_zero],
+      rw mk_coinductive_aux₂,
+      dsimp,
+      convert comm_zero.symm,
+      simp only [iso.inv_hom_id_assoc], },
+      { dsimp,
+        simp only [eq_self_iff_true, d_next_cochain_complex, dif_pos, d_from_comp_X_next_iso_assoc],
+        rw mk_coinductive_aux₂,
+        dsimp only,
+        simp only [iso.inv_hom_id_assoc], }, },
+  end }
+
+end
+
+end mk_coinductive
+
 end homotopy
 
 /--
@@ -771,4 +905,3 @@ def functor.map_homotopy_equiv (F : V ⥤ W) [F.additive] (h : homotopy_equiv C
   end }
 
 end category_theory
-