The smooth part of a module

Let A be a ring and J : ι → Submodule A A a nonempty family of left ideals that is directed downwards. The smooth part of an A-module M is its largest submodule which is smooth for J (TauCeti.smoothModules). Every linear map sends smooth parts into smooth parts, so the smooth part is a functor from all A-modules to smooth A-modules, and it is right adjoint to the inclusion of the smooth modules. Hence the smooth modules form a coreflective full subcategory of ModuleCat A and have all limits: the product of a family of smooth modules in this subcategory is the smooth part of their ordinary product, which is generally smaller.

A vector m lies in the smooth part exactly when its cyclic submodule A ∙ m is smooth. When the family is stable under right multiplication (for each b and i some J j satisfies J j * b ⊆ J i), this is simply the condition that m is killed by some J i. For the left ideals of a topological ring with continuous right multiplications forming a basis of neighborhoods of 0, this stability holds automatically.

Main definitions

• TauCeti.smoothPart J M: the supremum of the submodules of M all of whose vectors are killed by some J i; for nonempty directed J, the largest such submodule.
• TauCeti.smoothPartFunctor hJ: the smooth part as a functor ModuleCat A ⥤ smooth modules.
• TauCeti.smoothPartAdjunction hJ: the inclusion of smooth modules is left adjoint to the smooth part.

Main results

• TauCeti.mem_smoothPart_iff: m lies in the smooth part when A ∙ m is smooth.
• TauCeti.mem_smoothPart_iff_of_mul_mem, TauCeti.mem_smoothPart_iff_of_hasBasis: under right multiplication stability, m lies in the smooth part when some J i kills it.
• TauCeti.smoothPart_eq_top_iff: a module is smooth when it is its own smooth part.
• TauCeti.hasLimitsOfSize_smoothModules: the smooth modules have all limits.

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.

The smooth part of a module

def TauCeti.smoothPart {A : Type u} [Ring A] {ι : Type u_1} (J : ι → Submodule A A) (M : Type v) [AddCommGroup M] [Module A M] : Submodule A M

The smooth part of an A-module M for a family J of left ideals: the supremum of the submodules of M all of whose vectors are killed by some J i. When J is nonempty and directed downwards, it is the largest such submodule (le_smoothPart_iff).

theorem TauCeti.le_smoothPart {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} {M : Type v} [AddCommGroup M] [Module A M] {p : Submodule A M} (hp : ∀ m ∈ p, ∃ (i : ι), ∀ a ∈ J i, a • m = 0) : p ≤ smoothPart J M

A submodule all of whose vectors are killed by some J i lies in the smooth part.

theorem TauCeti.map_smoothPart_le {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} {M : Type v} [AddCommGroup M] [Module A M] {N : Type u_2} [AddCommGroup N] [Module A N] (f : M →ₗ[A] N) : Submodule.map f (smoothPart J M) ≤ smoothPart J N

Linear maps send smooth parts into smooth parts.

theorem TauCeti.exists_forall_smul_eq_zero_of_mem_smoothPart {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} {M : Type v} [AddCommGroup M] [Module A M] [Nonempty ι] (hJ : Directed (fun (x1 x2 : Submodule A A) => x1 ≥ x2) J) {m : M} (hm : m ∈ smoothPart J M) : ∃ (i : ι), ∀ a ∈ J i, a • m = 0

For a directed family J, every vector of the smooth part is killed by some J i.

theorem TauCeti.mem_smoothPart_iff {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} {M : Type v} [AddCommGroup M] [Module A M] [Nonempty ι] (hJ : Directed (fun (x1 x2 : Submodule A A) => x1 ≥ x2) J) {m : M} : m ∈ smoothPart J M ↔ ∀ (b : A), ∃ (i : ι), ∀ a ∈ J i, a • b • m = 0

For a directed family J, a vector lies in the smooth part exactly when its cyclic submodule is smooth: every b • m is killed by some J i.

theorem TauCeti.le_smoothPart_iff {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} {M : Type v} [AddCommGroup M] [Module A M] [Nonempty ι] (hJ : Directed (fun (x1 x2 : Submodule A A) => x1 ≥ x2) J) {p : Submodule A M} : p ≤ smoothPart J M ↔ ∀ m ∈ p, ∃ (i : ι), ∀ a ∈ J i, a • m = 0

For a directed family J, the smooth part is the largest submodule all of whose vectors are killed by some J i.

theorem TauCeti.mem_smoothPart_iff_of_mul_mem {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} {M : Type v} [AddCommGroup M] [Module A M] [Nonempty ι] (hJ : Directed (fun (x1 x2 : Submodule A A) => x1 ≥ x2) J) (hJb : ∀ (b : A) (i : ι), ∃ (j : ι), ∀ a ∈ J j, a * b ∈ J i) {m : M} : m ∈ smoothPart J M ↔ ∃ (i : ι), ∀ a ∈ J i, a • m = 0

If the directed family J is stable under right multiplication, in the sense that for every b and i some J j satisfies J j * b ⊆ J i, a vector lies in the smooth part exactly when it is killed by some J i.

theorem TauCeti.smoothPart_eq_top_iff {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} {M : Type v} [AddCommGroup M] [Module A M] [Nonempty ι] (hJ : Directed (fun (x1 x2 : Submodule A A) => x1 ≥ x2) J) : smoothPart J M = ⊤ ↔ smoothModules J ↧M

For a directed family J, a module is smooth exactly when it is its own smooth part.

theorem TauCeti.smoothModules_smoothPart {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} {M : Type v} [AddCommGroup M] [Module A M] [Nonempty ι] (hJ : Directed (fun (x1 x2 : Submodule A A) => x1 ≥ x2) J) : smoothModules J ↧↥(smoothPart J M)

For a directed family J, the smooth part of a module is a smooth module.

Left ideals of a topological ring

theorem TauCeti.exists_forall_mul_mem_of_hasBasis {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} [TopologicalSpace A] [SeparatelyContinuousMul A] (hJ : (nhds 0).HasBasis (fun (x : ι) => True) fun (i : ι) => ↑(J i)) (b : A) (i : ι) : ∃ (j : ι), ∀ a ∈ J j, a * b ∈ J i

If the left ideals J i form a basis of neighborhoods of 0 and right multiplications are continuous, then for every b and i some J j satisfies J j * b ⊆ J i.

theorem TauCeti.mem_smoothPart_iff_of_hasBasis {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} [TopologicalSpace A] [SeparatelyContinuousMul A] (hJ : (nhds 0).HasBasis (fun (x : ι) => True) fun (i : ι) => ↑(J i)) {M : Type u_2} [AddCommGroup M] [Module A M] {m : M} : m ∈ smoothPart J M ↔ ∃ (i : ι), ∀ a ∈ J i, a • m = 0

If the left ideals J i form a basis of neighborhoods of 0 and right multiplications are continuous, a vector lies in the smooth part exactly when it is killed by some J i.

The coreflection onto smooth modules

noncomputable def TauCeti.smoothPartFunctor {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} [Nonempty ι] (hJ : Directed (fun (x1 x2 : Submodule A A) => x1 ≥ x2) J) : CategoryTheory.Functor (ModuleCat A) (smoothModules J).FullSubcategory

For a directed family J, the smooth part as a functor from A-modules to smooth A-modules.

@[simp]

theorem TauCeti.smoothPartFunctor_obj_obj {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} [Nonempty ι] (hJ : Directed (fun (x1 x2 : Submodule A A) => x1 ≥ x2) J) (M : ModuleCat A) : ((smoothPartFunctor hJ).obj M).obj = ↧↥(smoothPart J ↑M)

The smooth part functor sends a module to its smooth part.

@[simp]

theorem TauCeti.smoothPartFunctor_map_hom {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} [Nonempty ι] (hJ : Directed (fun (x1 x2 : Submodule A A) => x1 ≥ x2) J) {M N : ModuleCat A} (f : M ⟶ N) : ((smoothPartFunctor hJ).map f).hom = ModuleCat.ofHom ((ModuleCat.Hom.hom f).restrict ⋯)

The smooth part of a linear map is its restriction.

noncomputable def TauCeti.smoothPartAdjunction {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).ι ⊣ smoothPartFunctor hJ

For a directed family J, the inclusion of smooth A-modules is left adjoint to the smooth part: linear maps from a smooth module N to M are the linear maps from N to the smooth part of M. The counit is the inclusion of the smooth part.

@[simp]

theorem TauCeti.smoothPartAdjunction_unit_app {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} [Nonempty ι] (hJ : Directed (fun (x1 x2 : Submodule A A) => x1 ≥ x2) J) (N : (smoothModules J).FullSubcategory) : (smoothPartAdjunction hJ).unit.app N = CategoryTheory.ObjectProperty.homMk (ModuleCat.ofHom (LinearMap.codRestrict (smoothPart J ↑N.obj) LinearMap.id ⋯))

@[simp]

theorem TauCeti.smoothPartAdjunction_counit_app {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} [Nonempty ι] (hJ : Directed (fun (x1 x2 : Submodule A A) => x1 ≥ x2) J) (M : ModuleCat A) : (smoothPartAdjunction hJ).counit.app M = ModuleCat.ofHom (smoothPart J ↑M).subtype

@[instance_reducible]

noncomputable def TauCeti.coreflectiveSmoothModules {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} [Nonempty ι] (hJ : Directed (fun (x1 x2 : Submodule A A) => x1 ≥ x2) J) : CategoryTheory.Coreflective (smoothModules J).ι

For a directed family J, the inclusion of smooth A-modules is coreflective, with coreflector the smooth part.

theorem TauCeti.hasLimitsOfSize_smoothModules {A : Type u} [Ring A] {ι : Type u_1} {J : ι → Submodule A A} [Nonempty ι] [UnivLE.{w, v}] (hJ : Directed (fun (x1 x2 : Submodule A A) => x1 ≥ x2) J) : CategoryTheory.Limits.HasLimitsOfSize.{t, w, v, max u (v + 1)} (smoothModules J).FullSubcategory

For a directed family J, the smooth A-modules have all limits. A limit of smooth modules can be computed as the smooth part of their limit in ModuleCat A.