adjunction — Mathlib

English

There exists a natural isomorphism between LocallyConstant.functor and the discrete functor.

Русский

Существует естественный изоморфизм между LocallyConstant.functor и дискретным функтором.

LaTeX

$$$\\text{functorIsoDiscrete} : \\mathrm{functor} \\cong \\mathrm{discrete}$$$

Lean4

/-- `LightCondMod.LocallyConstant.functor` is left adjoint to the forgetful functor from light condensed
`R`-modules to `R`-modules.
-/
noncomputable def adjunction : functor R ⊣ underlying (ModuleCat R) :=
  Adjunction.ofNatIsoLeft (discreteUnderlyingAdj _) (functorIsoDiscrete R).symm

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