English
If f is injective, the map f yields a linear equivalence between a submodule p and its image p.map f.
Русский
Если отображение инъективно, то подмодуль p эквивалентен (линейно изоморфен) своему образу p.map f.
LaTeX
$$$p \\cong_{\\text{lin}} p.map f$ (при инъективности f)$$
Lean4
/-- The pushforward of a submodule by an injective linear map is
linearly equivalent to the original submodule. See also `LinearEquiv.submoduleMap` for a
computable version when `f` has an explicit inverse. -/
noncomputable def equivMapOfInjective (f : F) (i : Injective f) (p : Submodule R M) : p ≃ₛₗ[σ₁₂] p.map f :=
{
Equiv.Set.image f p
i with
map_add' := by
intros
simp only [coe_add, map_add, Equiv.toFun_as_coe, Equiv.Set.image_apply]
rfl
map_smul' :=
by
intros
-- Note: https://github.com/leanprover-community/mathlib4/pull/8386 changed `map_smulₛₗ` into `map_smulₛₗ _`
simp only [coe_smul_of_tower, map_smulₛₗ _, Equiv.toFun_as_coe, Equiv.Set.image_apply]
rfl }
