English
The LocallyConstant functor is fully faithful when sending modules to light condensed modules.
Русский
Функтор LocallyConstant полно и верно сохраняет отображения между модулями в светло-конденсированные модули.
LaTeX
$$$\\text{FullyFaithful}((\\text{functor }R).\\mathrm{LocallyConstant})$$$
Lean4
instance (M : ModuleCat R) :
IsIso ((LightCondensed.forget R).map ((discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj M))) :=
by
dsimp [LightCondensed.forget, discreteUnderlyingAdj]
rw [← constantSheafAdj_counit_w]
refine IsIso.comp_isIso' inferInstance ?_
have : (constantSheaf (coherentTopology LightProfinite.{u}) (Type u)).Faithful :=
inferInstanceAs (discrete _).Faithful
have : (constantSheaf (coherentTopology LightProfinite.{u}) (Type u)).Full := inferInstanceAs (discrete (Type u)).Full
rw [← Sheaf.isConstant_iff_isIso_counit_app]
constructor
change (discrete _).essImage _
rw [essImage_eq_of_natIso LightCondSet.LocallyConstant.iso.symm]
exact obj_mem_essImage LightCondSet.LocallyConstant.functor M
