functorPullback — Mathlib

English

If x is compatible, then its pullback along a functor F is also compatible.

Русский

Если x совместимо, то вытяжка по функтору F также совместима.

LaTeX

$$$\\forall F; x.Compatible \\Rightarrow (x.functorPullback F).Compatible$$$

Lean4

theorem functorPullback (h : x.Compatible) : (x.functorPullback F).Compatible :=
  by
  intro Z₁ Z₂ W g₁ g₂ f₁ f₂ h₁ h₂ eq
  exact h (F.map g₁) (F.map g₂) h₁ h₂ (by simp only [← F.map_comp, eq])

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