English
Applying the congruence map to a linear map f yields the expected evaluation: (arrowCongr e1 e2 f) x = e2 (f (e1^{-1} x)).
Русский
Применение конгруэнтного отображения к линейному отображению f даёт ожидаемое: (arrowCongr e1 e2 f) x = e2(f(e1^{-1} x)).
LaTeX
$$$\text{arrowCongr } e_1 e_2 f x = e_2 \bigl(f (e_1^{-1} x)\bigr)$$$
Lean4
/-- A linear isomorphism between the domains and codomains of two spaces of linear maps gives a
linear isomorphism between the two function spaces.
See `LinearEquiv.arrowCongrAddEquiv` for the additive version of this isomorphism that works
over a not necessarily commutative semiring. -/
def arrowCongr (e₁ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂') : (M₁ →ₛₗ[σ₁₁'] M₁') ≃ₛₗ[σ₁'₂'] (M₂ →ₛₗ[σ₂₂'] M₂')
where
__ := arrowCongrAddEquiv e₁ e₂
map_smul' c f := by ext; simp [arrowCongrAddEquiv, map_smulₛₗ]
