mapComp_id_right — Mathlib

English

Inverse form of the previous right-id coherence relation.

Русский

Обратная форма предыдущего соотношения правого ид-coherence.

LaTeX

$$$\forall f:\; (F.mapComp f (id b)).inv = F.map f ◁ (F.mapId b).hom ≫ (\rho_{F.map f}).hom ≫ F.map₂ (\rho_ f).inv$$$

Lean4

theorem mapComp_id_right (f : a ⟶ b) :
    (F.mapComp f (𝟙 b)) = F.map₂Iso (ρ_ f) ≪≫ (ρ_ (F.map f)).symm ≪≫ (whiskerLeftIso (F.map f) (F.mapId b)).symm :=
  Iso.ext <| F.mapComp_id_right_hom f

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