category of discrete rings

Stream: maths

[Kenny Lau]

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]

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]

this is just a proof of concept

[Reid Barton]

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