Theorems · Theorem · category theory

ModuleCat.extendScalars_id_comp_assoc

∀ {R₁ R₂ : Type u₁} [inst : CommRing R₁] [inst_1 : CommRing R₂] (f₁₂ : R₁ →+* R₂)
  {Z : CategoryTheory.Functor (ModuleCat R₁) (ModuleCat R₂)} (h : ModuleCat.extendScalars f₁₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (ModuleCat.extendScalarsComp (RingHom.id R₁) f₁₂).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (ModuleCat.extendScalarsId R₁).hom (ModuleCat.extendScalars f₁₂))
        (CategoryTheory.CategoryStruct.comp (ModuleCat.extendScalars f₁₂).leftUnitor.hom h)) =
    h

Defined in: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Cited by: 0 results in Mathlib
Foundations: Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing CommRing

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites19

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

Quiver.Homstatement and proof · cited by 32,603
RingHom.idstatement and proof · cited by 18,349
CategoryTheory.CategoryStruct.compstatement and proof · cited by 17,999
CommRingstatement and proof · cited by 17,173
CategoryTheory.Functorstatement and proof · cited by 16,252
RingHomstatement and proof · cited by 10,189
CategoryTheory.Iso.homstatement and proof · cited by 7,684
CategoryTheory.Functor.compstatement · cited by 6,529
CategoryTheory.Category.assocproof · cited by 6,433
CategoryTheory.Functor.idstatement · cited by 3,333
CategoryTheory.Category.id_compproof · cited by 1,998
ModuleCatstatement and proof · cited by 1,429

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.