refactor(category_theory,algebra/category): make algebraic categories not [reducible] (#1491)

* refactor(category_theory,algebra/category): make algebraic categories not [reducible]

Adapted from part of #1438.

* Update src/algebra/category/CommRing/basic.lean

Co-Authored-By: Scott Morrison <scott@tqft.net>

* adding missing forget2 instances

* Converting Reid's comment to a [Note]

* adding examples testing coercions

Author: rwbarton

src/algebra/category/CommRing/basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Johannes Hölzl, Yury Kudryashov
 -/
 
-import algebra.category.Mon.basic
+import algebra.category.Group
 import category_theory.fully_faithful
 import algebra.ring
 import data.int.basic
@@ -18,103 +18,117 @@ We introduce the bundled categories:
 * `CommSemiRing`
 * `CommRing`
 along with the relevant forgetful functors between them.
+
+## Implementation notes
+
+See the note [locally reducible category instances].
+
 -/
 
 universes u v
 
 open category_theory
 
 /-- The category of semirings. -/
-@[reducible] def SemiRing : Type (u+1) := bundled semiring
+def SemiRing : Type (u+1) := bundled semiring
 
 namespace SemiRing
 
 /-- Construct a bundled SemiRing from the underlying type and typeclass. -/
 def of (R : Type u) [semiring R] : SemiRing := bundled.of R
 
+local attribute [reducible] SemiRing
+
+instance : has_coe_to_sort SemiRing := infer_instance
+
 instance (R : SemiRing) : semiring R := R.str
 
 instance bundled_hom : bundled_hom @ring_hom :=
 ⟨@ring_hom.to_fun, @ring_hom.id, @ring_hom.comp, @ring_hom.coe_inj⟩
 
-instance has_forget_to_Mon : has_forget₂ SemiRing.{u} Mon.{u} :=
-bundled_hom.mk_has_forget₂ @semiring.to_monoid (λ R₁ R₂ f, f.to_monoid_hom) (λ _ _ _, rfl)
+instance : concrete_category SemiRing := infer_instance
+
+instance has_forget_to_Mon : has_forget₂ SemiRing Mon :=
+bundled_hom.mk_has_forget₂ @semiring.to_monoid (λ R₁ R₂, ring_hom.to_monoid_hom) (λ _ _ _, rfl)
+instance has_forget_to_AddCommMon : has_forget₂ SemiRing AddCommMon :=
+-- can't use bundled_hom.mk_has_forget₂, since AddCommMon is an induced category
+{ forget₂ :=
+  { obj := λ R, AddCommMon.of R,
+    map := λ R₁ R₂ f, ring_hom.to_add_monoid_hom f } }
 
 end SemiRing
 
 /-- The category of rings. -/
-@[reducible] def Ring : Type (u+1) := bundled ring
+def Ring : Type (u+1) := induced_category SemiRing (bundled.map @ring.to_semiring)
 
 namespace Ring
 
-instance (R : Ring) : ring R := R.str
-
 /-- Construct a bundled Ring from the underlying type and typeclass. -/
 def of (R : Type u) [ring R] : Ring := bundled.of R
 
-instance bundled_hom : bundled_hom _ :=
-SemiRing.bundled_hom.full_subcategory @ring.to_semiring
+local attribute [reducible] Ring
+
+instance : has_coe_to_sort Ring := infer_instance
+
+instance (R : Ring) : ring R := R.str
+
+instance : concrete_category Ring := infer_instance
 
-instance has_forget_to_SemiRing : has_forget₂ Ring.{u} SemiRing.{u} :=
-SemiRing.bundled_hom.full_subcategory_has_forget₂ _
+instance has_forget_to_SemiRing : has_forget₂ Ring SemiRing := infer_instance
+instance has_forget_to_AddCommGroup : has_forget₂ Ring AddCommGroup :=
+-- can't use bundled_hom.mk_has_forget₂, since AddCommGroup is an induced category
+{ forget₂ :=
+  { obj := λ R, AddCommGroup.of R,
+    map := λ R₁ R₂ f, ring_hom.to_add_monoid_hom f } }
 
 end Ring
 
 /-- The category of commutative semirings. -/
-@[reducible] def CommSemiRing : Type (u+1) := bundled comm_semiring
+def CommSemiRing : Type (u+1) := induced_category SemiRing (bundled.map comm_semiring.to_semiring)
 
 namespace CommSemiRing
 
-instance (R : CommSemiRing) : comm_semiring R := R.str
-
 /-- Construct a bundled CommSemiRing from the underlying type and typeclass. -/
 def of (R : Type u) [comm_semiring R] : CommSemiRing := bundled.of R
 
-instance bundled_hom : bundled_hom _ :=
-SemiRing.bundled_hom.full_subcategory @comm_semiring.to_semiring
+local attribute [reducible] CommSemiRing
+
+instance : has_coe_to_sort CommSemiRing := infer_instance
+
+instance (R : CommSemiRing) : comm_semiring R := R.str
 
-instance has_forget_to_SemiRing : has_forget₂ CommSemiRing.{u} SemiRing.{u} :=
-bundled_hom.full_subcategory_has_forget₂ _ _
+instance : concrete_category CommSemiRing := infer_instance
+
+instance has_forget_to_SemiRing : has_forget₂ CommSemiRing SemiRing := infer_instance
 
 /-- The forgetful functor from commutative rings to (multiplicative) commutative monoids. -/
-instance has_forget_to_CommMon : has_forget₂ CommSemiRing.{u} CommMon.{u} :=
-bundled_hom.mk_has_forget₂
-  @comm_semiring.to_comm_monoid
-  (λ R₁ R₂ f, f.to_monoid_hom)
-  (by intros; refl)
+instance has_forget_to_CommMon : has_forget₂ CommSemiRing CommMon :=
+has_forget₂.mk'
+  (λ R : CommSemiRing, CommMon.of R) (λ R, rfl)
+  (λ R₁ R₂ f, f.to_monoid_hom) (by tidy)
 
 end CommSemiRing
 
 /-- The category of commutative rings. -/
-@[reducible] def CommRing : Type (u+1) := bundled comm_ring
+def CommRing : Type (u+1) := induced_category Ring (bundled.map comm_ring.to_ring)
 
 namespace CommRing
 
-instance (R : CommRing) : comm_ring R := R.str
-
 /-- Construct a bundled CommRing from the underlying type and typeclass. -/
 def of (R : Type u) [comm_ring R] : CommRing := bundled.of R
 
-instance bundled_hom : bundled_hom _ :=
-Ring.bundled_hom.full_subcategory @comm_ring.to_ring
+local attribute [reducible] CommRing
 
-@[simp] lemma id_eq (R : CommRing) : 𝟙 R = ring_hom.id R := rfl
-@[simp] lemma comp_eq {R₁ R₂ R₃ : CommRing} (f : R₁ ⟶ R₂) (g : R₂ ⟶ R₃) :
-  f ≫ g = g.comp f := rfl
+instance : has_coe_to_sort CommRing := infer_instance
+
+instance (R : CommRing) : comm_ring R := R.str
 
-@[simp] lemma forget_obj_eq_coe {R : CommRing} : (forget CommRing).obj R = R := rfl
-@[simp] lemma forget_map_eq_coe {R₁ R₂ : CommRing} (f : R₁ ⟶ R₂) :
-  (forget CommRing).map f = f :=
-rfl
+instance : concrete_category CommRing := infer_instance
 
-instance has_forget_to_Ring : has_forget₂ CommRing.{u} Ring.{u} :=
-by apply bundled_hom.full_subcategory_has_forget₂
+instance has_forget_to_Ring : has_forget₂ CommRing Ring := infer_instance
 
 /-- The forgetful functor from commutative rings to (multiplicative) commutative monoids. -/
-instance has_forget_to_CommSemiRing : has_forget₂ CommRing.{u} CommSemiRing.{u} :=
-bundled_hom.mk_has_forget₂
-  @comm_ring.to_comm_semiring
-  (λ _ _, id)
-  (by intros; refl)
+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)
 
 end CommRing

src/algebra/category/CommRing/colimits.lean

@@ -320,7 +320,7 @@ begin
     -- trans
     { exact eq.trans r_ih_h r_ih_k },
     -- map
-    { rw cocone.naturality_bundled, },
+    { rw cocone.naturality_concrete, },
     -- zero
     { erw is_ring_hom.map_zero ⇑((s.ι).app r), refl },
     -- one

src/algebra/category/CommRing/limits.lean

@@ -31,7 +31,7 @@ variables {J : Type u} [small_category J]
 
 instance comm_ring_obj (F : J ⥤ CommRing.{u}) (j) :
   comm_ring ((F ⋙ forget CommRing).obj j) :=
-by { dsimp, apply_instance }
+by { change comm_ring (F.obj j), apply_instance }
 
 instance sections_submonoid (F : J ⥤ CommRing.{u}) :
   is_submonoid (F ⋙ forget CommRing).sections :=

src/algebra/category/Group.lean

@@ -16,61 +16,71 @@ We introduce the bundled categories:
 * `CommGroup`
 * `AddCommGroup`
 along with the relevant forgetful functors between them, and to the bundled monoid categories.
+
+## Implementation notes
+
+See the note [locally reducible category instances].
 -/
 
 universes u v
 
 open category_theory
 
 /-- The category of groups and group morphisms. -/
-@[reducible, to_additive AddGroup]
-def Group : Type (u+1) := bundled group
+@[to_additive AddGroup]
+def Group : Type (u+1) := induced_category Mon (bundled.map group.to_monoid)
 
 namespace Group
 
-@[to_additive add_group]
-instance (G : Group) : group G := G.str
-
 /-- Construct a bundled Group from the underlying type and typeclass. -/
 @[to_additive] def of (X : Type u) [group X] : Group := bundled.of X
 
+local attribute [reducible] Group
+
 @[to_additive]
-instance bundled_hom : bundled_hom _ :=
-Mon.bundled_hom.full_subcategory @group.to_monoid
+instance : has_coe_to_sort Group := infer_instance
+
+@[to_additive add_group]
+instance (G : Group) : group G := G.str
 
 @[to_additive]
 instance : has_one Group := ⟨Group.of punit⟩
 
+@[to_additive]
+instance : concrete_category Group := infer_instance
+
 @[to_additive has_forget_to_AddMon]
-instance has_forget_to_Mon : has_forget₂ Group.{u} Mon.{u} :=
-Mon.bundled_hom.full_subcategory_has_forget₂ _
+instance has_forget_to_Mon : has_forget₂ Group Mon := infer_instance
 
 end Group
 
 
 /-- The category of commutative groups and group morphisms. -/
-@[reducible, to_additive AddCommGroup]
-def CommGroup : Type (u+1) := bundled comm_group
+@[to_additive AddCommGroup]
+def CommGroup : Type (u+1) := induced_category Group (bundled.map comm_group.to_group)
 
 namespace CommGroup
 
+/-- Construct a bundled CommGroup from the underlying type and typeclass. -/
+@[to_additive] def of (G : Type u) [comm_group G] : CommGroup := bundled.of G
+
+local attribute [reducible] CommGroup
+
+@[to_additive]
+instance : has_coe_to_sort CommGroup := infer_instance
+
 @[to_additive add_comm_group]
 instance (G : CommGroup) : comm_group G := G.str
 
-/-- Construct a bundled CommGroup from the underlying type and typeclass. -/
-@[to_additive] def of (G : Type u) [comm_group G] : CommGroup := bundled.of G
+@[to_additive] instance : has_one CommGroup := ⟨CommGroup.of punit⟩
 
-@[to_additive] instance : bundled_hom _ :=
-Group.bundled_hom.full_subcategory @comm_group.to_group
+@[to_additive] instance : concrete_category CommGroup := infer_instance
 
 @[to_additive has_forget_to_AddGroup]
-instance has_forget_to_Group : has_forget₂ CommGroup.{u} Group.{u} :=
-Group.bundled_hom.full_subcategory_has_forget₂ _
+instance has_forget_to_Group : has_forget₂ CommGroup Group := infer_instance
 
 @[to_additive has_forget_to_AddCommMon]
-instance has_forget_to_CommMon : has_forget₂ CommGroup.{u} CommMon.{u} :=
-CommMon.bundled_hom.full_subcategory_has_forget₂ comm_group.to_comm_monoid
-
-@[to_additive] instance : has_one CommGroup := ⟨CommGroup.of punit⟩
+instance has_forget_to_CommMon : has_forget₂ CommGroup CommMon :=
+induced_category.has_forget₂ (λ G : CommGroup, CommMon.of G)
 
 end CommGroup

src/algebra/category/Mon/basic.lean

@@ -16,50 +16,87 @@ We introduce the bundled categories:
 * `CommMon`
 * `AddCommMon`
 along with the relevant forgetful functors between them.
+
+## Implementation notes
+
+### Note [locally reducible category instances]
+
+We make SemiRing (and the other categories) locally reducible in order
+to define its instances. This is because writing, for example,
+
+  instance : concrete_category SemiRing := by { delta SemiRing, apply_instance }
+
+results in an instance of the form `id (bundled_hom.concrete_category _)`
+and this `id`, not being [reducible], prevents a later instance search
+(once SemiRing is no longer reducible) from seeing that the morphisms of
+SemiRing are really semiring morphisms (`→+*`), and therefore have a coercion
+to functions, for example. It's especially important that the `has_coe_to_sort`
+instance not contain an extra `id` as we want the `semiring ↥R` instance to
+also apply to `semiring R.α` (it seems to be impractical to guarantee that
+we always access `R.α` through the coercion rather than directly).
+
+TODO: Probably @[derive] should be able to create instances of the
+required form (without `id`), and then we could use that instead of
+this obscure `local attribute [reducible]` method.
 -/
 
 universes u v
 
 open category_theory
 
 /-- The category of monoids and monoid morphisms. -/
-@[reducible, to_additive AddMon]
+@[to_additive AddMon]
 def Mon : Type (u+1) := bundled monoid
 
 namespace Mon
 
-@[to_additive add_monoid]
-instance (x : Mon) : monoid x := x.str
-
 /-- Construct a bundled Mon from the underlying type and typeclass. -/
 @[to_additive]
 def of (M : Type u) [monoid M] : Mon := bundled.of M
 
+local attribute [reducible] Mon
+
+@[to_additive]
+instance : has_coe_to_sort Mon := infer_instance
+
+@[to_additive add_monoid]
+instance (M : Mon) : monoid M := M.str
+
 @[to_additive]
 instance bundled_hom : bundled_hom @monoid_hom :=
 ⟨@monoid_hom.to_fun, @monoid_hom.id, @monoid_hom.comp, @monoid_hom.coe_inj⟩
 
+@[to_additive]
+instance : concrete_category Mon := infer_instance
+
 end Mon
 
 /-- The category of commutative monoids and monoid morphisms. -/
-@[reducible, to_additive AddCommMon]
-def CommMon : Type (u+1) := bundled comm_monoid
+@[to_additive AddCommMon]
+def CommMon : Type (u+1) := induced_category Mon (bundled.map @comm_monoid.to_monoid)
 
 namespace CommMon
 
-@[to_additive add_comm_monoid]
-instance (x : CommMon) : comm_monoid x := x.str
-
 /-- Construct a bundled CommMon from the underlying type and typeclass. -/
 @[to_additive]
-def of (X : Type u) [comm_monoid X] : CommMon := bundled.of X
+def of (M : Type u) [comm_monoid M] : CommMon := bundled.of M
+
+local attribute [reducible] CommMon
 
 @[to_additive]
-instance bundled_hom : bundled_hom _ :=
-Mon.bundled_hom.full_subcategory @comm_monoid.to_monoid
+instance : has_coe_to_sort CommMon := infer_instance
+
+@[to_additive add_comm_monoid]
+instance (M : CommMon) : comm_monoid M := M.str
+
+@[to_additive]
+instance : concrete_category CommMon := infer_instance
 
 @[to_additive has_forget_to_AddMon]
-instance has_forget_to_Mon : has_forget₂ CommMon.{u} Mon.{u} :=
-Mon.bundled_hom.full_subcategory_has_forget₂ _
+instance has_forget_to_Mon : has_forget₂ CommMon Mon := infer_instance
 
 end CommMon
+
+-- We verify that the coercions of morphisms to functions work correctly:
+example {R S : Mon}     (f : R ⟶ S) : (R : Type) → (S : Type) := f
+example {R S : CommMon} (f : R ⟶ S) : (R : Type) → (S : Type) := f

src/algebra/category/Mon/colimits.lean

@@ -172,7 +172,7 @@ begin
     -- trans
     { exact eq.trans r_ih_h r_ih_k },
     -- map
-    { rw cocone.naturality_bundled, },
+    { rw cocone.naturality_concrete, },
     -- mul
     { rw is_monoid_hom.map_mul ⇑((s.ι).app r_j) },
     -- one