whiskerLeft_naturality_id — Mathlib

English

Naturality with right whiskering by identities in StrongTrans for Pseudofunctors.

Русский

Натуральность при правом взвешивании по единичным стрелкам в StrongTrans.

LaTeX

$$$$(\eta.naturality (\mathrm{Id} a)).hom \; ⟶ \; (\alpha_.).hom$$$$

Lean4

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

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