Skip to content

Instantly share code, notes, and snippets.

@ChrisHughes24
Last active October 15, 2021 12:30
Show Gist options
  • Save ChrisHughes24/a49961f41d9cc8b2475bcea8dc524951 to your computer and use it in GitHub Desktop.
Save ChrisHughes24/a49961f41d9cc8b2475bcea8dc524951 to your computer and use it in GitHub Desktop.
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]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment