endEquivSectionsFibers — Mathlib

English

Let C be a Galois category with a fiber functor F: C → FintypeCat. Then the endomorphism monoid End(F) is naturally isomorphic to the set of sections of the diagram (incl F) composed with F′ over all Galois objects; equivalently, End(F) is the limit of the fibers F(A) over all Galois objects A.

Русский

Пусть C — гaлoсовoе множество категорий с фибровой функторной связью F: C → FintypeCat. Тогда концевые эндоморфизмы F образуют моноид, естественным образом изоморфный множеству секций диаграммы (incl F) ∘ F′ по всем Galois-объектам; эквивалентно, End(F) является пределом фибр диаграммы A ↦ F(A) по всем Galois-объектам A.

LaTeX

$$$\\operatorname{End}(F) \\cong \\varprojlim_{A \\in \\mathsf{Galois}(F)} F(A).$$$

Lean4

/-- The endomorphisms of `F` are isomorphic to the limit over the fibers of `F` on all
Galois objects. -/
noncomputable def endEquivSectionsFibers : End F ≃ (incl F ⋙ F').sections :=
  let i1 : End F ≃ End F' := (FullyFaithful.whiskeringRight (FullyFaithful.ofFullyFaithful FintypeCat.incl) C).homEquiv
  let i2 : End F' ≅ (colimit ((incl F).op ⋙ coyoneda) ⟶ F') :=
    (yoneda.obj (F ⋙ FintypeCat.incl)).mapIso (colimit.isoColimitCocone ⟨cocone F, isColimit F⟩).op
  let i3 : (colimit ((incl F).op ⋙ coyoneda) ⟶ F') ≅ limit ((incl F ⋙ F') ⋙ uliftFunctor.{u₁}) :=
    colimitCoyonedaHomIsoLimit' (incl F) F'
  let i4 : limit (incl F ⋙ F' ⋙ uliftFunctor.{u₁}) ≃ ((incl F ⋙ F') ⋙ uliftFunctor.{u₁}).sections :=
    Types.limitEquivSections (incl F ⋙ (F ⋙ FintypeCat.incl) ⋙ uliftFunctor.{u₁, u₂})
  let i5 : ((incl F ⋙ F') ⋙ uliftFunctor.{u₁}).sections ≃ (incl F ⋙ F').sections :=
    (Types.sectionsEquiv (incl F ⋙ F')).symm
  i1.trans <| i2.toEquiv.trans <| i3.toEquiv.trans <| i4.trans i5

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