Theorems · Theorem · commutative algebra
CommRingCat.KaehlerDifferential.map_d
∀ {A B A' B' : CommRingCat} {f : A ⟶ B} {f' : A' ⟶ B'} {g : A ⟶ A'} {g' : B ⟶ B'}
(fac : CategoryTheory.CategoryStruct.comp g f' = CategoryTheory.CategoryStruct.comp f g') (b : ↑B),
(CategoryTheory.ConcreteCategory.hom (CommRingCat.KaehlerDifferential.map fac))
(CommRingCat.KaehlerDifferential.d b) =
CommRingCat.KaehlerDifferential.d ((CategoryTheory.ConcreteCategory.hom g') b)- Cited by
- 1 results in Mathlib
- Foundations
- Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites24
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.Functor.objstatement · cited by 19,642
- RingHom.idstatement · cited by 18,349
- CategoryTheory.CategoryStruct.compstatement and proof · cited by 17,999
- Algebraproof · cited by 11,388
- LinearMapstatement · cited by 10,215
- RingHomstatement · cited by 10,189
- Algebra.algebraMapproof · cited by 4,706
- CategoryTheory.ConcreteCategory.homstatement · cited by 4,022
- IsScalarTowerproof · cited by 3,896
- CommRingCatstatement and proof · cited by 2,333
Cited by1
Results whose statement or proof uses this declaration.
- PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_map_dproof · cited by 0