English
A CondensedMod version of Condensed.ofSheafProfinite: turning a Profinite-valued sheaf into a CondensedMod, given equalizer condition.
Русский
Версия CondensedMod от Condensed.ofSheafProfinite: переход от Profinite-представления к CondensedMod при условии равнителя.
LaTeX
$$$$\mathrm{CondensedMod.ofSheafProfinite}(F,hF) \in \mathrm{CondensedMod}(R).$$$$
Lean4
/-- A `CondensedMod` version of `Condensed.ofSheafProfinite`. -/
noncomputable abbrev ofSheafProfinite (F : Profinite.{u}ᵒᵖ ⥤ ModuleCat.{u + 1} R) [PreservesFiniteProducts F]
(hF : EqualizerCondition F) : CondensedMod R :=
haveI : HasLimitsOfSize.{u, u + 1} (ModuleCat R) := hasLimitsOfSizeShrink.{u, u + 1, u + 1, u + 1} _
Condensed.ofSheafProfinite F hF
