English
A linear isomorphism induces a linear equivalence on function spaces with a domain-multiplicative action.
Русский
Линейный изоморфизм индуцирует линейное эквив между пространствами функций с действием по домену-умножению.
LaTeX
$$$\text{domMulActCongrRight} : (M_1 \to_{\sigma_{11}'} M_1') \simeq (M_1 \to_{\sigma_{12}'} M_2')$$$
Lean4
/-- A linear isomorphism between the domains an codomains of two spaces of linear maps gives a
linear isomorphism with respect to an action on the domains. -/
@[simps]
def domMulActCongrRight [Semiring S] [Module S M₁] [SMulCommClass R₁ S M₁] [RingHomCompTriple σ₁₂' σ₂'₁' σ₁₁']
(e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂') : (M₁ →ₛₗ[σ₁₁'] M₁') ≃ₗ[Sᵈᵐᵃ] (M₁ →ₛₗ[σ₁₂'] M₂')
where
__ := arrowCongrAddEquiv (.refl ..) e₂
map_smul' := DomMulAct.mk.forall_congr_right.mp fun _ _ ↦ by ext; simp
