prod'_ε_fst — Mathlib

English

For functors F and G, the first component of the η-map of the prod' construction is the η-map of F (under mild compatibility assumptions).

Русский

Для функторов F и G первая компонента η-перехода конструирования prod' совпадает с η F (при некоторых условиях совместимости).

LaTeX

$$$ (\eta_{\mathrm{prod}'}(F,G))_{1} = \eta_F $$$

Lean4

@[simp]
theorem prod'_ε_fst : (ε (prod' F G)).1 = ε F :=
  by
  change _ ≫ F.map (𝟙 _) = _
  rw [Functor.map_id, Category.comp_id]
  rfl

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