English
There is a natural equivalence between ring homomorphisms R →+* S and R-module structures on S that make S a scalar tower over R.
Русский
Существует естественное эквивалентное соответствие между кольцевыми гомоморфизмами R →+* S и R-модульными структурами на S, делающими S скалярной башней над R.
LaTeX
$$$(R \\to+* S) \\simeq \\{\\ _{\\text{inst}} : \\text{Module } R S \\,|\\, \\ IsScalarTower R S S\\}$$$
Lean4
/-- A homomorphism between semirings R and S can be equivalently specified by a R-module
structure on S such that S/S/R is a scalar tower. -/
def ringHomEquivModuleIsScalarTower [Semiring R] [Semiring S] :
(R →+* S) ≃ { _inst : Module R S // IsScalarTower R S S }
where
toFun f := ⟨Module.compHom S f, SMul.comp.isScalarTower _⟩
invFun := fun ⟨_, _⟩ ↦ RingHom.smulOneHom
left_inv f := RingHom.ext fun r ↦ mul_one (f r)
right_inv := fun ⟨_, _⟩ ↦ Subtype.ext <| Module.ext <| funext₂ <| smul_one_smul S
