whiskerLeftIso_mapId — Mathlib

English

The left whiskering of a map by F.map f and F.mapId b preserves a specific isomorphism structure, expressed as a composition with mapComp and right unitor data.

Русский

Левый обхват отображения F.map f и F.mapId b сохраняет структуру изоморфизма через композицию mapComp и правого унитора.

LaTeX

$$$\\mathrm{whiskerLeftIso}(F.map f)(F.mapId b) = (F.mapComp f (\\mathbf{1} b))^{-1} \\circ F.map_2(\\rho_f)^{-1} \\circ (\\rho_{F.map f})^{-1}$$$

Lean4

theorem whiskerLeftIso_mapId (f : a ⟶ b) :
    whiskerLeftIso (F.map f) (F.mapId b) = (F.mapComp f (𝟙 b)).symm ≪≫ F.map₂Iso (ρ_ f) ≪≫ (ρ_ (F.map f)).symm := by
  simp [mapComp_id_right]

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