pullbackComp — Mathlib

English

Pullback along a composite f ≫ g is canonically isomorphic to the composition of pullbacks: S.pullback (f ≫ g) ≅ (S.pullback g).pullback f.

Русский

Вытягивание вдоль композиции f ≫ g канонически изоморфно композиции вытягиваний: S.pullback (f ≫ g) ≅ (S.pullback g).pullback f.

LaTeX

$$$S.pullback (f \circ g) \cong (S.pullback g).pullback f$$$

Lean4

/-- Pulling back with respect to a composition is the composition of the pullbacks. -/
def pullbackComp {X Y Z : C} (S : J.Cover X) (f : Z ⟶ Y) (g : Y ⟶ X) : S.pullback (f ≫ g) ≅ (S.pullback g).pullback f :=
  eqToIso <| Cover.ext _ _ fun Y f => by simp

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