the polynomial ring is the universal pointed ring

poly_universal.lean

import algebra
import tactic

/-!
# Polynomials as the universal pointed ring

A "pointed commutative ring" is a ring with an additional element,
which we call `point`.  Homomorphisms of pointed commutative rings are
ring homomorphisms that implement the class `pointed_hom`.

There is an adjunction between commutative rings and pointed
commutative rings.  Left adjoint to the forgetful functor is the
functor `poly` that adjoins an additional element, called the
"variable".  The pointed commutative ring `poly R` is the polynomial
ring R[x].   The map `to_poly R : R → poly R` is the natural inclusion.

Given a homomorphism `f` from a commutative ring R to a pointed
commutative ring R', `to_poly.map f` gives the induced homomorphism
`poly R → R'`.  This satisfies some universal properties
`to_poly.univ` and `to_poly.univ_uniq`, showing `poly R` is initial.

-/

universes u v

inductive pre_poly (R : Type u) : Type u
| incl (x : R) : pre_poly
| var : pre_poly
| add (a b : pre_poly) : pre_poly
| mul (a b : pre_poly) : pre_poly

open pre_poly

inductive pre_poly_rel' (R : Type u) [ring R] : pre_poly R → pre_poly R → Type u
| refl {a : pre_poly R} : pre_poly_rel' a a
| symm {a b : pre_poly R} (hab : pre_poly_rel' a b) : pre_poly_rel' b a
| trans {a b c : pre_poly R}
  (hab : pre_poly_rel' a b) (hbc : pre_poly_rel' b c) : pre_poly_rel' a c
| congr_add {a b a' b' : pre_poly R}
  (ha : pre_poly_rel' a a') (hb : pre_poly_rel' b b') :
  pre_poly_rel' (add a b) (add a' b')
| congr_mul {a b a' b' : pre_poly R}
  (ha : pre_poly_rel' a a') (hb : pre_poly_rel' b b') :
  pre_poly_rel' (mul a b) (mul a' b')
| add_assoc' (a b c : pre_poly R) : pre_poly_rel' (add (add a b) c) (add a (add b c))
| mul_assoc' (a b c : pre_poly R) : pre_poly_rel' (mul (mul a b) c) (mul a (mul b c))
| add_incl (x y : R) :
  pre_poly_rel' (add (incl x) (incl y)) (incl (x + y))
| mul_incl (x y : R) :
  pre_poly_rel' (mul (incl x) (incl y)) (incl (x * y))
| zero_add (a : pre_poly R) : pre_poly_rel' (add (incl 0) a) a
| add_zero (a : pre_poly R) : pre_poly_rel' (add a (incl 0)) a
| one_mul (a : pre_poly R) : pre_poly_rel' (mul (incl 1) a) a
| mul_one (a : pre_poly R) : pre_poly_rel' (mul a (incl 1)) a
| add_comm (a b : pre_poly R) : pre_poly_rel' (add a b) (add b a)
| mul_comm (a b : pre_poly R) : pre_poly_rel' (mul a b) (mul b a)
| left_distrib (a b c : pre_poly R) : pre_poly_rel' (mul a (add b c)) (add (mul a b) (mul a c))
| right_distrib (a b c : pre_poly R) : pre_poly_rel' (mul (add a b) c) (add (mul a c) (mul b c))
| add_left_neg (a : pre_poly R) : pre_poly_rel' (add (mul (incl (-1)) a) a) (incl 0)

inductive pre_poly_rel (R : Type u) [ring R] : pre_poly R → pre_poly R → Prop
| rel {a b : pre_poly R} (r : pre_poly_rel' R a b) : pre_poly_rel a b

/--
A quick way to convert a `pre_poly_rel'` to a `pre_poly_rel`.
-/
lemma pre_poly_rel'.rel {R : Type u} [ring R] {a b : pre_poly R} :
  pre_poly_rel' R a b → pre_poly_rel R a b :=
pre_poly_rel.rel

@[refl]
lemma pre_poly_rel.refl {R : Type u} [ring R] {a : pre_poly R} :
  pre_poly_rel R a a :=
pre_poly_rel.rel pre_poly_rel'.refl

@[symm]
lemma pre_poly_rel.symm {R : Type u} [ring R] {a b : pre_poly R} :
  pre_poly_rel R a b → pre_poly_rel R b a
| ⟨r⟩ := r.symm.rel

@[trans]
lemma pre_poly_rel.trans {R : Type u} [ring R] {a b c : pre_poly R} :
  pre_poly_rel R a b → pre_poly_rel R b c → pre_poly_rel R a c
| ⟨rab⟩ ⟨rbc⟩ := (rab.trans rbc).rel

instance pre_poly.setoid (R : Type u) [ring R] : setoid (pre_poly R) :=
{ r := pre_poly_rel R,
  iseqv := begin
    split, apply pre_poly_rel.refl,
    split, apply pre_poly_rel.symm,
    apply pre_poly_rel.trans
  end }

/--
The universal pointed ring that envelops a given ring (i.e., it's the polynomial ring with one variable).
-/
def poly (R : Type u) [ring R] := quotient (pre_poly.setoid R)


class pointed_comm_ring (R : Type u) extends comm_ring R :=
(point : R)

open pointed_comm_ring

class pointed_hom {α : Type u} {β : Type v} [pointed_comm_ring α] [pointed_comm_ring β] (f : α →+* β) : Prop :=
(map_point : f point = point)

instance poly.pointed_comm_ring (R : Type u) [ring R] : pointed_comm_ring (poly R) :=
{ add := λ a b, quotient.lift_on₂ a b
                  (λ a b, ⟦add a b⟧)
                  (λ a b a' b' ⟨ha⟩ ⟨hb⟩,
                    quotient.sound (pre_poly_rel'.congr_add ha hb).rel),
  mul := λ a b, quotient.lift_on₂ a b
                  (λ a b, ⟦mul a b⟧)
                  (λ a b a' b' ⟨ha⟩ ⟨hb⟩,
                    quotient.sound (pre_poly_rel'.congr_mul ha hb).rel),
  neg := λ a, quotient.lift_on a
                (λ a, ⟦mul (incl (-1)) a⟧)
                (λ a a' ⟨ha⟩, quotient.sound (pre_poly_rel'.congr_mul pre_poly_rel'.refl ha).rel),
  zero := ⟦incl 0⟧,
  one := ⟦incl 1⟧,
  point := ⟦var⟧,
  add_assoc := λ a b c,
    quotient.induction_on₃ a b c (λ a b c, quotient.sound (pre_poly_rel'.add_assoc' a b c).rel),
  mul_assoc := λ a b c,
    quotient.induction_on₃ a b c (λ a b c, quotient.sound (pre_poly_rel'.mul_assoc' a b c).rel),
  zero_add := λ a,
    quotient.induction_on a (λ a, quotient.sound (pre_poly_rel'.zero_add a).rel),
  add_zero := λ a,
    quotient.induction_on a (λ a, quotient.sound (pre_poly_rel'.add_zero a).rel),
  one_mul := λ a,
    quotient.induction_on a (λ a, quotient.sound (pre_poly_rel'.one_mul a).rel),
  mul_one := λ a,
    quotient.induction_on a (λ a, quotient.sound (pre_poly_rel'.mul_one a).rel),
  mul_comm := λ a b,
    quotient.induction_on₂ a b (λ a b, quotient.sound (pre_poly_rel'.mul_comm a b).rel),
  add_comm := λ a b,
    quotient.induction_on₂ a b (λ a b, quotient.sound (pre_poly_rel'.add_comm a b).rel),
  left_distrib := λ a b c,
    quotient.induction_on₃ a b c (λ a b c, quotient.sound (pre_poly_rel'.left_distrib a b c).rel),
  right_distrib := λ a b c,
    quotient.induction_on₃ a b c (λ a b c, quotient.sound (pre_poly_rel'.right_distrib a b c).rel),
  add_left_neg := λ a,
    quotient.induction_on a (λ a, quotient.sound (pre_poly_rel'.add_left_neg a).rel) }


/--
The canonical inclusion map from a ring into its polynomial ring
-/
def to_poly (R : Type u) [comm_ring R] : R →+* poly R :=
{ to_fun := λ x, ⟦incl x⟧,
  map_zero' := rfl,
  map_one' := rfl,
  map_add' := λ x y, quotient.sound (pre_poly_rel'.add_incl x y).symm.rel,
  map_mul' := λ x y, quotient.sound (pre_poly_rel'.mul_incl x y).symm.rel }

def to_poly.map_aux {R : Type u} [comm_ring R] {R' : Type v} [pointed_comm_ring R']
  (f : R →+* R') : pre_poly R → R'
| (incl x) := f x
| var := pointed_comm_ring.point
| (add a b) := to_poly.map_aux a + to_poly.map_aux b
| (mul a b) := to_poly.map_aux a * to_poly.map_aux b

namespace to_poly.map_aux
open pre_poly_rel'

/--
Show that `to_poly.map_aux` sends equivalent expressions to equal terms.
-/
lemma well_def {R : Type u} [comm_ring R] {R' : Type v} [pointed_comm_ring R'] (f : R →+* R') :
  Π {a b : pre_poly R}, pre_poly_rel' R a b → to_poly.map_aux f a = to_poly.map_aux f b
| a b refl := rfl
| a b (symm h) := (well_def h).symm
| a b (trans hac hcb) := eq.trans (well_def hac) (well_def hcb)
| _ _ (congr_add ha hb) := by { simp [to_poly.map_aux, well_def ha, well_def hb] }
| _ _ (congr_mul ha hb) := by { simp [to_poly.map_aux, well_def ha, well_def hb] }
| _ _ (add_assoc' a b c) := by { simp [to_poly.map_aux, add_assoc], }
| _ _ (mul_assoc' a b c) := by { simp [to_poly.map_aux, mul_assoc], }
| _ _ (add_incl x y) := by { simp [to_poly.map_aux], }
| _ _ (mul_incl x y) := by { simp [to_poly.map_aux], }
| _ _ (zero_add a) := by { simp [to_poly.map_aux] }
| _ _ (add_zero a) := by { simp [to_poly.map_aux] }
| _ _ (one_mul a) := by { simp [to_poly.map_aux] }
| _ _ (mul_one a) := by { simp [to_poly.map_aux] }
| _ _ (add_comm a b) := by { dsimp [to_poly.map_aux], ring }
| _ _ (mul_comm a b) := by { dsimp [to_poly.map_aux], ring }
| _ _ (left_distrib a b c) := by { dsimp [to_poly.map_aux], ring }
| _ _ (right_distrib a b c) := by { dsimp [to_poly.map_aux], ring }
| _ _ (add_left_neg a) := by { simp [to_poly.map_aux] }

end to_poly.map_aux

/--
Given a map from a commutative ring to a pointed commutative ring, lift it to being a map from the polynomial ring
-/
def to_poly.map {R : Type u} [comm_ring R] {R' : Type v} [pointed_comm_ring R']
  (f : R →+* R') : poly R →+* R' :=
{ to_fun := λ x, quotient.lift_on x (to_poly.map_aux f)
                   (λ a b ⟨hab⟩, to_poly.map_aux.well_def f hab),
  map_zero' := begin
    change quotient.lift_on ⟦incl 0⟧ (to_poly.map_aux f) _ = 0,
    simp [to_poly.map_aux],
  end,
  map_one' := begin
    change quotient.lift_on ⟦incl 1⟧ (to_poly.map_aux f) _ = 1,
    simp [to_poly.map_aux],
  end,
  map_add' := λ x y, quotient.induction_on₂ x y (λ x y, begin
    change quotient.lift_on ⟦add x y⟧ (to_poly.map_aux f) _ = _,
    simp [to_poly.map_aux],
  end),
  map_mul' := λ x y, quotient.induction_on₂ x y (λ x y, begin
    change quotient.lift_on ⟦mul x y⟧ (to_poly.map_aux f) _ = _,
    simp [to_poly.map_aux],
  end) }

instance {R : Type u} [comm_ring R] {R' : Type v} [pointed_comm_ring R'] (f : R →+* R') :
  pointed_hom (to_poly.map f) :=
{ map_point := rfl }

/--
Given a homomorphism from a commutative ring to a pointed ring, it factors through the polynomial ring.
-/
lemma to_poly.univ (R : Type u) [comm_ring R] (R' : Type v) [pointed_comm_ring R']
  (f : R →+* R') :
  (to_poly.map f).comp (to_poly R) = f :=
by { ext, refl }

/--
The homomorphism `to_poly.map f` is the unique map that fits into the commutative
triangle in `to_poly.univ`.
-/
lemma to_poly.univ_uniq (R : Type u) [comm_ring R] (R' : Type v) [pointed_comm_ring R']
  (f : R →+* R')
  (g : poly R →+* R') [pointed_hom g] (h : f = g.comp (to_poly R)) :
  g = to_poly.map f :=
begin
  subst f, ext, refine quotient.ind (λ x, _) x,
  induction x,
  refl,
  convert pointed_hom.map_point, apply_instance,
  have hm : ⟦x_a.add x_b⟧ = @has_add.add (poly R) _ ⟦x_a⟧ ⟦x_b⟧ := rfl,
  rw hm, simp [to_poly.map, x_ih_a, x_ih_b],
  have hm : ⟦x_a.mul x_b⟧ = @has_mul.mul (poly R) _ ⟦x_a⟧ ⟦x_b⟧ := rfl,
  rw hm, simp [to_poly.map, x_ih_a, x_ih_b],
end