English
Let p ⊆ V be finite-dimensional and f: V → V with f(p) ⊆ p and p, ker f disjoint; then p.comap f = p ⊔ ker f.
Русский
Пусть p ⊆ V конечномерно; если f(p) ⊆ p и p ∩ ker f = {0}, то f^{-1}(p) = p + ker f.
LaTeX
$$$[\operatorname{FiniteDimensional}_K p] \{f: V \to V\} (h: \forall x \in p, f x \in p) (h': \operatorname{Disjoint} p (\ker f)) : p.comap f = p \oplus ker f$$$
Lean4
theorem comap_eq_sup_ker_of_disjoint {p : Submodule K V} [FiniteDimensional K p] {f : V →ₗ[K] V} (h : ∀ x ∈ p, f x ∈ p)
(h' : Disjoint p (ker f)) : p.comap f = p ⊔ ker f :=
by
refine le_antisymm (fun x hx ↦ ?_) (sup_le_iff.mpr ⟨h, ker_le_comap _⟩)
obtain ⟨⟨y, hy⟩, hxy⟩ := surjective_of_injective ((injective_restrict_iff_disjoint h).mpr h') ⟨f x, hx⟩
replace hxy : f y = f x := by simpa [Subtype.ext_iff] using hxy
exact Submodule.mem_sup.mpr ⟨y, hy, x - y, by simp [hxy], add_sub_cancel y x⟩
