Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit b11f0f1

Browse files
urkudmergify[bot]
authored andcommitted
refactor(category_theory): refactor concrete categories (#1380)
* trying to use bundled homs * bundled monoids should use bundled homs * fixes * fixes * refactor(*): rewrite concrete categories * Add module documentation * local instance * Move files around; don't touch content yet * Move code around, fix some compile errors * Add `unbundled_hom.lean` * Turn `hom` into an argument of `(un)bundled_hom` For some reason, it helps Lean find coercions from `Ring` category morphisms to functions. * Define `unbundled_hom.mk_has_forget`; fix compile * Add some documentation * Fix compile * chore(category_theory): require morphisms live in Type * move back to Type * tweaks to doc-comments * fixing some formatting * Revert most of the changes to `data/mv_polynomials` * Drop unused argument, add a comment * Simplify universe levels in `concrete_category/basic`. Still fails to compile. * Simplify universe levels in `concrete_category/{un,}bundled_hom` * fixes * Fix an `import` * Doc cleanup * update post #1412 * Drop `simp` * Rename variable Co-Authored-By: Johan Commelin <johan@commelin.net> * Rename variable Co-Authored-By: Johan Commelin <johan@commelin.net> * Fix more issues reported by @rwbarton * Rename variable Co-Authored-By: Reid Barton <rwbarton@gmail.com> * Use `subtype.eq` instead of `subtype.ext.2` * Cleanup * Fix compile: now `ring_hom.ext` takes fewer explicit args * Fix compile * Run `sanity_check` on all files modified in this branch * Fix most of the issues reported * Except for the old ones in `mv_polynomial` (postponed to a separate PR) and a false positive in `single_obj` * Review `∀` vs `Π` * Remove some unnecessary parentheses * add comment * punit_instances: no need to explicitly provide constants and operations * Rename `has_forget` to `has_forget₂` * add comment, simplify comm_ring punit * Drop `private def free_obj` * documentation * fix comment * tweaks * comments * documentation on touched files * many doc-strings
1 parent 066d053 commit b11f0f1

34 files changed

+921
-514
lines changed

docs/references.bib

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -114,3 +114,13 @@ @book {riehl2017
114114
ISBN = {048680903X},
115115
URL = {http://www.math.jhu.edu/~eriehl/context.pdf},
116116
}
117+
118+
@article{ahrens2017,
119+
author = {Benedikt Ahrens and Peter LeFanu Lumsdaine},
120+
year = {2019},
121+
title = {Displayed Categories},
122+
journal = {Logical Methods in Computer Science},
123+
volume = {15},
124+
issue = {1},
125+
doi = {10.23638/LMCS-15(1:20)2019},
126+
}

src/algebra/category/CommRing/adjunctions.lean

Lines changed: 20 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -23,28 +23,30 @@ namespace CommRing
2323

2424
open_locale classical
2525

26-
private def free_obj (α : Type u) : CommRing.{u} := ⟨mv_polynomial α ℤ⟩
27-
26+
/--
27+
The free functor `Type u ⥤ CommRing.{u}` sending a type `X` to the multivariable (commutative)
28+
polynomials with variables `x : X`.
29+
-/
2830
def free : Type u ⥤ CommRing.{u} :=
29-
{ obj := free_obj,
30-
map := λ α β f, ⟨rename f, by apply_instance⟩, }
31+
{ obj := λ α, of (mv_polynomial α ℤ),
32+
-- TODO this should just be `ring_hom.of (rename f)`, but this causes a mysterious deterministic timeout!
33+
map := λ X Y f, @ring_hom.of _ _ _ _ (rename f) (by apply_instance),
34+
-- TODO these next two fields can be done by `tidy`, but the calls in `dsimp` and `simp` it generates are too slow.
35+
map_id' := λ X, ring_hom.ext $ funext $ rename_id,
36+
map_comp' := λ X Y Z f g, ring_hom.ext $ funext $ λ p, (rename_rename f g p).symm }
3137

32-
@[simp] lemma free_obj_α {α : Type u} :
33-
(free.obj α).α = mv_polynomial α ℤ := rfl
38+
@[simp] lemma free_obj_coe {α : Type u} :
39+
(free.obj α : Type u) = mv_polynomial α ℤ := rfl
3440

35-
@[simp] lemma free_map_val {α β : Type u} {f : α → β} :
36-
(free.map f).val = rename f := rfl
41+
@[simp] lemma free_map_coe {α β : Type u} {f : α → β} :
42+
(free.map f) = rename f := rfl
3743

38-
def hom_equiv (α : Type u) (R : CommRing.{u}) : (free.obj α ⟶ R) ≃ (α ⟶ forget.obj R) :=
39-
{ to_fun := λ f, f ∘ X,
40-
inv_fun := λ f, ⟨eval₂ (λ n : ℤ, (n : R)) f, by { unfold_coes, apply_instance }⟩,
41-
left_inv := λ f, bundled.hom_ext (@eval₂_hom_X _ _ _ _ _ f.val _),
42-
right_inv := λ x, by { ext1, unfold_coes, simp only [function.comp_app, eval₂_X] } }
43-
44-
def adj : free ⊣ (forget : CommRing ⥤ Type u) :=
44+
/--
45+
The free-forgetful adjunction for commutative rings.
46+
-/
47+
def adj : free ⊣ forget CommRing :=
4548
adjunction.mk_of_hom_equiv
46-
{ hom_equiv := hom_equiv,
47-
hom_equiv_naturality_left_symm' :=
48-
λ X X' Y f g, by { ext1, dsimp, apply eval₂_cast_comp } }.
49+
{ hom_equiv := λ X R, hom_equiv,
50+
hom_equiv_naturality_left_symm' := by {intros, ext, dsimp, apply eval₂_cast_comp} }
4951

5052
end CommRing
Lines changed: 79 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -1,86 +1,120 @@
1-
/- Copyright (c) 2018 Scott Morrison. All rights reserved.
1+
/-
2+
Copyright (c) 2018 Scott Morrison. All rights reserved.
23
Released under Apache 2.0 license as described in the file LICENSE.
3-
Authors: Scott Morrison, Johannes Hölzl
4-
5-
Introduce CommRing -- the category of commutative rings.
4+
Authors: Scott Morrison, Johannes Hölzl, Yury Kudryashov
65
-/
76

87
import algebra.category.Mon.basic
98
import category_theory.fully_faithful
109
import algebra.ring
1110
import data.int.basic
1211

12+
/-!
13+
# Category instances for semiring, ring, comm_semiring, and comm_ring.
14+
15+
We introduce the bundled categories:
16+
* `SemiRing`
17+
* `Ring`
18+
* `CommSemiRing`
19+
* `CommRing`
20+
along with the relevant forgetful functors between them.
21+
-/
22+
1323
universes u v
1424

1525
open category_theory
1626

27+
/-- The category of semirings. -/
28+
@[reducible] def SemiRing : Type (u+1) := bundled semiring
29+
30+
namespace SemiRing
31+
32+
/-- Construct a bundled SemiRing from the underlying type and typeclass. -/
33+
def of (R : Type u) [semiring R] : SemiRing := bundled.of R
34+
35+
instance (R : SemiRing) : semiring R := R.str
36+
37+
instance bundled_hom : bundled_hom @ring_hom :=
38+
⟨@ring_hom.to_fun, @ring_hom.id, @ring_hom.comp, @ring_hom.ext⟩
39+
40+
instance has_forget_to_Mon : has_forget₂ SemiRing.{u} Mon.{u} :=
41+
bundled_hom.mk_has_forget₂ @semiring.to_monoid (λ R₁ R₂ f, f.to_monoid_hom) (λ _ _ _, rfl)
42+
43+
end SemiRing
44+
1745
/-- The category of rings. -/
1846
@[reducible] def Ring : Type (u+1) := bundled ring
1947

20-
/-- The category of commutative rings. -/
21-
@[reducible] def CommRing : Type (u+1) := bundled comm_ring
22-
2348
namespace Ring
2449

25-
instance (x : Ring) : ring x := x.str
50+
instance (R : Ring) : ring R := R.str
2651

27-
instance concrete_is_ring_hom : concrete_category @is_ring_hom :=
28-
by introsI α ia; apply_instance,
29-
by introsI α β γ ia ib ic f g hf hg; apply_instance⟩
52+
/-- Construct a bundled Ring from the underlying type and typeclass. -/
53+
def of (R : Type u) [ring R] : Ring := bundled.of R
3054

31-
def of (α : Type u) [ring α] : Ring := ⟨α⟩
55+
instance bundled_hom : bundled_hom _ :=
56+
SemiRing.bundled_hom.full_subcategory @ring.to_semiring
3257

33-
abbreviation forget : Ring.{u} ⥤ Type u := forget
34-
35-
instance hom_is_ring_hom {R S : Ring} (f : R ⟶ S) : is_ring_hom (f : R → S) := f.2
58+
instance has_forget_to_SemiRing : has_forget₂ Ring.{u} SemiRing.{u} :=
59+
SemiRing.bundled_hom.full_subcategory_has_forget₂ _
3660

3761
end Ring
3862

39-
namespace CommRing
63+
/-- The category of commutative semirings. -/
64+
@[reducible] def CommSemiRing : Type (u+1) := bundled comm_semiring
4065

41-
instance (x : CommRing) : comm_ring x := x.str
66+
namespace CommSemiRing
4267

43-
abbreviation is_comm_ring_hom {α β} [comm_ring α] [comm_ring β] (f : α → β) : Prop :=
44-
is_ring_hom f
68+
instance (R : CommSemiRing) : comm_semiring R := R.str
4569

46-
instance concrete_is_comm_ring_hom : concrete_category @is_comm_ring_hom :=
47-
by introsI α ia; apply_instance,
48-
by introsI α β γ ia ib ic f g hf hg; apply_instance⟩
70+
/-- Construct a bundled CommSemiRing from the underlying type and typeclass. -/
71+
def of (R : Type u) [comm_semiring R] : CommSemiRing := bundled.of R
4972

50-
def of (α : Type u) [comm_ring α] : CommRing := ⟨α⟩
73+
instance bundled_hom : bundled_hom _ :=
74+
SemiRing.bundled_hom.full_subcategory @comm_semiring.to_semiring
5175

52-
abbreviation forget : CommRing.{u} ⥤ Type u := forget
76+
instance has_forget_to_SemiRing : has_forget₂ CommSemiRing.{u} SemiRing.{u} :=
77+
bundled_hom.full_subcategory_has_forget₂ _ _
5378

54-
instance hom_is_ring_hom {R S : CommRing} (f : R ⟶ S) : is_ring_hom (f : R → S) := f.2
79+
/-- The forgetful functor from commutative rings to (multiplicative) commutative monoids. -/
80+
instance has_forget_to_CommMon : has_forget₂ CommSemiRing.{u} CommMon.{u} :=
81+
bundled_hom.mk_has_forget₂
82+
@comm_semiring.to_comm_monoid
83+
(λ R₁ R₂ f, f.to_monoid_hom)
84+
(by intros; refl)
5585

56-
variables {R S T : CommRing.{u}}
86+
end CommSemiRing
5787

58-
-- TODO rename the next two definitions?
59-
def Int.cast {R : CommRing} : CommRing.of ℤ ⟶ R := { val := int.cast, property := by apply_instance }
88+
/-- The category of commutative rings. -/
89+
@[reducible] def CommRing : Type (u+1) := bundled comm_ring
6090

61-
def Int.hom_unique {R : CommRing} : unique (CommRing.of ℤ ⟶ R) :=
62-
{ default := Int.cast,
63-
uniq := λ f, subtype.ext.mpr $ funext $ int.eq_cast f f.2.map_one f.2.map_add }
91+
namespace CommRing
6492

65-
instance forget.faithful : faithful (forget) := {}
93+
instance (R : CommRing) : comm_ring R := R.str
6694

67-
instance forget_comm_ring (R : CommRing) : comm_ring (forget.obj R) := R.str
68-
instance forget_is_ring_hom {R S : CommRing} (f : R ⟶ S) : is_ring_hom (forget.map f) := f.property
95+
/-- Construct a bundled CommRing from the underlying type and typeclass. -/
96+
def of (R : Type u) [comm_ring R] : CommRing := bundled.of R
6997

70-
/-- The functor from commutative rings to rings. -/
71-
def to_Ring : CommRing.{u} ⥤ Ring.{u} :=
72-
{ obj := λ X, { α := X.1 },
73-
map := λ X Y f, ⟨ f, by apply_instance ⟩ }
98+
instance bundled_hom : bundled_hom _ :=
99+
Ring.bundled_hom.full_subcategory @comm_ring.to_ring
74100

75-
instance to_Ring.faithful : faithful (to_Ring) := {}
101+
@[simp] lemma id_eq (R : CommRing) : 𝟙 R = ring_hom.id R := rfl
102+
@[simp] lemma comp_eq {R₁ R₂ R₃ : CommRing} (f : R₁ ⟶ R₂) (g : R₂ ⟶ R₃) :
103+
f ≫ g = g.comp f := rfl
76104

77-
/-- The forgetful functor from commutative rings to (multiplicative) commutative monoids. -/
78-
def forget_to_CommMon : CommRing.{u} ⥤ CommMon.{u} :=
79-
{ obj := λ X, { α := X.1 },
80-
map := λ X Y f, ⟨ f, by apply_instance ⟩ }
105+
@[simp] lemma forget_obj_eq_coe {R : CommRing} : (forget CommRing).obj R = R := rfl
106+
@[simp] lemma forget_map_eq_coe {R₁ R₂ : CommRing} (f : R₁ ⟶ R₂) :
107+
(forget CommRing).map f = f :=
108+
rfl
81109

82-
instance forget_to_CommMon.faithful : faithful (forget_to_CommMon) := {}
110+
instance has_forget_to_Ring : has_forget₂ CommRing.{u} Ring.{u} :=
111+
by apply bundled_hom.full_subcategory_has_forget₂
83112

84-
example : faithful (forget_to_CommMon ⋙ CommMon.forget_to_Mon) := by apply_instance
113+
/-- The forgetful functor from commutative rings to (multiplicative) commutative monoids. -/
114+
instance has_forget_to_CommSemiRing : has_forget₂ CommRing.{u} CommSemiRing.{u} :=
115+
bundled_hom.mk_has_forget₂
116+
@comm_ring.to_comm_semiring
117+
(λ _ _, id)
118+
(by intros; refl)
85119

86120
end CommRing

src/algebra/category/CommRing/colimits.lean

Lines changed: 22 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,14 @@ Authors: Scott Morrison
66
import algebra.category.CommRing.basic
77
import category_theory.limits.limits
88

9+
/-!
10+
# The category of commutative rings has all colimits.
11+
12+
This file uses a "pre-automated" approach, just as for `Mon/colimits.lean`.
13+
It is a very uniform approach, that conceivably could be synthesised directly
14+
by a tactic that analyses the shape of `comm_ring` and `ring_hom`.
15+
-/
16+
917
universes u v
1018

1119
open category_theory
@@ -14,6 +22,7 @@ open category_theory.limits
1422
-- [ROBOT VOICE]:
1523
-- You should pretend for now that this file was automatically generated.
1624
-- It follows the same template as colimits in Mon.
25+
-- Note that this means this file does not meet documentation standards.
1726
/-
1827
`#print comm_ring` says:
1928
@@ -60,7 +69,7 @@ inductive relation : prequotient F → prequotient F → Prop
6069
| symm : Π (x y) (h : relation x y), relation y x
6170
| trans : Π (x y z) (h : relation x y) (k : relation y z), relation x z
6271
-- There's always a `map` relation
63-
| map : Π (j j' : J) (f : j ⟶ j') (x : (F.obj j).α), relation (of j' ((F.map f) x)) (of j x)
72+
| map : Π (j j' : J) (f : j ⟶ j') (x : (F.obj j).α), relation (of j' (F.map f x)) (of j x)
6473
-- Then one relation per operation, describing the interaction with `of`
6574
| zero : Π (j), relation (of j 0) zero
6675
| one : Π (j), relation (of j 1) one
@@ -261,31 +270,17 @@ instance : comm_ring (colimit_type F) :=
261270
@[simp] lemma quot_add (x y) : quot.mk setoid.r (add x y) = ((quot.mk setoid.r x) + (quot.mk setoid.r y) : colimit_type F) := rfl
262271
@[simp] lemma quot_mul (x y) : quot.mk setoid.r (mul x y) = ((quot.mk setoid.r x) * (quot.mk setoid.r y) : colimit_type F) := rfl
263272

264-
def colimit : CommRing := colimit_type F, by apply_instance⟩
273+
def colimit : CommRing := CommRing.of (colimit_type F)
265274

266275
def cocone_fun (j : J) (x : (F.obj j).α) : colimit_type F :=
267276
quot.mk _ (of j x)
268277

269-
instance cocone_is_hom (j : J) : is_ring_hom (cocone_fun F j) :=
270-
{ map_one :=
271-
begin
272-
apply quot.sound,
273-
apply relation.one,
274-
end,
275-
map_mul := λ x y,
276-
begin
277-
apply quot.sound,
278-
apply relation.mul,
279-
end,
280-
map_add := λ x y,
281-
begin
282-
apply quot.sound,
283-
apply relation.add,
284-
end }
285-
286278
def cocone_morphism (j : J) : F.obj j ⟶ colimit F :=
287-
{ val := cocone_fun F j,
288-
property := by apply_instance }
279+
{ to_fun := cocone_fun F j,
280+
map_one' := by apply quot.sound; apply relation.one,
281+
map_mul' := by intros; apply quot.sound; apply relation.mul,
282+
map_zero' := by apply quot.sound; apply relation.zero,
283+
map_add' := by intros; apply quot.sound; apply relation.add }
289284

290285
@[simp] lemma cocone_naturality {j j' : J} (f : j ⟶ j') :
291286
F.map f ≫ (cocone_morphism F j') = cocone_morphism F j :=
@@ -312,10 +307,6 @@ def colimit_cocone : cocone F :=
312307
| (add x y) := desc_fun_lift x + desc_fun_lift y
313308
| (mul x y) := desc_fun_lift x * desc_fun_lift y
314309

315-
@[simp] lemma naturality_bundled {G : J ⥤ CommRing} (s : cocone G) {j j' : J} (f : j ⟶ j') (x : G.obj j) :
316-
(s.ι.app j') ((G.map f) x) = (s.ι.app j) x :=
317-
congr_fun (congr_arg (λ k : G.obj j ⟶ s.X, (k : G.obj j → s.X)) (s.ι.naturality f)) x
318-
319310
def desc_fun (s : cocone F) : colimit_type F → s.X :=
320311
begin
321312
fapply quot.lift,
@@ -329,7 +320,7 @@ begin
329320
-- trans
330321
{ exact eq.trans r_ih_h r_ih_k },
331322
-- map
332-
{ rw naturality_bundled, },
323+
{ rw cocone.naturality_bundled, },
333324
-- zero
334325
{ erw is_ring_hom.map_zero ⇑((s.ι).app r), refl },
335326
-- one
@@ -375,26 +366,12 @@ begin
375366
}
376367
end
377368

378-
instance desc_fun_is_morphism (s : cocone F) : is_ring_hom (desc_fun F s) :=
379-
{ map_one := rfl,
380-
map_add := λ x y,
381-
begin
382-
induction x, induction y,
383-
refl,
384-
refl,
385-
refl,
386-
end,
387-
map_mul := λ x y,
388-
begin
389-
induction x, induction y,
390-
refl,
391-
refl,
392-
refl,
393-
end, }
394-
395369
@[simp] def desc_morphism (s : cocone F) : colimit F ⟶ s.X :=
396-
{ val := desc_fun F s,
397-
property := by apply_instance }
370+
{ to_fun := desc_fun F s,
371+
map_one' := rfl,
372+
map_zero' := rfl,
373+
map_add' := λ x y, by { induction x; induction y; refl },
374+
map_mul' := λ x y, by { induction x; induction y; refl }, }
398375

399376
def colimit_is_colimit : is_colimit (colimit_cocone F) :=
400377
{ desc := λ s, desc_morphism F s,

0 commit comments

Comments
 (0)