feat(category_theory/*/injective): definition of injective objects

src/algebra/homology/homotopy.lean

@@ -285,13 +285,13 @@ def comp_left_id {f : D ⟶ D} (h : homotopy f (𝟙 D)) (g : C ⟶ D) : homotop
 /-!
 Null homotopic maps can be constructed using the formula `hd+dh`. We show that
 these morphisms are homotopic to `0` and provide some convenient simplification
-lemmas that give a degreewise description of `hd+dh`, depending on whether we have 
+lemmas that give a degreewise description of `hd+dh`, depending on whether we have
 two differentials going to and from a certain degree, only one, or none.
 -/
 
 /-- The null homotopic map associated to a family `hom` of morphisms `C_i ⟶ D_j`.
 This is the same datum as for the field `hom` in the structure `homotopy`. For
-this definition, we do not need the field `zero` of that structure 
+this definition, we do not need the field `zero` of that structure
 as this definition uses only the maps `C_i ⟶ C_j` when `c.rel j i`. -/
 def null_homotopic_map (hom : Π i j, C.X i ⟶ D.X j) : C ⟶ D :=
 { f      := λ i, d_next i hom + prev_d i hom,
@@ -306,7 +306,7 @@ def null_homotopic_map (hom : Π i j, C.X i ⟶ D.X j) : C ⟶ D :=
       { dsimp [d_next], rw h, erw comp_zero, },
       { rw [d_next_eq hom w, ← category.assoc, C.d_comp_d' i j j' hij w, zero_comp], }, },
     rw [d_next_eq hom hij, prev_d_eq hom hij, preadditive.comp_add, preadditive.add_comp,
-      eq1, eq2, add_zero, zero_add, category.assoc], 
+      eq1, eq2, add_zero, zero_add, category.assoc],
   end }
 
 /-- Variant of `null_homotopic_map` where the input consists only of the
@@ -409,7 +409,7 @@ begin
 end
 
 @[simp]
-lemma null_homotopic_map_f_eq_zero {k₀ : ι} 
+lemma null_homotopic_map_f_eq_zero {k₀ : ι}
   (hk₀ : ∀ l : ι, ¬c.rel k₀ l) (hk₀' : ∀ l : ι, ¬c.rel l k₀)
   (hom : Π i j, C.X i ⟶ D.X j) :
   (null_homotopic_map hom).f k₀ = 0 :=
@@ -424,7 +424,7 @@ begin
 end
 
 @[simp]
-lemma null_homotopic_map'_f_eq_zero {k₀ : ι} 
+lemma null_homotopic_map'_f_eq_zero {k₀ : ι}
   (hk₀ : ∀ l : ι, ¬c.rel k₀ l) (hk₀' : ∀ l : ι, ¬c.rel l k₀)
   (h : Π i j, c.rel j i → (C.X i ⟶ D.X j)) :
   (null_homotopic_map' h).f k₀ = 0 :=
@@ -555,7 +555,7 @@ def mk_inductive : homotopy e 0 :=
       { simp only [d_next_succ_chain_complex],
         dsimp,
         simp only [category.comp_id, category.assoc, iso.inv_hom_id, d_from_comp_X_next_iso_assoc,
-          dite_eq_ite, if_true, eq_self_iff_true]}, },
+          dite_eq_ite, if_true, eq_self_iff_true], }, },
     { cases i,
       all_goals
       { simp only [prev_d_chain_complex],
@@ -568,6 +568,113 @@ end
 
 end mk_inductive
 
+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
+
+@[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]
+
+@[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, }
+
+-- 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, }
+
+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
 
 /--