English
The free construction is functorial; given a morphism f : X → Y in TopCat, there is a corresponding map freeObj R X → freeObj R Y in TopModuleCat R.
Русский
Свободная конструкция является функторной; для отображения f: X → Y в TopCat существует соответствующее отображение freeObj R X → freeObj R Y в TopModuleCat R.
LaTeX
$$$\\mathrm{freeMap}(f) : \\mathrm{freeObj}(R,X) \\to \\mathrm{freeObj}(R,Y)$$$
Lean4
/-- The free topological module over a topological space is functorial. -/
noncomputable def freeMap {X Y : TopCat.{v}} (f : X ⟶ Y) : freeObj R X ⟶ freeObj R Y :=
ConcreteCategory.ofHom
⟨Finsupp.lmapDomain _ _ f.hom, by
rw [continuous_iff_coinduced_le]
refine le_sInf fun (τ : TopologicalSpace (_ →₀ R)) ⟨hτ₁, hτ₂, hτ₃⟩ ↦ ?_
rw [coinduced_le_iff_le_induced]
refine
sInf_le
⟨continuousSMul_induced (Finsupp.lmapDomain _ _ f.hom), continuousAdd_induced (Finsupp.lmapDomain _ _ f.hom),
?_⟩
rw [← coinduced_le_iff_le_induced]
grw [← hτ₃, ← coinduced_mono (continuous_iff_coinduced_le.mp f.hom.2)]
rw [coinduced_compose, coinduced_compose]
congr! 1
ext x
simp [coe_freeObj]⟩
