English
There is a natural equivalence between monoid homomorphisms M →* N and MulAction M on N together with a scalar tower IsScalarTower M N N. Concretely, f ↦ (MulAction.compHom N f, IsScalarTower M N N) and conversely the inverse maps a compatible action to smulOneHom.
Русский
Существуют естественные взаимно однозначные соответствия между моноид-гомоморфизмами M →* N и структурой MulAction M на N с условием IsScalarTower M N N. Конструктивно: f ↦ (MulAction.compHom N f, IsScalarTower M N N); обратное восстанавливает smulOneHom из действия.
LaTeX
$$$\operatorname{MonoidHom}(M,N) \simeq \{\_inst : \operatorname{MulAction} M N \;\mid\; \operatorname{IsScalarTower} M N N\}$$$
Lean4
/-- A monoid homomorphism between two monoids M and N can be equivalently specified by a
multiplicative action of M on N that is compatible with the multiplication on N. -/
@[to_additive /-- A monoid homomorphism between two additive monoids M and N can be equivalently
specified by an additive action of M on N that is compatible with the addition on N. -/
]
def monoidHomEquivMulActionIsScalarTower (M N) [Monoid M] [Monoid N] :
(M →* N) ≃ { _inst : MulAction M N // IsScalarTower M N N }
where
toFun f := ⟨MulAction.compHom N f, SMul.comp.isScalarTower _⟩
invFun := fun ⟨_, _⟩ ↦ MonoidHom.smulOneHom
left_inv f := MonoidHom.ext fun m ↦ mul_one (f m)
right_inv := fun ⟨_, _⟩ ↦ Subtype.ext <| MulAction.ext <| funext₂ <| smul_one_smul N
