English
Let p ⊆ M, f: M₂ →ₛₗ[σ₂₁] M be a restricted linear map along p. Then Submodule.map (codRestrict p f h) p' equals comap p.subtype (p'.map f).
Русский
Пусть p ⊆ M, f: M₂ →ₛₗ[σ₂₁] M — ограниченное линейное отображение вдоль p. Тогда Submodule.map (codRestrict p f h) p' = comap p.subtype (p'.map f).
LaTeX
$$$ Submodule.map (codRestrict p f h) p' = comap p.subtype (p'.map f) $$$
Lean4
/-- A linear equivalence of two modules restricts to a linear equivalence from any submodule
`p` of the domain onto the image of that submodule.
This is the linear version of `AddEquiv.submonoidMap` and `AddEquiv.subgroupMap`.
This is `LinearEquiv.ofSubmodule'` but with `map` on the right instead of `comap` on the left. -/
def submoduleMap (p : Submodule R M) : p ≃ₛₗ[σ₁₂] ↥(p.map (e : M →ₛₗ[σ₁₂] M₂) : Submodule R₂ M₂) :=
{
((e : M →ₛₗ[σ₁₂] M₂).domRestrict p).codRestrict (p.map (e : M →ₛₗ[σ₁₂] M₂)) fun x =>
⟨x, by
simp only [LinearMap.domRestrict_apply, and_true, SetLike.coe_mem,
SetLike.mem_coe]⟩ with
invFun := fun y =>
⟨(e.symm : M₂ →ₛₗ[σ₂₁] M) y, by
rcases y with ⟨y', hy⟩
rw [Submodule.mem_map] at hy
rcases hy with ⟨x, hx, hxy⟩
subst hxy
simp only [symm_apply_apply, coe_coe, hx]⟩
left_inv := fun x => by
simp only [LinearMap.domRestrict_apply, LinearMap.codRestrict_apply, LinearMap.toFun_eq_coe, LinearEquiv.coe_coe,
LinearEquiv.symm_apply_apply, SetLike.eta]
right_inv := fun y => by
apply SetCoe.ext
simp only [LinearMap.domRestrict_apply, LinearMap.codRestrict_apply, LinearMap.toFun_eq_coe, LinearEquiv.coe_coe,
LinearEquiv.apply_symm_apply] }
