Discrete condensed R-modules

This file provides the necessary API to prove that a condensed R-module is discrete if and only if the underlying condensed set is (both for light condensed and condensed).

That is, it defines the functor CondensedMod.LocallyConstant.functor which takes an R-module to the condensed R-modules given by locally constant maps to it, and proves that this functor is naturally isomorphic to the constant sheaf functor (and the analogues for light condensed modules).

def CompHausLike.LocallyConstantModule.functorToPresheaves {P : TopCat → Prop} (R : Type (max u w)) [Ring R] : CategoryTheory.Functor (ModuleCat R) (CategoryTheory.Functor (CompHausLike P)ᵒᵖ (ModuleCat R))

The functor from the category of R-modules to presheaves on CompHausLike P given by locally constant maps.

@[simp]

theorem CompHausLike.LocallyConstantModule.functorToPresheaves_obj_obj_carrier {P : TopCat → Prop} (R : Type (max u w)) [Ring R] (X : ModuleCat R) (x✝ : (CompHausLike P)ᵒᵖ) : ↑(((functorToPresheaves R).obj X).obj x✝) = LocallyConstant ↑(Opposite.unop x✝).toTop ↑X

@[simp]

theorem CompHausLike.LocallyConstantModule.functorToPresheaves_obj_obj_isAddCommGroup {P : TopCat → Prop} (R : Type (max u w)) [Ring R] (X : ModuleCat R) (x✝ : (CompHausLike P)ᵒᵖ) : (((functorToPresheaves R).obj X).obj x✝).isAddCommGroup = LocallyConstant.instAddCommGroup

@[simp]

theorem CompHausLike.LocallyConstantModule.functorToPresheaves_map_app {P : TopCat → Prop} (R : Type (max u w)) [Ring R] {X✝ Y✝ : ModuleCat R} (f : X✝ ⟶ Y✝) (S : (CompHausLike P)ᵒᵖ) : ((functorToPresheaves R).map f).app S = ModuleCat.ofHom (LocallyConstant.mapₗ R (ModuleCat.Hom.hom f))

@[simp]

theorem CompHausLike.LocallyConstantModule.functorToPresheaves_obj_map {P : TopCat → Prop} (R : Type (max u w)) [Ring R] (X : ModuleCat R) {X✝ Y✝ : (CompHausLike P)ᵒᵖ} (f : X✝ ⟶ Y✝) : ((functorToPresheaves R).obj X).map f = ModuleCat.ofHom (LocallyConstant.comapₗ R (TopCat.Hom.hom f.unop.hom))

@[simp]

theorem CompHausLike.LocallyConstantModule.functorToPresheaves_obj_obj_isModule {P : TopCat → Prop} (R : Type (max u w)) [Ring R] (X : ModuleCat R) (x✝ : (CompHausLike P)ᵒᵖ) : (((functorToPresheaves R).obj X).obj x✝).isModule = LocallyConstant.instModule

def CompHausLike.LocallyConstantModule.functor {P : TopCat → Prop} (R : Type (max u w)) [Ring R] [HasExplicitFiniteCoproducts P] [HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) : CategoryTheory.Functor (ModuleCat R) (CategoryTheory.Sheaf (CategoryTheory.coherentTopology (CompHausLike P)) (ModuleCat R))

CompHausLike.LocallyConstantModule.functorToPresheaves lands in sheaves.

@[simp]

theorem CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isModule_smul_apply {P : TopCat → Prop} (R : Type (max u w)) [Ring R] [HasExplicitFiniteCoproducts P] [HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) (X : ModuleCat R) (x✝ : (CompHausLike P)ᵒᵖ) (n : R) (f : LocallyConstant ↑(Opposite.unop x✝).toTop ↑X) (a✝ : ↑(Opposite.unop x✝).toTop) : (SMul.smul n f) a✝ = n • f a✝

@[simp]

theorem CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_neg_apply {P : TopCat → Prop} (R : Type (max u w)) [Ring R] [HasExplicitFiniteCoproducts P] [HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) (X : ModuleCat R) (x✝ : (CompHausLike P)ᵒᵖ) (f : LocallyConstant ↑(Opposite.unop x✝).toTop ↑X) (a✝ : ↑(Opposite.unop x✝).toTop) : (-f) a✝ = -f a✝

@[simp]

theorem CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_nsmul_apply {P : TopCat → Prop} (R : Type (max u w)) [Ring R] [HasExplicitFiniteCoproducts P] [HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) (X : ModuleCat R) (x✝ : (CompHausLike P)ᵒᵖ) (n : ℕ) (x : LocallyConstant ↑(Opposite.unop x✝).toTop ↑X) (a✝ : ↑(Opposite.unop x✝).toTop) : (n • x) a✝ = n • x a✝

@[simp]

theorem CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_sub_apply {P : TopCat → Prop} (R : Type (max u w)) [Ring R] [HasExplicitFiniteCoproducts P] [HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) (X : ModuleCat R) (x✝ : (CompHausLike P)ᵒᵖ) (f g : LocallyConstant ↑(Opposite.unop x✝).toTop ↑X) (a : ↑(Opposite.unop x✝).toTop) : (f - g) a = f a - g a

@[simp]

theorem CompHausLike.LocallyConstantModule.functor_map_hom_app_hom_apply_apply {P : TopCat → Prop} (R : Type (max u w)) [Ring R] [HasExplicitFiniteCoproducts P] [HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) {X✝ Y✝ : ModuleCat R} (f : X✝ ⟶ Y✝) (S : (CompHausLike P)ᵒᵖ) (g : LocallyConstant ↑(Opposite.unop S).toTop ↑X✝) (a✝ : ↑(Opposite.unop S).toTop) : ((ModuleCat.Hom.hom (((functor R hs).map f).hom.app S)) g) a✝ = (ModuleCat.Hom.hom f) (g a✝)

@[simp]

theorem CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_add_apply {P : TopCat → Prop} (R : Type (max u w)) [Ring R] [HasExplicitFiniteCoproducts P] [HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) (X : ModuleCat R) (x✝ : (CompHausLike P)ᵒᵖ) (f g : LocallyConstant ↑(Opposite.unop x✝).toTop ↑X) (a : ↑(Opposite.unop x✝).toTop) : (f + g) a = f a + g a

@[simp]

theorem CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_zero_apply {P : TopCat → Prop} (R : Type (max u w)) [Ring R] [HasExplicitFiniteCoproducts P] [HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) (X : ModuleCat R) (x✝ : (CompHausLike P)ᵒᵖ) (a✝ : ↑(Opposite.unop x✝).toTop) : 0 a✝ = 0

@[simp]

theorem CompHausLike.LocallyConstantModule.functor_obj_obj_obj_carrier {P : TopCat → Prop} (R : Type (max u w)) [Ring R] [HasExplicitFiniteCoproducts P] [HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) (X : ModuleCat R) (x✝ : (CompHausLike P)ᵒᵖ) : ↑(((functor R hs).obj X).obj.obj x✝) = LocallyConstant ↑(Opposite.unop x✝).toTop ↑X

@[simp]

theorem CompHausLike.LocallyConstantModule.functor_obj_obj_map_hom_apply_apply {P : TopCat → Prop} (R : Type (max u w)) [Ring R] [HasExplicitFiniteCoproducts P] [HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) (X : ModuleCat R) {X✝ Y✝ : (CompHausLike P)ᵒᵖ} (f : X✝ ⟶ Y✝) (g : LocallyConstant ↑(Opposite.unop X✝).toTop ↑X) (a✝ : ↑(Opposite.unop Y✝).toTop) : ((ModuleCat.Hom.hom (((functor R hs).obj X).obj.map f)) g) a✝ = g ((TopCat.Hom.hom f.unop.hom) a✝)

@[simp]

theorem CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_zsmul_apply {P : TopCat → Prop} (R : Type (max u w)) [Ring R] [HasExplicitFiniteCoproducts P] [HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) (X : ModuleCat R) (x✝ : (CompHausLike P)ᵒᵖ) (n : ℤ) (x : LocallyConstant ↑(Opposite.unop x✝).toTop ↑X) (a✝ : ↑(Opposite.unop x✝).toTop) : (n • x) a✝ = n • x a✝

@[reducible, inline]

abbrev CondensedMod.LocallyConstant.functorToPresheaves (R : Type (u + 1)) [Ring R] : CategoryTheory.Functor (ModuleCat R) (CategoryTheory.Functor CompHausᵒᵖ (ModuleCat R))

functorToPresheaves in the case of CompHaus.

@[reducible, inline]

abbrev CondensedMod.LocallyConstant.functor (R : Type (u + 1)) [Ring R] : CategoryTheory.Functor (ModuleCat R) (CondensedMod R)

functorToPresheaves as a functor to condensed modules.

noncomputable def CondensedMod.LocallyConstant.functorIsoDiscreteAux₁ (R : Type (u + 1)) [Ring R] (M : ModuleCat R) : M ≅ ModuleCat.of R (LocallyConstant ↑(CompHaus.of PUnit.{u + 1}).toTop ↑M)

Auxiliary definition for functorIsoDiscrete.

noncomputable def CondensedMod.LocallyConstant.functorIsoDiscreteAux₂ (R : Type (u + 1)) [Ring R] (M : ModuleCat R) : (Condensed.discrete (ModuleCat R)).obj M ≅ (Condensed.discrete (ModuleCat R)).obj (ModuleCat.of R (LocallyConstant ↑(CompHaus.of PUnit.{u + 1}).toTop ↑M))

Auxiliary definition for functorIsoDiscrete.

instance CondensedMod.LocallyConstant.instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor (R : Type (u + 1)) [Ring R] (M : ModuleCat R) : CategoryTheory.IsIso ((Condensed.forget R).map ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj M)))

noncomputable def CondensedMod.LocallyConstant.functorIsoDiscreteComponents (R : Type (u + 1)) [Ring R] (M : ModuleCat R) : (Condensed.discrete (ModuleCat R)).obj M ≅ (functor R).obj M

Auxiliary definition for functorIsoDiscrete.

noncomputable def CondensedMod.LocallyConstant.functorIsoDiscrete (R : Type (u + 1)) [Ring R] : functor R ≅ Condensed.discrete (ModuleCat R)

CondensedMod.LocallyConstant.functor is naturally isomorphic to the constant sheaf functor from R-modules to condensed R-modules.

noncomputable def CondensedMod.LocallyConstant.adjunction (R : Type (u + 1)) [Ring R] : functor R ⊣ Condensed.underlying (ModuleCat R)

CondensedMod.LocallyConstant.functor is left adjoint to the forgetful functor from condensed R-modules to R-modules.

noncomputable def CondensedMod.LocallyConstant.fullyFaithfulFunctor (R : Type (u + 1)) [Ring R] : (functor R).FullyFaithful

CondensedMod.LocallyConstant.functor is fully faithful.

instance CondensedMod.LocallyConstant.instFaithfulModuleCatFunctor (R : Type (u + 1)) [Ring R] : (functor R).Faithful

instance CondensedMod.LocallyConstant.instFullModuleCatFunctor (R : Type (u + 1)) [Ring R] : (functor R).Full

instance CondensedMod.LocallyConstant.instFaithfulModuleCatCondensedDiscrete (R : Type (u + 1)) [Ring R] : (Condensed.discrete (ModuleCat R)).Faithful

instance CondensedMod.LocallyConstant.instFaithfulModuleCatSheafCompHausCoherentTopologyConstantSheaf (R : Type (u + 1)) [Ring R] : (CategoryTheory.constantSheaf (CategoryTheory.coherentTopology CompHaus) (ModuleCat R)).Faithful

instance CondensedMod.LocallyConstant.instFullModuleCatCondensedDiscrete (R : Type (u + 1)) [Ring R] : (Condensed.discrete (ModuleCat R)).Full

instance CondensedMod.LocallyConstant.instFullModuleCatSheafCompHausCoherentTopologyConstantSheaf (R : Type (u + 1)) [Ring R] : (CategoryTheory.constantSheaf (CategoryTheory.coherentTopology CompHaus) (ModuleCat R)).Full

instance CondensedMod.LocallyConstant.instFaithfulSheafCompHausCoherentTopologyTypeConstantSheaf : (CategoryTheory.constantSheaf (CategoryTheory.coherentTopology CompHaus) (Type (u + 1))).Faithful

instance CondensedMod.LocallyConstant.instFullSheafCompHausCoherentTopologyTypeConstantSheaf : (CategoryTheory.constantSheaf (CategoryTheory.coherentTopology CompHaus) (Type (u + 1))).Full

@[reducible, inline]

abbrev LightCondMod.LocallyConstant.functorToPresheaves (R : Type u) [Ring R] : CategoryTheory.Functor (ModuleCat R) (CategoryTheory.Functor LightProfiniteᵒᵖ (ModuleCat R))

functorToPresheaves in the case of LightProfinite.

@[reducible, inline]

abbrev LightCondMod.LocallyConstant.functor (R : Type u) [Ring R] : CategoryTheory.Functor (ModuleCat R) (LightCondMod R)

functorToPresheaves as a functor to light condensed modules.

noncomputable def LightCondMod.LocallyConstant.functorIsoDiscreteAux₁ (R : Type u) [Ring R] (M : ModuleCat R) : M ≅ ModuleCat.of R (LocallyConstant ↑(LightProfinite.of PUnit.{u + 1}).toTop ↑M)

Auxiliary definition for functorIsoDiscrete.

noncomputable def LightCondMod.LocallyConstant.functorIsoDiscreteAux₂ (R : Type u) [Ring R] (M : ModuleCat R) : (LightCondensed.discrete (ModuleCat R)).obj M ≅ (LightCondensed.discrete (ModuleCat R)).obj (ModuleCat.of R (LocallyConstant ↑(LightProfinite.of PUnit.{u + 1}).toTop ↑M))

Auxiliary definition for functorIsoDiscrete.

instance LightCondMod.LocallyConstant.instHasSheafifyLightProfiniteCoherentTopologyModuleCat (R : Type u) [Ring R] : CategoryTheory.HasSheafify (CategoryTheory.coherentTopology LightProfinite) (ModuleCat R)

instance LightCondMod.LocallyConstant.instIsIsoLightCondSetMapForgetAppLightCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor (R : Type u) [Ring R] (M : ModuleCat R) : CategoryTheory.IsIso ((LightCondensed.forget R).map ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj M)))

noncomputable def LightCondMod.LocallyConstant.functorIsoDiscreteComponents (R : Type u) [Ring R] (M : ModuleCat R) : (LightCondensed.discrete (ModuleCat R)).obj M ≅ (functor R).obj M

Auxiliary definition for functorIsoDiscrete.

noncomputable def LightCondMod.LocallyConstant.functorIsoDiscrete (R : Type u) [Ring R] : functor R ≅ LightCondensed.discrete (ModuleCat R)

LightCondMod.LocallyConstant.functor is naturally isomorphic to the constant sheaf functor from R-modules to light condensed R-modules.

noncomputable def LightCondMod.LocallyConstant.adjunction (R : Type u) [Ring R] : functor R ⊣ LightCondensed.underlying (ModuleCat R)

LightCondMod.LocallyConstant.functor is left adjoint to the forgetful functor from light condensed R-modules to R-modules.

noncomputable def LightCondMod.LocallyConstant.fullyFaithfulFunctor (R : Type u) [Ring R] : (functor R).FullyFaithful

LightCondMod.LocallyConstant.functor is fully faithful.

instance LightCondMod.LocallyConstant.instFaithfulModuleCatFunctor (R : Type u) [Ring R] : (functor R).Faithful

instance LightCondMod.LocallyConstant.instFullModuleCatFunctor (R : Type u) [Ring R] : (functor R).Full

instance LightCondMod.LocallyConstant.instFaithfulModuleCatLightCondensedDiscrete (R : Type u) [Ring R] : (LightCondensed.discrete (ModuleCat R)).Faithful

instance LightCondMod.LocallyConstant.instFaithfulModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf (R : Type u) [Ring R] : (CategoryTheory.constantSheaf (CategoryTheory.coherentTopology LightProfinite) (ModuleCat R)).Faithful

instance LightCondMod.LocallyConstant.instFullModuleCatLightCondensedDiscrete (R : Type u) [Ring R] : (LightCondensed.discrete (ModuleCat R)).Full

instance LightCondMod.LocallyConstant.instFullModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf (R : Type u) [Ring R] : (CategoryTheory.constantSheaf (CategoryTheory.coherentTopology LightProfinite) (ModuleCat R)).Full

instance LightCondMod.LocallyConstant.instFaithfulSheafLightProfiniteCoherentTopologyTypeConstantSheaf : (CategoryTheory.constantSheaf (CategoryTheory.coherentTopology LightProfinite) (Type u)).Faithful

instance LightCondMod.LocallyConstant.instFullSheafLightProfiniteCoherentTopologyTypeConstantSheaf : (CategoryTheory.constantSheaf (CategoryTheory.coherentTopology LightProfinite) (Type u)).Full