equivalenceOfEquiv — Mathlib

English

There is an equivalence between the Pi-category built from C indexed by I and that indexed by J via a given equivalence e: J ≃ I, realized by the appropriate functors and natural isomorphisms.

Русский

Существует эквивалентность между Pi-категорией, построенной на C с индексами I и Pi-категорией с индексами J через данную эквиваленцию e: J ≃ I, реализованная соответствующими функторами и естественными изоморфизмами.

LaTeX

$$$(\\forall i, C i) \\simeq (\\forall j, C (e j))$$$

Lean4

/-- Reindexing a family of categories gives equivalent `Pi` categories. -/
@[simps]
noncomputable def equivalenceOfEquiv (e : J ≃ I) : (∀ j, C (e j)) ≌ (∀ i, C i)
    where
  functor := pi' (fun i => Pi.eval _ (e.symm i) ⋙ (Pi.eqToEquivalence C (by simp)).functor)
  inverse := Functor.pi' (fun i' => Pi.eval _ (e i'))
  unitIso :=
    NatIso.pi'
      (fun i' =>
        leftUnitor _ ≪≫
          (Pi.evalCompEqToEquivalenceFunctor (fun j => C (e j)) (e.symm_apply_apply i')).symm ≪≫
            isoWhiskerLeft _ ((Pi.eqToEquivalenceFunctorIso C e (e.symm_apply_apply i')).symm) ≪≫
              (pi'CompEval _ _).symm ≪≫ isoWhiskerLeft _ (pi'CompEval _ _).symm ≪≫ (associator _ _ _).symm)
  counitIso :=
    NatIso.pi'
      (fun i =>
        (associator _ _ _).symm ≪≫
          isoWhiskerRight (pi'CompEval _ _) _ ≪≫
            Pi.evalCompEqToEquivalenceFunctor C (e.apply_symm_apply i) ≪≫ (leftUnitor _).symm)

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