Tannaka duality for rings

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

def ringEquivEndForget₂ (R : Type u) [Ring R] : R ≃+* CategoryTheory.End (CategoryTheory.AdditiveFunctor.of (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat))

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

Equations

• One or more equations did not get rendered due to their size.