instIsEquivalenceFunctorFunctorsInvertingWhiskeringLeftFunctor

English

The whiskering left functor, under localization hypotheses, is an equivalence of categories.

Русский

Функтор whiskeringLeft левого направления, при данных предположениях локализации, есть эквивалентность категорий.

LaTeX

$$$(whiskeringLeftFunctor L W E).IsEquivalence$$$

Lean4

instance : (whiskeringLeftFunctor L W E).IsEquivalence :=
  by
  let iso :
    (whiskeringLeft (MorphismProperty.Localization W) D E).obj (equivalenceFromModel L W).functor ⋙
        (Construction.whiskeringLeftEquivalence W E).functor ≅
      whiskeringLeftFunctor L W E :=
    NatIso.ofComponents
      (fun F =>
        eqToIso
          (by
            ext
            change (W.Q ⋙ Localization.Construction.lift L (inverts L W)) ⋙ F = L ⋙ F
            rw [Construction.fac]))
      (fun τ => by
        ext
        dsimp [Construction.whiskeringLeftEquivalence, equivalenceFromModel, whiskerLeft]
        erw [NatTrans.comp_app, NatTrans.comp_app, eqToHom_app, eqToHom_app, eqToHom_refl, eqToHom_refl, comp_id,
          id_comp]
        · rfl
        all_goals
          change (W.Q ⋙ Localization.Construction.lift L (inverts L W)) ⋙ _ = L ⋙ _
          rw [Construction.fac])
  exact Functor.isEquivalence_of_iso iso

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