surjective_range_liftQ — Mathlib

English

If range f ≤ ker g and g is surjective, then the lifted map (range f).liftQ g h is surjective.

Русский

Если range f ⊆ ker g и g сюръективно, тогда допустимое отображение range f .liftQ g h сюръективно.

LaTeX

$$$$ \\text{If } \\operatorname{range}(f) \\le \\ker g \\text{ and } g \\text{ is surjective, then } (\\operatorname{range}(f)).liftQ g h \\text{ is surjective}. $$$$

Lean4

theorem surjective_range_liftQ (h : range f ≤ ker g) (hg : Function.Surjective g) :
    Function.Surjective ((range f).liftQ g h) := by
  intro x₃
  obtain ⟨x₂, rfl⟩ := hg x₃
  exact ⟨Submodule.Quotient.mk x₂, rfl⟩

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