whiskerRight_naturality_comp — Mathlib

English

Naturality of whiskering on the right with composition: whiskering distributes over composition of arrows.

Русский

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

LaTeX

$$$\\forall f,g,h:\\; η.naturality(f\\;≫\\; g) \\;▷ h = F.mapComp f g \\;▷ η.app c \\;▷ h \\;≫ (α)^{-1} \\;≫ η.naturality f \\;▷ G.map g \\;▷ h \\;≫ (α).hom$$$

Lean4

@[reassoc (attr := simp)]
theorem whiskerRight_naturality_comp (f : a ⟶ b) (g : b ⟶ c) (h : G.obj c ⟶ a') :
    η.naturality (f ≫ g) ▷ h ≫ (α_ _ _ _).hom ≫ η.app a ◁ G.mapComp f g ▷ h =
      F.mapComp f g ▷ η.app c ▷ h ≫
        (α_ _ _ _).hom ▷ h ≫
          (α_ _ _ _).hom ≫
            F.map f ◁ η.naturality g ▷ h ≫
              (α_ _ _ _).inv ≫
                (α_ _ _ _).inv ▷ h ≫ η.naturality f ▷ G.map g ▷ h ≫ (α_ _ _ _).hom ▷ h ≫ (α_ _ _ _).hom :=
  by rw [← associator_naturality_middle, ← comp_whiskerRight_assoc, naturality_comp]; simp

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