feat(algebra/category/AddCommGroup): has_image_maps (#3366)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

src/algebra/category/Group/images.lean

@@ -85,7 +85,25 @@ noncomputable instance : has_image f :=
   { lift := image.lift,
     lift_fac' := image.lift_fac } }
 
-noncomputable instance : has_images.{0} AddCommGroup.{0} :=
+noncomputable instance : has_images AddCommGroup.{0} :=
 { has_image := infer_instance }
 
+-- We'll later get this as a consequence of `[abelian AddCommGroup]`.
+-- Nevertheless this instance has the desired definitional behaviour,
+-- and is useful in the meantime for doing cohomology.
+
+-- When the `[abelian AddCommGroup]` instance is available
+-- this instance should be reviewed, and ideally removed if the `[abelian]` instance
+-- provides something definitionally equivalent.
+noncomputable instance : has_image_maps AddCommGroup.{0} :=
+{ has_image_map := λ f g st,
+  { map :=
+    { to_fun := image.map ((forget AddCommGroup).map_arrow.map st),
+      map_zero' := by { ext, simp, },
+      map_add' := λ x y, by { ext, simp, refl, } } } }
+
+@[simp] lemma image_map {f g : arrow AddCommGroup.{0}} (st : f ⟶ g) (x : image f.hom):
+  (image.map st x).val = st.right x.1 :=
+rfl
+
 end AddCommGroup

src/category_theory/arrow.lean

@@ -112,4 +112,24 @@ end
 
 end arrow
 
+namespace functor
+
+universes v₁ v₂ u₁ u₂
+
+variables {C : Type u₁} [category.{v₁} C] {D : Type u₂} [category.{v₂} D]
+
+/-- A functor `C ⥤ D` induces a functor between the corresponding arrow categories. -/
+@[simps]
+def map_arrow (F : C ⥤ D) : arrow C ⥤ arrow D :=
+{ obj := λ a,
+  { left := F.obj a.left,
+    right := F.obj a.right,
+    hom := F.map a.hom, },
+  map := λ a b f,
+  { left := F.map f.left,
+    right := F.map f.right,
+    w' := by { have w := f.w, simp only [id_map] at w, dsimp, simp only [←F.map_comp, w], } } }
+
+end functor
+
 end category_theory

src/category_theory/limits/types.lean

@@ -129,4 +129,18 @@ noncomputable instance : has_image f :=
 noncomputable instance : has_images (Type u) :=
 { has_image := infer_instance }
 
+noncomputable instance : has_image_maps (Type u) :=
+{ has_image_map := λ f g st,
+  { map := λ x, ⟨st.right x.1, ⟨st.left (classical.some x.2),
+      begin
+        have p := st.w,
+        replace p := congr_fun p (classical.some x.2),
+        simp only [functor.id_map, types_comp_apply, subtype.val_eq_coe] at p,
+        erw [p, classical.some_spec x.2],
+      end⟩⟩ } }
+
+@[simp] lemma image_map {f g : arrow (Type u)} (st : f ⟶ g) (x : image f.hom) :
+  (image.map st x).val = st.right x.1 :=
+rfl
+
 end category_theory.limits.types