Bounded bilinear maps and bounded scalar actions over a normed ring

Over a seminormed commutative ring R, which need not be a field, an R-bilinear map β with ‖β x y‖ ≤ C * ‖x‖ * ‖y‖ is jointly continuous (LinearMap.continuous₂_of_bound), and so is a scalar action with ‖r • m‖ ≤ C * ‖r‖ * ‖m‖ (TauCeti.continuousSMul_of_norm_smul_le). For an R-algebra S, such a bound on the action makes the structure map bounded (TauCeti.exists_norm_algebraMap_le_of_norm_smul_le).

A fibrewise linear change of coordinates (x, v) ↦ (x, e x v), with e continuous at a, tends to (a, 0) at (a, 0) (ContinuousAt.tendsto_prodMk_clm_apply).

theorem LinearMap.continuous₂_of_bound {R : Type u_1} [SeminormedCommRing R] {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [SeminormedAddCommGroup X] [Module R X] [SeminormedAddCommGroup Y] [Module R Y] [SeminormedAddCommGroup Z] [Module R Z] (β : X →ₗ[R] Y →ₗ[R] Z) (C : ℝ) (hβ : ∀ (x : X) (y : Y), ‖(β x) y‖ ≤ C * ‖x‖ * ‖y‖) : Continuous fun (p : X × Y) => (β p.1) p.2

An R-bilinear map bounded by C * ‖x‖ * ‖y‖ is jointly continuous.

theorem TauCeti.continuousSMul_of_norm_smul_le {R : Type u_1} [SeminormedCommRing R] {M : Type u_2} [SeminormedAddCommGroup M] [Module R M] (h : ∃ (C : NNReal), ∀ (r : R) (m : M), ‖r • m‖ ≤ ↑C * ‖r‖ * ‖m‖) : ContinuousSMul R M

A scalar action bounded by C * ‖r‖ * ‖m‖ is continuous.

theorem TauCeti.exists_norm_algebraMap_le_of_norm_smul_le {R : Type u_1} [SeminormedCommRing R] {S : Type u_2} [SeminormedRing S] [Algebra R S] (h : ∃ (C : NNReal), ∀ (r : R) (s : S), ‖r • s‖ ≤ ↑C * ‖r‖ * ‖s‖) : ∃ (C : NNReal), ∀ (r : R), ‖(algebraMap R S) r‖ ≤ ↑C * ‖r‖

If the action of R on an R-algebra S is bounded, ‖r • s‖ ≤ C * ‖r‖ * ‖s‖, then so is the structure map: ‖algebraMap R S r‖ ≤ C * ‖1‖ * ‖r‖.

theorem ContinuousAt.tendsto_prodMk_clm_apply {𝕜 : Type u_2} {X : Type u_3} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [TopologicalSpace X] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {e : X → E →L[𝕜] F} {a : X} (he : ContinuousAt e a) : Filter.Tendsto (fun (z : X × E) => (z.1, (e z.1) z.2)) (nhds (a, 0)) (nhds (a, 0))

A fibrewise linear change of coordinates (x, v) ↦ (x, e x v), with e continuous at a, tends to (a, 0) at (a, 0).