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]
:
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.
Instances For
@[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)ᵒᵖ),
((CompHausLike.LocallyConstantModule.functorToPresheaves R).map f).app S = LocallyConstant.mapₗ R f
@[simp]
theorem
CompHausLike.LocallyConstantModule.functorToPresheaves_obj_obj
{P : TopCat → Prop}
(R : Type (max u w))
[Ring R]
(X : ModuleCat R)
:
∀ (x : (CompHausLike P)ᵒᵖ),
((CompHausLike.LocallyConstantModule.functorToPresheaves R).obj X).obj x = match x with
| Opposite.op S => ModuleCat.of R (LocallyConstant ↑S.toTop ↑X)
@[simp]
theorem
CompHausLike.LocallyConstantModule.functorToPresheaves_obj_map
{P : TopCat → Prop}
(R : Type (max u w))
[Ring R]
(X : ModuleCat R)
:
∀ {X_1 Y : (CompHausLike P)ᵒᵖ} (f : X_1 ⟶ Y),
((CompHausLike.LocallyConstantModule.functorToPresheaves R).obj X).map f = 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)
:
CompHausLike.LocallyConstantModule.functorToPresheaves lands in sheaves.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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]
functorToPresheaves in the case of CompHaus.
Equations
Instances For
@[reducible, inline]
functorToPresheaves as a functor to condensed modules.
Equations
Instances For
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
- CondensedMod.LocallyConstant.functorIsoDiscreteAux₁ R M = { hom := LocallyConstant.constₗ R, inv := LocallyConstant.evalₗ R PUnit.unit, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
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
Instances For
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)))
Equations
- ⋯ = ⋯
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.
Instances For
CondensedMod.LocallyConstant.functor is naturally isomorphic to the constant sheaf functor from
R-modules to condensed R-modules.
Equations
Instances For
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
Instances For
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.
Instances For
instance
CondensedMod.LocallyConstant.instFaithfulModuleCatFunctor
(R : Type (u + 1))
[Ring R]
:
(CondensedMod.LocallyConstant.functor R).Faithful
Equations
- ⋯ = ⋯
instance
CondensedMod.LocallyConstant.instFullModuleCatFunctor
(R : Type (u + 1))
[Ring R]
:
(CondensedMod.LocallyConstant.functor R).Full
Equations
- ⋯ = ⋯
instance
CondensedMod.LocallyConstant.instFaithfulModuleCatCondensedDiscrete
(R : Type (u + 1))
[Ring R]
:
(Condensed.discrete (ModuleCat R)).Faithful
Equations
- ⋯ = ⋯
instance
CondensedMod.LocallyConstant.instFaithfulModuleCatSheafCompHausCoherentTopologyConstantSheaf
(R : Type (u + 1))
[Ring R]
:
(CategoryTheory.constantSheaf (CategoryTheory.coherentTopology CompHaus) (ModuleCat R)).Faithful
Equations
- ⋯ = ⋯
instance
CondensedMod.LocallyConstant.instFullModuleCatCondensedDiscrete
(R : Type (u + 1))
[Ring R]
:
(Condensed.discrete (ModuleCat R)).Full
Equations
- ⋯ = ⋯
instance
CondensedMod.LocallyConstant.instFullModuleCatSheafCompHausCoherentTopologyConstantSheaf
(R : Type (u + 1))
[Ring R]
:
Equations
- ⋯ = ⋯
@[reducible, inline]
functorToPresheaves in the case of LightProfinite.
Equations
Instances For
@[reducible, inline]
functorToPresheaves as a functor to light condensed modules.
Equations
Instances For
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
- LightCondMod.LocallyConstant.functorIsoDiscreteAux₁ R M = { hom := LocallyConstant.constₗ R, inv := LocallyConstant.evalₗ R PUnit.unit, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
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
Instances For
instance
LightCondMod.LocallyConstant.instHasSheafifyLightProfiniteCoherentTopologyModuleCat
(R : Type u)
[Ring R]
:
Equations
- ⋯ = ⋯
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)))
Equations
- ⋯ = ⋯
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.
Instances For
LightCondMod.LocallyConstant.functor is naturally isomorphic to the constant sheaf functor from
R-modules to light condensed R-modules.
Equations
Instances For
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
Instances For
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.
Instances For
instance
LightCondMod.LocallyConstant.instFaithfulModuleCatFunctor
(R : Type u)
[Ring R]
:
(LightCondMod.LocallyConstant.functor R).Faithful
Equations
- ⋯ = ⋯
instance
LightCondMod.LocallyConstant.instFullModuleCatFunctor
(R : Type u)
[Ring R]
:
(LightCondMod.LocallyConstant.functor R).Full
Equations
- ⋯ = ⋯
instance
LightCondMod.LocallyConstant.instFaithfulModuleCatLightCondensedDiscrete
(R : Type u)
[Ring R]
:
(LightCondensed.discrete (ModuleCat R)).Faithful
Equations
- ⋯ = ⋯
instance
LightCondMod.LocallyConstant.instFaithfulModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf
(R : Type u)
[Ring R]
:
Equations
- ⋯ = ⋯
instance
LightCondMod.LocallyConstant.instFullModuleCatLightCondensedDiscrete
(R : Type u)
[Ring R]
:
(LightCondensed.discrete (ModuleCat R)).Full
Equations
- ⋯ = ⋯
instance
LightCondMod.LocallyConstant.instFullModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf
(R : Type u)
[Ring R]
:
Equations
- ⋯ = ⋯