English
If e: α ≃ β, then conj(e) is the canonical identification (an equivalence) between endomorphisms of α and endomorphisms of β, given by f ↦ e ∘ f ∘ e^{-1}. This is the same as arrowCongr e e.
Русский
Пусть e: α ≃ β. Тогда conj(e) задаёт каноническое соответствие между концевыми отображениями α→α и β→β, заданное отображением f ↦ e ∘ f ∘ e^{-1}. Это то же самое, что arrowCongr e e.
LaTeX
$$$ \operatorname{conj}(e) = \operatorname{arrowCongr}(e, e) $$$
Lean4
/-- Conjugate a map `f : α → α` by an equivalence `α ≃ β`. -/
@[simps! (attr := grind =) apply]
def conj (e : α ≃ β) : (α → α) ≃ (β → β) :=
arrowCongr e e
