iso_inv_app — Mathlib

English

Explicit form of the inverse component of the iso adjunction is given by a long explicit composition of shifted maps and unit/counit components.

Русский

Явное выражение обратной компоненты изоморфизма сопряжения через длинную явную композицию сдвигов и единицы/кавиности.

LaTeX

$$$ (\mathrm{iso}(\mathrm{adj}, a))^{-1}_{Y} = \text{long composition of shifted maps and unit/counit}$$$

Lean4

@[reassoc]
theorem iso_inv_app (Y : D) :
    (iso adj a).inv.app Y =
      adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫
        G.map ((shiftFunctorCompIsoId D b a h).inv.app (F.obj ((shiftFunctor C a).obj (G.obj Y)))) ≫
          G.map ((shiftFunctor D a).map ((shiftFunctor D b).map ((F.commShiftIso a).hom.app (G.obj Y)))) ≫
            G.map
                ((shiftFunctor D a).map
                  ((shiftFunctorCompIsoId D a b (by rw [eq_neg_of_add_eq_zero_left h, add_neg_cancel])).hom.app
                    (F.obj (G.obj Y)))) ≫
              G.map ((shiftFunctor D a).map (adj.counit.app Y)) :=
  by
  obtain rfl : b = -a := by rw [← add_left_inj a, h, neg_add_cancel]
  simp only [iso, iso', shiftEquiv', Equiv.toFun_as_coe, conjugateIsoEquiv_apply_inv, conjugateEquiv_apply_app,
    Functor.comp_obj, comp_unit_app, Functor.id_obj, Equivalence.toAdjunction_unit, Equivalence.Equivalence_mk'_unit,
    Iso.symm_hom, Functor.comp_map, comp_counit_app, Equivalence.toAdjunction_counit,
    Equivalence.Equivalence_mk'_counit, Functor.map_shiftFunctorCompIsoId_hom_app, assoc, Functor.map_comp]
  slice_lhs 3 4 => rw [← Functor.map_comp, ← Functor.map_comp, Iso.inv_hom_id_app]
  simp only [Functor.comp_obj, Functor.map_id, id_comp, assoc]

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