English
Given an AlgEquiv f: A ≃ₐ[R] B, there is a natural AlgEquiv between Submodules: Submodule R A ≃ₐ[Ideal R] Submodule R B, induced by f.
Русский
Для AlgEquiv f: A ≃ₐ[R] B существует естественный AlgEquiv между Submodule R A и Submodule R B, индуцированный f.
LaTeX
$$$\\text{Submodule}(R,A) \\simeq_{\\text{Alg}} \\text{Submodule}(R,B)$$$
Lean4
/-- `Submonoid.map` as an `AlgEquiv`, when applied to an `AlgEquiv`. -/
-- TODO: when A, B noncommutative, still has `MulEquiv`.
@[simps!]
def mapAlgEquiv (f : A ≃ₐ[R] B) : Submodule R A ≃ₐ[Ideal R] Submodule R B
where
__ := mapAlgHom f
invFun := mapAlgHom f.symm
left_inv I := (map_comp _ _ I).symm.trans <| (congr_arg (map · I) <| LinearMap.ext (f.left_inv ·)).trans (map_id I)
right_inv I := (map_comp _ _ I).symm.trans <| (congr_arg (map · I) <| LinearMap.ext (f.right_inv ·)).trans (map_id I)
