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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

theorem CompHausLike.LocallyConstantModule.functorToPresheaves_map_app_hom {P : TopCat → Prop} (R : Type (max u w)) [Ring R] {X✝ Y✝ : ModuleCat R} (f : X✝ ⟶ Y✝) (S : (CompHausLike P)ᵒᵖ) : (((CompHausLike.LocallyConstantModule.functorToPresheaves R).map f).app S).hom = LocallyConstant.mapₗ R f.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)ᵒᵖ) : (((CompHausLike.LocallyConstantModule.functorToPresheaves R).obj X).obj x✝).isModule = LocallyConstant.instModule

@[simp]

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

@[simp]

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

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

CompHausLike.LocallyConstantModule.functorToPresheaves lands in sheaves.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CompHausLike.LocallyConstantModule.functor_map_val {P : TopCat → Prop} (R : Type (max u w)) [Ring R] [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑f) {X✝ Y✝ : ModuleCat R} (f : X✝ ⟶ Y✝) : ((CompHausLike.LocallyConstantModule.functor R hs).map f).val = (CompHausLike.LocallyConstantModule.functorToPresheaves R).map f

@[simp]

theorem CompHausLike.LocallyConstantModule.functor_obj_val {P : TopCat → Prop} (R : Type (max u w)) [Ring R] [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑f) (X : ModuleCat R) : ((CompHausLike.LocallyConstantModule.functor R hs).obj X).val = (CompHausLike.LocallyConstantModule.functorToPresheaves R).obj X

@[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.

Equations

• CondensedMod.LocallyConstant.functorToPresheaves R = CompHausLike.LocallyConstantModule.functorToPresheaves R

@[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.

Equations

• CondensedMod.LocallyConstant.functor R = CompHausLike.LocallyConstantModule.functor R CondensedMod.LocallyConstant.functor.proof_1

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• CondensedMod.LocallyConstant.functorIsoDiscreteAux₂ R M = (Condensed.discrete (ModuleCat R)).mapIso (CondensedMod.LocallyConstant.functorIsoDiscreteAux₁ R M)

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 ((CondensedMod.LocallyConstant.functor R).obj M)))

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

Auxiliary definition for functorIsoDiscrete.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• CondensedMod.LocallyConstant.functorIsoDiscrete R = CategoryTheory.NatIso.ofComponents (fun (M : ModuleCat R) => (CondensedMod.LocallyConstant.functorIsoDiscreteComponents R M).symm) ⋯

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

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

Equations

• CondensedMod.LocallyConstant.adjunction R = (Condensed.discreteUnderlyingAdj (ModuleCat R)).ofNatIsoLeft (CondensedMod.LocallyConstant.functorIsoDiscrete R).symm

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

CondensedMod.LocallyConstant.functor is fully faithful.

Equations

• One or more equations did not get rendered due to their size.

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

instance CondensedMod.LocallyConstant.instFullModuleCatFunctor (R : Type (u + 1)) [Ring R] : (CondensedMod.LocallyConstant.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.

Equations

• LightCondMod.LocallyConstant.functorToPresheaves R = CompHausLike.LocallyConstantModule.functorToPresheaves R

@[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.

Equations

• LightCondMod.LocallyConstant.functor R = CompHausLike.LocallyConstantModule.functor R LightCondMod.LocallyConstant.functor.proof_1

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• LightCondMod.LocallyConstant.functorIsoDiscreteAux₂ R M = (LightCondensed.discrete (ModuleCat R)).mapIso (LightCondMod.LocallyConstant.functorIsoDiscreteAux₁ R M)

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 ((LightCondMod.LocallyConstant.functor R).obj M)))

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

Auxiliary definition for functorIsoDiscrete.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LightCondMod.LocallyConstant.functorIsoDiscrete (R : Type u) [Ring R] : LightCondMod.LocallyConstant.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.

Equations

• LightCondMod.LocallyConstant.functorIsoDiscrete R = CategoryTheory.NatIso.ofComponents (fun (M : ModuleCat R) => (LightCondMod.LocallyConstant.functorIsoDiscreteComponents R M).symm) ⋯

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

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

Equations

• LightCondMod.LocallyConstant.adjunction R = (LightCondensed.discreteUnderlyingAdj (ModuleCat R)).ofNatIsoLeft (LightCondMod.LocallyConstant.functorIsoDiscrete R).symm

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

LightCondMod.LocallyConstant.functor is fully faithful.

Equations

• One or more equations did not get rendered due to their size.

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

instance LightCondMod.LocallyConstant.instFullModuleCatFunctor (R : Type u) [Ring R] : (LightCondMod.LocallyConstant.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