withModuleTopologyAdj — Mathlib

English

There is an adjunction between withModuleTopology and forget₂ (TopModuleCat R) ⟶ ModuleCat R.

Русский

Существуют сопряжения между withModuleTopology и forget₂ (TopModuleCat R) ⟶ ModuleCat R.

LaTeX

$$$\\text{withModuleTopology} \\dashv \\text{forget₂}$$$

Lean4

/-- The adjunction between `withModuleTopology` and the forgetful functor. -/
def withModuleTopologyAdj : withModuleTopology R ⊣ forget₂ (TopModuleCat R) (ModuleCat R)
    where
  unit := 𝟙 _
  counit :=
    { app X := ofHom (X := (withModuleTopology R).obj (.of R X)) ⟨.id, IsModuleTopology.continuous_of_linearMap _⟩ }

Похожие утверждения