feat(algebra/category/Module): compare concrete and abstract kernels (#…

…6938)




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

src/algebra/category/Module/basic.lean

@@ -68,12 +68,12 @@ namespace Module
 instance : has_coe_to_sort (Module.{v} R) :=
 { S := Type v, coe := Module.carrier }
 
-instance : category (Module.{v} R) :=
+instance Module_category : category (Module.{v} R) :=
 { hom   := λ M N, M →ₗ[R] N,
   id    := λ M, 1,
   comp  := λ A B C f g, g.comp f }
 
-instance : concrete_category.{v} (Module.{v} R) :=
+instance Module_concrete_category : concrete_category.{v} (Module.{v} R) :=
 { forget := { obj := λ R, R, map := λ R S f, (f : R → S) },
   forget_faithful := { } }
 

src/algebra/category/Module/kernels.lean

@@ -63,4 +63,47 @@ lemma has_kernels_Module : has_kernels (Module R) :=
 lemma has_cokernels_Module : has_cokernels (Module R) :=
 ⟨λ X Y f, has_colimit.mk ⟨_, cokernel_is_colimit f⟩⟩
 
+open_locale Module
+
+local attribute [instance] has_kernels_Module
+local attribute [instance] has_cokernels_Module
+
+variables {G H : Module.{v} R} (f : G ⟶ H)
+
+/--
+The categorical kernel of a morphism in `Module`
+agrees with the usual module-theoretical kernel.
+-/
+noncomputable def kernel_iso_ker {G H : Module.{v} R} (f : G ⟶ H) :
+  kernel f ≅ Module.of R (f.ker) :=
+limit.iso_limit_cone ⟨_, kernel_is_limit f⟩
+
+-- We now show this isomorphism commutes with the inclusion of the kernel into the source.
+
+@[simp, elementwise] lemma kernel_iso_ker_inv_kernel_ι :
+  (kernel_iso_ker f).inv ≫ kernel.ι f = f.ker.subtype :=
+limit.iso_limit_cone_inv_π _ _
+
+@[simp, elementwise] lemma kernel_iso_ker_hom_ker_subtype :
+  (kernel_iso_ker f).hom ≫ f.ker.subtype = kernel.ι f :=
+is_limit.cone_point_unique_up_to_iso_inv_comp _ (limit.is_limit _) zero
+
+/--
+The categorical cokernel of a morphism in `Module`
+agrees with the usual module-theoretical quotient.
+-/
+noncomputable def cokernel_iso_range_quotient {G H : Module.{v} R} (f : G ⟶ H) :
+  cokernel f ≅ Module.of R (f.range.quotient) :=
+colimit.iso_colimit_cocone ⟨_, cokernel_is_colimit f⟩
+
+-- We now show this isomorphism commutes with the projection of target to the cokernel.
+
+@[simp, elementwise] lemma cokernel_π_cokernel_iso_range_quotient_hom :
+  cokernel.π f ≫ (cokernel_iso_range_quotient f).hom = f.range.mkq :=
+by { convert colimit.iso_colimit_cocone_ι_hom _ _; refl, }
+
+@[simp, elementwise] lemma range_mkq_cokernel_iso_range_quotient_inv :
+  ↿f.range.mkq ≫ (cokernel_iso_range_quotient f).inv = cokernel.π f :=
+by { convert colimit.iso_colimit_cocone_ι_inv ⟨_, cokernel_is_colimit f⟩ _; refl, }
+
 end Module

src/algebra/category/Mon/basic.lean

@@ -6,6 +6,7 @@ Authors: Scott Morrison
 import category_theory.concrete_category.bundled_hom
 import category_theory.concrete_category.reflects_isomorphisms
 import algebra.punit_instances
+import tactic.elementwise
 
 /-!
 # Category instances for monoid, add_monoid, comm_monoid, and add_comm_monoid.

src/category_theory/concrete_category/basic.lean

@@ -116,6 +116,12 @@ congr_fun ((forget C).map_iso f).hom_inv_id x
   f.hom (f.inv y) = y :=
 congr_fun ((forget C).map_iso f).inv_hom_id y
 
+lemma concrete_category.congr_hom {X Y : C} {f g : X ⟶ Y} (h : f = g) (x : X) : f x = g x :=
+congr_fun (congr_arg (λ f : X ⟶ Y, (f : X → Y)) h) x
+
+lemma concrete_category.congr_arg {X Y : C} (f : X ⟶ Y) {x x' : X} (h : x = x') : f x = f x' :=
+congr_arg (f : X → Y) h
+
 /-- In any concrete category, injective morphisms are monomorphisms. -/
 lemma concrete_category.mono_of_injective {X Y : C} (f : X ⟶ Y) (i : function.injective f) :
   mono f :=