surjective_χ — Mathlib

English

For any X and any φ: X → Ω, there exists a Z and a mono i: Z → X such that φ = 𝒞.χ(i).

Русский

Для произвольного X и любого φ: X → Ω найдется объект Z и моно i: Z → X такое, что φ = 𝒞.χ(i).

LaTeX

$$$\forall X: C, \forall φ: X \to 𝒞.Ω, \exists Z, \exists i: Z \to X, Mono(i), φ = 𝒞.χ(i)$$$

Lean4

theorem surjective_χ {X : C} (φ : X ⟶ 𝒞.Ω) : ∃ (Z : C) (i : Z ⟶ X) (_ : Mono i), φ = 𝒞.χ i :=
  ⟨Limits.pullback φ 𝒞.truth, pullback.fst _ _, inferInstance,
    𝒞.uniq _ (by convert IsPullback.of_hasPullback φ 𝒞.truth)⟩

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