Tannaka duality for rings

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

theorem CategoryTheory.End.ext_iff {C : Type u} [CategoryStruct.{v, u} C] {X : C} {x y : End X} : x = y ↔ x.asHom = y.asHom

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

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.