Zulip Chat Archive

Stream: maths

Topic: category of discrete rings


view this post on Zulip 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

view this post on Zulip 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 }

view this post on Zulip Kenny Lau (Jun 22 2019 at 21:08):

this is just a proof of concept

view this post on Zulip 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