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.

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

R ≃+* category_theory.End (category_theory.AdditiveFunctor.of (category_theory.forget₂ (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

ring_equiv_End_forget₂ R = {to_fun := λ (r : R), {app := λ (M : Module R), distrib_mul_action.to_add_monoid_hom ↥M r, naturality' := _}, inv_fun := λ (φ : category_theory.End (category_theory.AdditiveFunctor.of (category_theory.forget₂ (Module R) AddCommGroup))), ⇑(φ.app (Module.of R R)) 1, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}