English
In a cartesian closed setting with an adjunction L ⊣ F and an object A ∈ C, the mate of the Frobenius morphism for F and h equals the expComparison natural transformation, i.e. conjugateEquiv of appropriate adjunction data matches expComparison natTrans.
Русский
В декартово замкнутой категории с компоновкой сопряжения L ⊣ F и объектом A ∈ C, сопряжение форми-фробениуса сопряжения соответствует естественному преобразованию expComparison natTrans.
LaTeX
$$$ \text{conjugateEquiv}(h \cdot \text{exp.adjunction}(A), (\text{exp.adjunction}(F(A)) \cdot h))
(\text{frobeniusMorphism } F h A).\mathrm{natTrans} = (\text{expComparison } F A).\mathrm{natTrans} $$$
Lean4
theorem frobeniusMorphism_mate (h : L ⊣ F) (A : C) :
conjugateEquiv (h.comp (exp.adjunction A)) ((exp.adjunction (F.obj A)).comp h) (frobeniusMorphism F h A).natTrans =
(expComparison F A).natTrans :=
by
unfold expComparison frobeniusMorphism
have conjeq :=
iterated_mateEquiv_conjugateEquiv h h (exp.adjunction (F.obj A)) (exp.adjunction A)
(prodComparisonNatTrans L (F.obj A) ≫ Functor.whiskerLeft L ((curriedTensor C).map (h.counit.app A)))
rw [← conjeq]
congr 1
apply congr_arg
ext B
unfold mateEquiv
simp only [Functor.comp_obj, curriedTensor_obj_obj, Equiv.coe_fn_mk, Functor.whiskerRight_comp,
Functor.whiskerLeft_comp, assoc, NatTrans.comp_app, Functor.id_obj, Functor.rightUnitor_inv_app,
Functor.whiskerLeft_app, Functor.associator_hom_app, Functor.associator_inv_app, Functor.whiskerRight_app,
prodComparisonNatTrans_app, curriedTensor_map_app, Functor.comp_map, curriedTensor_obj_map,
Functor.leftUnitor_hom_app, comp_id, id_comp, prodComparisonNatIso_inv, NatIso.isIso_inv_app]
rw [← F.map_comp, ← F.map_comp]
simp only [Functor.map_comp]
apply IsIso.eq_inv_of_inv_hom_id
simp only [assoc]
rw [prodComparison_natural_whiskerLeft, prodComparison_natural_whiskerRight_assoc]
slice_lhs 2 3 => rw [← prodComparison_comp]
simp only [assoc]
unfold prodComparison
simp
