indiscreteAdj — Mathlib

English

The various adjunctions between TopModuleCat, TopCat, and ModuleCat are compatible via the forgetful functors.

Русский

Различные сопряжения между TopModuleCat, TopCat и ModuleCat совместимы через забывающие функторы.

LaTeX

$$$(withModuleTopology ⊣ forget₂) \\text{ and } (indiscrete ⊣ forget₂)$ are compatible$$

Lean4

/-- The adjunction between the forgetful functor and the indiscrete topology functor. -/
def indiscreteAdj : forget₂ (TopModuleCat.{v} R) (ModuleCat.{v} R) ⊣ indiscrete.{v} R
    where
  counit := 𝟙 _
  unit :=
    { app X := ConcreteCategory.ofHom (C := TopModuleCat R) ⟨.id, by rw [continuous_iff_coinduced_le]; exact le_top⟩ }

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