whiskerLeft_left_fst — Mathlib

English

The left whiskering by R along f, composed with fst, reduces to fst on the base morphism.

Русский

Левое запотягивание по R вдоль f, композицию с fst сводит к fst на базовом морфизме.

LaTeX

$$$ (R \\downarrow f).left \\circ \\mathrm{fst} = \\mathrm{fst} $$$

Lean4

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

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