pullback_χ_obj_mk_truth — Mathlib

English

The χ-map of the pullback object of φ with truth yields φ.

Русский

Отображение χ от объекта вытягивания (pullback) φ через truth равно φ.

LaTeX

$$$𝒞.χ ((Subobject.pullback φ).obj 𝒞.truth_{as_subobject}).arrow = φ$$$

Lean4

@[simp]
theorem pullback_χ_obj_mk_truth {Z X : C} (i : Z ⟶ X) [Mono i] :
    (Subobject.pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject = .mk i :=
  Subobject.pullback_obj_mk (𝒞.isPullback i).flip

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