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

src/algebra/homology/additive.lean

@@ -239,3 +239,40 @@ nat_iso.of_components (λ X,
   ((single₀_map_homological_complex F).inv.app X).f (n+1) = 0 := rfl
 
 end chain_complex
+
+namespace cochain_complex
+
+def single₀_map_homological_complex (F : V ⥤ W) [F.additive] :
+  single₀ V ⋙ F.map_homological_complex _ ≅ F ⋙ single₀ W :=
+nat_iso.of_components (λ X,
+{ hom := { f := λ i, match i with
+    | 0 := 𝟙 _
+    | (i+1) := F.map_zero_object.hom
+    end, },
+  inv := { f := λ i, match i with
+    | 0 := 𝟙 _
+    | (i+1) := F.map_zero_object.inv
+    end, },
+  hom_inv_id' := begin
+    ext (_|i),
+    { unfold_aux, simp, },
+    { unfold_aux,
+      dsimp,
+      simp only [comp_f, id_f, zero_comp],
+      exact (zero_of_source_iso_zero _ F.map_zero_object).symm, }
+  end,
+  inv_hom_id' := by { ext (_|i); { unfold_aux, dsimp, simp, }, }, })
+  (λ X Y f, by { ext (_|i); { unfold_aux, dsimp, simp, }, }).
+
+@[simp] lemma single₀_map_homological_complex_hom_app_zero (F : V ⥤ W) [F.additive] (X : V) :
+  ((single₀_map_homological_complex F).hom.app X).f 0 = 𝟙 _ := rfl
+@[simp] lemma single₀_map_homological_complex_hom_app_succ
+  (F : V ⥤ W) [F.additive] (X : V) (n : ℕ) :
+  ((single₀_map_homological_complex F).hom.app X).f (n+1) = 0 := rfl
+@[simp] lemma single₀_map_homological_complex_inv_app_zero (F : V ⥤ W) [F.additive] (X : V) :
+  ((single₀_map_homological_complex F).inv.app X).f 0 = 𝟙 _ := rfl
+@[simp] lemma single₀_map_homological_complex_inv_app_succ
+  (F : V ⥤ W) [F.additive] (X : V) (n : ℕ) :
+  ((single₀_map_homological_complex F).inv.app X).f (n+1) = 0 := rfl
+
+end cochain_complex

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.
 
@@ -632,7 +632,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],
@@ -645,6 +645,146 @@ 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.
+
+To simplify the situation, we only construct homotopies of the form `homotopy e 0`.
+`homotopy.equiv_sub_zero` can provide the general case.
+
+Notice however, that this construction does not have particularly good definitional properties:
+we have to insert `eq_to_hom` in several places.
+Hopefully this is okay in most applications, where we only need to have the existence of some
+homotopy.
+-/
+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 +911,3 @@ def functor.map_homotopy_equiv (F : V ⥤ W) [F.additive] (h : homotopy_equiv C
   end }
 
 end category_theory
-

src/category_theory/abelian/exact.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
 import category_theory.abelian.basic
+import category_theory.abelian.opposite
 import algebra.homology.exact
 import tactic.tfae
 
@@ -186,4 +187,21 @@ lemma epi_iff_cokernel_π_eq_zero : epi f ↔ cokernel.π f = 0 :=
 
 end
 
+section opposite
+
+instance exact.op [exact f g] : exact g.op f.op :=
+begin
+  rw exact_iff,
+  refine ⟨by simp [← op_comp], _⟩,
+  apply_fun quiver.hom.unop,
+  swap,
+  { exact quiver.hom.unop_inj },
+  simp only [unop_comp, unop_zero],
+  rw [cokernel.π_op, kernel.ι_op],
+  simp only [unop_comp, cokernel.π_op, eq_to_hom_refl, kernel.ι_op, category.id_comp,
+    category.assoc, kernel_comp_cokernel_assoc, zero_comp, comp_zero, unop_zero],
+end
+
+end opposite
+
 end category_theory.abelian

src/category_theory/abelian/injective.lean

@@ -0,0 +1,58 @@
+import category_theory.abelian.exact
+import category_theory.preadditive.injective_resolution
+
+noncomputable theory
+
+open category_theory
+open category_theory.limits
+
+universes v u
+
+namespace category_theory
+
+open category_theory.injective
+
+variables {C : Type u} [category.{v} C]
+
+section
+
+variables [enough_injectives C] [abelian C]
+
+lemma exact_d_f {X Y : C} (f : X ⟶ Y) : exact f (d f) :=
+(abelian.exact_iff _ _).2 $
+  ⟨by simp, zero_of_comp_mono (ι _) $ by rw [category.assoc, kernel.condition]⟩
+
+end
+
+namespace InjectiveResolution
+
+variables [abelian C] [enough_injectives C]
+
+@[simps]
+def of_cocomplex (Z : C) : cochain_complex C ℕ :=
+cochain_complex.mk'
+  (injective.under Z) (injective.syzygies (injective.ι Z)) (injective.d (injective.ι Z))
+  (λ ⟨X, Y, f⟩, ⟨injective.syzygies f, injective.d f, (exact_d_f f).w⟩)
+
+@[irreducible] def of (Z : C) : InjectiveResolution Z :=
+{ cocomplex := of_cocomplex Z,
+  ι := cochain_complex.mk_hom _ _ (injective.ι Z) 0
+    (by { simp only [of_cocomplex_d, eq_self_iff_true, eq_to_hom_refl, category.comp_id,
+      dite_eq_ite, if_true, exact.w],
+      exact (exact_d_f (injective.ι Z)).w, } ) (λ n _, ⟨0, by ext⟩),
+  injective := by { rintros (_|_|_|n); { apply injective.injective_under, } },
+  exact₀ := by simpa using exact_d_f (injective.ι Z),
+  exact := by { rintros (_|n); { simp, apply exact_d_f } },
+  mono := injective.ι_mono Z }
+
+@[priority 100]
+instance (Z : C) : has_injective_resolution Z :=
+{ out := ⟨of Z⟩ }
+
+@[priority 100]
+instance : has_injective_resolutions C :=
+{ out := λ _, infer_instance }
+
+end InjectiveResolution
+
+end category_theory

src/category_theory/abelian/opposite.lean

@@ -107,6 +107,20 @@ def kernel_unop_unop : kernel g.unop ≅ (cokernel g).unop :=
 def cokernel_unop_unop : cokernel g.unop ≅ (kernel g).unop :=
 (cokernel_unop_op g).unop.symm
 
+lemma cokernel.π_op : (cokernel.π f.op).unop =
+  (cokernel_op_unop f).hom ≫ kernel.ι f ≫ eq_to_hom (opposite.unop_op _).symm :=
+begin
+  dsimp [cokernel_op_unop],
+  simp,
+end
+
+lemma kernel.ι_op : (kernel.ι f.op).unop =
+  eq_to_hom (opposite.unop_op _) ≫ cokernel.π f ≫ (kernel_op_unop f).inv :=
+begin
+  dsimp [kernel_op_unop],
+  simp,
+end
+
 end
 
 end category_theory