Theorems · Definition · category theory

ModuleCat.monModuleEquivalenceAlgebraForget

{R : Type u} →
  [inst : CommRing R] →
    ModuleCat.MonModuleEquivalenceAlgebra.functor.comp (CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)) ≅
      CategoryTheory.Mon.forget (ModuleCat R)

The equivalence Mon (ModuleCat R) ≌ AlgCat R is naturally compatible with the forgetful functors to ModuleCat R.

Defined in: Mathlib.CategoryTheory.Monoidal.Internal.Module
Cited by: 0 results in Mathlib
Foundations: Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites17

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

RingHom.idstatement · cited by 18,349
CommRingstatement and proof · cited by 17,173
CategoryTheory.Functorstatement · cited by 16,252
LinearMapstatement · cited by 10,215
CategoryTheory.Functor.compstatement · cited by 6,529
CategoryTheory.Isostatement · cited by 3,963
AlgHomstatement · cited by 3,236
ModuleCatstatement and proof · cited by 1,429
ModuleCat.carrierstatement · cited by 997
CategoryTheory.Monstatement and proof · cited by 465
CategoryTheory.forget₂statement · cited by 260
ModuleCat.ofHomproof · cited by 200

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.