isColimitLocallyConstantPresheaf — Mathlib

English

A specialized inv_comp equality for FinYoneda isomorphisms stating the expected commutativity with precomposition.

Русский

Уравнение inv_comp в контексте FinYoneda выражает требуемую коммутативность с предсоставлением.

LaTeX

$$$(\\text{isoFinYonedaComponents_inv_comp } F X Y)\\; (f) \\; (g) :\\; (\\text{Hom } X Y) \\to ...$$$

Lean4

/-- The functor `locallyConstantPresheaf` takes sequential limits of finite sets with surjective
projection maps to colimits.
-/
noncomputable def isColimitLocallyConstantPresheaf (hc : IsLimit c) [∀ i, Epi (c.π.app i)] :
    IsColimit <| (locallyConstantPresheaf X).mapCocone c.op :=
  by
  refine Types.FilteredColimit.isColimitOf _ _ ?_ ?_
  · intro (f : LocallyConstant c.pt X)
    obtain ⟨j, h⟩ :=
      Profinite.exists_locallyConstant.{_, 0} (lightToProfinite.mapCone c) (isLimitOfPreserves lightToProfinite hc) f
    exact ⟨⟨j⟩, h⟩
  · intro ⟨i⟩ ⟨j⟩ (fi : LocallyConstant _ _) (fj : LocallyConstant _ _)
      (h : fi.comap (c.π.app i).hom = fj.comap (c.π.app j).hom)
    obtain ⟨k, ki, kj, _⟩ := IsCofilteredOrEmpty.cone_objs i j
    refine ⟨⟨k⟩, ki.op, kj.op, ?_⟩
    dsimp
    ext x
    obtain ⟨x, hx⟩ := ((LightProfinite.epi_iff_surjective (c.π.app k)).mp inferInstance) x
    rw [← hx]
    change fi ((c.π.app k ≫ (F ⋙ toLightProfinite).map _) x) = fj ((c.π.app k ≫ (F ⋙ toLightProfinite).map _) x)
    have h := LocallyConstant.congr_fun h x
    rwa [c.w, c.w]

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