Theorems · Definition · commutative algebra
CommRingCat.KaehlerDifferential.map
{A B A' B' : CommRingCat} →
{f : A ⟶ B} →
{f' : A' ⟶ B'} →
{g : A ⟶ A'} →
{g' : B ⟶ B'} →
CategoryTheory.CategoryStruct.comp g f' = CategoryTheory.CategoryStruct.comp f g' →
(CommRingCat.KaehlerDifferential f ⟶
(ModuleCat.restrictScalars (CommRingCat.Hom.hom g')).obj (CommRingCat.KaehlerDifferential f'))The map KaehlerDifferential f ⟶ (ModuleCat.restrictScalars g').obj (KaehlerDifferential f')
induced by a commutative square (given by an equality g ≫ f' = f ≫ g')
in the category CommRingCat.
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.Functor.objstatement · cited by 19,642
- CategoryTheory.CategoryStruct.compstatement and proof · cited by 17,999
- IsScalarTowerproof · cited by 3,896
- CommRingCatstatement and proof · cited by 2,333
- ModuleCatstatement · cited by 1,429
- CommRingCat.carrierstatement and proof · cited by 1,096
- CommRingCat.Hom.homstatement · cited by 432
- KaehlerDifferentialproof · cited by 204
- ModuleCat.ofHomproof · cited by 200
- ModuleCat.restrictScalarsstatement · cited by 148
Cited by4
Results whose statement or proof uses this declaration.
- PresheafOfModules.DifferentialsConstruction.relativeDifferentials'proof · cited by 3
- CommRingCat.KaehlerDifferential.map_dstatement · cited by 1
- CommRingCat.KaehlerDifferential.map.congr_simpstatement and proof · cited by 0
- PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_mapstatement · cited by 0