id — Mathlib · SciLib

English

If f is a split epimorphism, then its section s satisfies f ∘ s = id_Y; equivalently s is a right inverse of f.

Русский

Пусть f — разложимый эпиморфизм. Тогда существует секция s: Y → X такая, что f ∘ s = id_Y; то есть s является правой обратной к f.

LaTeX

$$$\exists s: Y \to X\;\big(\;f \circ s = \mathrm{id}_Y\;\).$$$

Lean4

@[reassoc (attr := simp)]
theorem id {X Y : C} (f : X ⟶ Y) [hf : IsSplitEpi f] : section_ f ≫ f = 𝟙 Y :=
  hf.exists_splitEpi.some.id

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