equivProdOfSurjectiveOfIsCompl — Mathlib

English

The canonical identification of the equivalence with the pair of maps (f,g) is the identity on F×G.

Русский

Каноническим образом идентификация эквивалентности сообразуется с парой отображений (f,g).

LaTeX

$$$(equivProdOfSurjectiveOfIsCompl f g hf hg hfg : E\to F\times G) = f.prod g$$$

Lean4

/-- If `f : E →ₗ[R] F` and `g : E →ₗ[R] G` are two surjective linear maps and
their kernels are complement of each other, then `x ↦ (f x, g x)` defines
a linear equivalence `E ≃ₗ[R] F × G`. -/
def equivProdOfSurjectiveOfIsCompl (f : E →ₗ[R] F) (g : E →ₗ[R] G) (hf : range f = ⊤) (hg : range g = ⊤)
    (hfg : IsCompl (ker f) (ker g)) : E ≃ₗ[R] F × G :=
  LinearEquiv.ofBijective (f.prod g)
    ⟨by simp [← ker_eq_bot, hfg.inf_eq_bot], by
      rw [← range_eq_top]
      simp [range_prod_eq hfg.sup_eq_top, *]⟩

Похожие утверждения