forget₂Adj — Mathlib

English

There is an adjunction forget₂ between CommRingCat and CommMonCat, provided by the initial object.

Русский

Существует адъюнкция forget₂ между CommRingCat и CommMonCat, задаваемая начальным объектом.

LaTeX

$$$\text{forget₂Adj} : \mathrm{CommRingCat} \dashv \mathrm{CommMonCat}$$$

Lean4

/-- The adjunction `G ↦ ℤ[G]` and `R ↦ Rˣ` between `CommGrpCat` and `CommRing`. -/
def forget₂Adj {R : CommRingCat.{u}} (hR : Limits.IsInitial R) : monoidAlgebra R ⋙ Under.forget R ⊣ forget₂ _ _ :=
  (monoidAlgebraAdj R).comp (Under.equivalenceOfIsInitial hR).toAdjunction

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