feat(order/category/DecLinOrder): updates to concrete_category, and instances for order categories

src/algebra/category/CommRing/adjunctions.lean

@@ -31,7 +31,7 @@ def free : Type u ⥤ CommRing.{u} :=
 { obj := λ α, of (mv_polynomial α ℤ),
   -- TODO this should just be `ring_hom.of (rename f)`, but this causes a mysterious deterministic timeout!
   map := λ X Y f, @ring_hom.of _ _ _ _ (rename f) (by apply_instance),
-  -- TODO these next two fields can be done by `tidy`, but the calls in `dsimp` and `simp` it generates are too slow.
+  -- TODO these next two fields can be done by `tidy`, but the calls in `dsimp` and `simp` it generates are rather slow.
   map_id' := λ X, ring_hom.ext $ funext $ rename_id,
   map_comp' := λ X Y Z f g, ring_hom.ext $ funext $ λ p, (rename_rename f g p).symm }
 
@@ -41,12 +41,19 @@ def free : Type u ⥤ CommRing.{u} :=
 @[simp] lemma free_map_coe {α β : Type u} {f : α → β} :
   ⇑(free.map f) = rename f := rfl
 
+namespace adj
+-- The next two definitions are (unfortunate) "implementation details", helping the elaborator / typeclass search.
+def hom_equiv (X : Type u) (R : CommRing) := hom_equiv R X
+instance (R : CommRing) : is_ring_hom (λ (n : ℤ), (n : R)) := by tidy
+end adj
+open adj
+
 /--
 The free-forgetful adjunction for commutative rings.
 -/
-def adj : free ⊣ forget CommRing :=
+def adj : free ⊣ forget CommRing.{u} :=
 adjunction.mk_of_hom_equiv
-{ hom_equiv := λ X R, hom_equiv,
-  hom_equiv_naturality_left_symm' := by {intros, ext, dsimp, apply eval₂_cast_comp} }
+{ hom_equiv := λ X R, hom_equiv X R,
+  hom_equiv_naturality_left_symm' := by { intros, ext, dsimp, apply eval₂_cast_comp } }
 
 end CommRing

src/algebra/category/CommRing/basic.lean

@@ -32,89 +32,70 @@ namespace SemiRing
 /-- Construct a bundled SemiRing from the underlying type and typeclass. -/
 def of (R : Type u) [semiring R] : SemiRing := bundled.of R
 
-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.ext⟩
 
+instance (R : SemiRing) : semiring R := R.str
+
 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)
 
 end SemiRing
 
 /-- The category of rings. -/
-@[reducible] def Ring : Type (u+1) := bundled ring
+@[reducible] def Ring : Type (u+1) := induced_category SemiRing (bundled.map @ring.to_semiring.{u})
 
 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
+instance (R : Ring) : ring R := R.str
 
-instance has_forget_to_SemiRing : has_forget₂ Ring.{u} SemiRing.{u} :=
-SemiRing.bundled_hom.full_subcategory_has_forget₂ _
+example : concrete_category Ring.{u} := infer_instance
+example : has_forget₂ Ring.{u} SemiRing.{u} := infer_instance
 
 end Ring
 
 /-- The category of commutative semirings. -/
-@[reducible] def CommSemiRing : Type (u+1) := bundled comm_semiring
+@[reducible] def CommSemiRing : Type (u+1) := induced_category SemiRing (bundled.map comm_semiring.to_semiring.{u})
 
 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
+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₂ _ _
+-- These examples verify that we have successfully provided the expected instances.
+example : concrete_category CommSemiRing.{u} := infer_instance
+example : has_forget₂ CommSemiRing.{u} SemiRing.{u} := 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)
+has_forget₂.mk'
+  (λ R : CommSemiRing.{u}, 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
+-- TODO experiment with making @[reducible] local
+@[reducible] def CommRing : Type (u+1) := induced_category Ring (bundled.map comm_ring.to_ring.{u})
 
 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
-
-@[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
-
-@[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 (R : CommRing) : comm_ring R := R.str
 
-instance has_forget_to_Ring : has_forget₂ CommRing.{u} Ring.{u} :=
-by apply bundled_hom.full_subcategory_has_forget₂
+-- These examples verify that we have successfully provided the expected instances.
+example : concrete_category CommRing.{u} := infer_instance
+example : has_forget₂ CommRing.{u} Ring.{u} := infer_instance
 
-/-- The forgetful functor from commutative rings to (multiplicative) commutative monoids. -/
+/-- The forgetful functor from commutative rings to commutative semirings. -/
 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)
+has_forget₂.mk' (λ R : CommRing.{u}, CommSemiRing.of R) (λ R, rfl) (λ R₁ R₂ f, f) (by tidy)
 
 end CommRing

src/algebra/category/CommRing/colimits.lean

@@ -53,7 +53,7 @@ variables {J : Type v} [small_category J] (F : J ⥤ CommRing.{v})
 
 inductive prequotient
 -- There's always `of`
-| of : Π (j : J) (x : (F.obj j).α), prequotient
+| of : Π (j : J) (x : F.obj j), prequotient
 -- Then one generator for each operation
 | zero {} : prequotient
 | one {} : prequotient
@@ -69,13 +69,13 @@ inductive relation : prequotient F → prequotient F → Prop
 | symm : Π (x y) (h : relation x y), relation y x
 | trans : Π (x y z) (h : relation x y) (k : relation y z), relation x z
 -- There's always a `map` relation
-| map : Π (j j' : J) (f : j ⟶ j') (x : (F.obj j).α), relation (of j' (F.map f x)) (of j x)
+| map : Π (j j' : J) (f : j ⟶ j') (x : F.obj j), relation (of j' (F.map f x)) (of j x)
 -- Then one relation per operation, describing the interaction with `of`
 | zero : Π (j), relation (of j 0) zero
 | one : Π (j), relation (of j 1) one
-| neg : Π (j) (x : (F.obj j).α), relation (of j (-x)) (neg (of j x))
-| add : Π (j) (x y : (F.obj j).α), relation (of j (x + y)) (add (of j x) (of j y))
-| mul : Π (j) (x y : (F.obj j).α), relation (of j (x * y)) (mul (of j x) (of j y))
+| neg : Π (j) (x : F.obj j), relation (of j (-x)) (neg (of j x))
+| add : Π (j) (x y : F.obj j), relation (of j (x + y)) (add (of j x) (of j y))
+| mul : Π (j) (x y : F.obj j), relation (of j (x * y)) (mul (of j x) (of j y))
 -- Then one relation per argument of each operation
 | neg_1 : Π (x x') (r : relation x x'), relation (neg x) (neg x')
 | add_1 : Π (x x' y) (r : relation x x'), relation (add x y) (add x' y)
@@ -272,7 +272,7 @@ instance : comm_ring (colimit_type F) :=
 
 def colimit : CommRing := CommRing.of (colimit_type F)
 
-def cocone_fun (j : J) (x : (F.obj j).α) : colimit_type F :=
+def cocone_fun (j : J) (x : F.obj j) : colimit_type F :=
 quot.mk _ (of j x)
 
 def cocone_morphism (j : J) : F.obj j ⟶ colimit F :=
@@ -296,8 +296,7 @@ by { rw ←cocone_naturality F f, refl }
 
 def colimit_cocone : cocone F :=
 { X := colimit F,
-  ι :=
-  { app := cocone_morphism F } }.
+  ι := { app := cocone_morphism F } }.
 
 @[simp] def desc_fun_lift (s : cocone F) : prequotient F → s.X
 | (of j x)  := (s.ι.app j) x
@@ -320,17 +319,17 @@ begin
     -- trans
     { exact eq.trans r_ih_h r_ih_k },
     -- map
-    { rw cocone.naturality_bundled, },
+    { apply cocone.naturality_bundled', },
     -- zero
-    { erw is_ring_hom.map_zero ⇑((s.ι).app r), refl },
+    { exact ((s.ι).app r).map_zero, }, -- TODO why doesn't `simp only [ring_hom.map_zero]` work?
     -- one
-    { erw is_ring_hom.map_one ⇑((s.ι).app r), refl },
+    { exact ((s.ι).app r).map_one },
     -- neg
-    { rw is_ring_hom.map_neg ⇑((s.ι).app r_j) },
+    { simp only [ring_hom.map_neg], },
     -- add
-    { rw is_ring_hom.map_add ⇑((s.ι).app r_j) },
+    { simp only [ring_hom.map_add], },
     -- mul
-    { rw is_ring_hom.map_mul ⇑((s.ι).app r_j) },
+    { simp only [ring_hom.map_mul], },
     -- neg_1
     { rw r_ih, },
     -- add_1
@@ -384,23 +383,14 @@ def colimit_is_colimit : is_colimit (colimit_cocone F) :=
       erw w',
       refl, },
     { simp only [desc_morphism, quot_zero],
-      erw is_ring_hom.map_zero ⇑m,
+      erw m.map_zero, -- TODO why doesn't simp only [ring_hom.map_zero] work?
       refl, },
     { simp only [desc_morphism, quot_one],
-      erw is_ring_hom.map_one ⇑m,
-      refl, },
-    { simp only [desc_morphism, quot_neg],
-      erw is_ring_hom.map_neg ⇑m,
-      rw [x_ih],
-      refl, },
-    { simp only [desc_morphism, quot_add],
-      erw is_ring_hom.map_add ⇑m,
-      rw [x_ih_a, x_ih_a_1],
-      refl, },
-    { simp only [desc_morphism, quot_mul],
-      erw is_ring_hom.map_mul ⇑m,
-      rw [x_ih_a, x_ih_a_1],
+      erw m.map_one,
       refl, },
+    { simp only [desc_morphism, quot_neg, ring_hom.map_neg, x_ih], },
+    { simp only [desc_morphism, quot_add, ring_hom.map_add, x_ih_a, x_ih_a_1], },
+    { simp only [desc_morphism, quot_mul, ring_hom.map_mul, x_ih_a, x_ih_a_1], },
     refl
   end }.
 

src/algebra/category/CommRing/limits.lean

@@ -12,7 +12,7 @@ import algebra.pi_instances
 /-!
 # The category of commutative rings has all limits
 
-Further, these limits are preserves by the forgetful functor --- that is,
+Further, these limits are preserved by the forgetful functor --- that is,
 the underlying types are just the limits in the category of types.
 
 ## Further work
@@ -71,10 +71,10 @@ instance sections_add_subgroup (F : J ⥤ CommRing.{u}) :
   is_add_subgroup (F ⋙ forget CommRing).sections :=
 { neg_mem := λ a ah j j' f,
   begin
-    erw [functor.comp_map, forget_map_eq_coe, (F.map f).map_neg],
+    dsimp,
     dsimp [functor.sections] at ah,
-    rw ah f,
-    refl,
+    -- pi.neg_apply is hard to use as a `simp` lemma; you need to specify the arguments by hand
+    simp only [ring_hom.map_neg, pi.neg_apply a j, pi.neg_apply a j', neg_inj', ah],
   end,
   ..(CommRing.sections_add_submonoid F) }
 
@@ -88,24 +88,26 @@ instance limit_comm_ring (F : J ⥤ CommRing.{u}) :
 @subtype.comm_ring ((Π (j : J), (F ⋙ forget _).obj j)) (by apply_instance) _
   (by convert (CommRing.sections_subring F))
 
-instance limit_π_is_ring_hom (F : J ⥤ CommRing.{u}) (j) :
-  is_ring_hom (limit.π (F ⋙ forget CommRing) j) :=
+instance limit_π_is_semiring_hom (F : J ⥤ CommRing.{u}) (j) :
+  is_semiring_hom (limit.π (F ⋙ forget CommRing) j) :=
 { map_one := by { simp only [types.types_limit_π], refl },
+  map_zero := by { simp only [types.types_limit_π], refl },
   map_mul := λ x y, by { simp only [types.types_limit_π], refl },
   map_add := λ x y, by { simp only [types.types_limit_π], refl } }
 
+namespace CommRing_has_limits
 -- The next two definitions are used in the construction of `has_limits CommRing`.
 -- After that, the limits should be constructed using the generic limits API,
 -- e.g. `limit F`, `limit.cone F`, and `limit.is_limit F`.
 
-private def limit (F : J ⥤ CommRing.{u}) : cone F :=
+def limit (F : J ⥤ CommRing.{u}) : cone F :=
 { X := ⟨limit (F ⋙ forget _), by apply_instance⟩,
   π :=
   { app := λ j, ring_hom.of $ limit.π (F ⋙ forget _) j,
     naturality' := λ j j' f,
       ring_hom.ext ((limit.cone (F ⋙ forget _)).π.naturality f) } }
 
-private def limit_is_limit (F : J ⥤ CommRing.{u}) : is_limit (limit F) :=
+def limit_is_limit (F : J ⥤ CommRing.{u}) : is_limit (limit F) :=
 begin
   refine is_limit.of_faithful
     (forget CommRing) (limit.is_limit _)
@@ -120,6 +122,9 @@ begin
     erw (s.π.app j).map_add, refl }
 end
 
+end CommRing_has_limits
+open CommRing_has_limits
+
 /-- The category of commutative rings has all limits. -/
 instance CommRing_has_limits : has_limits.{u} CommRing.{u} :=
 { has_limits_of_shape := λ J 𝒥,

src/algebra/category/Group.lean

@@ -24,52 +24,45 @@ open category_theory
 
 /-- The category of groups and group morphisms. -/
 @[reducible, to_additive AddGroup]
-def Group : Type (u+1) := bundled group
+def Group : Type (u+1) := induced_category Mon (bundled.map group.to_monoid.{u})
 
 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
 
-@[to_additive]
-instance bundled_hom : bundled_hom _ :=
-Mon.bundled_hom.full_subcategory @group.to_monoid
+@[to_additive add_group]
+instance (G : Group) : group G := G.str
 
 @[to_additive]
 instance : has_one Group := ⟨Group.of punit⟩
 
-@[to_additive has_forget_to_AddMon]
-instance has_forget_to_Mon : has_forget₂ Group.{u} Mon.{u} :=
-Mon.bundled_hom.full_subcategory_has_forget₂ _
+-- These examples verify that we have successfully provided the expected instances.
+example : concrete_category Group.{u} := infer_instance
+example : has_forget₂ Group.{u} Mon.{u} := infer_instance
 
 end Group
 
 
 /-- The category of commutative groups and group morphisms. -/
 @[reducible, to_additive AddCommGroup]
-def CommGroup : Type (u+1) := bundled comm_group
+def CommGroup : Type (u+1) := induced_category Group (bundled.map comm_group.to_group.{u})
 
 namespace CommGroup
 
-@[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 : bundled_hom _ :=
-Group.bundled_hom.full_subcategory @comm_group.to_group
+@[to_additive add_comm_group]
+instance (G : CommGroup) : comm_group G := G.str
 
-@[to_additive has_forget_to_AddGroup]
-instance has_forget_to_Group : has_forget₂ CommGroup.{u} Group.{u} :=
-Group.bundled_hom.full_subcategory_has_forget₂ _
+-- These examples verify that we have successfully provided the expected instances.
+example : concrete_category CommGroup.{u} := infer_instance
+example : has_forget₂ CommGroup.{u} Group.{u} := 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
+induced_category.has_forget₂ (λ G : CommGroup, CommMon.of G)
 
 @[to_additive] instance : has_one CommGroup := ⟨CommGroup.of punit⟩