pullback_id — Mathlib

English

For any object X, pulling back along the identity map yields the same subobject.

Русский

Для любого объекта X вытягивание вдоль тождественного отображения даёт тот же подобъект.

LaTeX

$$$(\mathrm{pullback}(\mathrm{id}_X)).\mathrm{obj}(x) = x$$$

Lean4

theorem pullback_id (x : Subobject X) : (pullback (𝟙 X)).obj x = x :=
  by
  induction x using Quotient.inductionOn' with
  | _ f
  exact Quotient.sound ⟨MonoOver.pullbackId.app f⟩

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