/
adjunctions.lean
53 lines (42 loc) · 1.56 KB
/
adjunctions.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
/-
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.CommRing.basic
import data.mv_polynomial
/-!
Multivariable polynomials on a type is the left adjoint of the
forgetful functor from commutative rings to types.
-/
noncomputable theory
universe u
open mv_polynomial
open category_theory
namespace CommRing
open_locale classical
/--
The free functor `Type u ⥤ CommRing` sending a type `X` to the multivariable (commutative)
polynomials with variables `x : X`.
-/
def free : Type u ⥤ CommRing :=
{ obj := λ α, of (mv_polynomial α ℤ),
map := λ X Y f, ((rename f : mv_polynomial X ℤ →ₐ[ℤ] mv_polynomial Y ℤ) :
(mv_polynomial X ℤ →+* mv_polynomial Y ℤ)),
-- TODO these next two fields can be done by `tidy`, but the calls in `dsimp` and `simp` it
-- generates are too slow.
map_id' := λ X, ring_hom.ext $ rename_id,
map_comp' := λ X Y Z f g, ring_hom.ext $ λ p, (rename_rename f g p).symm }
@[simp] lemma free_obj_coe {α : Type u} :
(free.obj α : Type u) = mv_polynomial α ℤ := rfl
@[simp] lemma free_map_coe {α β : Type u} {f : α → β} :
⇑(free.map f) = rename f := rfl
/--
The free-forgetful adjunction for commutative rings.
-/
def adj : free ⊣ forget CommRing :=
adjunction.mk_of_hom_equiv
{ hom_equiv := λ X R, hom_equiv,
hom_equiv_naturality_left_symm' :=
λ _ _ Y f g, ring_hom.ext $ λ x, eval₂_cast_comp f (int.cast_ring_hom Y) g x }
end CommRing