feat(linear_algebra/linear_combination): algebra structure on lc

src/linear_algebra/linear_combination.lean

@@ -5,7 +5,7 @@ Authors: Johannes Hölzl, Mario Carneiro
 
 The module `lc α β` of linear combinations over `β` (`α` is the scalar ring)
 -/
-import linear_algebra.basic
+import linear_algebra.basic ring_theory.algebra
 noncomputable theory
 
 open classical function lattice
@@ -257,3 +257,146 @@ lemma linear_eq_on {f g : β →ₗ[α] γ} (H : ∀x∈s, f x = g x) {x} (h : x
 by apply span_induction h H; simp {contextual := tt}
 
 end module
+
+namespace lc
+open finsupp
+/-
+If A is an R-algebra, then there is a natural algebra structure
+on lc R A. If A is commutative, then so is lc R A.
+-/
+
+section algebra
+variables {R : Type*} {A : Type*} [comm_ring R] [ring A] [algebra R A]
+variables (f g h : lc R A)
+
+def one : lc R A := single 1 1
+
+instance : has_one (lc R A) := ⟨one⟩
+
+lemma one_def : (1 : lc R A) = single 1 1 := rfl
+
+def mul := f.sum $ λ r a, g.sum $ λ s b, single (r * s) (a * b)
+
+instance : has_mul (lc R A) := ⟨mul⟩
+
+lemma mul_def :
+  f * g = (f.sum $ λ r a, g.sum $ λ s b, single (r * s) (a * b)) := rfl
+
+@[simp] lemma one_mul : 1 * f = f :=
+by simp [one_def, mul_def, sum_single_index]
+
+@[simp] lemma mul_one : f * 1 = f :=
+by simp [one_def, mul_def, sum_single_index]
+
+lemma mul_assoc : (f * g) * h = f * (g * h) :=
+begin
+  repeat {rw mul_def},
+  iterate 2 { rw sum_sum_index, congr' 1, funext, rw sum_sum_index },
+  { simp only [sum_single_index, zero_mul, sum_zero, single_zero, mul_zero],
+    congr' 1, funext,
+    repeat {rw mul_assoc} },
+  all_goals { intros, try {rw ← sum_add}, simp [left_distrib, right_distrib] }
+end
+
+instance : monoid (lc R A) :=
+{ mul := mul,
+  mul_assoc := mul_assoc,
+  one_mul := one_mul,
+  mul_one := mul_one,
+  ..lc.has_one }
+
+lemma left_distrib : f * (g + h) = f * g + f * h :=
+by simp only [mul_def, sum_add_index, left_distrib, sum_add, sum_zero, mul_zero,
+  single_add, single_zero, eq_self_iff_true, add_right_inj, forall_3_true_iff, forall_true_iff]
+
+lemma right_distrib : (f + g) * h = f * h + g * h :=
+by simp only [mul_def, sum_add_index, right_distrib, sum_add, sum_zero, zero_mul,
+  single_add, single_zero, eq_self_iff_true, add_right_inj, forall_3_true_iff, forall_true_iff]
+
+instance : ring (lc R A) :=
+{ left_distrib := left_distrib,
+  right_distrib := right_distrib,
+  ..lc.monoid,
+  ..lc.add_comm_group }
+
+instance single.is_ring_hom : is_ring_hom (single 1 : R → lc R A) :=
+{ map_one := rfl,
+  map_mul := λ _ _, by simp [mul_def, sum_single_index],
+  map_add := λ _ _, single_add }
+
+instance single_swap.is_monoid_hom :
+  is_monoid_hom ((λ r, single (algebra_map A r) 1) : R → lc R A) :=
+{ map_one := by simpa,
+  map_mul := λ _ _, by simp [mul_def, sum_single_index] }
+
+instance : algebra R (lc R A) :=
+{ to_fun := single 1,
+  hom := by apply_instance,
+  commutes' := by simp [mul_def, sum_single_index, mul_comm],
+  smul_def' := λ r f, finsupp.induction f (by simp) $ λ a b f ha hb IH,
+    by simp [mul_def, sum_single_index, smul_add, IH, left_distrib] }
+
+instance total.is_ring_hom : is_ring_hom (lc.total R A) :=
+{ map_one := by rw [one_def, total_single, one_smul],
+  map_mul := λ f g,
+  begin
+    repeat {erw total_apply},
+    rw [mul_def, sum_mul],
+    simp only [mul_sum],
+    iterate 2 {
+      rw sum_sum_index,
+      apply finset.sum_congr rfl,
+      intros _ _,
+      change finsupp.sum _ _ = _ },
+    { change _ = _ • _ * _ • _,
+      rw [algebra.smul_mul_assoc, algebra.mul_smul_comm, smul_smul, sum_single_index],
+      apply zero_smul },
+    all_goals { simp [add_smul, smul_add] },
+  end,
+  map_add := (lc.total R A).map_add }
+
+def atotal : lc R A →ₐ[R] A :=
+{ hom := by apply_instance,
+  commutes' := λ r, by convert total_single _ _; simp [algebra.smul_def],
+  ..lc.total R A }
+
+section
+open finset
+
+lemma support_mul (f g : lc R A) :
+  (f * g).support ⊆ (image (λ x : A × A, x.fst * x.snd) $ f.support.product g.support) :=
+begin
+  refine subset.trans support_sum _,
+  intros a' ha,
+  rcases mem_bind.mp ha with ⟨a, ha₁, ha₂⟩,
+  rcases mem_bind.mp (finsupp.support_sum ha₂) with ⟨b, hb₁, hb₂⟩,
+  have H := set.mem_singleton_iff.mp (finsupp.support_single_subset hb₂),
+  rw mem_image,
+  use (a, b),
+  simp [*, mem_product],
+end
+
+end
+
+end algebra
+
+section comm
+open finset
+variables {R : Type*} {A : Type*} [comm_ring R] [comm_ring A] [algebra R A]
+variables (f g : lc R A)
+
+lemma mul_comm : f * g = g * f :=
+begin
+  simp only [mul_def, finsupp.sum],
+  rw sum_comm,
+  iterate 2 {congr' 1, funext},
+  congr' 1; rw mul_comm,
+end
+
+instance : comm_ring (lc R A) :=
+{ mul_comm := mul_comm,
+  ..lc.ring }
+
+end comm
+
+end lc