Smooth modules and discrete modules

Let A be a ring and J : ι → Submodule A A a family of left ideals of A. An A-module M is smooth for J when every vector is killed by one of the J i, that is ∀ m : M, ∃ i, ∀ a ∈ J i, a • m = 0. For the enveloping algebra of an affine Lie algebra 𝔤̂ and the left ideals J N generated by 𝔤 ⊗ tᴺ ℂ[[t]], these are the smooth 𝔤̂-modules of the representation theory of affine Lie algebras. When A carries a topology, M is a discrete module when every orbit map a ↦ a • m is continuous for the discrete topology on M, as for the discrete modules of a profinite group in Galois cohomology.

Both notions are properties of objects of ModuleCat A, and their full subcategories are the categories of smooth and of discrete A-modules. This file proves:

• both properties are closed under subobjects and quotients, hence under isomorphisms, kernels, cokernels and images, and contain the zero module (for smoothness, when ι is nonempty);
• when the family J is directed downwards, smoothness is closed under all colimits (in particular arbitrary direct sums) and under finite limits (in particular finite products), so the smooth modules form an abelian category;
• for an arbitrary topology on A, the discrete modules are closed under all colimits and under finite limits, so they form an abelian category;
• when addition by a constant is continuous on A, the discrete modules are the smooth modules for the family of all open left ideals;
• when the J i form a basis of neighborhoods of 0, smoothness for J and discreteness coincide;
• restriction of scalars along a ring homomorphism preserves smoothness when the pulled-back ideals dominate the given family, and preserves discreteness along a continuous one.

Main definitions

• TauCeti.smoothModules J: the modules every vector of which is killed by some J i.
• TauCeti.discreteModules A: the modules all of whose orbit maps are continuous for the discrete topology on the module.

Main results

• TauCeti.isClosedUnderColimitsOfShape_smoothModules, TauCeti.isClosedUnderFiniteLimits_smoothModules: closure of smoothness for a directed family under colimits and finite limits.
• TauCeti.smoothModules_directSum: a direct sum of smooth modules is smooth.
• TauCeti.discreteModules_iff_isOpen: a module is discrete if and only if every set {a | a • m = x} is open.
• TauCeti.discreteModules_of_iSup_range_eq_top: a module spanned by the images of linear maps out of discrete modules is discrete; hence discreteness is closed under colimits.
• TauCeti.discreteModules_eq_smoothModules: discrete modules are the smooth modules for the family of open left ideals.
• TauCeti.smoothModules_eq_discreteModules: if the J i form a basis of neighborhoods of 0, smoothness for J is discreteness.
• TauCeti.smoothModules_restrictScalars, TauCeti.discreteModules_restrictScalars: restriction of scalars preserves both properties.

References

• Edward Frenkel, Langlands Correspondence for Loop Groups, Cambridge Studies in Advanced Mathematics 103, Cambridge University Press, 2007, Section 2.1, for smooth modules over the completed enveloping algebra of an affine Lie algebra.
• Jean-Pierre Serre, Galois Cohomology, Springer, 1997, Chapter I, Section 2.1, for discrete modules over a profinite group.

Smooth modules

def TauCeti.smoothModules {A : Type u} [Ring A] {ι : Type u_1} (J : ι → Submodule A A) : CategoryTheory.ObjectProperty (ModuleCat A)

The modules that are smooth for a family J of left ideals of A: every vector is killed by one of the J i.

theorem TauCeti.smoothModules_iff {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} {M : ModuleCat A} : smoothModules J M ↔ ∀ (m : ↑M), ∃ (i : ι), ∀ a ∈ J i, a • m = 0

A module is smooth for J when every vector is killed by one of the J i.

theorem TauCeti.smoothModules_le_of_forall_exists_le {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} {ι' : Type u_2} {J' : ι' → Submodule A A} (h : ∀ (i : ι), ∃ (i' : ι'), J' i' ≤ J i) : smoothModules J ≤ smoothModules J'

Smoothness for J implies smoothness for J' when every J i contains some J' i'.

instance TauCeti.instIsClosedUnderSubobjectsModuleCatSmoothModules {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} : (smoothModules J).IsClosedUnderSubobjects

Smoothness passes to the source of an injective linear map.

instance TauCeti.instIsClosedUnderQuotientsModuleCatSmoothModules {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} : (smoothModules J).IsClosedUnderQuotients

Smoothness passes to the target of a surjective linear map.

instance TauCeti.instContainsZeroModuleCatSmoothModulesOfNonempty {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} [Nonempty ι] : (smoothModules J).ContainsZero

The zero module is smooth as soon as the family J is nonempty.

theorem TauCeti.smoothModules_submodule {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} {M : ModuleCat A} (hM : smoothModules J M) (p : Submodule A ↑M) : smoothModules J ↧↥p

A submodule of a smooth module is smooth.

theorem TauCeti.smoothModules_quotient {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} {M : ModuleCat A} (hM : smoothModules J M) (p : Submodule A ↑M) : smoothModules J ↧(↑M ⧸ p)

A quotient of a smooth module is smooth.

theorem TauCeti.smoothModules_range {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} {M N : ModuleCat A} (f : M ⟶ N) (hM : smoothModules J M) : smoothModules J ↧↥(ModuleCat.Hom.hom f).range

The image of a linear map out of a smooth module is smooth.

theorem TauCeti.smoothModules_of_iSup_range_eq_top {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} [Nonempty ι] (hJ : Directed (fun (x1 x2 : Submodule A A) => x1 ≥ x2) J) {κ : Type u_2} {M : κ → ModuleCat A} {N : ModuleCat A} (f : (k : κ) → ↑(M k) →ₗ[A] ↑N) (hf : ⨆ (k : κ), (f k).range = ⊤) (hM : ∀ (k : κ), smoothModules J (M k)) : smoothModules J N

For a directed family J, a module spanned by the images of linear maps out of smooth modules is smooth.

theorem TauCeti.isClosedUnderColimitsOfShape_smoothModules {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} [Nonempty ι] (hJ : Directed (fun (x1 x2 : Submodule A A) => x1 ≥ x2) J) (K : Type u_2) [CategoryTheory.Category.{v_1, u_2} K] : (smoothModules J).IsClosedUnderColimitsOfShape K

For a directed family J, smoothness is closed under colimits of any shape.

theorem TauCeti.isClosedUnderFiniteLimits_smoothModules {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} [Nonempty ι] (hJ : Directed (fun (x1 x2 : Submodule A A) => x1 ≥ x2) J) : (smoothModules J).IsClosedUnderFiniteLimits

For a directed family J, smoothness is closed under finite limits.

theorem TauCeti.smoothModules_directSum {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} [Nonempty ι] (hJ : Directed (fun (x1 x2 : Submodule A A) => x1 ≥ x2) J) {κ : Type w} (M : κ → ModuleCat A) (hM : ∀ (k : κ), smoothModules J (M k)) : smoothModules J ↧(DirectSum κ fun (k : κ) => ↑(M k))

For a directed family J, a direct sum of smooth modules is smooth.

instance TauCeti.instPreservesMonomorphismsFullSubcategoryModuleCatSmoothModulesιOfNonempty {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} [Nonempty ι] : (smoothModules J).ι.PreservesMonomorphisms

The inclusion of smooth modules into all A-modules preserves monomorphisms: a monomorphism of smooth modules is injective.

theorem TauCeti.smoothModules_restrictScalars {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} {B : Type u'} [Ring B] (f : B →+* A) {ι' : Type u_2} {J' : ι' → Submodule B B} (h : ∀ (i : ι), ∃ (i' : ι'), J' i' ≤ Ideal.comap f (J i)) {M : ModuleCat A} (hM : smoothModules J M) : smoothModules J' ((ModuleCat.restrictScalars f).obj M)

Restriction of scalars along f : B →+* A sends modules smooth for J to modules smooth for J' when every pulled-back ideal f⁻¹(J i) contains some J' i'.

Discrete modules

def TauCeti.discreteModules (A : Type u) [Ring A] [TopologicalSpace A] : CategoryTheory.ObjectProperty (ModuleCat A)

The discrete A-modules: every orbit map a ↦ a • m is continuous for the discrete topology on the module.

theorem TauCeti.discreteModules_iff {A : Type u} [Ring A] [TopologicalSpace A] {M : ModuleCat A} : discreteModules A M ↔ ∀ (m : ↑M), Continuous fun (a : A) => a • m

A module is discrete when every orbit map is continuous for the discrete topology on the module.

theorem TauCeti.discreteModules_iff_isOpen {A : Type u} [Ring A] [TopologicalSpace A] {M : ModuleCat A} : discreteModules A M ↔ ∀ (m x : ↑M), IsOpen {a : A | a • m = x}

A module is discrete if and only if every set {a | a • m = x} is open.

instance TauCeti.instIsClosedUnderSubobjectsModuleCatDiscreteModules {A : Type u} [Ring A] [TopologicalSpace A] : (discreteModules A).IsClosedUnderSubobjects

Discreteness passes to the source of an injective linear map.

instance TauCeti.instContainsZeroModuleCatDiscreteModules {A : Type u} [Ring A] [TopologicalSpace A] : (discreteModules A).ContainsZero

The zero module is discrete.

theorem TauCeti.discreteModules_of_iSup_range_eq_top {A : Type u} [Ring A] [TopologicalSpace A] {κ : Type u_2} {M : κ → ModuleCat A} {N : ModuleCat A} (f : (k : κ) → ↑(M k) →ₗ[A] ↑N) (hf : ⨆ (k : κ), (f k).range = ⊤) (hM : ∀ (k : κ), discreteModules A (M k)) : discreteModules A N

A module spanned by the images of linear maps out of discrete modules is discrete.

instance TauCeti.instIsClosedUnderQuotientsModuleCatDiscreteModules {A : Type u} [Ring A] [TopologicalSpace A] : (discreteModules A).IsClosedUnderQuotients

Discreteness passes to the target of a surjective linear map.

instance TauCeti.instIsClosedUnderColimitsOfShapeModuleCatDiscreteModules {A : Type u} [Ring A] [TopologicalSpace A] (K : Type u_2) [CategoryTheory.Category.{v_1, u_2} K] : (discreteModules A).IsClosedUnderColimitsOfShape K

Discreteness is closed under colimits of any shape.

instance TauCeti.instIsClosedUnderFiniteLimitsModuleCatDiscreteModules {A : Type u} [Ring A] [TopologicalSpace A] : (discreteModules A).IsClosedUnderFiniteLimits

Discreteness is closed under finite limits.

theorem TauCeti.discreteModules_prod {A : Type u} [Ring A] [TopologicalSpace A] {M : ModuleCat A} {N : ModuleCat A} (hM : discreteModules A M) (hN : discreteModules A N) : discreteModules A ↧(↑M × ↑N)

The product of two discrete modules, with the componentwise action, is discrete.

theorem TauCeti.discreteModules_eq_smoothModules {A : Type u} [Ring A] [TopologicalSpace A] [SeparatelyContinuousAdd A] : discreteModules A = smoothModules Subtype.val

When addition by a constant is continuous on A, the discrete modules are the smooth modules for the family of open left ideals of A.

theorem TauCeti.smoothModules_le_discreteModules {A : Type u} [Ring A] {ι : Type u_1} [TopologicalSpace A] {J : ι → Submodule A A} [SeparatelyContinuousAdd A] (hJ : ∀ (i : ι), ↑(J i) ∈ nhds 0) : smoothModules J ≤ discreteModules A

If every J i is a neighborhood of 0 and addition by a constant is continuous, modules smooth for J are discrete.

theorem TauCeti.discreteModules_le_smoothModules {A : Type u} [Ring A] {ι : Type u_1} [TopologicalSpace A] {J : ι → Submodule A A} (hJ : ∀ s ∈ nhds 0, ∃ (i : ι), ↑(J i) ⊆ s) : discreteModules A ≤ smoothModules J

If every neighborhood of 0 contains some J i, discrete modules are smooth for J.

theorem TauCeti.smoothModules_eq_discreteModules {A : Type u} [Ring A] {ι : Type u_1} [TopologicalSpace A] {J : ι → Submodule A A} [SeparatelyContinuousAdd A] (hJ : (nhds 0).HasBasis (fun (x : ι) => True) fun (i : ι) => ↑(J i)) : smoothModules J = discreteModules A

If the J i form a basis of neighborhoods of 0 and addition by a constant is continuous, smoothness for J is discreteness.

theorem TauCeti.discreteModules_restrictScalars {A : Type u} [Ring A] [TopologicalSpace A] {B : Type u'} [Ring B] [TopologicalSpace B] {f : B →+* A} (hf : Continuous ⇑f) {M : ModuleCat A} (hM : discreteModules A M) : discreteModules B ((ModuleCat.restrictScalars f).obj M)

Restriction of scalars along a continuous ring homomorphism preserves discreteness.

theorem ModuleCat.isClosed_annihilator_of_discreteModules {A : Type u} [Ring A] [TopologicalSpace A] (M : ModuleCat A) (hM : TauCeti.discreteModules A M) : IsClosed ↑(Module.annihilator A ↑M)

The action annihilator of a discrete module is closed.