Uniform approximation by products

We show that if X, Y are compact Hausdorff spaces with X profinite, then any continuous function on X × Y valued in a ring (with a uniform structure) can be uniformly approximated by finite sums of functions of the form f x * g y.

theorem ContinuousMap.exists_finite_sum_smul_approximation_of_mem_uniformity {X : Type u_1} {Y : Type u_2} {R : Type u_3} {V : Type u_4} [TopologicalSpace X] [TotallyDisconnectedSpace X] [T2Space X] [CompactSpace X] [TopologicalSpace Y] [CompactSpace Y] [AddCommGroup V] [UniformSpace V] [IsUniformAddGroup V] {S : Set (V × V)} [TopologicalSpace R] [MonoidWithZero R] [MulActionWithZero R V] (f : C(X × Y, V)) (hS : S ∈ uniformity V) : ∃ (n : ℕ) (g : Fin n → C(X, R)) (h : Fin n → C(Y, V)), ∀ (x : X) (y : Y), (f (x, y), ∑ i : Fin n, (g i) x • (h i) y) ∈ S

A continuous function on X × Y, taking values in an R-module with a uniform structure, can be uniformly approximated by sums of functions of the form (x, y) ↦ f x • g y.

Note that no continuity properties are assumed either for multiplication on R, or for the scalar multiplication of R on V.

theorem ContinuousMap.exists_finite_sum_mul_approximation_of_mem_uniformity {X : Type u_1} {Y : Type u_2} {R : Type u_3} [TopologicalSpace X] [TotallyDisconnectedSpace X] [T2Space X] [CompactSpace X] [TopologicalSpace Y] [CompactSpace Y] [Ring R] [UniformSpace R] [IsUniformAddGroup R] (f : C(X × Y, R)) {S : Set (R × R)} (hS : S ∈ uniformity R) : ∃ (n : ℕ) (g : Fin n → C(X, R)) (h : Fin n → C(Y, R)), ∀ (x : X) (y : Y), (f (x, y), ∑ i : Fin n, (g i) x * (h i) y) ∈ S

A continuous function on X × Y, taking values in a ring R equipped with a uniformity compatible with addition, can be uniformly approximated by sums of functions of the form (x, y) ↦ f x * g y.

Note that no assumption is needed relating the multiplication on R to the uniformity.

def ContinuousMap.prodMul {X : Type u_5} {Y : Type u_6} {R : Type u_7} [TopologicalSpace X] [TopologicalSpace Y] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] : C(X, R) →ₗ[R] C(Y, R) →ₗ[R] C(X × Y, R)

The natural bilinear map sending f, g to the function (x, y) ↦ f x * g y on X × Y.

Equations

• ContinuousMap.prodMul = LinearMap.mk₂ R (fun (f : C(X, R)) (g : C(Y, R)) => f.comp ContinuousMap.fst * g.comp ContinuousMap.snd) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem ContinuousMap.prodMul_apply {X : Type u_5} {Y : Type u_6} {R : Type u_7} [TopologicalSpace X] [TopologicalSpace Y] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] (f : C(X, R)) (g : C(Y, R)) (p : X × Y) : ((prodMul f) g) p = f p.1 * g p.2

theorem ContinuousMap.prodMul_def {X : Type u_5} {Y : Type u_6} {R : Type u_7} [TopologicalSpace X] [TopologicalSpace Y] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] (f : C(X, R)) (g : C(Y, R)) : (prodMul f) g = f.comp fst * g.comp snd

def ContinuousMap.tensorHom {X : Type u_5} {Y : Type u_6} {R : Type u_7} [TopologicalSpace X] [TopologicalSpace Y] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] : TensorProduct R C(X, R) C(Y, R) →ₗ[R] C(X × Y, R)

Tensor product version of ContinuousMap.prodMul.

Equations

• ContinuousMap.tensorHom = TensorProduct.lift ContinuousMap.prodMul

@[simp]

theorem ContinuousMap.tensorHom_tmul {X : Type u_5} {Y : Type u_6} {R : Type u_7} [TopologicalSpace X] [TopologicalSpace Y] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] (f : C(X, R)) (g : C(Y, R)) : tensorHom (f ⊗ₜ[R] g) = (prodMul f) g

theorem ContinuousMap.denseRange_tensorHom {X : Type u_5} {Y : Type u_6} {R : Type u_7} [TopologicalSpace X] [TopologicalSpace Y] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace X] [T2Space X] [CompactSpace Y] [T2Space Y] [TotallyDisconnectedSpace X] : DenseRange ⇑tensorHom