iso — Mathlib

English

There is an isomorphism between the Locally Constant functor and a discrete underlying theory for light profinite types.

Русский

Существует изоморфизм между функтором локально-константным и дискретной базой для светлых профинитных типов.

LaTeX

$$$\mathrm{Iso} \bigl( \mathrm{LightCondSet.LocallyConstant.functor}, \mathrm{LightCondensed.discrete} \bigr)$$$

Lean4

/-- `LightCondSet.LocallyConstant.functor` is isomorphic to `LightCondensed.discrete`
(by uniqueness of adjoints).
-/
noncomputable def iso : functor ≅ LightCondensed.discrete (Type u) :=
  (LocallyConstant.adjunction _ _).leftAdjointUniq (LightCondensed.discreteUnderlyingAdj _)

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