English
If f: M → N is injective and p ≤ range f, then p.comap f ≃ p as linear spaces, giving a natural isomorphism between p pulled back along f and p.
Русский
Если f: M → N инъективно и p ≤ range f, то p.comap f эквивалентно p как линейные пространства, образуя изоморфизм между подпространствами.
LaTeX
$$$p\\comap f \\simeq p$ under the given injectivity and inclusion conditions.$$
Lean4
/-- A linear injection `M ↪ N` restricts to an equivalence `f⁻¹ p ≃ p` for any submodule `p`
contained in its range. -/
@[simps! apply]
noncomputable def comap_equiv_self_of_inj_of_le {f : M →ₗ[R] N} {p : Submodule R N} (hf : Injective f)
(h : p ≤ LinearMap.range f) : p.comap f ≃ₗ[R] p :=
LinearEquiv.ofBijective ((f ∘ₗ (p.comap f).subtype).codRestrict p <| fun ⟨_, hx⟩ ↦ mem_comap.mp hx)
(⟨fun x y hxy ↦ by simpa using hf (Subtype.ext_iff.mp hxy), fun ⟨x, hx⟩ ↦ by obtain ⟨y, rfl⟩ := h hx;
exact ⟨⟨y, hx⟩, by simp [Subtype.ext_iff]⟩⟩)
