instFaithfulModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf

English

There is an isomorphism of functors between the discrete functor on modules and LocallyConstant functor.

Русский

Существует изоморфизм функторов между дискретным функтором на модулях и LocallyConstant функтором.

LaTeX

$$$\\mathrm{discrete} \\cong (\\mathrm{LocallyConstant})$$$

Lean4

instance : (constantSheaf (coherentTopology LightProfinite.{u}) (ModuleCat.{u} R)).Faithful :=
  inferInstanceAs (discrete.{u} (ModuleCat R)).Faithful

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