w — Mathlib · SciLib

English

The π-component at one equals left side composition with res.

Русский

Компонента π на один равна композиции слева с res.

LaTeX

$$$(\mathrm{fork F U}).\pi_{\mathrm{one}} = \mathrm{res} F U \;\circ\; \mathrm{leftRes} F U$$$

Lean4

@[elementwise]
theorem w : res F U ≫ leftRes F U = res F U ≫ rightRes F U :=
  by
  dsimp [res, leftRes, rightRes]
  ext
  simp only [limit.lift_π, limit.lift_π_assoc, Fan.mk_π_app, Category.assoc]
  rw [← F.map_comp]
  rw [← F.map_comp]
  congr 1

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