English
If ι is finite, and B, C are R-modules with the module topology, then any bilinear map (ι → R) × B → C is continuous.
Русский
Если ι конечен, и B, C — R-модули с модульной топологией, то любая билинейная карта (ι → R) × B → C непрерывна.
LaTeX
$$$Continuous\_bilinear\_of\_pi\_fintype(ι, bil)$$$
Lean4
/-- If `n` is finite and `B`,`C` are `R`-modules with the module topology,
then any bilinear map `Rⁿ × B → C` is automatically continuous.
Note that whilst this result works for semirings, for rings this result is superseded
by `IsModuleTopology.continuous_bilinear_of_finite_left`.
-/
theorem continuous_bilinear_of_pi_fintype (ι : Type*) [Finite ι] (bil : (ι → R) →ₗ[R] B →ₗ[R] C) :
Continuous (fun ab ↦ bil ab.1 ab.2 : ((ι → R) × B → C)) := by
classical
cases nonempty_fintype ι
have h :
(fun fb ↦ bil fb.1 fb.2 : ((ι → R) × B → C)) = (fun fb ↦ ∑ i, ((fb.1 i) • (bil (Finsupp.single i 1) fb.2) : C)) :=
by
ext ⟨f, b⟩
nth_rw 1 [← Finset.univ_sum_single f]
simp_rw [← Finsupp.single_eq_pi_single, map_sum, LinearMap.coeFn_sum, Finset.sum_apply]
refine Finset.sum_congr rfl (fun x _ ↦ ?_)
rw [← Finsupp.smul_single_one]
push_cast
simp
rw [h]
-- But this map is obviously continuous, because for a fixed `i`, `bil (single i 1)` is
-- linear and thus continuous, and scalar multiplication and finite sums are continuous
haveI : ContinuousAdd C := toContinuousAdd R C
fun_prop
