feat(category_theory/abelian): equivalence between subobjects and quo…

…tients (#15494)

src/category_theory/abelian/subobject.lean

@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2022 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import category_theory.abelian.opposite
+import category_theory.subobject.limits
+
+/-!
+# Equivalence between subobjects and quotients in an abelian category
+
+-/
+
+open category_theory category_theory.limits opposite
+
+universes v u
+
+noncomputable theory
+
+namespace category_theory.abelian
+variables {C : Type u} [category.{v} C]
+
+/-- In an abelian category, the subobjects and quotient objects of an object `X` are
+    order-isomorphic via taking kernels and cokernels.
+    Implemented here using subobjects in the opposite category,
+    since mathlib does not have a notion of quotient objects at the time of writing. -/
+@[simps]
+def subobject_iso_subobject_op [abelian C] (X : C) : subobject X ≃o (subobject (op X))ᵒᵈ :=
+begin
+  refine order_iso.of_hom_inv (cokernel_order_hom X) (kernel_order_hom X) _ _,
+  { change (cokernel_order_hom X).comp (kernel_order_hom X) = _,
+    refine order_hom.ext _ _ (funext (subobject.ind _ _)),
+    introsI A f hf,
+    dsimp only [order_hom.comp_coe, function.comp_app, kernel_order_hom_coe, subobject.lift_mk,
+      cokernel_order_hom_coe, order_hom.id_coe, id.def],
+    refine subobject.mk_eq_mk_of_comm _ _ ⟨_, _, quiver.hom.unop_inj _, quiver.hom.unop_inj _⟩ _,
+    { exact (abelian.epi_desc f.unop _ (cokernel.condition (kernel.ι f.unop))).op },
+    { exact (cokernel.desc _ _ (kernel.condition f.unop)).op },
+    { simp only [← cancel_epi (cokernel.π (kernel.ι f.unop)), unop_comp, quiver.hom.unop_op,
+        unop_id_op, cokernel.π_desc_assoc, comp_epi_desc, category.comp_id] },
+    { simp only [← cancel_epi f.unop, unop_comp, quiver.hom.unop_op, unop_id, comp_epi_desc_assoc,
+        cokernel.π_desc, category.comp_id] },
+    { exact quiver.hom.unop_inj (by simp only [unop_comp, quiver.hom.unop_op, comp_epi_desc]) } },
+  { change (kernel_order_hom X).comp (cokernel_order_hom X) = _,
+    refine order_hom.ext _ _ (funext (subobject.ind _ _)),
+    introsI A f hf,
+    dsimp only [order_hom.comp_coe, function.comp_app, cokernel_order_hom_coe, subobject.lift_mk,
+      kernel_order_hom_coe, order_hom.id_coe, id.def, unop_op, quiver.hom.unop_op],
+    refine subobject.mk_eq_mk_of_comm _ _ ⟨_, _, _, _⟩ _,
+    { exact abelian.mono_lift f _ (kernel.condition (cokernel.π f)) },
+    { exact kernel.lift _ _ (cokernel.condition f) },
+    { simp only [← cancel_mono (kernel.ι (cokernel.π f)), category.assoc, image.fac, mono_lift_comp,
+        category.id_comp, auto_param_eq] },
+    { simp only [← cancel_mono f, category.assoc, mono_lift_comp, image.fac, category.id_comp,
+        auto_param_eq] },
+    { simp only [mono_lift_comp] } }
+end
+
+end category_theory.abelian

src/category_theory/subobject/basic.lean

@@ -98,6 +98,43 @@ namespace subobject
 abbreviation mk {X A : C} (f : A ⟶ X) [mono f] : subobject X :=
 (to_thin_skeleton _).obj (mono_over.mk' f)
 
+section
+local attribute [ext] category_theory.comma
+
+protected lemma ind {X : C} (p : subobject X → Prop)
+  (h : ∀ ⦃A : C⦄ (f : A ⟶ X) [mono f], by exactI p (subobject.mk f)) (P : subobject X) : p P :=
+begin
+  apply quotient.induction_on',
+  intro a,
+  convert h a.arrow,
+  ext; refl
+end
+
+protected lemma ind₂ {X : C} (p : subobject X → subobject X → Prop)
+  (h : ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [mono f] [mono g],
+    by exactI p (subobject.mk f) (subobject.mk g)) (P Q : subobject X) : p P Q :=
+begin
+  apply quotient.induction_on₂',
+  intros a b,
+  convert h a.arrow b.arrow;
+  ext; refl
+end
+
+end
+
+/-- Declare a function on subobjects of `X` by specifying a function on monomorphisms with
+    codomain `X`. -/
+protected def lift {α : Sort*} {X : C} (F : Π ⦃A : C⦄ (f : A ⟶ X) [mono f], α)
+  (h : ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [mono f] [mono g] (i : A ≅ B),
+    i.hom ≫ g = f → by exactI F f = F g) : subobject X → α :=
+λ P, quotient.lift_on' P (λ m, by exactI F m.arrow) $ λ m n ⟨i⟩,
+  h m.arrow n.arrow ((mono_over.forget X ⋙ over.forget X).map_iso i) (over.w i.hom)
+
+@[simp]
+protected lemma lift_mk {α : Sort*} {X : C} (F : Π ⦃A : C⦄ (f : A ⟶ X) [mono f], α) {h A}
+  (f : A ⟶ X) [mono f] : subobject.lift F h (subobject.mk f) = F f :=
+rfl
+
 /-- The category of subobjects is equivalent to the `mono_over` category. It is more convenient to
 use the former due to the partial order instance, but oftentimes it is easier to define structures
 on the latter. -/

src/category_theory/subobject/limits.lean

@@ -22,6 +22,7 @@ universes v u
 noncomputable theory
 
 open category_theory category_theory.category category_theory.limits category_theory.subobject
+  opposite
 
 variables {C : Type u} [category.{v} C] {X Y Z : C}
 
@@ -203,6 +204,50 @@ begin
   { simp, },
 end
 
+/-- Taking cokernels is an order-reversing map from the subobjects of `X` to the quotient objects
+    of `X`. -/
+@[simps]
+def cokernel_order_hom [has_cokernels C] (X : C) : subobject X →o (subobject (op X))ᵒᵈ :=
+{ to_fun := subobject.lift (λ A f hf, subobject.mk (cokernel.π f).op)
+  begin
+    rintros A B f g hf hg i rfl,
+    refine subobject.mk_eq_mk_of_comm _ _ (iso.op _) (quiver.hom.unop_inj _),
+    { exact (is_colimit.cocone_point_unique_up_to_iso (colimit.is_colimit _)
+        (is_cokernel_epi_comp (colimit.is_colimit _) i.hom rfl)).symm },
+    { simp only [iso.comp_inv_eq, iso.op_hom, iso.symm_hom, unop_comp, quiver.hom.unop_op,
+        colimit.comp_cocone_point_unique_up_to_iso_hom, cofork.of_π_ι_app, coequalizer.cofork_π] }
+  end,
+  monotone' := subobject.ind₂ _ $
+  begin
+    introsI A B f g hf hg h,
+    dsimp only [subobject.lift_mk],
+    refine subobject.mk_le_mk_of_comm (cokernel.desc f (cokernel.π g) _).op _,
+    { rw [← subobject.of_mk_le_mk_comp h, category.assoc, cokernel.condition, comp_zero] },
+    { exact quiver.hom.unop_inj (cokernel.π_desc _ _ _) }
+  end }
+
+/-- Taking kernels is an order-reversing map from the quotient objects of `X` to the subobjects of
+    `X`. -/
+@[simps]
+def kernel_order_hom [has_kernels C] (X : C) : (subobject (op X))ᵒᵈ →o subobject X :=
+{ to_fun := subobject.lift (λ A f hf, subobject.mk (kernel.ι f.unop))
+  begin
+    rintros A B f g hf hg i rfl,
+    refine subobject.mk_eq_mk_of_comm _ _ _ _,
+    { exact is_limit.cone_point_unique_up_to_iso (limit.is_limit _)
+        (is_kernel_comp_mono (limit.is_limit (parallel_pair g.unop 0)) i.unop.hom rfl) },
+    { dsimp,
+      simp only [←iso.eq_inv_comp, limit.cone_point_unique_up_to_iso_inv_comp, fork.of_ι_π_app] }
+  end,
+  monotone' := subobject.ind₂ _ $
+  begin
+    introsI A B f g hf hg h,
+    dsimp only [subobject.lift_mk],
+    refine subobject.mk_le_mk_of_comm (kernel.lift g.unop (kernel.ι f.unop) _) _,
+    { rw [← subobject.of_mk_le_mk_comp h, unop_comp, kernel.condition_assoc, zero_comp] },
+    { exact quiver.hom.op_inj (by simp) }
+  end }
+
 end kernel
 
 section image