mapComp'_whiskerRight_comp_mapComp'

English

Coherence for a lax functor: a specific associativity-like identity holds between composed map components and whiskered maps, controlled by the associator.

Русский

Связанность для лаксовой функтора: выполняется тождество, напоминающее ассоциативность, между составленными map-компонентами и обвешенными отображениями, управляемое ассоциатором.

LaTeX

$$$F.mapComp' f_{02} f_{23} f \\\\triangleright F.map f_{23} \\\\\\n = F.mapComp' f_{01} f_{13} f \\\\triangleleft F.map f_{01} \\\\\\n \\\\triangleleft F.mapComp' f_{12} f_{23} f_{13} h_{13} \\\\wedge (\\\\alpha_{f_{01},f_{12},f_{23}})^{-1}$$$

Lean4

@[reassoc]
theorem mapComp'_whiskerRight_comp_mapComp' (hf : f₀₂ ≫ f₂₃ = f) :
    F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂ ▷ F.map f₂₃ ≫ F.mapComp' f₀₂ f₂₃ f =
      (α_ _ _ _).hom ≫ F.map f₀₁ ◁ F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃ ≫ F.mapComp' f₀₁ f₁₃ f :=
  by rw [whiskerLeft_mapComp'_comp_mapComp' _ _ _ _ _ _ f h₀₂ h₁₃, Iso.hom_inv_id_assoc]

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