# mathlibdocumentation

algebra.category.Module.tannaka

# Tannaka duality for rings #

A ring R is equivalent to the endomorphisms of the additive forgetful functor Module R ⥤ AddCommGroup.

def ring_equiv_End_forget₂ (R : Type u) [ring R] :

An ingredient of Tannaka duality for rings: A ring R is equivalent to the endomorphisms of the additive forgetful functor Module R ⥤ AddCommGroup.

Equations