English
There is a natural isomorphism between the set of compatible families of additive monoid homomorphisms and ring homomorphisms from the direct sum to R.
Русский
Существует естественное изоморфизм между множеством совместимых семейств гомоморфизмов аддитивных моноидов и кольцевыми гомоморфизмами из прямой суммы в R.
LaTeX
$$$$\text{An equivalence }\mathrm{liftRingHom}:\{f: \forall i, A_i\to+ R\mid f\text{ satisfies unit and compatibilities}\} \simeq (\bigoplus_i A_i) \to^{+*} R.$$$$
Lean4
/-- Families of `AddMonoidHom`s preserving `DirectSum.One.one` and `DirectSum.Mul.mul`
are isomorphic to `RingHom`s on `⨁ i, A i`. This is a stronger version of `DFinsupp.liftAddHom`.
-/
@[simps]
def liftRingHom :
{ f : ∀ {i}, A i →+ R //
f GradedMonoid.GOne.one = 1 ∧ ∀ {i j} (ai : A i) (aj : A j), f (GradedMonoid.GMul.mul ai aj) = f ai * f aj } ≃
((⨁ i, A i) →+* R)
where
toFun f := toSemiring (fun _ => f.1) f.2.1 f.2.2
invFun
F :=
⟨by intro i; exact (F : (⨁ i, A i) →+ R).comp (of _ i),
by
simp only [AddMonoidHom.comp_apply]
rw [← F.map_one]
rfl, by
intro i j ai aj
simp only [AddMonoidHom.comp_apply, AddMonoidHom.coe_coe]
rw [← F.map_mul (of A i ai), of_mul_of ai]⟩
left_inv
f := by
ext xi xv
exact toAddMonoid_of (fun _ => f.1) xi xv
right_inv
F := by
apply RingHom.coe_addMonoidHom_injective
refine DirectSum.addHom_ext' (fun xi ↦ AddMonoidHom.ext (fun xv ↦ ?_))
simp only [DirectSum.toAddMonoid_of, AddMonoidHom.comp_apply, toSemiring_coe_addMonoidHom]
