English
There is an adjunction monoidAlgebra R ⊣ Under.forget R ⋙ forget₂ _ _ between CommRingCat and Under.
Русский
Существует адъюнкция monoidAlgebra R ⊣ Under.forget R ⋙ forget₂ _ _ между CommRingCat и Under.
LaTeX
$$$\text{monoidAlgebraAdj } R : \text{monoidAlgebra } R \dashv Under.forget R \circ forget₂$$$
Lean4
/-- The adjunction `G ↦ R[G]` and `S ↦ Sˣ` between `CommGrpCat` and `R-Alg`. -/
def monoidAlgebraAdj (R : CommRingCat.{u}) : monoidAlgebra R ⊣ Under.forget R ⋙ forget₂ _ _
where
unit := { app G := CommMonCat.ofHom (MonoidAlgebra.of R G) }
counit :=
{
app
S :=
Under.homMk (CommRingCat.ofHom (MonoidAlgebra.liftNCRingHom S.hom.hom (.id _) fun _ _ ↦ .all _ _))
(by ext; simp [MonoidAlgebra.liftNCRingHom]),
naturality S T
f := by
ext : 2
apply MonoidAlgebra.ringHom_ext <;> intro <;> simp [MonoidAlgebra.liftNCRingHom, ← Under.w f, -Under.w] }
left_triangle_components
G := by
ext : 2
apply MonoidAlgebra.ringHom_ext <;> intro <;> simp [MonoidAlgebra.liftNCRingHom]
right_triangle_components S := by dsimp; ext; simp [MonoidAlgebra.liftNCRingHom]
