English
If range f and range g are disjoint submodules of M₃, then ker(f.coprod g) = (ker f) × (ker g).
Русский
Если образы range f и range g являются поперечными подмодулями в M₃, то ker(f.coprod g) = (ker f) × (ker g).
LaTeX
$$$\\operatorname{ker}(f \\ coprod\\ g) = (\\ker f) \\times (\\ker g)\\quad\\text{whenever}\\quad \\mathrm{range}(f) \\cap \\mathrm{range}(g) = \\{0\\}.$$$
Lean4
theorem ker_coprod_of_disjoint_range {M₂ : Type*} [AddCommGroup M₂] [Module R M₂] {M₃ : Type*} [AddCommGroup M₃]
[Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (hd : Disjoint (range f) (range g)) :
ker (f.coprod g) = (ker f).prod (ker g) :=
by
apply le_antisymm _ (ker_prod_ker_le_ker_coprod f g)
rintro ⟨y, z⟩ h
simp only [mem_ker, mem_prod, coprod_apply] at h ⊢
have : f y ∈ (range f) ⊓ (range g) :=
by
simp only [true_and, mem_range, mem_inf, exists_apply_eq_apply]
use -z
rwa [eq_comm, map_neg, ← sub_eq_zero, sub_neg_eq_add]
rw [hd.eq_bot, mem_bot] at this
rw [this] at h
simpa [this] using h
