funny_error.lean

-- in this construction we do not care about the polynomials
-- we only want its universal mapping property

import data.finsupp data.equiv

class algebra (R : out_param Type*) (A : Type*)
  [out_param $ comm_ring R] extends comm_ring A :=
(f : R → A) [hom : is_ring_hom f]

instance algebra.to_is_ring_hom (R : out_param Type*) (A : Type*)
  [out_param $ comm_ring R] [algebra R A] : is_ring_hom (algebra.f A) :=
algebra.hom A

instance algebra.to_module (R : out_param Type*) (A : Type*)
  [out_param $ comm_ring R] [algebra R A] : module R A :=
{ smul := λ r x, algebra.f A r * x,
  smul_add := λ r x y, mul_add (algebra.f A r) x y,
  add_smul := λ r s x, show algebra.f A (r + s) * x
      = algebra.f A r * x + algebra.f A s * x,
    by rw [is_ring_hom.map_add (algebra.f A), add_mul],
  mul_smul := λ r s x, show algebra.f A (r * s) * x
      = algebra.f A r * (algebra.f A s * x),
    by rw [is_ring_hom.map_mul (algebra.f A), mul_assoc],
  one_smul := λ x, show algebra.f A 1 * x = x,
    by rw [is_ring_hom.map_one (algebra.f A), one_mul] }

theorem algebra.smul_def (R : out_param Type*) (A : Type*)
  [out_param $ comm_ring R] [algebra R A] (c : R) (x : A) :
  c • x = algebra.f A c * x := rfl

class is_alg_hom {R : out_param Type*} {A : Type*} {B : Type*}
  [out_param $ comm_ring R] [algebra R A] [algebra R B]
  (φ : A → B) extends is_ring_hom φ : Prop :=
(commute : ∀ r, φ (algebra.f A r) = algebra.f B r)

def alg_hom {R : out_param Type*} (A : Type*) (B : Type*)
  [out_param $ comm_ring R] [algebra R A] [algebra R B] :=
{ φ : A → B // is_alg_hom φ }

instance alg_hom.to_is_alg_hom {R : out_param Type*} (A : Type*) (B : Type*)
  [out_param $ comm_ring R] [algebra R A] [algebra R B]
  (φ : alg_hom A B) : is_alg_hom φ.val :=
φ.property

instance alg_hom.to_is_ring_hom {R : out_param Type*} (A : Type*) (B : Type*)
  [out_param $ comm_ring R] [algebra R A] [algebra R B]
  (φ : alg_hom A B) : is_ring_hom φ.val :=
by apply_instance

variables (R : Type*) [decidable_eq R] [comm_ring R]

def polynomial : Type* := ℕ →₀ R

instance polynomial.comm_ring : comm_ring (polynomial R) :=
finsupp.to_comm_ring

instance polynomial.algebra : algebra R (polynomial R) :=
{ f := λ r, finsupp.single 0 r,
  hom :=
  { map_add := λ x y, finsupp.single_add,
    map_mul := λ x y, show finsupp.single (0 + 0) (x * y) = _, from finsupp.single_mul_single.symm,
    map_one := rfl } }

def polynomial.UMP (A : Type*) [algebra R A] :
  A ≃ alg_hom (polynomial R) A :=
{ to_fun := λ r, ⟨λ f, f.sum $ λ n c, c • r^n,
    have H1 : ∀ n c, finsupp.sum (finsupp.single n c) (λ (n : ℕ) (c : R), c • r ^ n) = c • r ^ n,
      from λ n c, finsupp.sum_single_index zero_smul,
    have Hp : ∀ f g : polynomial R, finsupp.sum (f + g) (λ (n : ℕ) (c : R), c • r ^ n) =
        finsupp.sum f (λ (n : ℕ) (c : R), c • r ^ n)
        + finsupp.sum g (λ (n : ℕ) (c : R), c • r ^ n),
      from λ f g, finsupp.sum_add_index (λ _, zero_smul) (λ _ _ _, add_smul),
    { map_add := Hp,
      map_mul :=
  begin
    intros f g,
    change finsupp.sum (f * g) (λ (n : ℕ) (c : R), c • r ^ n) =
      finsupp.sum f (λ (n : ℕ) (c : R), c • r ^ n) * finsupp.sum g (λ (n : ℕ) (c : R), c • r ^ n),
    rw [finsupp.mul_def, finsupp.sum_sum_index],
    apply finsupp.induction f,
    { simp [finsupp.sum_zero_index] },
    { intros n c f hf hc ih,
      rw [finsupp.sum_add_index, finsupp.sum_single_index, ih],
      rw [Hp, H1, add_mul],
      suffices : finsupp.sum (finsupp.sum g (λ (a₂ : ℕ) (b₂ : R), finsupp.single (n + a₂) (c * b₂)))
        (λ (n : ℕ) (c : R), c • r ^ n)
        = c • r ^ n * finsupp.sum g (λ (n : ℕ) (c : R), c • r ^ n),
      { rw this },
      apply finsupp.induction g,
      { simp [finsupp.sum_zero_index] },
      { intros n c g hg hc ih,
        rw [finsupp.sum_add_index, finsupp.sum_single_index],
        rw [Hp, H1, ih, Hp, H1],
        rw [mul_add, mul_smul, pow_add],
        rw [algebra.smul_def, algebra.smul_def, algebra.smul_def, algebra.smul_def],
        ac_refl,
        { rw [mul_zero, finsupp.single_zero] },
        { intros, rw [mul_zero, finsupp.single_zero] },
        { intros,
          rw [mul_add, finsupp.single_add] } },
      { convert finsupp.sum_zero_index,
        convert finsupp.sum_zero,
        funext,
        rw [zero_mul, finsupp.single_zero],
        apply_instance, apply_instance },
      { intros,
        convert finsupp.sum_zero_index,
        convert finsupp.sum_zero,
        funext,
        rw [zero_mul, finsupp.single_zero],
        apply_instance, apply_instance },
      { intros a r s,
        apply finsupp.induction g,
        { simp [finsupp.sum_zero_index] },
        { intros n c g hg hc ih,
          convert Hp _ _,
          convert finsupp.sum_add,
          { funext, rw [add_mul, finsupp.single_add] },
          apply_instance, apply_instance } } },
      { intros, apply zero_smul },
      { intros, apply add_smul }
  end,
      map_one := by convert H1 0 1; rw [one_smul]; refl,
      commute := λ r, by unfold algebra.f;
        rw [finsupp.sum_single_index];
        [apply mul_one, { change (0:R) • (1:A) = 0, apply zero_smul }]}⟩,
  inv_fun := λ φ, φ.1 (finsupp.single 1 1),
  left_inv := λ r, by dsimp; rw [finsupp.sum_single_index];
    [{ change (1:R) • (r^1:A) = r, rw [one_smul, pow_one] },
     { change (0:R) • (r^1:A) = 0, apply zero_smul }],
  right_inv := _ }