Continuous maps on a topological magma, and the coordinate embeddings of a product

Continuous-map constructions that use the multiplication of a topological magma, next to Mathlib's ContinuousMap.mulLeft and ContinuousMap.mulRight, and the convergence of the coordinate embeddings Pi.mulSingle of a product of pointed topological spaces, next to Mathlib's continuous_mulSingle.

Main definitions

• ContinuousMap.compSwapShearMulRight: the family x ↦ (y ↦ Ψ y (y * x)) attached to a two-variable continuous map Ψ, that is, Ψ precomposed with the coordinate swap followed by the shear (a, b) ↦ (a, a * b) of Homeomorph.shearMulRight, with ContinuousMap.compSwapShearMulRight_apply_apply its pointwise formula.

Main results

• TauCeti.tendsto_mulSingle_cofinite: in a product ∀ i, M i of pointed topological spaces, the elements Pi.mulSingle i (x i) supported at a single coordinate tend to 1 along the cofinite filter on the index type.

noncomputable def ContinuousMap.compSwapShearMulRight {X : Type u_1} [TopologicalSpace X] [Mul X] [ContinuousMul X] [LocallyCompactSpace X] {Z : Type u_2} [TopologicalSpace Z] (Ψ : C(X, C(X, Z))) : C(X, C(X, Z))

The family x ↦ (y ↦ Ψ y (y * x)) attached to a two-variable continuous map Ψ: the uncurried Ψ precomposed with the coordinate swap (x, y) ↦ (y, x) followed by the shear (a, b) ↦ (a, a * b) of Homeomorph.shearMulRight, curried again. Local compactness makes evaluation continuous, which is what makes the family jointly continuous.

Equations

• Ψ.compSwapShearMulRight = { toFun := fun (p : X × X) => (Ψ p.2) (p.2 * p.1), continuous_toFun := ⋯ }.curry

@[simp]

theorem ContinuousMap.compSwapShearMulRight_apply_apply {X : Type u_1} [TopologicalSpace X] [Mul X] [ContinuousMul X] [LocallyCompactSpace X] {Z : Type u_2} [TopologicalSpace Z] (Ψ : C(X, C(X, Z))) (x y : X) : (Ψ.compSwapShearMulRight x) y = (Ψ y) (y * x)

theorem TauCeti.tendsto_mulSingle_cofinite {ι : Type u_1} [DecidableEq ι] {M : ι → Type u_2} [(i : ι) → One (M i)] [(i : ι) → TopologicalSpace (M i)] (x : (i : ι) → M i) : Filter.Tendsto (fun (i : ι) => Pi.mulSingle i (x i)) Filter.cofinite (nhds 1)

The coordinate embeddings of a product tend to 1 along the cofinite filter. For any family x, the element Pi.mulSingle i (x i) of the product, supported at the single coordinate i, tends to 1 as i leaves every finite set.

theorem TauCeti.tendsto_single_cofinite {ι : Type u_1} [DecidableEq ι] {M : ι → Type u_2} [(i : ι) → Zero (M i)] [(i : ι) → TopologicalSpace (M i)] (x : (i : ι) → M i) : Filter.Tendsto (fun (i : ι) => Pi.single i (x i)) Filter.cofinite (nhds 0)

The coordinate embeddings of a product tend to 0 along the cofinite filter. For any family x, the element Pi.single i (x i) of the product, supported at the single coordinate i, tends to 0 as i leaves every finite set.