English
The LocallyConstant functor is naturally isomorphic to the discrete functor.
Русский
Функтор локально-константный естественно изоморфен дискретному функтору.
LaTeX
$$$\text{LocallyConstant.functor} \cong \text{Discretized.functor}$$$
Lean4
/-- `CondensedMod.LocallyConstant.functor` is naturally isomorphic to the constant sheaf functor from
`R`-modules to 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 [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
