## Stream: maths

### Topic: category of discrete rings

#### Kenny Lau (Jun 22 2019 at 21:08):

import category_theory.concrete_category data.polynomial

universes u v

/-- Discrete Commutative Rings (with unity) -/
structure DCRing : Type (u+1) :=
(carrier : Type u)
(cring : comm_ring carrier)
(discrete : decidable_eq carrier)
attribute [instance] DCRing.cring DCRing.discrete

namespace DCRing

instance : has_coe_to_sort DCRing.{u} :=
⟨Type u, DCRing.carrier⟩

instance (R : DCRing) : comm_ring R := R.cring
instance (R : DCRing) : decidable_eq R := R.discrete

instance : category_theory.category DCRing.{u} :=
{ hom := λ R S, { f : R → S // is_ring_hom f },
id := λ R, ⟨id, is_ring_hom.id⟩,
comp := λ R S T f g, ⟨g.1 ∘ f.1, @@is_ring_hom.comp _ _ f.1 f.2 _ g.1 g.2⟩ }

instance (R S : DCRing) : has_coe_to_fun (R ⟶ S) :=
⟨λ f, R → S, subtype.val⟩

instance (R S : DCRing) (f : R ⟶ S) : is_ring_hom f := f.2

@[extensionality] theorem hom_ext {R S : DCRing} {f g : R ⟶ S} (H : ∀ x, f x = g x) : f = g :=
subtype.eq $funext H def polynomial : DCRing.{u} ⥤ DCRing.{u} := { obj := λ R, ⟨polynomial R, polynomial.comm_ring, polynomial.decidable_eq⟩, map := λ R S f, ⟨polynomial.map f, polynomial.map.is_ring_hom f⟩, map_id' := λ R, hom_ext$ λ x, polynomial.map_id,
map_comp' := λ R S T f g, hom_ext $λ x, (polynomial.map_map f g x).symm } end DCRing  #### Kenny Lau (Jun 22 2019 at 21:08): main result: def polynomial : DCRing.{u} ⥤ DCRing.{u} := { obj := λ R, ⟨polynomial R, polynomial.comm_ring, polynomial.decidable_eq⟩, map := λ R S f, ⟨polynomial.map f, polynomial.map.is_ring_hom f⟩, map_id' := λ R, hom_ext$ λ x, polynomial.map_id,
map_comp' := λ R S T f g, hom_ext \$ λ x, (polynomial.map_map f g x).symm }


#### Kenny Lau (Jun 22 2019 at 21:08):

this is just a proof of concept

#### Reid Barton (Jun 22 2019 at 22:58):

Still like the concept although possibly we can find a word more obviously irrelevant to classical mathematics than "discrete"

Last updated: May 11 2021 at 15:12 UTC