right_unitality_hom — Mathlib

English

The map δ sends the unit to the right unitor via F, preserving the unit on the right under the monoidal structure.

Русский

Карта δ отправляет единицу к правому унитору через F, сохраняет единичность справа в моноидальной структуре.

LaTeX

$$$δ F X (I) \\circ (F.obj X \\triangleleft η F) \\circ (ρ_{F X})^{hom} = F.map (ρ_X)^{hom}$$$

Lean4

@[reassoc (attr := simp)]
theorem right_unitality_hom (X : C) : δ F X (𝟙_ C) ≫ F.obj X ◁ η F ≫ (ρ_ (F.obj X)).hom = F.map (ρ_ X).hom := by
  rw [← Category.assoc, ← Iso.eq_comp_inv, right_unitality, ← Category.assoc, ← F.map_comp, Iso.hom_inv_id, F.map_id,
    id_comp]

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