Theorems · Definition · category theory
ModuleCat.restrictScalarsCongr
{R : Type u₁} →
{S : Type u₂} →
[inst : Ring R] →
[inst_1 : Ring S] → {f g : R →+* S} → f = g → (ModuleCat.restrictScalars f ≅ ModuleCat.restrictScalars g)Restrictions scalars along equal ring homomorphisms are naturally isomorphic.
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 35 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homproof · cited by 32,603
- CategoryTheory.Functor.objproof · cited by 19,642
- CategoryTheory.Functorstatement · cited by 16,252
- RingHomstatement and proof · cited by 10,189
- Ringstatement and proof · cited by 7,463
- CategoryTheory.Isostatement · cited by 3,963
- ModuleCatstatement and proof · cited by 1,429
- AddEquivproof · cited by 1,087
- ModuleCat.carrierproof · cited by 997
- Equiv.toFunproof · cited by 279
- CategoryTheory.NatIso.ofComponentsproof · cited by 178
- AddEquiv.toEquivproof · cited by 174
Cited by4
Results whose statement or proof uses this declaration.
- SheafOfModules.pushforwardCongrproof · cited by 9
- ModuleCat.restrictScalarsCongr_hom_appstatement · cited by 0
- ModuleCat.restrictScalarsCongr_inv_appstatement · cited by 0
- ModuleCat.restrictScalarsCongr_symmstatement · cited by 0