pullback_obj — Mathlib

English

The object (pullback f).obj x is represented by the subobject mk (pullback.snd x.arrow f).

Русский

Объект (pullback f).obj x задаётся как mk( pullback.snd x.arrow f ).

LaTeX

$$$(pullback f).obj x = \mathrm{mk}(\mathrm{pullback.snd} \\ x.arrow \\ f)$$$

Lean4

theorem pullback_obj {X Y : C} (f : Y ⟶ X) (x : Subobject X) : (pullback f).obj x = mk (pullback.snd x.arrow f) :=
  by
  obtain ⟨Z, i, _, rfl⟩ := mk_surjective x
  rw [pullback_obj_mk (IsPullback.of_hasPullback i f)]
  exact
    mk_eq_mk_of_comm _ _ (asIso (pullback.map i f (mk i).arrow f (underlyingIso i).inv (𝟙 _) (𝟙 _) (by simp) (by simp)))
      (by simp)

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