Theorems · Definition · category theory
ModuleCat.extendRestrictScalarsAdj
{R : Type u₁} →
{S : Type u₂} →
[inst : CommRing R] →
[inst_1 : CommRing S] → (f : R →+* S) → ModuleCat.extendScalars f ⊣ ModuleCat.restrictScalars fGiven commutative rings R, S and a ring hom f : R →+* S, the extension and restriction of
scalars by f are adjoint to each other.
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- RingHomstatement and proof · cited by 10,189
- ModuleCatstatement and proof · cited by 1,429
- CategoryTheory.Adjunctionstatement · cited by 524
- ModuleCat.restrictScalarsstatement · cited by 148
- ModuleCat.extendScalarsstatement · cited by 39
- CategoryTheory.Adjunction.mk'proof · cited by 7
- ModuleCat.ExtendRestrictScalarsAdj.counitproof · cited by 1
- ModuleCat.ExtendRestrictScalarsAdj.homEquivproof · cited by 1
- ModuleCat.ExtendRestrictScalarsAdj.unitproof · cited by 1
Cited by10
Results whose statement or proof uses this declaration.
- ModuleCat.extendScalarsCompproof · cited by 10
- ModuleCat.extendScalarsIdproof · cited by 8
- ModuleCat.extendRestrictScalarsAdj_homEquiv_applystatement · cited by 5
- ModuleCat.extendScalarsComp_hom_app_one_tmulproof · cited by 3
- ModuleCat.extendRestrictScalarsAdj_counit_app_apply_one_tmulstatement · cited by 1
- ModuleCat.homEquiv_extendScalarsIdstatement · cited by 1
- ModuleCat.homEquiv_extendScalarsCompstatement and proof · cited by 1
- ModuleCat.extendRestrictScalarsAdj_unit_app_applystatement · cited by 0
- comonadicExtendScalarsproof · cited by 0
- ModuleCat.restrictScalars_μ_tmulproof · cited by 0