English
A family of additive monoid homomorphisms preserving unit and multiplication yields a Ring structure on the direct sum.
Русский
Семейство гомоморфизмов, сохраняющих единицу и умножение, задаёт кольцо на прямой сумме.
LaTeX
$$$$\\text{toSemiring}(f) : (\\bigoplus_i A_i) \\to \\* R\\,,$$ with hone and hmul ensuring a RingHom on the DirectSum.$$
Lean4
/-- A family of `AddMonoidHom`s preserving `DirectSum.One.one` and `DirectSum.Mul.mul`
describes a `RingHom`s on `⨁ i, A i`. This is a stronger version of `DirectSum.toMonoid`.
Of particular interest is the case when `A i` are bundled subobjects, `f` is the family of
coercions such as `AddSubmonoid.subtype (A i)`, and the `[GSemiring A]` structure originates from
`DirectSum.gsemiring.ofAddSubmonoids`, in which case the proofs about `GOne` and `GMul`
can be discharged by `rfl`. -/
@[simps]
def toSemiring (f : ∀ i, A i →+ R) (hone : f _ GradedMonoid.GOne.one = 1)
(hmul : ∀ {i j} (ai : A i) (aj : A j), f _ (GradedMonoid.GMul.mul ai aj) = f _ ai * f _ aj) : (⨁ i, A i) →+* R :=
{ toAddMonoid f with
toFun := toAddMonoid f
map_one' := by
change (toAddMonoid f) (of _ 0 _) = 1
rw [toAddMonoid_of]
exact hone
map_mul' := by
rw [(toAddMonoid f).map_mul_iff]
refine DirectSum.addHom_ext' (fun xi ↦ AddMonoidHom.ext (fun xv ↦ ?_))
refine DirectSum.addHom_ext' (fun yi ↦ AddMonoidHom.ext (fun yv ↦ ?_))
change toAddMonoid f (of A xi xv * of A yi yv) = toAddMonoid f (of A xi xv) * toAddMonoid f (of A yi yv)
simp_rw [of_mul_of, toAddMonoid_of]
exact hmul _ _ }
