refactor(algebra/category/*/limits): refactor concrete limits (#3463)

We used to construct categorical limits for `AddCommGroup` and `CommRing`.

Now we construct them for
* `(Add)(Comm)Mon`
* `(Add)(Comm)Group`
* `(Comm)(Semi)Ring`
* `Module R`
* `Algebra R`

Even better, we reuse structure along the way, and show that all the relevant forgetful functors preserve limits.

We're still not at the point were this can either be done by
* automation, or
* noticing that everything is a model of a Lawvere theory
but ... maybe one day.



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

Author: kim-em

src/algebra/category/Algebra/limits.lean

@@ -0,0 +1,134 @@
+/-
+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.Algebra.basic
+import algebra.category.Module.limits
+import algebra.category.CommRing.limits
+
+/-!
+# The category of R-algebras has all limits
+
+Further, these limits are preserved by the forgetful functor --- that is,
+the underlying types are just the limits in the category of types.
+-/
+
+open category_theory
+open category_theory.limits
+
+universe u
+
+namespace Algebra
+
+variables {R : Type u} [comm_ring R]
+variables {J : Type u} [small_category J]
+
+instance semiring_obj (F : J ⥤ Algebra R) (j) :
+  semiring ((F ⋙ forget (Algebra R)).obj j) :=
+by { change semiring (F.obj j), apply_instance }
+
+instance algebra_obj (F : J ⥤ Algebra R) (j) :
+  algebra R ((F ⋙ forget (Algebra R)).obj j) :=
+by { change algebra R (F.obj j), apply_instance }
+
+/--
+The flat sections of a functor into `Algebra R` form a submodule of all sections.
+-/
+def sections_subalgebra (F : J ⥤ Algebra R) :
+  subalgebra R (Π j, F.obj j) :=
+{ carrier := SemiRing.sections_subsemiring (F ⋙ forget₂ (Algebra R) Ring ⋙ forget₂ Ring SemiRing),
+  algebra_map_mem' := λ r j j' f, (F.map f).commutes r, }
+
+
+instance limit_semiring (F : J ⥤ Algebra R) :
+  ring (limit (F ⋙ forget (Algebra R))) :=
+begin
+  change ring (sections_subalgebra F),
+  apply_instance,
+end
+
+instance limit_algebra (F : J ⥤ Algebra R) :
+  algebra R (limit (F ⋙ forget (Algebra R))) :=
+begin
+  change algebra R (sections_subalgebra F),
+  apply_instance,
+end
+
+/-- `limit.π (F ⋙ forget (Algebra R)) j` as a `alg_hom`. -/
+def limit_π_alg_hom (F : J ⥤ Algebra R) (j) :
+  limit (F ⋙ forget (Algebra R)) →ₐ[R] (F ⋙ forget (Algebra R)).obj j :=
+{ commutes' := λ r, rfl,
+  ..SemiRing.limit_π_ring_hom (F ⋙ forget₂ (Algebra R) Ring ⋙ forget₂ Ring SemiRing) j }
+
+namespace has_limits
+-- The next two definitions are used in the construction of `has_limits (Algebra R)`.
+-- After that, the limits should be constructed using the generic limits API,
+-- e.g. `limit F`, `limit.cone F`, and `limit.is_limit F`.
+
+/--
+Construction of a limit cone in `Algebra R`.
+(Internal use only; use the limits API.)
+-/
+def limit (F : J ⥤ Algebra R) : cone F :=
+{ X := Algebra.of R (limit (F ⋙ forget _)),
+  π :=
+  { app := limit_π_alg_hom F,
+    naturality' := λ j j' f,
+      alg_hom.coe_fn_inj ((limit.cone (F ⋙ forget _)).π.naturality f) } }
+
+/--
+Witness that the limit cone in `Algebra R` is a limit cone.
+(Internal use only; use the limits API.)
+-/
+def limit_is_limit (F : J ⥤ Algebra R) : is_limit (limit F) :=
+begin
+  refine is_limit.of_faithful
+    (forget (Algebra R)) (limit.is_limit _)
+    (λ s, { .. }) (λ s, rfl),
+  { simp only [forget_map_eq_coe, alg_hom.map_one, functor.map_cone_π], refl, },
+  { intros x y, simp only [forget_map_eq_coe, alg_hom.map_mul, functor.map_cone_π], refl, },
+  { simp only [forget_map_eq_coe, alg_hom.map_zero, functor.map_cone_π], refl, },
+  { intros x y, simp only [forget_map_eq_coe, alg_hom.map_add, functor.map_cone_π], refl, },
+  { intros r, ext j, dsimp, erw (s.π.app j).commutes r, refl, },
+end
+
+end has_limits
+
+open has_limits
+
+/-- The category of R-algebras has all limits. -/
+instance has_limits : has_limits (Algebra R) :=
+{ has_limits_of_shape := λ J 𝒥,
+  { has_limit := λ F, by exactI
+    { cone     := limit F,
+      is_limit := limit_is_limit F } } }
+
+/--
+The forgetful functor from R-algebras to rings preserves all limits.
+-/
+instance forget₂_Ring_preserves_limits : preserves_limits (forget₂ (Algebra R) Ring) :=
+{ preserves_limits_of_shape := λ J 𝒥,
+  { preserves_limit := λ F,
+    by exactI preserves_limit_of_preserves_limit_cone
+      (limit.is_limit F) (limit.is_limit (F ⋙ forget₂ (Algebra R) Ring)) } }
+
+/--
+The forgetful functor from R-algebras to R-modules preserves all limits.
+-/
+instance forget₂_Module_preserves_limits : preserves_limits (forget₂ (Algebra R) (Module R)) :=
+{ preserves_limits_of_shape := λ J 𝒥,
+  { preserves_limit := λ F,
+    by exactI preserves_limit_of_preserves_limit_cone
+      (limit.is_limit F) (limit.is_limit (F ⋙ forget₂ (Algebra R) (Module R))) } }
+
+/--
+The forgetful functor from R-algebras to types preserves all limits.
+-/
+instance forget_preserves_limits : preserves_limits (forget (Algebra R)) :=
+{ preserves_limits_of_shape := λ J 𝒥,
+  { preserves_limit := λ F,
+    by exactI preserves_limit_of_preserves_limit_cone
+      (limit.is_limit F) (limit.is_limit (F ⋙ forget _)) } }
+
+end Algebra

src/algebra/category/CommRing/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, Johannes Hölzl, Yury Kudryashov
 -/
-import algebra.category.Group
+import algebra.category.Group.basic
+import category_theory.reflect_isomorphisms
 import data.equiv.ring
 
 /-!
@@ -124,6 +125,9 @@ instance has_forget_to_Ring : has_forget₂ CommRing Ring := bundled_hom.forget
 instance has_forget_to_CommSemiRing : has_forget₂ CommRing CommSemiRing :=
 has_forget₂.mk' (λ R : CommRing, CommSemiRing.of R) (λ R, rfl) (λ R₁ R₂ f, f) (by tidy)
 
+instance : full (forget₂ CommRing CommSemiRing) :=
+{ preimage := λ X Y f, f, }
+
 end CommRing
 
 -- This example verifies an improvement possible in Lean 3.8.
@@ -149,6 +153,16 @@ 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`. -/

src/algebra/category/CommRing/colimits.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import algebra.category.CommRing.basic
+import category_theory.limits.limits
+import category_theory.limits.concrete_category
 
 /-!
 # The category of commutative rings has all colimits.