mathlib3 documentation

algebra.category.Module.tannaka

Tannaka duality for rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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

Equations