whiskerRight_naturality_naturality

English

Naturality of whiskering on the left distributes over the composition of morphisms; equality of two composites holds after whiskering by f.

Русский

Натуральность левостороннего whisker удерживает композицию; равенство двух композиторов сохраняется после обвивки слева константной f.

LaTeX

$$$\\forall f,g,h, η, θ, β:\\; F,G : \\dots,\quad f \\;◁ G.map_2 β \\;▷ θ.app b \\;≫ f ◁ θ.naturality h = f ◁ η.naturality g \\;≫ f ◁ θ.app a \\;▷ G.map_2 β.$$$

Lean4

@[reassoc (attr := simp)]
theorem whiskerRight_naturality_naturality {f g : a ⟶ b} (β : f ⟶ g) (h : G.obj b ⟶ a') :
    F.map₂ β ▷ η.app b ▷ h ≫ η.naturality g ▷ h =
      η.naturality f ▷ h ≫ (α_ _ _ _).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ _ _ _).inv :=
  by rw [← comp_whiskerRight, naturality_naturality, comp_whiskerRight, whisker_assoc]

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