English
An isomorphism is established between structured families and RingHom objects from the direct sum, preserving unit and multiplication across indices.
Русский
Установлено изоморфизм между структурированными семействами и объектами RingHom от прямой суммы, сохраняющими единицу и умножение по индексам.
LaTeX
$$$$\mathrm{liftRingHom}:\Big\{ f: \forall {i}, A_i \to+ R \,\Big|\, f(1)=1 \land \forall i,j\, f(i)\cdot f(j)=f(i\ast j) \Big\} \cong (\bigoplus_i A_i) \to^{+*} R.$$$$
Lean4
/-- A direct sum of copies of a `Semiring` inherits the multiplication structure. -/
instance directSumGSemiring {R : Type*} [AddMonoid ι] [Semiring R] : DirectSum.GSemiring fun _ : ι => R
where
__ := NonUnitalNonAssocSemiring.directSumGNonUnitalNonAssocSemiring ι
__ := Monoid.gMonoid ι
natCast n := n
natCast_zero := Nat.cast_zero
natCast_succ := Nat.cast_succ
