English
IsIso of counit for discrete underlying adjunctions holds.
Русский
IsIso для counit в дискретных подстках сохраняется.
LaTeX
$$$\operatorname{IsIso}\bigl((\text{CounitDiscreteUnderlyingAdj}).app\bigr)$$$
Lean4
instance (M : ModuleCat R) :
IsIso ((forget R).map ((discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj M))) :=
by
dsimp [Condensed.forget, discreteUnderlyingAdj]
rw [← constantSheafAdj_counit_w]
refine IsIso.comp_isIso' inferInstance ?_
have : (constantSheaf (coherentTopology CompHaus) (Type (u + 1))).Faithful := inferInstanceAs (discrete _).Faithful
have : (constantSheaf (coherentTopology CompHaus) (Type (u + 1))).Full := inferInstanceAs (discrete _).Full
rw [← Sheaf.isConstant_iff_isIso_counit_app]
constructor
change (discrete _).essImage _
rw [essImage_eq_of_natIso CondensedSet.LocallyConstant.iso.symm]
exact obj_mem_essImage CondensedSet.LocallyConstant.functor M
