pullback_map_self — Mathlib

English

Pullback along f followed by map f yields the identity on Subobject X.

Русский

Вытягивание вдоль f, затем map f возвращает единицу на Subobject(X).

LaTeX

$$$\forall g:\mathrm{Subobject}(X), \; (\mathrm{pullback}(f)).\mathrm{obj}((\mathrm{map}(f)).\mathrm{obj}(g)) = g$$$

Lean4

@[simp]
theorem pullback_map_self [HasPullbacks C] (f : X ⟶ Y) [Mono f] (g : Subobject X) :
    (pullback f).obj ((map f).obj g) = g := by
  revert g
  exact Quotient.ind (fun g' => Quotient.sound ⟨(MonoOver.pullbackMapSelf f).app _⟩)

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