ofSection — Mathlib

English

Given a chosen section s of the projection, one obtains a cokernel data for the cokernel presentation.

Русский

При заданной секции отображения получаем данные коконernel для коконernelной презентации.

LaTeX

$$$\\text{ofSection}(s,\\,hs):\\ pres_2.\\mathrm{CokernelData}\\ f\\ g_1$ with lift and $\\pi$-lift defined by $s$.$$

Lean4

/-- Constructor for `Presentation.CokernelData` in case we have a chosen set-theoretic
section of the projection `(pres₂.G →₀ A) → M₂`. -/
@[simps]
def ofSection (s : M₂ → (pres₂.G →₀ A)) (hs : ∀ (m₂ : M₂), pres₂.π (s m₂) = m₂) : pres₂.CokernelData f g₁
    where
  lift i := s (f (g₁ i))
  π_lift i := by simp [hs]

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