whiskerRight_naturality_id — Mathlib

English

Naturality of whiskering on the right with identity: whiskering by identity interacts with left/right unitors as expected.

Русский

Натуральность обвязки справа единичной стрелой: обвязка справа через единичность ведет к согласованному поведению левого/правого униторов.

LaTeX

$$$\\forall a, a':\\; η.naturality(\\mathbf{1}_a) \\;▷ f \\;≫ (α)^{-1} \\;≫ η.app a \\;▷ G.mapId a \\;▷ f \\; = \\; F.mapId a \\;▷ η.app a \\;▷ f \\;≫ (λ_ (η.app a)).hom \\;▷ f \\;≫ (ρ_ (η.app a)).inv \\;▷ f$$$

Lean4

@[reassoc (attr := simp)]
theorem whiskerRight_naturality_id (f : G.obj a ⟶ a') :
    η.naturality (𝟙 a) ▷ f ≫ (α_ _ _ _).hom ≫ η.app a ◁ G.mapId a ▷ f =
      F.mapId a ▷ η.app a ▷ f ≫ (λ_ (η.app a)).hom ▷ f ≫ (ρ_ (η.app a)).inv ▷ f ≫ (α_ _ _ _).hom :=
  by rw [← associator_naturality_middle, ← comp_whiskerRight_assoc, naturality_id]; simp

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