English
Postcomposition with a multiplicative equivalence e : N1 ≃* N2 induces an equivalence between MonoidHoms M →* N1 and MonoidHoms M →* N2.
Русский
Посткомпозиция с умножительной эквивалентностью e : N1 ≃* N2 индуцирует эквивалентность между MonoidHom M →* N1 и MonoidHom M →* N2.
LaTeX
$$$ (M \to^* N_1) \cong^* (M \to^* N_2), \quad f \mapsto e \circ f, \quad g \mapsto e^{-1} \circ g. $$$
Lean4
/-- The equivalence `(M →* N₁) ≃ (M →* N₂)` obtained by postcomposition with
a multiplicative equivalence `e : N₁ ≃* N₂`. -/
@[to_additive (attr := simps) /-- The equivalence `(M →+ N₁) ≃ (M →+ N₂)` obtained by postcomposition with
an additive equivalence `e : N₁ ≃+ N₂`. -/
]
def monoidHomCongrRightEquiv (e : N₁ ≃* N₂) : (M →* N₁) ≃ (M →* N₂)
where
toFun := e.toMonoidHom.comp
invFun := e.symm.toMonoidHom.comp
left_inv f := by ext; simp
right_inv f := by ext; simp
