nonempty_cokernelData — Mathlib

English

There exists a nonempty cokernel data for a given presentation, map, and generator set, since the projection has a right inverse on π.

Русский

Существуют не пустые данные коконель для данной презентации и набора генераторов, потому что проекция имеет правую обратную на π.

LaTeX

$$$\\exists s:\\, pres_2.\\text{CokernelData}\\ f\\ g_1$ such that $\\forall m_2,\\, pres_2.π(s(m_2))=m_2$.$$

Lean4

instance nonempty_cokernelData : Nonempty (pres₂.CokernelData f g₁) :=
  by
  obtain ⟨s, hs⟩ := pres₂.surjective_π.hasRightInverse
  exact ⟨CokernelData.ofSection _ _ _ s hs⟩

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