pullback_comp — Mathlib

English

Pullback along a composition equals composition of pullbacks: pulling back along f ≫ g is the same as first along g, then along f.

Русский

Вытягивание вдоль композиции равно композиции вытягиваний: вытягивание вдоль f ≫ g равно вытягиванию вдоль g затем f.

LaTeX

$$$\mathrm{pullback}(f \circ g) = \mathrm{pullback}(f) \circ \mathrm{pullback}(g)$$$

Lean4

theorem pullback_comp (f : X ⟶ Y) (g : Y ⟶ Z) (x : Subobject Z) :
    (pullback (f ≫ g)).obj x = (pullback f).obj ((pullback g).obj x) :=
  by
  induction x using Quotient.inductionOn' with
  | _ t
  exact Quotient.sound ⟨(MonoOver.pullbackComp _ _).app t⟩

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