Continuous maps on a one-point compactification vanishing at infinity

Let S be a discrete space. A finitely supported function S →₀ M into a topological space M with a zero extends by 0 at ∞ to a continuous map on the one-point compactification S⁺ of S, since it is eventually 0 along the cofinite filter. When M is a discrete topological module, conversely, a continuous map S⁺ → M that vanishes at ∞ is determined by its values on S, and these values form a finitely supported function: continuity at ∞ says that all but finitely many of them are 0. The two constructions are the mutually inverse linear maps of TauCeti.OnePoint.finsuppLinearEquivKerEvalInfty, an isomorphism between S →₀ M and the kernel of evaluation at ∞ on C(S⁺, M).

Main definitions

• TauCeti.OnePoint.continuousMapOfFinsupp: the extension by 0 at ∞ of a finitely supported function on a discrete space, as a continuous map on the one-point compactification, for any topological codomain.
• TauCeti.OnePoint.finsuppLinearEquivKerEvalInfty: the linear isomorphism between S →₀ M and the continuous maps S⁺ → M vanishing at ∞, for S and M discrete.

theorem TauCeti.OnePoint.finite_setOf_apply_coe_ne_apply_infty {S : Type u} [TopologicalSpace S] [DiscreteTopology S] {Y : Type u_1} [TopologicalSpace Y] [DiscreteTopology Y] (f : C(OnePoint S, Y)) : {s : S | f ↑s ≠ f OnePoint.infty}.Finite

A continuous map from the one-point compactification of a discrete space to a discrete space takes the value f ∞ at all but finitely many points of S.

noncomputable def TauCeti.OnePoint.continuousMapOfFinsupp {S : Type u} [TopologicalSpace S] [DiscreteTopology S] (M : Type v) [Zero M] [TopologicalSpace M] (g : S →₀ M) : C(OnePoint S, M)

A finitely supported function S →₀ M is eventually 0 along the cofinite filter, so its extension by 0 at ∞ is continuous on the one-point compactification of the discrete space S, whatever the topology of M.

Equations

• TauCeti.OnePoint.continuousMapOfFinsupp M g = OnePoint.continuousMapMkDiscrete (⇑g) 0 ⋯

@[simp]

theorem TauCeti.OnePoint.continuousMapOfFinsupp_apply_coe {S : Type u} [TopologicalSpace S] [DiscreteTopology S] (M : Type v) [Zero M] [TopologicalSpace M] (g : S →₀ M) (s : S) : (continuousMapOfFinsupp M g) ↑s = g s

@[simp]

theorem TauCeti.OnePoint.continuousMapOfFinsupp_apply_infty {S : Type u} [TopologicalSpace S] [DiscreteTopology S] (M : Type v) [Zero M] [TopologicalSpace M] (g : S →₀ M) : (continuousMapOfFinsupp M g) OnePoint.infty = 0

noncomputable def TauCeti.OnePoint.finsuppLinearEquivKerEvalInfty (S : Type u) [TopologicalSpace S] [DiscreteTopology S] (R : Type u_1) [Semiring R] (M : Type v) [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] [Module R M] [ContinuousConstSMul R M] [DiscreteTopology M] : (S →₀ M) ≃ₗ[R] ↥(↑(ContinuousMap.evalCLM R OnePoint.infty)).ker

Continuous maps vanishing at infinity are finitely supported functions. For a discrete space S and a discrete topological module M, restriction to S identifies the continuous maps S⁺ → M vanishing at ∞ with the finitely supported functions S →₀ M, as R-modules. The inverse extends a finitely supported function by 0 at ∞.

Equations

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

@[simp]

theorem TauCeti.OnePoint.coe_finsuppLinearEquivKerEvalInfty_apply (S : Type u) [TopologicalSpace S] [DiscreteTopology S] (R : Type u_1) [Semiring R] (M : Type v) [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] [Module R M] [ContinuousConstSMul R M] [DiscreteTopology M] (g : S →₀ M) : ↑((finsuppLinearEquivKerEvalInfty S R M) g) = continuousMapOfFinsupp M g

@[simp]

theorem TauCeti.OnePoint.finsuppLinearEquivKerEvalInfty_symm_apply (S : Type u) [TopologicalSpace S] [DiscreteTopology S] (R : Type u_1) [Semiring R] (M : Type v) [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] [Module R M] [ContinuousConstSMul R M] [DiscreteTopology M] (f : ↥(↑(ContinuousMap.evalCLM R OnePoint.infty)).ker) (s : S) : ((finsuppLinearEquivKerEvalInfty S R M).symm f) s = ↑f ↑s