English
Postcomposition with a multiplicative equivalence e : M1 ≃* M2 gives a canonical equivalence between MonoidHom M1 N and MonoidHom M2 N; f ↦ f ∘ e⁻¹, with inverse g ↦ g ∘ e.
Русский
Посткомпозиция с умножительной эквивалентностью e : M1 ≃* M2 даёт каноническое соответствие между моноид-гомоморфизмами M1 →* N и M2 →* N: f ↦ f ∘ e⁻¹, с обратной g ↦ g ∘ e.
LaTeX
$$$ (M_1 \to^* N) \cong (M_2 \to^* N), \quad f \mapsto f \circ e^{-1}, \quad g \mapsto g \circ e. $$$
Lean4
/-- The equivalence `(M₁ →* N) ≃ (M₂ →* N)` obtained by postcomposition with
a multiplicative equivalence `e : M₁ ≃* M₂`. -/
@[to_additive (attr := simps) /-- The equivalence `(M₁ →+ N) ≃ (M₂ →+ N)` obtained by postcomposition with
an additive equivalence `e : M₁ ≃+ M₂`. -/
]
def monoidHomCongrLeftEquiv (e : M₁ ≃* M₂) : (M₁ →* N) ≃ (M₂ →* N)
where
toFun f := f.comp e.symm.toMonoidHom
invFun f := f.comp e.toMonoidHom
left_inv f := by ext; simp
right_inv f := by ext; simp
