English
An isomorphism between function spaces induced by linear equivalences e1 and e2 is an additive equivalence commuting with addition.
Русский
Изоморфизм между пространствами функций, индуцируемый линейными эквивалентами e1 и e2, является аддитивным сопоставлением, сохраняющим сложение.
LaTeX
$$$[\text{simps}]\text{ def arrowCongrAddEquiv }(e_1,e_2): (M_1 \to_{\sigma_{11}'} M_1') \oplus (M_2 \to_{\sigma_{11}'} M_2') \to+ (M_2 \to_{\sigma_{22}'} M_2')$$$
Lean4
/-- A linear isomorphism between the domains and codomains of two spaces of linear maps gives an
additive isomorphism between the two function spaces.
See also `LinearEquiv.arrowCongr` for the linear version of this isomorphism. -/
@[simps]
def arrowCongrAddEquiv (e₁ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂') : (M₁ →ₛₗ[σ₁₁'] M₁') ≃+ (M₂ →ₛₗ[σ₂₂'] M₂')
where
toFun f := (e₂.comp f).comp e₁.symm.toLinearMap
invFun f := (e₂.symm.comp f).comp e₁.toLinearMap
left_inv
f := by
ext x
simp only [symm_apply_apply, Function.comp_apply, coe_comp, coe_coe]
right_inv
f := by
ext x
simp only [Function.comp_apply, apply_symm_apply, coe_comp, coe_coe]
map_add' f
g := by
ext x
simp only [map_add, add_apply, Function.comp_apply, coe_comp, coe_coe]
