feat(category_theory, algebra/category): AddCommGroup is well-powered (#7006)

TwoFX · TwoFX · commit 29b834dfbba4 · 2021-04-09T03:28:24.000Z
diff --git a/src/algebra/category/Group/subobject.lean b/src/algebra/category/Group/subobject.lean
@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2021 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import algebra.category.Group.Z_Module_equivalence
+import algebra.category.Module.subobject
+
+/-!
+# The category of abelian groups is well-powered
+-/
+
+open category_theory
+
+universe u
+
+namespace AddCommGroup
+
+instance well_powered_AddCommGroup : well_powered (AddCommGroup.{u}) :=
+well_powered_of_equiv (forget₂ (Module.{u} ℤ) AddCommGroup.{u}).as_equivalence
+
+end AddCommGroup
diff --git a/src/category_theory/subobject/mono_over.lean b/src/category_theory/subobject/mono_over.lean
@@ -137,6 +137,12 @@ lemma lift_comm (F : over Y ⥤ over X)
   lift F h ⋙ mono_over.forget X = mono_over.forget Y ⋙ F :=
 rfl
 
+@[simp]
+lemma lift_obj_arrow {Y : D} (F : over Y ⥤ over X)
+  (h : ∀ (f : mono_over Y), mono (F.obj ((mono_over.forget Y).obj f)).hom) (f : mono_over Y) :
+  ((lift F h).obj f).arrow = (F.obj ((forget Y).obj f)).hom :=
+rfl
+
 /--
 Monomorphisms over an object `f : over A` in an over category
 are equivalent to monomorphisms over the source of `f`.
@@ -226,12 +232,26 @@ instance faithful_map (f : X ⟶ Y) [mono f] : faithful (map f) := {}.
 /--
 Isomorphic objects have equivalent `mono_over` categories.
 -/
-def map_iso {A B : C} (e : A ≅ B) : mono_over A ≌ mono_over B :=
+@[simps] def map_iso {A B : C} (e : A ≅ B) : mono_over A ≌ mono_over B :=
 { functor := map e.hom,
   inverse := map e.inv,
   unit_iso := ((map_comp _ _).symm ≪≫ eq_to_iso (by simp) ≪≫ map_id).symm,
   counit_iso := ((map_comp _ _).symm ≪≫ eq_to_iso (by simp) ≪≫ map_id) }
 
+section
+variables (X)
+
+/-- An equivalence of categories `e` between `C` and `D` induces an equivalence between
+    `mono_over X` and `mono_over (e.functor.obj X)` whenever `X` is an object of `C`. -/
+@[simps] def congr (e : C ≌ D) : mono_over X ≌ mono_over (e.functor.obj X) :=
+{ functor := lift (over.post e.functor) $ λ f, by { dsimp, apply_instance },
+  inverse := (lift (over.post e.inverse) $ λ f, by { dsimp, apply_instance })
+    ⋙ (map_iso (e.unit_iso.symm.app X)).functor,
+  unit_iso := nat_iso.of_components (λ Y, iso_mk (e.unit_iso.app Y) (by tidy)) (by tidy),
+  counit_iso := nat_iso.of_components (λ Y, iso_mk (e.counit_iso.app Y) (by tidy)) (by tidy) }
+
+end
+
 section
 variable [has_pullbacks C]
 
diff --git a/src/category_theory/subobject/well_powered.lean b/src/category_theory/subobject/well_powered.lean
@@ -24,11 +24,11 @@ and
 `equiv_shrink (subobject X) : subobject X ≃ shrink (subobject X)`.
 -/
 
-universes v u
+universes v u₁ u₂
 
 namespace category_theory
 
-variables (C : Type u) [category.{v} C]
+variables (C : Type u₁) [category.{v} C]
 
 /--
 A category (with morphisms in `Type v`) is well-powered if `subobject X` is `v`-small for every `X`.
@@ -43,7 +43,7 @@ instance small_subobject [well_powered C] (X : C) : small.{v} (subobject X) :=
 well_powered.subobject_small X
 
 @[priority 100]
-instance well_powered_of_small_category (C : Type u) [small_category C] : well_powered C :=
+instance well_powered_of_small_category (C : Type u₁) [small_category C] : well_powered C :=
 {}
 
 variables {C}
@@ -57,10 +57,27 @@ theorem well_powered_of_essentially_small_mono_over
   well_powered C :=
 { subobject_small := λ X, (essentially_small_mono_over_iff_small_subobject X).mp (h X), }
 
+section
 variables [well_powered C]
 
 instance essentially_small_mono_over (X : C) :
   essentially_small.{v} (mono_over X) :=
 (essentially_small_mono_over_iff_small_subobject X).mpr (well_powered.subobject_small X)
 
+end
+
+section equivalence
+variables {D : Type u₂} [category.{v} D]
+
+theorem well_powered_of_equiv (e : C ≌ D) [well_powered C] : well_powered D :=
+well_powered_of_essentially_small_mono_over $
+  λ X, (essentially_small_congr (mono_over.congr X e.symm)).2 $ by apply_instance
+
+/-- Being well-powered is preserved by equivalences, as long as the two categories involved have
+    their morphisms in the same universe. -/
+theorem well_powered_congr (e : C ≌ D) : well_powered C ↔ well_powered D :=
+⟨λ i, by exactI well_powered_of_equiv e, λ i, by exactI well_powered_of_equiv e.symm⟩
+
+end equivalence
+
 end category_theory
