English
Inverse composition formula specialized to isoLocallyConstantOfIsColimit: the inverse comp acts like counit and precomposed maps reflect pointwise behavior.
Русский
Формула обратной композиции для isoLocallyConstantOfIsColimit: обратная композиция действует как counit и отображения принимают по точкам.
LaTeX
$$$(\\text{isoLocallyConstantOfIsColimit } X hX).inv (\\text{f}) = \\cdot$ (explicit colimit/whisker maps) $.$$$
Lean4
theorem isoLocallyConstantOfIsColimit_inv (X : Profinite.{u}ᵒᵖ ⥤ Type (u + 1)) [PreservesFiniteProducts X]
(hX : ∀ S : Profinite.{u}, (IsColimit <| X.mapCocone S.asLimitCone.op)) :
(isoLocallyConstantOfIsColimit X hX).inv = (CompHausLike.LocallyConstant.counitApp.{u, u + 1} 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 + 1} 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 + 1} (X := X) (Y := X) (f := f)
intro x
rw [incl_of_counitAppApp]
simp only [counitAppAppImage]
letI : Fintype (fiber.{u, u + 1} f x) := Fintype.ofInjective (sigmaIncl.{u, u + 1} f x).1 Subtype.val_injective
apply injective_of_mono (isoFinYonedaComponents X (fiber.{u, u + 1} f x)).hom
ext y
simp only [isoFinYonedaComponents_hom_apply, ← FunctorToTypes.map_comp_apply, ← op_comp]
rw [show (Profinite.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 + 1} f x)]
simpa [← isoFinYonedaComponents_hom_apply] using x.map_eq_image f y
