poly_assoc.lean

import linear_algebra.finsupp

variables {R α M N P : Type} [comm_ring R] [add_comm_group M] [module R M]
variables [add_comm_group N] [module R N]
variables [add_comm_group P] [module R P]

noncomputable theory

namespace poly_example

variables (R α)

@[derive add_comm_group, derive module R]
def free_module : Type := finsupp α R

variables {R α}

def lift (f : α → M) : free_module R α →ₗ[R] M :=
finsupp.total _ _ _ f

def X (a : α) : free_module R α := finsupp.single a 1

@[simp] lemma lift_X (f : α → M) (a : α) : lift f (X a : free_module R α) = f a :=
by simp [lift, X]

@[ext] lemma hom_ext {f g : free_module R α →ₗ[R] M} (h : ∀ a, f (X a) = g (X a)) : f = g :=
by ext; simp [*, X] at *

def lcomp : (M →ₗ[R] N) →ₗ[R] (P →ₗ[R] M) →ₗ[R] (P →ₗ[R] N) :=
{ to_fun := λ f,
  { to_fun := linear_map.comp f,
    map_add' := by intros; ext; simp,
    map_smul' := by intros; ext; simp },
  map_add' := by intros; ext; simp,
  map_smul' := by intros; ext; simp }

def lcompop : (P →ₗ[R] M) →ₗ[R] (M →ₗ[R] N) →ₗ[R] (P →ₗ[R] N) :=
{ to_fun := λ f,
  { to_fun := λ g, linear_map.comp g f,
    map_add' := by intros; ext; simp,
    map_smul' := by intros; ext; simp },
  map_add' := by intros; ext; simp,
  map_smul' := by intros; ext; simp }

def swap : (M →ₗ[R] N →ₗ[R] P) →ₗ[R] (N →ₗ[R] M →ₗ[R] P) :=
{ to_fun := λ f,
  { to_fun := λ n,
    { to_fun := λ m, f m n,
      map_add' := λ _ _, by rw [f.map_add]; refl,
      map_smul' := λ _ _, by rw [f.map_smul]; refl, },
    map_add' := λ _ _, by simp only [(f _).map_add]; refl,
    map_smul' := λ _ _, by simp only [(f _).map_smul]; refl },
  map_add' := λ _ _, rfl,
  map_smul' := λ _ _, rfl }

variable {M}

attribute [irreducible] free_module lift X

def mul : free_module R ℕ →ₗ[R] free_module R ℕ →ₗ[R] free_module R ℕ :=
lift (λ n, lift (λ m, X (n + m)))

lemma mul_assoc (p q r : free_module R ℕ) : mul (mul p q) r = mul p (mul q r) :=
show (lcomp (@mul R _)).comp mul p q r = (lcompop (@mul R _)).comp (lcomp.comp mul) p q r,
--by congr' 3; ext; simp [lcomp, lcompop, mul, add_assoc]
begin
  congr' 3,
  apply hom_ext,
  intro,
  apply hom_ext,
  intro, 
  apply hom_ext,
  intro,
  dsimp [lcomp, lcompop, mul],
  rw [lift_X, lift_X, lift_X, lift_X, lift_X, lift_X, lift_X, add_assoc],
end

lemma mul_comm (p q : free_module R ℕ) : mul p q = mul q p :=
show mul p q = swap mul p q, by congr' 2; ext; simp [mul, swap, add_comm]