English
If s is nonempty and p_i are submodules with a bi-supremum equal to top, then their comap under a surjective map has top as a supremum.
Русский
Если множество индексов непусто и biSup p_i = top, то подмодули comap f(p_i) имеют верхнюю грань.
LaTeX
$$$\bigvee_{i\in s} (p_i).comap f = \top$$$
Lean4
theorem _root_.LinearMap.range_domRestrict_eq_range_iff {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} :
LinearMap.range (f.domRestrict S) = LinearMap.range f ↔ S ⊔ (LinearMap.ker f) = ⊤ :=
by
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
· rw [eq_top_iff]
intro x _
have : f x ∈ LinearMap.range f := LinearMap.mem_range_self f x
rw [← h] at this
obtain ⟨y, hy⟩ : ∃ y : S, f.domRestrict S y = f x := this
have : (y : M) + (x - y) ∈ S ⊔ (LinearMap.ker f) := Submodule.add_mem_sup y.2 (by simp [← hy])
simpa using this
· refine le_antisymm (LinearMap.range_domRestrict_le_range f S) ?_
rintro x ⟨y, rfl⟩
obtain ⟨s, hs, t, ht, rfl⟩ : ∃ s, s ∈ S ∧ ∃ t, t ∈ LinearMap.ker f ∧ s + t = y := Submodule.mem_sup.1 (by simp [h])
exact ⟨⟨s, hs⟩, by simp [LinearMap.mem_ker.1 ht]⟩
