The internal hom of topological modules

This file equips the category of topological modules with an internal hom TopModuleCat.linHom, the space of continuous linear maps carrying the topology induced from the compact-open topology, together with its functoriality (TopModuleCat.linHomMap) and a constructor (TopModuleCat.homOfBilinear) bundling a bilinear pairing with jointly continuous uncurried form into a morphism to the internal hom.

Material destined for Mathlib.Algebra.Category.ModuleCat.Topology.Basic.

@[reducible, inline]

abbrev TopModuleCat.linHom {k : Type u} [CommRing k] [TopologicalSpace k] (M1 M2 : TopModuleCat k) : TopModuleCat k

The internal hom of two topological modules: the space of continuous linear maps A →L[k] B carrying the topology induced from the compact-open topology on C(A, B).

Equations

• M1.linHom M2 = TopModuleCat.of k (↑M1.toModuleCat →L[k] ↑M2.toModuleCat)

def TopModuleCat.linHomMap {k : Type u} [CommRing k] [TopologicalSpace k] {A A' B B' : TopModuleCat k} (a : A' ⟶ A) (b : B ⟶ B') : A.linHom B ⟶ A'.linHom B'

Pre- and post-composition induce a morphism between the internal homs of topological modules.

Equations

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

@[simp]

theorem TopModuleCat.linHomMap_apply {k : Type u} [CommRing k] [TopologicalSpace k] {A A' B B' : TopModuleCat k} (a : A' ⟶ A) (b : B ⟶ B') (φ : ↑(A.linHom B).toModuleCat) (x : ↑A'.toModuleCat) : ((CategoryTheory.ConcreteCategory.hom (linHomMap a b)) φ) x = (Hom.hom b) (φ ((Hom.hom a) x))

def TopModuleCat.homOfBilinear {k : Type u} [CommRing k] [TopologicalSpace k] {A B C : TopModuleCat k} (F : ↑A.toModuleCat → ↑B.toModuleCat →L[k] ↑C.toModuleCat) (hadd : ∀ (a a' : ↑A.toModuleCat) (b : ↑B.toModuleCat), (F (a + a')) b = (F a) b + (F a') b) (hsmul : ∀ (c : k) (a : ↑A.toModuleCat) (b : ↑B.toModuleCat), (F (c • a)) b = c • (F a) b) (hF : Continuous fun (p : ↑A.toModuleCat × ↑B.toModuleCat) => (F p.1) p.2) : A ⟶ B.linHom C

Bundle a bilinear pairing with jointly continuous uncurried form into a morphism to the internal hom. Stating this for abstract topological modules keeps all instance searches on abstract carriers.

Equations

• TopModuleCat.homOfBilinear F hadd hsmul hF = TopModuleCat.ofHom { toFun := F, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem TopModuleCat.homOfBilinear_apply {k : Type u} [CommRing k] [TopologicalSpace k] {A B C : TopModuleCat k} (F : ↑A.toModuleCat → ↑B.toModuleCat →L[k] ↑C.toModuleCat) (hadd : ∀ (a a' : ↑A.toModuleCat) (b : ↑B.toModuleCat), (F (a + a')) b = (F a) b + (F a') b) (hsmul : ∀ (c : k) (a : ↑A.toModuleCat) (b : ↑B.toModuleCat), (F (c • a)) b = c • (F a) b) (hF : Continuous fun (p : ↑A.toModuleCat × ↑B.toModuleCat) => (F p.1) p.2) (a : ↑A.toModuleCat) : (CategoryTheory.ConcreteCategory.hom (homOfBilinear F hadd hsmul hF)) a = F a