whiskerRight_naturality_id — Mathlib

English

Naturality for the right whiskering by identities in StrongTrans context.

Русский

Натуральность для правого взвешивания по identiy в контексте StrongTrans.

LaTeX

$$$f \triangleleft (\theta.naturality (\mathrm{Id} a)).hom \; ⟶ \; (\alpha_{_ _ _}).hom \; ⟶ \; F.mapId a \; ⟶ \dots$$$

Lean4

@[reassoc (attr := simp), to_app]
theorem whiskerRight_naturality_id (f : G.obj a ⟶ a') :
    (η.naturality (𝟙 a)).hom ▷ f ≫ (α_ _ _ _).hom ≫ η.app a ◁ G.mapId a ▷ f =
      F.mapId a ▷ η.app a ▷ f ≫ (λ_ (η.app a)).hom ▷ f ≫ (ρ_ (η.app a)).inv ▷ f ≫ (α_ _ _ _).hom :=
  η.toOplax.whiskerRight_naturality_id _

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