From be63ea29b2a9081ef04d982c4ec6a0bb55f5506e Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Wed, 10 Aug 2022 10:23:29 +0000 Subject: [PATCH] feat(category_theory/abelian): equivalence between subobjects and quotients (#15494) --- src/category_theory/abelian/subobject.lean | 59 ++++++++++++++++++++++ src/category_theory/subobject/basic.lean | 37 ++++++++++++++ src/category_theory/subobject/limits.lean | 45 +++++++++++++++++ 3 files changed, 141 insertions(+) create mode 100644 src/category_theory/abelian/subobject.lean diff --git a/src/category_theory/abelian/subobject.lean b/src/category_theory/abelian/subobject.lean new file mode 100644 index 0000000000000..7f5afbcfaa553 --- /dev/null +++ b/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 diff --git a/src/category_theory/subobject/basic.lean b/src/category_theory/subobject/basic.lean index 46565079d87dd..10c301af39121 100644 --- a/src/category_theory/subobject/basic.lean +++ b/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. -/ diff --git a/src/category_theory/subobject/limits.lean b/src/category_theory/subobject/limits.lean index e880716772f18..3bc6056120a1c 100644 --- a/src/category_theory/subobject/limits.lean +++ b/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