whiskerRight_toPlus_comp_plusCompIso_hom

English

The map (diagramCompIso F P X).hom is compatible with the universal arrows ι of the multicospan diagram, i.e., the expected compatibility condition holds.

Русский

Гом-компонента diagramCompIso F P X совместима с стрелами ι многоцепной диаграммы.

LaTeX

$$$(J.diagramCompIso F P X).hom \circ ι = F.map(ι)$$$

Lean4

@[reassoc (attr := simp)]
theorem whiskerRight_toPlus_comp_plusCompIso_hom : whiskerRight (J.toPlus _) _ ≫ (J.plusCompIso F P).hom = J.toPlus _ :=
  by
  ext
  dsimp [toPlus]
  simp only [ι_plusCompIso_hom, Functor.map_comp, Category.assoc]
  simp only [← Category.assoc]
  congr 1
  dsimp only [diagram] -- Need to unfold `diagram` before `ext` applies.

  ext a
  rw [Category.assoc, diagramCompIso_hom_ι, ← F.map_comp]
  simp only [unop_op, limit.lift_π, Multifork.ofι_π_app, Functor.comp_obj, Functor.comp_map]

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