adj — Mathlib

English

There is a free-forgetful adjunction between Type and Mod_R, with free left adjoint to forgetful right, describing the universal property of free modules.

Русский

Существует свободно-забывающий адъюнкт между множеством и Mod_R: свободный слева и забывающий справа, задающий универсальное свойство свободных модулей.

LaTeX

$$$\mathrm{free} \dashv \mathrm{forget}(\mathrm{ModuleCat}(R))$$$

Lean4

/-- The free-forgetful adjunction for R-modules.
-/
def adj : free R ⊣ forget (ModuleCat.{u} R) :=
  Adjunction.mkOfHomEquiv
    { homEquiv := fun _ _ => freeHomEquiv
      homEquiv_naturality_left_symm := fun {X Y M} f g ↦ by ext; simp [freeHomEquiv] }

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