expComparison_ev — Mathlib

English

The exponential comparison map is natural in A: for f: A' ⟶ A, the whiskered precomposition equality holds.

Русский

Экспоненциальное сравнение естественно по A: для f: A' ⟶ A выполняется равенство с whiskerLeft.

LaTeX

$$$ (\expComparison F A).whiskerBottom (pre (F.map f)) = (\expComparison F A').whiskerTop (pre f) $$$

Lean4

theorem expComparison_ev (A B : C) :
    F.obj A ◁ ((expComparison F A).natTrans.app B) ≫ (exp.ev (F.obj A)).app (F.obj B) =
      inv (prodComparison F _ _) ≫ F.map ((exp.ev _).app _) :=
  by
  convert mateEquiv_counit _ _ (prodComparisonNatIso F A).inv B using 2
  apply IsIso.inv_eq_of_hom_inv_id
  simp only [prodComparisonNatTrans_app, prodComparisonNatIso_inv, NatIso.isIso_inv_app, IsIso.hom_inv_id]

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