English
Let f: M → M₂ and g: M → M₃ be linear maps. If the sum of their kernels ker f ⊔ ker g equals the whole space, then the range of the paired map f.prod g is exactly the product range, i.e., range(f × g) = range(f) × range(g).
Русский
Пусть f: M → M₂ и g: M → M₃ — линейные отображения. Если сумма их ядер покрывает всё пространство, то область значений пары (f, g) равна произведению областей значений: range(f × g) = range(f) × range(g).
LaTeX
$$$\\ker f \\sqcup \\ker g = \\top \\quad\\Rightarrow\\quad \\operatorname{range}(f\\,\\text{prod}\\, g) = \\operatorname{range}(f) \\;\\mathrm{.prod}\\; \\operatorname{range}(g)$$$
Lean4
/-- If the union of the kernels `ker f` and `ker g` spans the domain, then the range of
`Prod f g` is equal to the product of `range f` and `range g`. -/
theorem range_prod_eq {f : M →ₗ[R] M₂} {g : M →ₗ[R] M₃} (h : ker f ⊔ ker g = ⊤) :
range (prod f g) = (range f).prod (range g) :=
by
refine le_antisymm (f.range_prod_le g) ?_
simp only [SetLike.le_def, prod_apply, mem_range, mem_prod, exists_imp, and_imp, Prod.forall, Pi.prod]
rintro _ _ x rfl y rfl
simp only [Prod.mk_inj, ← sub_mem_ker_iff (f := f)]
have : y - x ∈ ker f ⊔ ker g := by simp only [h, mem_top]
rcases mem_sup.1 this with ⟨x', hx', y', hy', H⟩
refine ⟨x' + x, ?_, ?_⟩
· rwa [add_sub_cancel_right]
· simp [← eq_sub_iff_add_eq.1 H, map_add, mem_ker.mp hy']
