From 40d09b0f8f2193ceda525cf0aa8ae52d7eade857 Mon Sep 17 00:00:00 2001
From: kckennylau <kc_kennylau@yahoo.com.hk>
Date: Sun, 17 Feb 2019 03:46:37 +0000
Subject: [PATCH] feat(ring_theory): free_ring and free_comm_ring

---
 src/ring_theory/free_comm_ring.lean | 267 ++++++++++++++++++++++++++++
 src/ring_theory/free_ring.lean      | 208 ++++++++++++++++++++++
 2 files changed, 475 insertions(+)
 create mode 100644 src/ring_theory/free_comm_ring.lean
 create mode 100644 src/ring_theory/free_ring.lean

diff --git a/src/ring_theory/free_comm_ring.lean b/src/ring_theory/free_comm_ring.lean
new file mode 100644
index 0000000000000..80c9f6bff5cdd
--- /dev/null
+++ b/src/ring_theory/free_comm_ring.lean
@@ -0,0 +1,267 @@
+import group_theory.free_abelian_group data.equiv.algebra data.polynomial ring_theory.ideal_operations
+
+universes u v
+
+def free_comm_ring (α : Type u) : Type u :=
+free_abelian_group $ multiset α
+
+namespace free_comm_ring
+
+variables (α : Type u)
+
+instance : add_comm_group (free_comm_ring α) :=
+{ .. free_abelian_group.add_comm_group (multiset α) }
+
+instance : semigroup (free_comm_ring α) :=
+{ mul := λ x, free_abelian_group.lift $ λ s2, free_abelian_group.lift (λ s1, free_abelian_group.of $ s1 + s2) x,
+  mul_assoc := λ x y z, begin
+    unfold has_mul.mul,
+    refine free_abelian_group.induction_on z rfl _ _ _,
+    { intros s3, rw [free_abelian_group.lift.of, free_abelian_group.lift.of],
+      refine free_abelian_group.induction_on y rfl _ _ _,
+      { intros s2, iterate 3 { rw free_abelian_group.lift.of },
+        refine free_abelian_group.induction_on x rfl _ _ _,
+        { intros s1, iterate 3 { rw free_abelian_group.lift.of }, rw add_assoc },
+        { intros s1 ih, iterate 3 { rw free_abelian_group.lift.neg }, rw ih },
+        { intros x1 x2 ih1 ih2, iterate 3 { rw free_abelian_group.lift.add }, rw [ih1, ih2] } },
+      { intros s2 ih, iterate 4 { rw free_abelian_group.lift.neg }, rw ih },
+      { intros y1 y2 ih1 ih2, iterate 4 { rw free_abelian_group.lift.add }, rw [ih1, ih2] } },
+    { intros s3 ih, iterate 3 { rw free_abelian_group.lift.neg }, rw ih },
+    { intros z1 z2 ih1 ih2, iterate 2 { rw free_abelian_group.lift.add }, rw [ih1, ih2],
+      exact (free_abelian_group.lift.add _ _ _).symm }
+  end }
+
+instance : ring (free_comm_ring α) :=
+{ one := free_abelian_group.of 0,
+  mul_one := λ x, begin
+    unfold has_mul.mul semigroup.mul has_one.one,
+    rw free_abelian_group.lift.of,
+    refine free_abelian_group.induction_on x rfl _ _ _,
+    { intros s, rw [free_abelian_group.lift.of, add_zero] },
+    { intros s ih, rw [free_abelian_group.lift.neg, ih] },
+    { intros x1 x2 ih1 ih2, rw [free_abelian_group.lift.add, ih1, ih2] }
+  end,
+  one_mul := λ x, begin
+    unfold has_mul.mul semigroup.mul has_one.one,
+    refine free_abelian_group.induction_on x rfl _ _ _,
+    { intros s, rw [free_abelian_group.lift.of, free_abelian_group.lift.of, zero_add] },
+    { intros s ih, rw [free_abelian_group.lift.neg, ih] },
+    { intros x1 x2 ih1 ih2, rw [free_abelian_group.lift.add, ih1, ih2] }
+  end,
+  left_distrib := λ x y z, free_abelian_group.lift.add _ _ _,
+  right_distrib := λ x y z, begin
+    unfold has_mul.mul semigroup.mul,
+    refine free_abelian_group.induction_on z rfl _ _ _,
+    { intros s, iterate 3 { rw free_abelian_group.lift.of }, rw free_abelian_group.lift.add, refl },
+    { intros s ih, iterate 3 { rw free_abelian_group.lift.neg }, rw [ih, neg_add], refl },
+    { intros z1 z2 ih1 ih2, iterate 3 { rw free_abelian_group.lift.add }, rw [ih1, ih2],
+      rw [add_assoc, add_assoc], congr' 1, apply add_left_comm }
+  end,
+  .. free_comm_ring.add_comm_group α,
+  .. free_comm_ring.semigroup α }
+
+instance : comm_ring (free_comm_ring α) :=
+{ mul_comm := λ x y, begin
+    refine free_abelian_group.induction_on x (zero_mul y) _ _ _,
+    { intros s, refine free_abelian_group.induction_on y (zero_mul _).symm _ _ _,
+      { intros t, unfold has_mul.mul semigroup.mul ring.mul,
+        iterate 4 { rw free_abelian_group.lift.of }, rw add_comm },
+      { intros t ih, rw [mul_neg_eq_neg_mul_symm, ih, neg_mul_eq_neg_mul] },
+      { intros y1 y2 ih1 ih2, rw [mul_add, add_mul, ih1, ih2] } },
+    { intros s ih, rw [neg_mul_eq_neg_mul_symm, ih, neg_mul_eq_mul_neg] },
+    { intros x1 x2 ih1 ih2, rw [add_mul, mul_add, ih1, ih2] }
+  end
+  .. free_comm_ring.ring α }
+
+variables {α}
+def of (x : α) : free_comm_ring α :=
+free_abelian_group.of [x]
+
+section lift
+
+variables {β : Type v} [comm_ring β] (f : α → β)
+
+def lift : free_comm_ring α → β :=
+free_abelian_group.lift $ λ s, (s.map f).prod
+
+@[simp] lemma lift_zero : lift f 0 = 0 := rfl
+
+@[simp] lemma lift_one : lift f 1 = 1 :=
+free_abelian_group.lift.of _ _
+
+@[simp] lemma lift_of (x : α) : lift f (of x) = f x :=
+(free_abelian_group.lift.of _ _).trans $ mul_one _
+
+@[simp] lemma lift_add (x y) : lift f (x + y) = lift f x + lift f y :=
+free_abelian_group.lift.add _ _ _
+
+@[simp] lemma lift_neg (x) : lift f (-x) = -lift f x :=
+free_abelian_group.lift.neg _ _
+
+@[simp] lemma lift_sub (x y) : lift f (x - y) = lift f x - lift f y :=
+free_abelian_group.lift.sub _ _ _
+
+@[simp] lemma lift_mul (x y) : lift f (x * y) = lift f x * lift f y :=
+begin
+  refine free_abelian_group.induction_on y (mul_zero _).symm _ _ _,
+  { intros s2, conv { to_lhs, dsimp only [(*), mul_zero_class.mul, semiring.mul, ring.mul, semigroup.mul] },
+    rw [free_abelian_group.lift.of, lift, free_abelian_group.lift.of],
+    refine free_abelian_group.induction_on x (zero_mul _).symm _ _ _,
+    { intros s1, iterate 3 { rw free_abelian_group.lift.of }, rw [multiset.map_add, multiset.prod_add] },
+    { intros s1 ih, iterate 3 { rw free_abelian_group.lift.neg }, rw [ih, neg_mul_eq_neg_mul] },
+    { intros x1 x2 ih1 ih2, iterate 3 { rw free_abelian_group.lift.add }, rw [ih1, ih2, add_mul] } },
+  { intros s2 ih, rw [mul_neg_eq_neg_mul_symm, lift_neg, lift_neg, mul_neg_eq_neg_mul_symm, ih] },
+  { intros y1 y2 ih1 ih2, rw [mul_add, lift_add, lift_add, mul_add, ih1, ih2] },
+end
+
+instance : is_ring_hom (lift f) :=
+{ map_one := lift_one f,
+  map_mul := lift_mul f,
+  map_add := lift_add f }
+
+@[simp] lemma lift_pow (x) (n : ℕ) : lift f (x ^ n) = lift f x ^ n :=
+is_semiring_hom.map_pow _ x n
+
+theorem lift_unique (f : free_comm_ring α → β) [is_ring_hom f] : f = lift (f ∘ of) :=
+funext $ λ x, @@free_abelian_group.lift.ext _ _ _
+  (is_ring_hom.is_add_group_hom f)
+  (is_ring_hom.is_add_group_hom $ lift $ f ∘ of)
+  (λ s, multiset.induction_on s ((is_ring_hom.map_one f).trans $ eq.symm $ lift_one _)
+    (λ hd tl ih, show f (of hd * free_abelian_group.of tl) = lift (f ∘ of) (of hd * free_abelian_group.of tl),
+      by rw [is_ring_hom.map_mul f, lift_mul, lift_of, ih]))
+
+end lift
+
+variables {β : Type v} (f : α → β)
+
+def map : free_comm_ring α → free_comm_ring β :=
+lift $ of ∘ f
+
+instance : monad free_comm_ring :=
+{ map := λ _ _, map,
+  pure := λ _, of,
+  bind := λ _ _ x f, lift f x }
+
+end free_comm_ring
+
+def free_comm_ring_pempty_equiv_int : free_comm_ring pempty.{u+1} ≃r ℤ :=
+{ to_fun := free_comm_ring.lift $ pempty.rec _,
+  inv_fun := coe,
+  left_inv := λ x, free_abelian_group.induction_on x rfl
+    (λ s, multiset.induction_on s rfl $ pempty.rec _)
+    (λ s ih, by rw [free_comm_ring.lift_neg, int.cast_neg, ih])
+    (λ x1 x2 ih1 ih2, by rw [free_comm_ring.lift_add, int.cast_add, ih1, ih2]),
+  right_inv := λ i, int.induction_on i rfl
+    (λ i ih, by rw [int.cast_add, int.cast_one, free_comm_ring.lift_add, free_comm_ring.lift_one, ih])
+    (λ i ih, by rw [int.cast_sub, int.cast_one, free_comm_ring.lift_sub, free_comm_ring.lift_one, ih]),
+  hom := by apply_instance }
+
+def free_comm_ring_punit_equiv_polynomial_int : free_comm_ring punit.{u+1} ≃r polynomial ℤ :=
+{ to_fun := free_comm_ring.lift $ λ _, polynomial.X,
+  inv_fun := polynomial.eval₂ coe (free_comm_ring.of punit.star),
+  left_inv := λ x, begin
+    haveI : is_semiring_hom (coe : int → free_comm_ring punit.{u+1}) :=
+      @@is_ring_hom.is_semiring_hom _ _ _ (@@int.cast.is_ring_hom _),
+    exact free_abelian_group.induction_on x rfl
+    (λ s, multiset.induction_on s rfl $ λ hd tl ih, show polynomial.eval₂ coe (free_comm_ring.of punit.star)
+          (free_comm_ring.lift (λ (_x : punit), polynomial.X) (free_comm_ring.of hd * free_abelian_group.of tl)) =
+        free_comm_ring.of hd * free_abelian_group.of tl,
+      by cases hd; rw [free_comm_ring.lift_mul, free_comm_ring.lift_of, polynomial.eval₂_mul, polynomial.eval₂_X, ih])
+    (λ s ih, by rw [free_comm_ring.lift_neg, ← neg_one_mul, polynomial.eval₂_mul,
+        ← polynomial.C_1, ← polynomial.C_neg, polynomial.eval₂_C,
+        int.cast_neg, int.cast_one, neg_one_mul, ih])
+    (λ x1 x2 ih1 ih2, by rw [free_comm_ring.lift_add, polynomial.eval₂_add, ih1, ih2])
+  end,
+  right_inv := λ x, begin
+    haveI : is_semiring_hom (coe : int → free_comm_ring punit.{u+1}) :=
+      @@is_ring_hom.is_semiring_hom _ _ _ (@@int.cast.is_ring_hom _),
+    have : ∀ i : ℤ, free_comm_ring.lift (λ _ : punit, polynomial.X) ↑i = polynomial.C i,
+    { exact λ i, int.induction_on i
+      (by rw [int.cast_zero, free_comm_ring.lift_zero, polynomial.C_0])
+      (λ i ih, by rw [int.cast_add, int.cast_one, free_comm_ring.lift_add, free_comm_ring.lift_one, ih, polynomial.C_add, polynomial.C_1])
+      (λ i ih, by rw [int.cast_sub, int.cast_one, free_comm_ring.lift_sub, free_comm_ring.lift_one, ih, polynomial.C_sub, polynomial.C_1]) },
+    exact polynomial.induction_on x
+    (λ i, by rw [polynomial.eval₂_C, this])
+    (λ p q ihp ihq, by rw [polynomial.eval₂_add, free_comm_ring.lift_add, ihp, ihq])
+    (λ n i ih, by rw [polynomial.eval₂_mul, polynomial.eval₂_pow, polynomial.eval₂_C, polynomial.eval₂_X,
+        free_comm_ring.lift_mul, free_comm_ring.lift_pow, free_comm_ring.lift_of, this])
+  end,
+  hom := by apply_instance }
+
+variables (α : Type u) [comm_ring α]
+
+def polynomial' : Type u :=
+ideal.quotient (ideal.span
+  (insert (free_comm_ring.of (some 1) - 1)
+    (set.range (λ xy : α × α, free_comm_ring.of (some (xy.1 + xy.2)) - (free_comm_ring.of (some xy.1) + free_comm_ring.of (some xy.2))) ∪
+    set.range (λ xy : α × α, free_comm_ring.of (some (xy.1 * xy.2)) - (free_comm_ring.of (some xy.1) * free_comm_ring.of (some xy.2))))) : ideal (free_comm_ring (option α)))
+
+namespace polynomial'
+
+instance : comm_ring (polynomial' α) :=
+ideal.quotient.comm_ring _
+
+variables {α}
+
+def C (x : α) : polynomial' α :=
+ideal.quotient.mk _ (free_comm_ring.of $ some x)
+
+def X : polynomial' α :=
+ideal.quotient.mk _ (free_comm_ring.of none)
+
+instance C.is_ring_hom : is_ring_hom (@C α _) :=
+{ map_one := ideal.quotient.eq.2 $ ideal.subset_span $ or.inl rfl,
+  map_mul := λ x y, ideal.quotient.eq.2 $ ideal.subset_span $ or.inr $ or.inr $
+    set.mem_range.2 ⟨(x, y), rfl⟩,
+  map_add := λ x y, ideal.quotient.eq.2 $ ideal.subset_span $ or.inr $ or.inl $
+    set.mem_range.2 ⟨(x, y), rfl⟩ }
+
+variables {β : Type v} [comm_ring β]
+
+section eval₂
+
+def eval₂ (f : α → β) [is_ring_hom f] (x : β) : polynomial' α → β :=
+ideal.quotient.lift _ (free_comm_ring.lift $ λ s, option.rec_on s x f) $ λ p hp, begin
+  refine submodule.span_induction hp _ rfl _ _,
+  { intros p hp, cases hp with hp hp,
+    { subst hp, rw [free_comm_ring.lift_sub, free_comm_ring.lift_of, free_comm_ring.lift_one],
+      change f 1 - 1 = 0, rw [is_ring_hom.map_one f, sub_self] },
+    rcases hp with ⟨⟨s, t⟩, rfl⟩ | ⟨⟨s, t⟩, rfl⟩,
+    { simp only [free_comm_ring.lift_sub, free_comm_ring.lift_add, free_comm_ring.lift_of],
+      rw [is_ring_hom.map_add f, sub_self] },
+    { simp only [free_comm_ring.lift_sub, free_comm_ring.lift_mul, free_comm_ring.lift_of],
+      rw [is_ring_hom.map_mul f, sub_self] } },
+  { intros y z ih1 ih2, rw [free_comm_ring.lift_add, ih1, ih2, add_zero] },
+  { intros y z ih, rw [smul_eq_mul, free_comm_ring.lift_mul, ih, mul_zero] }
+end
+
+variables (f : α → β) [is_ring_hom f]
+
+@[simp] lemma eval₂_add (x p q) : eval₂ f x (p + q) = eval₂ f x p + eval₂ f x q :=
+quotient.induction_on₂' p q $ λ _ _, free_comm_ring.lift_add _ _ _
+
+@[simp] lemma eval₂_neg (x p) : eval₂ f x (-p) = -eval₂ f x p :=
+quotient.induction_on' p $ λ _, free_comm_ring.lift_neg _ _
+
+@[simp] lemma eval₂_sub (x p q) : eval₂ f x (p - q) = eval₂ f x p - eval₂ f x q :=
+quotient.induction_on₂' p q $ λ _ _, free_comm_ring.lift_sub _ _ _
+
+end eval₂
+
+theorem eval₂_unique (f : polynomial' α → β) [is_ring_hom f] :
+  f = eval₂ (f ∘ C) (f X) :=
+funext $ λ p, quotient.induction_on' p $ λ x, begin
+  change f (ideal.quotient.mk _ x) = eval₂ (f ∘ C) (f X) (ideal.quotient.mk _ x),
+  refine free_abelian_group.induction_on x (is_ring_hom.map_zero f) _ _ _,
+  { intros s, unfold eval₂, rw [ideal.quotient.lift_mk, free_comm_ring.lift, free_abelian_group.lift.of],
+    refine multiset.induction_on s (is_ring_hom.map_one f) _,
+    rintros (_|x) s ih,
+    { change f (X * ideal.quotient.mk _ (free_abelian_group.of s)) = _,
+      simp only [multiset.map_cons, multiset.prod_cons, is_ring_hom.map_mul f, ih] },
+    { change f (C x * ideal.quotient.mk _ (free_abelian_group.of s)) = _,
+      simp only [multiset.map_cons, multiset.prod_cons, is_ring_hom.map_mul f, ih] } },
+  { intros s ih, rw [ideal.quotient.mk_neg, is_ring_hom.map_neg f, ih, eval₂_neg] },
+  { intros s1 s2 ih1 ih2, rw [ideal.quotient.mk_add, is_ring_hom.map_add f, ih1, ih2, eval₂_add] }
+end
+
+end polynomial'
diff --git a/src/ring_theory/free_ring.lean b/src/ring_theory/free_ring.lean
new file mode 100644
index 0000000000000..d67360c686f52
--- /dev/null
+++ b/src/ring_theory/free_ring.lean
@@ -0,0 +1,208 @@
+import group_theory.free_abelian_group data.equiv.algebra data.polynomial
+
+universes u v
+
+def free_ring (α : Type u) : Type u :=
+free_abelian_group $ list α
+
+namespace free_ring
+
+variables (α : Type u)
+
+instance : add_comm_group (free_ring α) :=
+{ .. free_abelian_group.add_comm_group (list α) }
+
+instance : semigroup (free_ring α) :=
+{ mul := λ x, free_abelian_group.lift $ λ L2, free_abelian_group.lift (λ L1, free_abelian_group.of $ L1 ++ L2) x,
+  mul_assoc := λ x y z, begin
+    unfold has_mul.mul,
+    refine free_abelian_group.induction_on z rfl _ _ _,
+    { intros L3, rw [free_abelian_group.lift.of, free_abelian_group.lift.of],
+      refine free_abelian_group.induction_on y rfl _ _ _,
+      { intros L2, iterate 3 { rw free_abelian_group.lift.of },
+        refine free_abelian_group.induction_on x rfl _ _ _,
+        { intros L1, iterate 3 { rw free_abelian_group.lift.of }, rw list.append_assoc },
+        { intros L1 ih, iterate 3 { rw free_abelian_group.lift.neg }, rw ih },
+        { intros x1 x2 ih1 ih2, iterate 3 { rw free_abelian_group.lift.add }, rw [ih1, ih2] } },
+      { intros L2 ih, iterate 4 { rw free_abelian_group.lift.neg }, rw ih },
+      { intros y1 y2 ih1 ih2, iterate 4 { rw free_abelian_group.lift.add }, rw [ih1, ih2] } },
+    { intros L3 ih, iterate 3 { rw free_abelian_group.lift.neg }, rw ih },
+    { intros z1 z2 ih1 ih2, iterate 2 { rw free_abelian_group.lift.add }, rw [ih1, ih2],
+      exact (free_abelian_group.lift.add _ _ _).symm }
+  end }
+
+instance : ring (free_ring α) :=
+{ one := free_abelian_group.of [],
+  mul_one := λ x, begin
+    unfold has_mul.mul semigroup.mul has_one.one,
+    rw free_abelian_group.lift.of,
+    refine free_abelian_group.induction_on x rfl _ _ _,
+    { intros L, rw [free_abelian_group.lift.of, list.append_nil] },
+    { intros L ih, rw [free_abelian_group.lift.neg, ih] },
+    { intros x1 x2 ih1 ih2, rw [free_abelian_group.lift.add, ih1, ih2] }
+  end,
+  one_mul := λ x, begin
+    unfold has_mul.mul semigroup.mul has_one.one,
+    refine free_abelian_group.induction_on x rfl _ _ _,
+    { intros L, rw [free_abelian_group.lift.of, free_abelian_group.lift.of, list.nil_append] },
+    { intros L ih, rw [free_abelian_group.lift.neg, ih] },
+    { intros x1 x2 ih1 ih2, rw [free_abelian_group.lift.add, ih1, ih2] }
+  end,
+  left_distrib := λ x y z, free_abelian_group.lift.add _ _ _,
+  right_distrib := λ x y z, begin
+    unfold has_mul.mul semigroup.mul,
+    refine free_abelian_group.induction_on z rfl _ _ _,
+    { intros L, iterate 3 { rw free_abelian_group.lift.of }, rw free_abelian_group.lift.add, refl },
+    { intros L ih, iterate 3 { rw free_abelian_group.lift.neg }, rw [ih, neg_add], refl },
+    { intros z1 z2 ih1 ih2, iterate 3 { rw free_abelian_group.lift.add }, rw [ih1, ih2],
+      rw [add_assoc, add_assoc], congr' 1, apply add_left_comm }
+  end,
+  .. free_ring.add_comm_group α,
+  .. free_ring.semigroup α }
+
+instance pempty_comm_ring : comm_ring (free_ring pempty.{u+1}) :=
+{ mul_comm := λ x y, begin
+    refine free_abelian_group.induction_on x _ _ _ _,
+    { change 0 * y = y * 0, rw [zero_mul, mul_zero] },
+    { intros L, cases L with hd tl ih,
+      { change 1 * y = y * 1, rw [one_mul, mul_one] },
+      cases hd },
+    { intros L ih, rw [neg_mul_eq_neg_mul_symm, ih, neg_mul_eq_mul_neg] },
+    { intros x1 x2 ih1 ih2, rw [add_mul, mul_add, ih1, ih2] }
+  end,
+  .. free_ring.ring pempty }
+
+instance punit_comm_ring : comm_ring (free_ring punit.{u+1}) :=
+{ mul_comm := λ x y, begin
+    refine free_abelian_group.induction_on x _ _ _ _,
+    { change 0 * y = y * 0, rw [zero_mul, mul_zero] },
+    { intros L1, refine free_abelian_group.induction_on y _ _ _ _,
+      { change (_ * 0 : free_ring _) = 0 * _, rw [mul_zero, zero_mul] },
+      { intros L2, unfold has_mul.mul semigroup.mul ring.mul,
+        iterate 4 { rw free_abelian_group.lift.of }, congr' 1,
+        induction L1 with hd1 tl1 ih1,
+        { rw [list.nil_append, list.append_nil] },
+        { rw [list.cons_append, ih1], clear ih1,
+          induction L2 with hd2 tl2 ih2, { refl },
+          cases hd1, cases hd2, rw [list.cons_append, ih2, list.cons_append] } },
+      { intros L2 ih, rw [mul_neg_eq_neg_mul_symm, ih, neg_mul_eq_neg_mul] },
+      { intros y1 y2 ih1 ih2, rw [mul_add, add_mul, ih1, ih2] } },
+    { intros L ih, rw [neg_mul_eq_neg_mul_symm, ih, neg_mul_eq_mul_neg] },
+    { intros x1 x2 ih1 ih2, rw [add_mul, mul_add, ih1, ih2] }
+  end,
+  .. free_ring.ring punit }
+
+variables {α}
+def of (x : α) : free_ring α :=
+free_abelian_group.of [x]
+
+section lift
+
+variables {β : Type v} [ring β] (f : α → β)
+
+def lift : free_ring α → β :=
+free_abelian_group.lift $ λ L, (L.map f).prod
+
+@[simp] lemma lift_zero : lift f 0 = 0 := rfl
+
+@[simp] lemma lift_one : lift f 1 = 1 :=
+free_abelian_group.lift.of _ _
+
+@[simp] lemma lift_of (x : α) : lift f (of x) = f x :=
+(free_abelian_group.lift.of _ _).trans $ one_mul _
+
+@[simp] lemma lift_add (x y) : lift f (x + y) = lift f x + lift f y :=
+free_abelian_group.lift.add _ _ _
+
+@[simp] lemma lift_neg (x) : lift f (-x) = -lift f x :=
+free_abelian_group.lift.neg _ _
+
+@[simp] lemma lift_sub (x y) : lift f (x - y) = lift f x - lift f y :=
+free_abelian_group.lift.sub _ _ _
+
+@[simp] lemma lift_mul (x y) : lift f (x * y) = lift f x * lift f y :=
+begin
+  refine free_abelian_group.induction_on y (mul_zero _).symm _ _ _,
+  { intros L2, conv { to_lhs, dsimp only [(*), mul_zero_class.mul, semiring.mul, ring.mul, semigroup.mul] },
+    rw [free_abelian_group.lift.of, lift, free_abelian_group.lift.of],
+    refine free_abelian_group.induction_on x (zero_mul _).symm _ _ _,
+    { intros L1, iterate 3 { rw free_abelian_group.lift.of }, rw [list.map_append, list.prod_append] },
+    { intros L1 ih, iterate 3 { rw free_abelian_group.lift.neg }, rw [ih, neg_mul_eq_neg_mul] },
+    { intros x1 x2 ih1 ih2, iterate 3 { rw free_abelian_group.lift.add }, rw [ih1, ih2, add_mul] } },
+  { intros L2 ih, rw [mul_neg_eq_neg_mul_symm, lift_neg, lift_neg, mul_neg_eq_neg_mul_symm, ih] },
+  { intros y1 y2 ih1 ih2, rw [mul_add, lift_add, lift_add, mul_add, ih1, ih2] },
+end
+
+instance : is_ring_hom (lift f) :=
+{ map_one := lift_one f,
+  map_mul := lift_mul f,
+  map_add := lift_add f }
+
+@[simp] lemma lift_pow (x) (n : ℕ) : lift f (x ^ n) = lift f x ^ n :=
+is_semiring_hom.map_pow _ x n
+
+theorem lift_unique (f : free_ring α → β) [is_ring_hom f] : f = lift (f ∘ of) :=
+funext $ λ x, @@free_abelian_group.lift.ext _ _ _
+  (is_ring_hom.is_add_group_hom f)
+  (is_ring_hom.is_add_group_hom $ lift $ f ∘ of)
+  (λ L, list.rec_on L ((is_ring_hom.map_one f).trans $ eq.symm $ lift_one _)
+    (λ hd tl ih, show f (of hd * free_abelian_group.of tl) = lift (f ∘ of) (of hd * free_abelian_group.of tl),
+      by rw [is_ring_hom.map_mul f, lift_mul, lift_of, ih]))
+
+end lift
+
+variables {β : Type v} (f : α → β)
+
+def map : free_ring α → free_ring β :=
+lift $ of ∘ f
+
+instance : monad free_ring :=
+{ map := λ _ _, map,
+  pure := λ _, of,
+  bind := λ _ _ x f, lift f x }
+
+end free_ring
+
+def free_ring_pempty_equiv_int : free_ring pempty.{u+1} ≃r ℤ :=
+{ to_fun := free_ring.lift $ pempty.rec _,
+  inv_fun := coe,
+  left_inv := λ x, free_abelian_group.induction_on x rfl
+    (λ L, list.rec_on L rfl $ pempty.rec _)
+    (λ L ih, by rw [free_ring.lift_neg, int.cast_neg, ih])
+    (λ x1 x2 ih1 ih2, by rw [free_ring.lift_add, int.cast_add, ih1, ih2]),
+  right_inv := λ i, int.induction_on i rfl
+    (λ i ih, by rw [int.cast_add, int.cast_one, free_ring.lift_add, free_ring.lift_one, ih])
+    (λ i ih, by rw [int.cast_sub, int.cast_one, free_ring.lift_sub, free_ring.lift_one, ih]),
+  hom := by apply_instance }
+
+def free_ring_punit_equiv_polynomial_int : free_ring punit.{u+1} ≃r polynomial ℤ :=
+{ to_fun := free_ring.lift $ λ _, polynomial.X,
+  inv_fun := polynomial.eval₂ coe (free_ring.of punit.star),
+  left_inv := λ x, begin
+    haveI : is_semiring_hom (coe : int → free_ring punit.{u+1}) :=
+      @@is_ring_hom.is_semiring_hom _ _ _ (@@int.cast.is_ring_hom _),
+    exact free_abelian_group.induction_on x rfl
+    (λ L, list.rec_on L rfl $ λ hd tl ih, show polynomial.eval₂ coe (free_ring.of punit.star)
+          (free_ring.lift (λ (_x : punit), polynomial.X) (free_ring.of hd * free_abelian_group.of tl)) =
+        free_ring.of hd * free_abelian_group.of tl,
+      by cases hd; rw [free_ring.lift_mul, free_ring.lift_of, polynomial.eval₂_mul, polynomial.eval₂_X, ih])
+    (λ L ih, by rw [free_ring.lift_neg, ← neg_one_mul, polynomial.eval₂_mul,
+        ← polynomial.C_1, ← polynomial.C_neg, polynomial.eval₂_C,
+        int.cast_neg, int.cast_one, neg_one_mul, ih])
+    (λ x1 x2 ih1 ih2, by rw [free_ring.lift_add, polynomial.eval₂_add, ih1, ih2])
+  end,
+  right_inv := λ x, begin
+    haveI : is_semiring_hom (coe : int → free_ring punit.{u+1}) :=
+      @@is_ring_hom.is_semiring_hom _ _ _ (@@int.cast.is_ring_hom _),
+    have : ∀ i : ℤ, free_ring.lift (λ _ : punit, polynomial.X) ↑i = polynomial.C i,
+    { exact λ i, int.induction_on i
+      (by rw [int.cast_zero, free_ring.lift_zero, polynomial.C_0])
+      (λ i ih, by rw [int.cast_add, int.cast_one, free_ring.lift_add, free_ring.lift_one, ih, polynomial.C_add, polynomial.C_1])
+      (λ i ih, by rw [int.cast_sub, int.cast_one, free_ring.lift_sub, free_ring.lift_one, ih, polynomial.C_sub, polynomial.C_1]) },
+    exact polynomial.induction_on x
+    (λ i, by rw [polynomial.eval₂_C, this])
+    (λ p q ihp ihq, by rw [polynomial.eval₂_add, free_ring.lift_add, ihp, ihq])
+    (λ n i ih, by rw [polynomial.eval₂_mul, polynomial.eval₂_pow, polynomial.eval₂_C, polynomial.eval₂_X,
+        free_ring.lift_mul, free_ring.lift_pow, free_ring.lift_of, this])
+  end,
+  hom := by apply_instance }