isoLocallyConstantOfIsColimit_inv

English

For a functor F with the property PreservesFiniteProducts, and for any finite X, F preserves limits of shape (Discrete X.carrier).

Русский

Для функторa F, сохраняющего конечные произведения, и для любого конечного X, F сохраняет пределы формы (Discrete X.carrier).

LaTeX

$$$\forall X$, \operatorname{PreservesLimitsOfShape}(\mathrm{Discrete}(X\!_.\mathrm{carrier}), F)$$$

Lean4

theorem isoLocallyConstantOfIsColimit_inv (X : LightProfinite.{u}ᵒᵖ ⥤ Type u) [PreservesFiniteProducts X]
    (hX : ∀ S : LightProfinite.{u}, (IsColimit <| X.mapCocone (coconeRightOpOfCone S.asLimitCone))) :
    (isoLocallyConstantOfIsColimit X hX).inv = (CompHausLike.LocallyConstant.counitApp.{u, u} X) :=
  by
  dsimp [isoLocallyConstantOfIsColimit]
  simp only [Category.assoc]
  rw [Iso.inv_comp_eq]
  ext S : 2
  apply colimit.hom_ext
  intro ⟨Y, _, g⟩
  suffices
    _ ≫ (isoFinYonedaComponents _ _).inv ≫ X.map g =
      (locallyConstantPresheaf _).map g ≫ counitAppApp (Opposite.unop S) X
    by simpa [locallyConstantIsoFinYoneda, isoFinYoneda, counitApp]
  erw [(counitApp.{u, u} X).naturality]
  simp only [← Category.assoc, op_obj, functorToPresheaves_obj_obj]
  congr
  ext f
  simp only [types_comp_apply, counitApp_app]
  apply presheaf_ext.{u, u} (X := X) (Y := X) (f := f)
  intro x
  rw [incl_of_counitAppApp]
  simp only [counitAppAppImage]
  letI : Fintype (fiber.{u, u} f x) := Fintype.ofInjective (sigmaIncl.{u, u} f x).1 Subtype.val_injective
  apply injective_of_mono (isoFinYonedaComponents X (fiber.{u, u} f x)).hom
  ext y
  simp only [isoFinYonedaComponents_hom_apply, ← FunctorToTypes.map_comp_apply, ← op_comp]
  rw [show (LightProfinite.of PUnit.{u + 1}).const y ≫ IsTerminal.from _ (fiber f x) = 𝟙 _ from rfl]
  simp only [op_comp, FunctorToTypes.map_comp_apply, op_id, FunctorToTypes.map_id_apply]
  rw [← isoFinYonedaComponents_inv_comp X _ (sigmaIncl.{u, u} f x)]
  simpa [← isoFinYonedaComponents_hom_apply] using x.map_eq_image f y

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