mapComp'_comp_id — Mathlib

English

In Strict Pseudofunctor setting, the mapComp' along an identity reduces to a right unitor iso with a mapped identity.

Русский

В контексте Strict Pseudofunctor отображение композиции вдоль идентичности сводится к rightUnitorIso и отображению.

LaTeX

$$mapComp'_comp_id for f with id reduces to (ρ)^{-1} followed by whiskerLeftIso with id$$

Lean4

theorem mapComp'_comp_id {b₀ b₁ : B} (f : b₀ ⟶ b₁) :
    F.mapComp' f (𝟙 b₁) f = (ρ_ _).symm ≪≫ whiskerLeftIso _ (F.mapId b₁).symm :=
  by
  ext
  rw [mapComp']
  dsimp
  rw [F.mapComp_id_right_hom f, Strict.rightUnitor_eqToIso, eqToIso.hom, ← F.map₂_comp_assoc, eqToHom_trans,
    eqToHom_refl, PrelaxFunctor.map₂_id, Category.id_comp]

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