quotientEquivOfIsCompl — Mathlib

English

If p,q are submodules with IsCompl, the quotient E/p is linearly isomorphic to q via the quotientEquivOfIsCompl; i.e., there is a linear equivalence (E/p) ≃_R q.

Русский

Если p и q подподмодули с IsCompl, то фактор-модуль E/p изоморфен q через quotientEquivOfIsCompl; существует линейное эквивалентное отображение (E/p) ≃_R q.

LaTeX

$$$(E/p) \\cong_R q$$$

Lean4

/-- If `q` is a complement of `p`, then `M/p ≃ q`. -/
def quotientEquivOfIsCompl (h : IsCompl p q) : (E ⧸ p) ≃ₗ[R] q :=
  LinearEquiv.symm <|
    LinearEquiv.ofBijective (p.mkQ.comp q.subtype)
      ⟨by rw [← ker_eq_bot, ker_comp, ker_mkQ, disjoint_iff_comap_eq_bot.1 h.symm.disjoint], by
        rw [← range_eq_top, range_comp, range_subtype, map_mkQ_eq_top, h.sup_eq_top]⟩

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