feat(algebra/category/*): forget reflects isos (#3600)

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

src/algebra/category/Algebra/basic.lean

@@ -109,3 +109,12 @@ def alg_equiv_iso_Algebra_iso {X Y : Type u}
 
 instance (X : Type u) [ring X] [algebra R X] : has_coe (subalgebra R X) (Algebra R) :=
 ⟨ λ N, Algebra.of R N ⟩
+
+instance Algebra.forget_reflects_isos : reflects_isomorphisms (forget (Algebra.{u} R)) :=
+{ reflects := λ X Y f _,
+  begin
+    resetI,
+    let i := as_iso ((forget (Algebra.{u} R)).map f),
+    let e : X ≃ₐ[R] Y := { ..f, ..i.to_equiv },
+    exact { ..e.to_Algebra_iso },
+  end }

src/algebra/category/CommRing/basic.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Johannes Hölzl, Yury Kudryashov
 -/
 import algebra.category.Group.basic
-import category_theory.reflect_isomorphisms
 import data.equiv.ring
 
 /-!
@@ -153,16 +152,6 @@ variables {X Y : Type u}
 
 end ring_equiv
 
-namespace Ring
-
-instance : reflects_isomorphisms (forget₂ Ring AddCommGroup) :=
-{ reflects := λ R S f i, by exactI
-  { ..ring_equiv.to_Ring_iso
-    { ..(as_iso ((forget₂ Ring AddCommGroup).map f)).AddCommGroup_iso_to_add_equiv,
-      ..f } } }
-
-end Ring
-
 namespace category_theory.iso
 
 /-- Build a `ring_equiv` from an isomorphism in the category `Ring`. -/
@@ -196,3 +185,23 @@ def ring_equiv_iso_CommRing_iso {X Y : Type u} [comm_ring X] [comm_ring Y] :
   (X ≃+* Y) ≅ (CommRing.of X ≅ CommRing.of Y) :=
 { hom := λ e, e.to_CommRing_iso,
   inv := λ i, i.CommRing_iso_to_ring_equiv, }
+
+instance Ring.forget_reflects_isos : reflects_isomorphisms (forget Ring.{u}) :=
+{ reflects := λ X Y f _,
+  begin
+    resetI,
+    let i := as_iso ((forget Ring).map f),
+    let e : X ≃+* Y := { ..f, ..i.to_equiv },
+    exact { ..e.to_Ring_iso },
+  end }
+
+instance CommRing.forget_reflects_isos : reflects_isomorphisms (forget CommRing.{u}) :=
+{ reflects := λ X Y f _,
+  begin
+    resetI,
+    let i := as_iso ((forget CommRing).map f),
+    let e : X ≃+* Y := { ..f, ..i.to_equiv },
+    exact { ..e.to_CommRing_iso },
+  end }
+
+example : reflects_isomorphisms (forget₂ Ring AddCommGroup) := by apply_instance

src/algebra/category/Group/adjunctions.lean

@@ -3,7 +3,7 @@ Copyright (c) 2019 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Johannes Hölzl
 -/
-import algebra.category.Group
+import algebra.category.Group.basic
 import group_theory.free_abelian_group
 
 /-!

src/algebra/category/Group/basic.lean

@@ -253,3 +253,23 @@ def mul_equiv_perm {α : Type u} : Aut α ≃* equiv.perm α :=
 iso_perm.Group_iso_to_mul_equiv
 
 end category_theory.Aut
+
+@[to_additive]
+instance Group.forget_reflects_isos : reflects_isomorphisms (forget Group.{u}) :=
+{ reflects := λ X Y f _,
+  begin
+    resetI,
+    let i := as_iso ((forget Group).map f),
+    let e : X ≃* Y := { ..f, ..i.to_equiv },
+    exact { ..e.to_Group_iso },
+  end }
+
+@[to_additive]
+instance CommGroup.forget_reflects_isos : reflects_isomorphisms (forget CommGroup.{u}) :=
+{ reflects := λ X Y f _,
+  begin
+    resetI,
+    let i := as_iso ((forget CommGroup).map f),
+    let e : X ≃* Y := { ..f, ..i.to_equiv },
+    exact { ..e.to_CommGroup_iso },
+  end }

src/algebra/category/Group/images.lean

@@ -3,7 +3,9 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import algebra.category.Group
+import algebra.category.Group.basic
+import category_theory.limits.shapes.images
+import category_theory.limits.types
 
 /-!
 # The category of commutative additive groups has images.

src/algebra/category/Mon/basic.lean

@@ -3,7 +3,8 @@ Copyright (c) 2018 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import category_theory.concrete_category
+import category_theory.concrete_category.bundled_hom
+import category_theory.concrete_category.reflects_isomorphisms
 import algebra.punit_instances
 
 /-!
@@ -182,3 +183,30 @@ def mul_equiv_iso_CommMon_iso {X Y : Type u} [comm_monoid X] [comm_monoid Y] :
   (X ≃* Y) ≅ (CommMon.of X ≅ CommMon.of Y) :=
 { hom := λ e, e.to_CommMon_iso,
   inv := λ i, i.CommMon_iso_to_mul_equiv, }
+
+@[to_additive]
+instance Mon.forget_reflects_isos : reflects_isomorphisms (forget Mon.{u}) :=
+{ reflects := λ X Y f _,
+  begin
+    resetI,
+    let i := as_iso ((forget Mon).map f),
+    let e : X ≃* Y := { ..f, ..i.to_equiv },
+    exact { ..e.to_Mon_iso },
+  end }
+
+@[to_additive]
+instance CommMon.forget_reflects_isos : reflects_isomorphisms (forget CommMon.{u}) :=
+{ reflects := λ X Y f _,
+  begin
+    resetI,
+    let i := as_iso ((forget CommMon).map f),
+    let e : X ≃* Y := { ..f, ..i.to_equiv },
+    exact { ..e.to_CommMon_iso },
+  end }
+
+/-!
+Once we've shown that the forgetful functors to type reflect isomorphisms,
+we automatically obtain that the `forget₂` functors between our concrete categories
+reflect isomorphisms.
+-/
+example : reflects_isomorphisms (forget₂ CommMon Mon) := by apply_instance

src/category_theory/concrete_category/reflects_isomorphisms.lean

@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2020 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import category_theory.concrete_category.basic
+import category_theory.reflects_isomorphisms
+
+/-!
+A `forget₂ C D` forgetful functor between concrete categories `C` and `D`
+whose forgetful functors both reflect isomorphisms, itself reflects isomorphisms.
+-/
+
+universes u
+
+open category_theory
+
+instance : reflects_isomorphisms (forget (Type u)) :=
+{ reflects := λ X Y f i, i }
+
+variables (C : Type (u+1)) [large_category C] [concrete_category C]
+variables (D : Type (u+1)) [large_category D] [concrete_category D]
+
+/--
+A `forget₂ C D` forgetful functor between concrete categories `C` and `D`
+where `forget C` reflects isomorphisms, itself reflects isomorphisms.
+-/
+@[priority 50] -- Even lower than the instance from `full` and `faithful`.
+instance [has_forget₂ C D] [reflects_isomorphisms (forget C)] :
+  reflects_isomorphisms (forget₂ C D) :=
+{ reflects := λ X Y f i,
+  begin
+    resetI,
+    haveI i' : is_iso ((forget D).map ((forget₂ C D).map f)) := functor.map_is_iso (forget D) _,
+    haveI : is_iso ((forget C).map f) :=
+    begin
+      have := has_forget₂.forget_comp,
+      dsimp at this,
+      rw ←this,
+      exact i',
+    end,
+    apply is_iso_of_reflects_iso f (forget C),
+  end }

src/category_theory/limits/cones.lean

@@ -5,6 +5,7 @@ Authors: Stephen Morgan, Scott Morrison, Floris van Doorn
 -/
 import category_theory.const
 import category_theory.yoneda
+import category_theory.reflects_isomorphisms
 
 universes v u u' -- declare the `v`'s first; see `category_theory.category` for an explanation
 
@@ -180,6 +181,16 @@ namespace cones
 { hom := { hom := φ.hom },
   inv := { hom := φ.inv, w' := λ j, φ.inv_comp_eq.mpr (w j) } }
 
+/--
+Given a cone morphism whose object part is an isomorphism, produce an
+isomorphism of cones.
+-/
+def cone_iso_of_hom_iso {K : J ⥤ C} {c d : cone K} (f : c ⟶ d) [i : is_iso f.hom] :
+  is_iso f :=
+{ inv :=
+  { hom := i.inv,
+    w' := λ j, (as_iso f.hom).inv_comp_eq.2 (f.w j).symm } }
+
 @[simps] def postcompose {G : J ⥤ C} (α : F ⟶ G) : cone F ⥤ cone G :=
 { obj := λ c, { X := c.X, π := c.π ≫ α },
   map := λ c₁ c₂ f, { hom := f.hom, w' :=
@@ -268,6 +279,20 @@ instance functoriality_full [full G] [faithful G] : full (functoriality F G) :=
 instance functoriality_faithful [faithful G] : faithful (cones.functoriality F G) :=
 { map_injective' := λ X Y f g e, by { ext1, injection e, apply G.map_injective h_1 } }
 
+/--
+If `F` reflects isomorphisms, then `cones.functoriality F` reflects isomorphisms
+as well.
+-/
+instance reflects_cone_isomorphism (F : C ⥤ D) [reflects_isomorphisms F] (K : J ⥤ C) :
+  reflects_isomorphisms (cones.functoriality K F) :=
+begin
+  constructor,
+  introsI,
+  haveI : is_iso (F.map f.hom) := (cones.forget (K ⋙ F)).map_is_iso ((cones.functoriality K F).map f),
+  haveI := reflects_isomorphisms.reflects F f.hom,
+  apply cone_iso_of_hom_iso
+end
+
 end
 
 end cones
@@ -295,6 +320,16 @@ namespace cocones
 { hom := { hom := φ.hom },
   inv := { hom := φ.inv, w' := λ j, φ.comp_inv_eq.mpr (w j).symm } }
 
+/--
+Given a cocone morphism whose object part is an isomorphism, produce an
+isomorphism of cocones.
+-/
+def cocone_iso_of_hom_iso {K : J ⥤ C} {c d : cocone K} (f : c ⟶ d) [i : is_iso f.hom] :
+  is_iso f :=
+{ inv :=
+  { hom := i.inv,
+    w' := λ j, (as_iso f.hom).comp_inv_eq.2 (f.w j).symm } }
+
 @[simps] def precompose {G : J ⥤ C} (α : G ⟶ F) : cocone F ⥤ cocone G :=
 { obj := λ c, { X := c.X, ι := α ≫ c.ι },
   map := λ c₁ c₂ f, { hom := f.hom } }
@@ -381,6 +416,20 @@ instance functoriality_full [full G] [faithful G] : full (functoriality F G) :=
 instance functoriality_faithful [faithful G] : faithful (functoriality F G) :=
 { map_injective' := λ X Y f g e, by { ext1, injection e, apply G.map_injective h_1 } }
 
+/--
+If `F` reflects isomorphisms, then `cocones.functoriality F` reflects isomorphisms
+as well.
+-/
+instance reflects_cocone_isomorphism (F : C ⥤ D) [reflects_isomorphisms F] (K : J ⥤ C) :
+  reflects_isomorphisms (cocones.functoriality K F) :=
+begin
+  constructor,
+  introsI,
+  haveI : is_iso (F.map f.hom) := (cocones.forget (K ⋙ F)).map_is_iso ((cocones.functoriality K F).map f),
+  haveI := reflects_isomorphisms.reflects F f.hom,
+  apply cocone_iso_of_hom_iso
+end
+
 end
 end cocones
 

src/category_theory/limits/limits.lean

@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Reid Barton, Mario Carneiro, Scott Morrison, Floris van Doorn
 -/
 import category_theory.adjunction.basic
-import category_theory.reflect_isomorphisms
+import category_theory.limits.cones
+import category_theory.reflects_isomorphisms
 
 open category_theory category_theory.category category_theory.functor opposite
 
@@ -86,7 +87,7 @@ def of_point_iso {r t : cone F} (P : is_limit r) [i : is_iso (P.lift t)] : is_li
 of_iso_limit P
 begin
   haveI : is_iso (P.lift_cone_morphism t).hom := i,
-  haveI : is_iso (P.lift_cone_morphism t) := cone_iso_of_hom_iso _,
+  haveI : is_iso (P.lift_cone_morphism t) := cones.cone_iso_of_hom_iso _,
   symmetry,
   apply as_iso (P.lift_cone_morphism t),
 end
@@ -397,7 +398,7 @@ def of_point_iso {r t : cocone F} (P : is_colimit r) [i : is_iso (P.desc t)] : i
 of_iso_colimit P
 begin
   haveI : is_iso (P.desc_cocone_morphism t).hom := i,
-  haveI : is_iso (P.desc_cocone_morphism t) := cocone_iso_of_hom_iso _,
+  haveI : is_iso (P.desc_cocone_morphism t) := cocones.cocone_iso_of_hom_iso _,
   apply as_iso (P.desc_cocone_morphism t),
 end
 

src/category_theory/monad/algebra.lean

@@ -5,7 +5,7 @@ Authors: Scott Morrison, Bhavik Mehta
 -/
 import category_theory.monad.basic
 import category_theory.adjunction.basic
-import category_theory.reflect_isomorphisms
+import category_theory.reflects_isomorphisms
 
 /-!
 # Eilenberg-Moore (co)algebras for a (co)monad

src/category_theory/over.lean

@@ -5,7 +5,7 @@ Authors: Johan Commelin
 -/
 import category_theory.comma
 import category_theory.punit
-import category_theory.reflect_isomorphisms
+import category_theory.reflects_isomorphisms
 
 /-!
 # Over and under categories