whiskerRight_left_fst — Mathlib

English

In the Over category over X with pullbacks, whiskering on the right preserves the left projection: (f ▷ R).left ≫ pullback.fst = pullback.fst ≫ f.left.

Русский

В категории Over над X с помощью pullback переход правого whisker сохраняет левую проекцию: (f ▷ R).left ≫ pullback.fst = pullback.fst ≫ f.left.

LaTeX

$$$(f \;▷\; R).left \;\gg\; pullback.fst _ _ = pullback.fst _ _ \;\gg\; f.left$$$

Lean4

@[reassoc (attr := simp)]
theorem whiskerRight_left_fst {R S T : Over X} (f : S ⟶ T) :
    (f ▷ R).left ≫ pullback.fst _ _ = pullback.fst _ _ ≫ f.left :=
  limit.lift_π _ _

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