Theorems · Theorem · algebraic geometry
CommRingCat.KaehlerDifferential.map.congr_simp
∀ {A B A' B' : CommRingCat} {f : A ⟶ B} {f' : A' ⟶ B'} {g g_1 : A ⟶ A'} (e_g : g = g_1) {g' : B ⟶ B'}
(fac : CategoryTheory.CategoryStruct.comp g f' = CategoryTheory.CategoryStruct.comp f g'),
CommRingCat.KaehlerDifferential.map fac = CommRingCat.KaehlerDifferential.map ⋯- Cited by
- 0 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.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.Functor.objstatement · cited by 19,642
- CategoryTheory.CategoryStruct.compstatement and proof · cited by 17,999
- CommRingCatstatement and proof · cited by 2,333
- ModuleCatstatement · cited by 1,429
- CommRingCat.carrierstatement · cited by 1,096
- CommRingCat.Hom.homstatement · cited by 432
- ModuleCat.restrictScalarsstatement · cited by 148
- CommRingCat.KaehlerDifferentialstatement · cited by 8
- CommRingCat.KaehlerDifferential.mapstatement and proof · cited by 3
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.