Continuous coinduction and enough injectives for smooth modules

Let f : R →+* A be a ring homomorphism and J : ι → Submodule A A a nonempty family of left ideals of A that is directed downwards. The coinduction of an R-module V is the smooth part (TauCeti.smoothPart) of Mathlib's coextension of scalars Hom_R(A, V), on which A acts by (b • g) a = g (a * b). It is right adjoint to the functor sending a smooth A-module to its underlying R-module, obtained by composing Mathlib's ModuleCat.restrictCoextendScalarsAdj with the smooth-part coreflection.

A left ideal I kills g : Hom_R(A, V) exactly when I ⊆ ker g. Hence, when the family J is also stable under right multiplication, g lies in the coinduction exactly when its kernel contains some J i. When the J i form a basis of neighborhoods of 0 in a topological ring, this says that g is continuous for the discrete topology on V, so that the coinduction is the module Hom_cont,R(A, V) of continuous R-linear maps.

The underlying-module functor is faithful and preserves monomorphisms, so the coinduction preserves injective objects; over a semisimple ring R, such as a field, every coinduced module is injective. The unit of the adjunction is the injective map m ↦ (a ↦ a • m), so coinduction along ℤ →+* A shows that the category of smooth A-modules has enough injectives. Consequently the smooth modules over A : Type u, with modules in universe max u w, have Ext groups in the universe max u w of their morphisms, so derived functors of smooth modules can be computed with injective resolutions.

Main definitions

• TauCeti.coinduction f hJ: the functor from R-modules to smooth A-modules sending V to the smooth part of its coextension of scalars Hom_R(A, V); this is Hom_cont,R(A, V) when the J i form a basis of neighborhoods of 0.
• TauCeti.coinductionAdjunction f hJ: the underlying R-module functor of smooth A-modules is left adjoint to the coinduction.

Main results

• TauCeti.mem_smoothPart_coextendScalars_iff: g lies in the coinduction when some J i lies in its kernel.
• TauCeti.mem_smoothPart_coextendScalars_iff_continuous: for a basis of neighborhoods of 0, g lies in the coinduction when it is continuous for the discrete topology on V.
• TauCeti.coinductionAdjunction_unit_app_injective: the unit m ↦ (a ↦ a • m) is injective.
• TauCeti.injective_coinduction_obj: coinduction preserves injective objects.
• TauCeti.enoughInjectives_smoothModules: smooth modules have enough injectives.
• TauCeti.hasExt_smoothModules: smooth modules have Ext groups in the universe of morphisms.
• TauCeti.hasExt_discreteModules: discrete modules likewise have native Ext groups.

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.5, for the analogous coinduced discrete modules of continuous maps out of a profinite group.

Smooth vectors of the coextension of scalars

theorem TauCeti.forall_smul_coextendScalars_eq_zero_iff {R : Type u₁} {A : Type u} [Ring R] [Ring A] {f : R →+* A} {V : ModuleCat R} (I : Submodule A A) (g : ↑((ModuleCat.coextendScalars f).obj V)) : (∀ a ∈ I, a • g = 0) ↔ ∀ a ∈ I, ((ModuleCat.CoextendScalars.equiv f V) g) a = 0

A left ideal I kills an R-linear map g : A → V of the coextension of scalars exactly when I lies in the kernel of g.

theorem TauCeti.mem_smoothPart_coextendScalars_iff {R : Type u₁} {A : Type u} [Ring R] [Ring A] {f : R →+* A} {ι : Type u_1} {J : ι → Submodule A A} {V : ModuleCat R} [Nonempty ι] (hJ : Directed (fun (x1 x2 : Submodule A A) => x1 ≥ x2) J) (hJb : ∀ (b : A) (i : ι), ∃ (j : ι), ∀ a ∈ J j, a * b ∈ J i) {g : ↑((ModuleCat.coextendScalars f).obj V)} : g ∈ smoothPart J ↑((ModuleCat.coextendScalars f).obj V) ↔ ∃ (i : ι), ∀ a ∈ J i, ((ModuleCat.CoextendScalars.equiv f V) g) a = 0

If the directed family J is stable under right multiplication, an R-linear map g : A → V lies in the smooth part of the coextension of scalars exactly when some J i lies in its kernel.

theorem TauCeti.mem_smoothPart_coextendScalars_iff_continuous {R : Type u₁} {A : Type u} [Ring R] [Ring A] {f : R →+* A} {ι : Type u_1} {J : ι → Submodule A A} {V : ModuleCat R} [TopologicalSpace A] [SeparatelyContinuousAdd A] [SeparatelyContinuousMul A] (hJ : (nhds 0).HasBasis (fun (x : ι) => True) fun (i : ι) => ↑(J i)) {g : ↑((ModuleCat.coextendScalars f).obj V)} : g ∈ smoothPart J ↑((ModuleCat.coextendScalars f).obj V) ↔ Continuous fun (a : A) => ((ModuleCat.CoextendScalars.equiv f V) g) a

If the left ideals J i form a basis of neighborhoods of 0 in a topological ring, an R-linear map g : A → V lies in the smooth part of the coextension of scalars exactly when it is continuous for the discrete topology on V.

The coinduction functor and its adjunction

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

The coinduction of R-modules to smooth A-modules along f : R →+* A: the smooth part of the coextension of scalars Hom_R(A, V), which is the module of continuous R-linear maps A → V when the J i form a basis of neighborhoods of 0 (TauCeti.mem_smoothPart_coextendScalars_iff_continuous).

@[simp]

theorem TauCeti.coinduction_obj_obj {R : Type u₁} {A : Type u} [Ring R] [Ring A] (f : R →+* A) {ι : Type u_1} {J : ι → Submodule A A} [Nonempty ι] (hJ : Directed (fun (x1 x2 : Submodule A A) => x1 ≥ x2) J) (V : ModuleCat R) : ((coinduction f hJ).obj V).obj = ↧↥(smoothPart J ↑((ModuleCat.coextendScalars f).obj V))

The coinduction of V is the smooth part of the coextension of scalars of V.

theorem TauCeti.coinduction_map_hom_apply {R : Type u₁} {A : Type u} [Ring R] [Ring A] (f : R →+* A) {ι : Type u_1} {J : ι → Submodule A A} [Nonempty ι] (hJ : Directed (fun (x1 x2 : Submodule A A) => x1 ≥ x2) J) {V W : ModuleCat R} (φ : V ⟶ W) (g : ↥(smoothPart J ↑((ModuleCat.coextendScalars f).obj V))) (a : A) : ((ModuleCat.CoextendScalars.equiv f W) ↑((ModuleCat.Hom.hom ((coinduction f hJ).map φ).hom) g)) a = (CategoryTheory.ConcreteCategory.hom φ) (((ModuleCat.CoextendScalars.equiv f V) ↑g) a)

The coinduction of a linear map φ is postcomposition with φ.

noncomputable def TauCeti.coinductionAdjunction {R : Type u₁} {A : Type u} [Ring R] [Ring A] (f : R →+* A) {ι : Type u_1} {J : ι → Submodule A A} [Nonempty ι] (hJ : Directed (fun (x1 x2 : Submodule A A) => x1 ≥ x2) J) : (smoothModules J).ι.comp (ModuleCat.restrictScalars f) ⊣ coinduction f hJ

The underlying R-module functor of smooth A-modules is left adjoint to the coinduction: R-linear maps from a smooth A-module M to V are the A-linear maps from M to the smooth part of the coextension of scalars Hom_R(A, V), which is the module of continuous R-linear maps A → V when the J i form a basis of neighborhoods of 0.

theorem TauCeti.coinductionAdjunction_unit_app_apply {R : Type u₁} {A : Type u} [Ring R] [Ring A] (f : R →+* A) {ι : Type u_1} {J : ι → Submodule A A} [Nonempty ι] (hJ : Directed (fun (x1 x2 : Submodule A A) => x1 ≥ x2) J) (M : (smoothModules J).FullSubcategory) (m : ↑M.obj) (a : A) : ((ModuleCat.CoextendScalars.equiv f (((smoothModules J).ι.comp (ModuleCat.restrictScalars f)).obj M)) ↑((ModuleCat.Hom.hom ((coinductionAdjunction f hJ).unit.app M).hom) m)) a = a • m

The unit of the coinduction adjunction sends m to the orbit map a ↦ a • m.

theorem TauCeti.coinductionAdjunction_counit_app_apply {R : Type u₁} {A : Type u} [Ring R] [Ring A] (f : R →+* A) {ι : Type u_1} {J : ι → Submodule A A} [Nonempty ι] (hJ : Directed (fun (x1 x2 : Submodule A A) => x1 ≥ x2) J) (V : ModuleCat R) (g : ↥(smoothPart J ↑((ModuleCat.coextendScalars f).obj V))) : (ModuleCat.Hom.hom ((coinductionAdjunction f hJ).counit.app V)) g = ((ModuleCat.CoextendScalars.equiv f V) ↑g) 1

The counit of the coinduction adjunction is evaluation at 1.

theorem TauCeti.coinductionAdjunction_homEquiv_apply_apply {R : Type u₁} {A : Type u} [Ring R] [Ring A] (f : R →+* A) {ι : Type u_1} {J : ι → Submodule A A} [Nonempty ι] (hJ : Directed (fun (x1 x2 : Submodule A A) => x1 ≥ x2) J) {M : (smoothModules J).FullSubcategory} {V : ModuleCat R} (φ : ((smoothModules J).ι.comp (ModuleCat.restrictScalars f)).obj M ⟶ V) (m : ↑M.obj) (a : A) : ((ModuleCat.CoextendScalars.equiv f V) ↑((ModuleCat.Hom.hom (((coinductionAdjunction f hJ).homEquiv M V) φ).hom) m)) a = (ModuleCat.Hom.hom φ) (a • m)

The A-linear map to the coinduction corresponding to an R-linear map φ : M → V sends m to a ↦ φ (a • m).

theorem TauCeti.coinductionAdjunction_homEquiv_symm_apply {R : Type u₁} {A : Type u} [Ring R] [Ring A] (f : R →+* A) {ι : Type u_1} {J : ι → Submodule A A} [Nonempty ι] (hJ : Directed (fun (x1 x2 : Submodule A A) => x1 ≥ x2) J) {M : (smoothModules J).FullSubcategory} {V : ModuleCat R} (ψ : M ⟶ (coinduction f hJ).obj V) (m : ↑M.obj) : (ModuleCat.Hom.hom (((coinductionAdjunction f hJ).homEquiv M V).symm ψ)) m = ((ModuleCat.CoextendScalars.equiv f V) ↑((ModuleCat.Hom.hom ψ.hom) m)) 1

The R-linear map corresponding to an A-linear map ψ to the coinduction is evaluation of ψ at 1.

theorem TauCeti.coinductionAdjunction_unit_app_injective {R : Type u₁} {A : Type u} [Ring R] [Ring A] (f : R →+* A) {ι : Type u_1} {J : ι → Submodule A A} [Nonempty ι] (hJ : Directed (fun (x1 x2 : Submodule A A) => x1 ≥ x2) J) (M : (smoothModules J).FullSubcategory) : Function.Injective ⇑(ModuleCat.Hom.hom ((coinductionAdjunction f hJ).unit.app M).hom)

The unit m ↦ (a ↦ a • m) of the coinduction adjunction is injective, by evaluation at 1.

theorem TauCeti.injective_coinduction_obj {R : Type u₁} {A : Type u} [Ring R] [Ring A] (f : R →+* A) {ι : Type u_1} {J : ι → Submodule A A} [Nonempty ι] (hJ : Directed (fun (x1 x2 : Submodule A A) => x1 ≥ x2) J) (V : ModuleCat R) (hV : CategoryTheory.Injective V) : CategoryTheory.Injective ((coinduction f hJ).obj V)

Coinduction sends injective R-modules to injective smooth A-modules, since its left adjoint, the underlying R-module functor, preserves monomorphisms.

theorem TauCeti.injective_coinduction_obj_of_isSemisimpleRing {R : Type u₁} {A : Type u} [Ring R] [Ring A] (f : R →+* A) {ι : Type u_1} {J : ι → Submodule A A} [Nonempty ι] [IsSemisimpleRing R] (hJ : Directed (fun (x1 x2 : Submodule A A) => x1 ≥ x2) J) (V : ModuleCat R) : CategoryTheory.Injective ((coinduction f hJ).obj V)

Over a semisimple ring R, for instance a field, every R-module is injective, so the coinduction of every R-module is an injective smooth A-module.

Enough injectives and Ext

theorem TauCeti.enoughInjectives_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) : CategoryTheory.EnoughInjectives (smoothModules J).FullSubcategory

For a directed family J of left ideals of A : Type u, the smooth A-modules in universe max u w have enough injectives: every smooth module embeds, through the unit of the coinduction adjunction along ℤ →+* A, into the coinduction of an injective abelian group.

theorem TauCeti.hasExt_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) [CategoryTheory.Abelian (smoothModules J).FullSubcategory] : CategoryTheory.HasExt (smoothModules J).FullSubcategory

For a directed family J of left ideals of A : Type u, the abelian category of smooth A-modules in universe max u w has Ext groups in the universe max u w of its morphisms. This holds for any abelian structure on the smooth modules, for instance the one inherited from ModuleCat A through TauCeti.isClosedUnderFiniteLimits_smoothModules.

instance TauCeti.hasExt_discreteModules {A : Type u} [Ring A] [TopologicalSpace A] [SeparatelyContinuousAdd A] : CategoryTheory.HasExt (discreteModules A).FullSubcategory

Discrete modules over a topological ring with separately continuous addition have native Ext groups in the universe of their morphisms. They are the smooth modules for all open left ideals, a nonempty family directed by intersection.