English
If A is finite as an R-module, then every bilinear map bil : A → B → C is continuous as a function on A × B.
Русский
Если A конечно по отношению к модулю над R, то вся билинейная карта bil: A × B → C непрерывна на A × B.
LaTeX
$$$\\text{If } \\text{Module.Finite}(R,A) \\text{ and } bil: A \\to\\! B \\to C,\\;\\ bil\\;\\text{is continuous on } A \\times B.$$$
Lean4
/-- If `A`, `B` and `C` have the module topology, and if furthermore `A` is a finite `R`-module,
then any bilinear map `A × B → C` is automatically continuous
-/
@[continuity, fun_prop]
theorem continuous_bilinear_of_finite_left [Module.Finite R A] (bil : A →ₗ[R] B →ₗ[R] C) :
Continuous (fun ab ↦ bil ab.1 ab.2 : (A × B → C)) := by
-- `A` is finite and hence admits a surjection from `Rⁿ` for some finite `n`.
obtain ⟨m, f, hf⟩ := Module.Finite.exists_fin' R A
let bil' : (Fin m → R) →ₗ[R] B →ₗ[R] C := bil.comp f
let φ := f.prodMap (LinearMap.id : B →ₗ[R] B)
have hφ : Function.Surjective φ :=
Function.Surjective.prodMap hf fun b ↦
⟨b, rfl⟩
-- ... and thus a quotient map, so it suffices to prove that the composite `Rⁿ × B → C` is
-- continuous.
rw [Topology.IsQuotientMap.continuous_iff (isQuotientMap_of_surjective hφ)]
-- But this follows from an earlier result.
exact continuous_bilinear_of_pi_fintype (Fin m) bil'
