map_app_comp_π — Mathlib

English

Natural transformations in the DayConvolutionInternalHom satisfy a compatibility with π components: for G' and H' and a morphism f: G → G', the induced map commutes with π.

Русский

Натуральные преобразования DayConvolutionInternalHom согласованы по компонентам π: для отображения f: G → G' выполняется commuting с π-компонентами.

LaTeX

$$$\\bigl(\\mathcal{H}.map f \\mathcal{H}')_{c} \\circ \\pi_{c,j}^{\\mathcal{H}'} = \\pi_{c,j}^{\\mathcal{H}} \\circ (\\mathsf{ihom}(F\\!,j))\\!\\bigl( f_{j\\otimes c} \\bigr)$$$

Lean4

@[reassoc (attr := simp)]
theorem map_app_comp_π (ℌ : DayConvolutionInternalHom F G H) {G' : C ⥤ V} {H' : C ⥤ V} (f : G ⟶ G')
    (ℌ' : DayConvolutionInternalHom F G' H') (c : C) (j : C) :
    (ℌ.map f ℌ').app c ≫ ℌ'.π c j = ℌ.π c j ≫ (ihom <| F.obj j).map (f.app <| j ⊗ c) :=
  by
  dsimp [map]
  rw [← Wedge.mk_ι (F := dayConvolutionInternalHomDiagramFunctor F |>.obj _ |>.obj c) (H'.obj c) (ℌ'.π c) (ℌ'.hπ c),
    Wedge.IsLimit.lift_ι (ℌ'.isLimitWedge c)]

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