δ_fst — Mathlib

English

For any X, Y in C, the δ morphism composed with fst equals the map of fst: δ F X Y ; fst = F.map (fst X Y).

Русский

Для любых X, Y в C отображение δ F X Y, после-comпозиция с fst даёт F.map(fst X Y).

LaTeX

$$$\delta F X Y \;\circ \mathrm{fst}(F\,X)\,(F\,Y) = F\ map(\mathrm{fst} X Y)$$$

Lean4

@[reassoc (attr := simp)]
theorem δ_fst (X Y : C) : δ F X Y ≫ fst _ _ = F.map (fst _ _) :=
  by
  trans F.map (X ◁ toUnit Y) ≫ F.map (ρ_ X).hom
  · rw [← whiskerLeft_fst _ (F.map (toUnit Y)), δ_natural_right_assoc]
    simp [← OplaxMonoidal.right_unitality_hom, rightUnitor_hom (F.obj X)]
  · simp [← Functor.map_comp, rightUnitor_hom]

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