ker_eq_bot_range_liftQ_iff — Mathlib

English

For h: range f ≤ ker g, ker((range f).liftQ g h) = {0} iff ker g = range f.

Русский

Для h: range f ≤ ker g, ker((range f).liftQ g h) = {0} тогда и только тогда, когда ker g = range f.

LaTeX

$$$$ \\ker((\\operatorname{range} f).liftQ g h) = \\{0\\} \\iff \\ker g = \\operatorname{range} f. $$$$

Lean4

theorem ker_eq_bot_range_liftQ_iff (h : range f ≤ ker g) : ker ((range f).liftQ g h) = ⊥ ↔ ker g = range f :=
  by
  simp only [Submodule.ext_iff, mem_ker, Submodule.mem_bot, mem_range]
  constructor
  · intro hfg x
    simpa using hfg (Submodule.Quotient.mk x)
  · intro hfg x
    obtain ⟨x, rfl⟩ := Submodule.Quotient.mk_surjective _ x
    simpa using hfg x

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