mapPairComp_inv_app_left — Mathlib

English

If α is an isomorphism of functors, then whiskering α on the right commutes with inv on the right.

Русский

Если α — изоморфизм функторов, тогда ослабление справа сохранит обратное на правой стороне.

LaTeX

$$$ (\mathrm{mapIsoWhiskerRight} α H).\mathrm{inv} = \mathrm{mapWhiskerRight} α^{-1} H $$$

Lean4

@[simp]
theorem mapPairComp_inv_app_left (c : C) : (mapPairComp Fₗ Fᵣ Gₗ Gᵣ).inv.app (left c) = 𝟙 (left (Gₗ.obj (Fₗ.obj c))) :=
  by
  dsimp [mapPairComp]
  simp

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