whiskerLeft_naturality_id — Mathlib

English

Naturality of whiskering with identity: whiskering by identity behaves coherently with unitors.

Русский

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

LaTeX

$$$f \\;◁ \\; θ.naturality(\\mathbf{1}_a) \\;≫\\; f \\;◁ θ.app a \\;◁ H.mapId a = f \\;◁ G.mapId a \\;▷ θ.app a \\;≫ f \\;◁ (λ_ (θ.app a)).hom \\;≫ f \\;◁ (ρ_ (θ.app a)).inv$$$

Lean4

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

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