English
The LocallyConstant functor is fully faithful; in particular, its associated functor is fully faithful.
Русский
Функтор LocallyConstant полно и верно сохраняет морфизмы.
LaTeX
$$$\\text{FullyFaithful}((\\text{functor }R))$$$
Lean4
/-- `LightCondMod.LocallyConstant.functor` is naturally isomorphic to the constant sheaf functor from
`R`-modules to light condensed `R`-modules.
-/
noncomputable def functorIsoDiscrete : functor R ≅ discrete _ :=
NatIso.ofComponents (fun M ↦ (functorIsoDiscreteComponents R M).symm) fun f ↦
by
dsimp
rw [Iso.eq_inv_comp, ← Category.assoc, Iso.comp_inv_eq]
dsimp [functorIsoDiscreteComponents]
rw [Category.assoc, ← Iso.eq_inv_comp, ← (discreteUnderlyingAdj (ModuleCat R)).counit_naturality]
simp only [← assoc]
congr 1
rw [← Iso.comp_inv_eq]
apply Sheaf.hom_ext
simp [functorIsoDiscreteAux₂, ← Functor.map_comp]
rfl
