ring homomorphism commuting with direct sum inclusion

Stream: Is there code for X?

[Jujian Zhang]

f is a homomorphism between graded rings, is there a short proof for f commuting with of where of B i is the inclusion from $B_i \to \oplus_i B_i$ and similar for of A i, i.e. the following:

example {ι : Type*} [add_comm_monoid ι] (A B : ι → Type*) [Π (i : ι), add_comm_monoid (A i)]
  [Π (i : ι), add_comm_monoid (B i)] [gcomm_semiring A] [gcomm_semiring B]
  (f : (⨁ i, A i) →+* (⨁ i, B i)) (i : ι) (x : ⨁ i, A i) :
  f (of A i (x i)) = of B i ((f x) i) := sorry

[Johan Commelin]

@Jujian Zhang that's not true in general right? A hom of graded rings is a ring hom + a proof that it preserves the grading.

[Johan Commelin]

Also, not every graded ring in mathlib will be defeq to ⨁ i, A i, right? Something like mv_polynomial isn't of that shape. So I think a morphism of graded rings should take that into account.

[Kevin Buzzard]

I guess a counterexample would be the map on polynomial rings $k[X]\to k[X]$ sending $X$ to $X^2$.