English
If two linear maps f:E→F and g:E→G are surjective and ker f, ker g are complementary, then E is linearly isomorphic to F × G via x↦(f x, g x).
Русский
Если f: E→F и g: E→G сюръективны и ker f, ker g образуют дополнение, то существует линейное биективное отображение E ≃ F×G через x↦(f x, g x).
LaTeX
$$$\text{If } range(f)=⊤,\ range(g)=⊤,\ IsCompl(ker f, ker g)\text{ then } E \cong F\times G.$$$
Lean4
/-- The natural linear equivalence between `(p →ₗ[R₁] F) × (q →ₗ[R₁] F)` and `E →ₗ[R₁] F`. -/
def ofIsComplProdEquiv {p q : Submodule R₁ E} (h : IsCompl p q) : ((p →ₗ[R₁] F) × (q →ₗ[R₁] F)) ≃ₗ[R₁] E →ₗ[R₁] F :=
{ ofIsComplProd h with
invFun := fun φ => ⟨φ.domRestrict p, φ.domRestrict q⟩
left_inv := fun φ ↦ by
ext x
· exact ofIsCompl_left_apply h x
· exact ofIsCompl_right_apply h x
right_inv := fun φ ↦ by
ext x
obtain ⟨a, b, hab, _⟩ := existsUnique_add_of_isCompl h x
rw [← hab]; simp }
