[Merged by Bors] - feat(ring_theory/graded_algebra/basic): add lemma proj_homogeneous_mul

src/ring_theory/graded_algebra/basic.lean

@@ -103,6 +103,37 @@ dfinsupp.mem_support_iff.trans add_submonoid_class.coe_eq_zero.not.symm
 
 end graded_ring
 
+section add_left_cancel_monoid
+
+open direct_sum
+
+lemma direct_sum.decompose_mul_add_of_left_mem {ι σ A}
+  [decidable_eq ι] [add_left_cancel_monoid ι] [semiring A]
+  [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) [graded_ring 𝒜]
+  {i : ι} (a : 𝒜 i) {b : A} {j : ι} :
+  decompose 𝒜 (↑a * b) (i + j) =
+    @graded_monoid.ghas_mul.mul ι (λ i, 𝒜 i) _ _ _ _ a (decompose 𝒜 b j) :=
+begin
+  ext,
+  dsimp,
+  classical,
+  by_cases INEQ : a = 0,
+  { rw [INEQ, add_submonoid_class.coe_zero, zero_mul, zero_mul, decompose_zero, zero_apply,
+      add_submonoid_class.coe_zero], },
+
+  simp_rw [decompose_mul, direct_sum.coe_mul_apply, decompose_coe, direct_sum.support_of _ i a INEQ,
+    finset.singleton_product, finset.map_filter, finset.sum_map, function.comp,
+    function.embedding.coe_fn_mk],
+  dsimp,
+  simp_rw [direct_sum.of_eq_same, ←finset.mul_sum, add_right_inj, finset.filter_eq'],
+  by_cases hb : decompose 𝒜 b j = 0,
+  { rw [if_neg (dfinsupp.not_mem_support_iff.mpr hb), finset.sum_empty, hb,
+      add_submonoid_class.coe_zero] },
+  { rw [if_pos (dfinsupp.mem_support_iff.mpr hb), finset.sum_singleton] }
+end
+
+end add_left_cancel_monoid
+
 section graded_algebra
 variables [decidable_eq ι] [add_monoid ι] [comm_semiring R] [semiring A] [algebra R A]
 variables (𝒜 : ι → submodule R A)