English
There is a concrete description of the left adjoint to the forgetful functor from TopModuleCat(R) to TopCat, given by freeAdj. It provides explicit unit and counit maps for the adjunction, exhibiting a canonical free-forgetful adjunction.
Русский
Существует явное описание левого сопряжённого к забывающему функтору из TopModuleCat(R) в TopCat, заданное как freeAdj. Оно задаёт явные единицы и сопряжения для строгости данного сопряжения.
LaTeX
$$$\text{freeAdj}: \text{free}(R) \dashv \text{forget}_{TopModuleCat(R) \to TopCat}.$$$
Lean4
/-- The free-forgetful adjoint for `TopModuleCat R`. -/
noncomputable def freeAdj : free.{max v u} R ⊣ forget₂ (TopModuleCat.{max v u} R) TopCat.{max v u}
where
unit :=
{ app X := TopCat.ofHom ⟨(Finsupp.single · 1), continuous_iff_coinduced_le.mpr (le_sInf fun _ h ↦ h.2.2)⟩,
naturality {X Y} f := by ext x; simp [freeMap_map] }
counit :=
{
app
X :=
ConcreteCategory.ofHom (C := TopModuleCat R)
⟨Finsupp.lift _ R X id, by
rw [continuous_iff_le_induced]
refine
sInf_le
⟨continuousSMul_induced (Finsupp.lift _ R X id), continuousAdd_induced (Finsupp.lift _ R X id), ?_⟩
rw [coinduced_le_iff_le_induced, induced_compose]
convert induced_id.symm.le
ext
simp [coe_freeObj]⟩,
naturality {X Y}
f := by
ext1
apply ContinuousLinearMap.coe_injective
refine Finsupp.lhom_ext' fun a ↦ LinearMap.ext_ring ?_
dsimp [freeObj, freeMap]
simp }
left_triangle_components
X := by
ext1
apply ContinuousLinearMap.coe_injective
refine Finsupp.lhom_ext' fun a ↦ LinearMap.ext_ring ?_
simp [freeMap, freeObj]
right_triangle_components
X := by
ext
simp [freeObj]
