ringEquivEndForget₂ — Mathlib

English

An ingredient of Tannaka duality: the ring R is canonically isomorphic to the endomorphism ring of the additive forgetful functor from modules to abelian groups.

Русский

Часть теоремы Таннаки: кольцо R канонически изоморфно кольцу концевых 自-образований аддитивного функторa забывания модулей к абелевым группам.

LaTeX

$$$R \cong \mathrm{End}(\mathrm{Forget}_R)\quad\text{as rings}$$$

Lean4

/-- An ingredient of 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 ≃+* End (AdditiveFunctor.of (forget₂ (ModuleCat.{u} R) AddCommGrpCat.{u}))
    where
  toFun r := { app := fun M => @AddCommGrpCat.ofHom M.carrier M.carrier _ _ (DistribMulAction.toAddMonoidHom M r) }
  invFun φ := φ.app (ModuleCat.of R R) (1 : R)
  left_inv := by
    intro r
    simp
  right_inv := by
    intro φ
    apply NatTrans.ext
    ext M (x : M)
    have w := CategoryTheory.congr_fun (φ.naturality (ModuleCat.ofHom (LinearMap.toSpanSingleton R M x))) (1 : R)
    exact w.symm.trans (congr_arg (φ.app M) (one_smul R x))
  map_add' := by
    intros
    apply NatTrans.ext
    ext
    simp only [AdditiveFunctor.of_fst, ModuleCat.forget₂_obj, DistribMulAction.toAddMonoidHom_apply, add_smul,
      AddCommGrpCat.hom_ofHom]
    rfl
  map_mul' := by
    intros
    apply NatTrans.ext
    ext
    simp only [AdditiveFunctor.of_fst, ModuleCat.forget₂_obj, DistribMulAction.toAddMonoidHom_apply, mul_smul,
      AddCommGrpCat.hom_ofHom]
    rfl

Похожие утверждения