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

[jjaassoonn]

added a lemma stating that $(ab)_{i+j}=ab_j$ for homogeneous $a$ with degree $I$

Co-authored-by: Eric Wieser @eric-wieser

---

[eric-wieser]

Here's the version that I think we should have:

lemma direct_sum.coe_decompose_mul_add_of_left_mem {ι σ A}
  [decidable_eq ι] [add_left_cancel_monoid ι] [semiring A]
  [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι → σ) [graded_ring 𝒜]
  {a b : A} {i j : ι} (a_mem : a ∈ 𝒜 i) :
  (decompose 𝒜 (a * b) (i + j) : A) = a * decompose 𝒜 b j :=
begin
  lift a to ↥(𝒜 i) using a_mem,
  change ↥(𝒜 i) at a,
  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

We should probably have the right version too

Note in particular that hb wasn't needed.

[eric-wieser]

Or maybe even the stronger version,

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

for which there might be a shorter proof

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests