[Merged by Bors] - feat(ring_theory/polynomial/homogenous): add a direct_sum.gcomm_monoid instance

[eric-wieser]

This also corrects a stupid typo I made in direct_sum.comm_ring which was previously declared a ring!

---

I started out on trying to show:

/-- `homogeneous_component` but better? -/
def homogeneous_component' [comm_semiring R] (n : ℕ) :
  mv_polynomial σ R →ₗ[R] homogeneous_submodule σ R n :=
let f := finsupp.restrict_dom R R {d : σ →₀ ℕ | ∑ i in d.support, d i = n} in
(submodule.of_le $ (homogenous_submodule_eq_finsupp_supported _ _ _).symm.le).comp f

-- the real goal would be to make this an alg_hom, but baby steps!
def homogeneous_components [comm_semiring R] (n : ℕ) :
  mv_polynomial σ R →+* (⨁ i, homogeneous_submodule σ R i) :=
add_monoid_algebra.lift_nc_ring_hom
  { to_fun := λ r, r • 1,  -- this is basically `algebra_map`, which doesn't exist yet.
    map_one' := by { ext, simp, },
    map_mul' := λ x y, by { ext, simp, sorry },
    map_zero' := zero_smul _ _,
    map_add' := λ x y, add_smul _ _ _,}
  sorry
  sorry

but I think there's some API missing around direct_sum before that becomes easy, so want to punt it to future work, possibly for someone else.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

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