coev_expComparison — Mathlib

English

For A1,A2,A3 exponentiable, and f:A1⟶A2, g:A2⟶A3, we have pre (f ≫ g) = pre g ≫ pre f.

Русский

Для A1,A2,A3 экспоненцируемых и f:A1⟶A2, g:A2⟶A3 имеем pre (f ≫ g) = pre g ≫ pre f.

LaTeX

$$$ {A_1 A_2 A_3 : C} [Exponentiable A_1] [Exponentiable A_2] [Exponentiable A_3] (f : A_1 ⟶ A_2) (g : A_2 ⟶ A_3) :\n \operatorname{pre} (f \gg g) = \operatorname{pre} g \gg \operatorname{pre} f$$$

Lean4

theorem coev_expComparison (A B : C) :
    F.map ((exp.coev A).app B) ≫ (expComparison F A).natTrans.app (A ⊗ B) =
      (exp.coev _).app (F.obj B) ≫ (exp (F.obj A)).map (inv (prodComparison F A B)) :=
  by
  convert unit_mateEquiv _ _ (prodComparisonNatIso F A).inv B using 3
  apply IsIso.inv_eq_of_hom_inv_id
  simp

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