Theorems · Theorem · category theory
ModuleCat.extendScalarsComp_hom_app_one_tmul
∀ {R₁ R₂ R₃ : Type u₁} [inst : CommRing R₁] [inst_1 : CommRing R₂] [inst_2 : CommRing R₃] (f₁₂ : R₁ →+* R₂)
(f₂₃ : R₂ →+* R₃) (M : ModuleCat R₁) (m : ↑M),
(CategoryTheory.ConcreteCategory.hom ((ModuleCat.extendScalarsComp f₁₂ f₂₃).hom.app M)) (1 ⊗ₜ[R₁] m) =
1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m)- Cited by
- 3 results in Mathlib
- Foundations
- Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites33
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Quiver.Homproof · cited by 32,603
- CategoryTheory.Functor.objstatement and proof · cited by 19,642
- RingHom.idstatement · cited by 18,349
- CategoryTheory.CategoryStruct.compproof · cited by 17,999
- CommRingstatement and proof · cited by 17,173
- CategoryTheory.Functorstatement · cited by 16,252
- LinearMapstatement · cited by 10,215
- RingHomstatement and proof · cited by 10,189
- CategoryTheory.Functor.mapproof · cited by 8,698
- CategoryTheory.Iso.homstatement and proof · cited by 7,684
- CategoryTheory.NatTrans.appstatement and proof · cited by 7,406
Cited by3
Results whose statement or proof uses this declaration.
- ModuleCat.extendScalars_id_compproof · cited by 1
- ModuleCat.extendScalars_assocproof · cited by 1
- ModuleCat.extendScalars_comp_idproof · cited by 1