fintypeDiagram — Mathlib

English

For a Profinite X, the functor DiscreteQuotient X ⥤ FintypeCat has a limit isomorphic to X.

Русский

Для профинитного пространства X отношенный к нему функтор DiscreteQuotient X ⥤ FintypeCat имеет предел, изоморфный X.

LaTeX

$$$\lim(\mathrm{DiscreteQuotient}(X) \xrightarrow{\mathrm{fintypeDiagram}} \mathrm{FintypeCat}) \cong X$$$

Lean4

/-- The functor `DiscreteQuotient X ⥤ Fintype` whose limit is isomorphic to `X`. -/
def fintypeDiagram : DiscreteQuotient X ⥤ FintypeCat
    where
  obj S := @FintypeCat.of S (Fintype.ofFinite S)
  map f := DiscreteQuotient.ofLE f.le
  map_comp _ _ := by funext; cat_disch

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