feat: port CategoryTheory.Abelian.Subobject (#3607)

Mathlib.lean

@@ -374,6 +374,7 @@ import Mathlib.CategoryTheory.Abelian.Basic
 import Mathlib.CategoryTheory.Abelian.FunctorCategory
 import Mathlib.CategoryTheory.Abelian.Images
 import Mathlib.CategoryTheory.Abelian.NonPreadditive
+import Mathlib.CategoryTheory.Abelian.Subobject
 import Mathlib.CategoryTheory.Adjunction.Basic
 import Mathlib.CategoryTheory.Adjunction.Comma
 import Mathlib.CategoryTheory.Adjunction.Evaluation

Mathlib/CategoryTheory/Abelian/Subobject.lean

@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2022 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+
+! This file was ported from Lean 3 source module category_theory.abelian.subobject
+! leanprover-community/mathlib commit 70fd9563a21e7b963887c9360bd29b2393e6225a
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.CategoryTheory.Subobject.Limits
+import Mathlib.CategoryTheory.Abelian.Basic
+
+/-!
+# Equivalence between subobjects and quotients in an abelian category
+
+-/
+
+
+open CategoryTheory CategoryTheory.Limits Opposite
+
+universe v u
+
+noncomputable section
+
+namespace CategoryTheory.Abelian
+
+variable {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 subobjectIsoSubobjectOp [Abelian C] (X : C) : Subobject X ≃o (Subobject (op X))ᵒᵈ := by
+  refine' OrderIso.ofHomInv (cokernelOrderHom X) (kernelOrderHom X) _ _
+  · change (cokernelOrderHom X).comp (kernelOrderHom X) = _
+    refine' OrderHom.ext _ _ (funext (Subobject.ind _ _))
+    intro A f hf
+    dsimp only [OrderHom.comp_coe, Function.comp_apply, kernelOrderHom_coe, Subobject.lift_mk,
+      cokernelOrderHom_coe, OrderHom.id_coe, id.def]
+    refine' Subobject.mk_eq_mk_of_comm _ _ ⟨_, _, Quiver.Hom.unop_inj _, Quiver.Hom.unop_inj _⟩ _
+    · exact (Abelian.epiDesc f.unop _ (cokernel.condition (kernel.ι f.unop))).op
+    · exact (cokernel.desc _ _ (kernel.condition f.unop)).op
+    · rw [← cancel_epi (cokernel.π (kernel.ι f.unop))]
+      simp only [unop_comp, Quiver.Hom.unop_op, unop_id_op, cokernel.π_desc_assoc,
+        comp_epiDesc, Category.comp_id]
+    · simp only [← cancel_epi f.unop, unop_comp, Quiver.Hom.unop_op, unop_id, comp_epiDesc_assoc,
+        cokernel.π_desc, Category.comp_id]
+    · exact Quiver.Hom.unop_inj (by simp only [unop_comp, Quiver.Hom.unop_op, comp_epiDesc])
+  · change (kernelOrderHom X).comp (cokernelOrderHom X) = _
+    refine' OrderHom.ext _ _ (funext (Subobject.ind _ _))
+    intro A f hf
+    dsimp only [OrderHom.comp_coe, Function.comp_apply, cokernelOrderHom_coe, Subobject.lift_mk,
+      kernelOrderHom_coe, OrderHom.id_coe, id.def, unop_op, Quiver.Hom.unop_op]
+    refine' Subobject.mk_eq_mk_of_comm _ _ ⟨_, _, _, _⟩ _
+    · exact Abelian.monoLift f _ (kernel.condition (cokernel.π f))
+    · exact kernel.lift _ _ (cokernel.condition f)
+    · simp only [← cancel_mono (kernel.ι (cokernel.π f)), Category.assoc, image.fac, monoLift_comp,
+        Category.id_comp]
+    · simp only [← cancel_mono f, Category.assoc, monoLift_comp, image.fac, Category.id_comp]
+    · simp only [monoLift_comp]
+#align category_theory.abelian.subobject_iso_subobject_op CategoryTheory.Abelian.subobjectIsoSubobjectOp
+
+/-- A well-powered abelian category is also well-copowered. -/
+instance wellPowered_opposite [Abelian C] [WellPowered C] : WellPowered Cᵒᵖ
+    where subobject_small X :=
+    (small_congr (subobjectIsoSubobjectOp (unop X)).toEquiv).1 inferInstance
+#align category_theory.abelian.well_powered_opposite CategoryTheory.Abelian.wellPowered_opposite
+
+end CategoryTheory.Abelian