Documentation Verification Report

Basic

📁 Source: Mathlib/Algebra/Category/ModuleCat/Differentials/Basic.lean

Statistics

Metric	Count
Definitions `KaehlerDifferential`, `D`, `d`, `map`, `d`, `desc`, `mk`	7
Theorems `ext`, `ext_iff`, `map_d`, `d_add`, `d_map`, `d_mul`, `desc_d`	7
Total	14

CommRingCat

Definitions

Name	Category	Theorems
`KaehlerDifferential` 📖	CompOp	5 math math: `KaehlerDifferential.map_d`, `ModuleCat.Derivation.desc_d`, `PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_map_d`, `PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_obj`, `KaehlerDifferential.ext_iff`

CommRingCat.KaehlerDifferential

Definitions

Name	Category	Theorems
`D` 📖	CompOp	—
`d` 📖	CompOp	4 math math: `map_d`, `ModuleCat.Derivation.desc_d`, `PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_map_d`, `ext_iff`
`map` 📖	CompOp	2 math math: `map_d`, `PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`DFunLike.coe` `CommRingCat.KaehlerDifferential` `ModuleCat.carrier` `CommRingCat.carrier` `CommRing.toRing` `CommRingCat.commRing` `CategoryTheory.ConcreteCategory.hom` `ModuleCat` `ModuleCat.moduleCategory` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `d`	—	—	`sub_eq_zero` `Algebra.to_smulCommClass` `smulCommClass_self` `KaehlerDifferential.span_range_derivation` `Submodule.span_le` `SetLike.mem_coe` `LinearMap.mem_ker` `ModuleCat.hom_sub` `LinearMap.sub_apply` `ModuleCat.hom_ext` `LinearMap.ker_eq_top` `top_le_iff`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `CommRingCat.KaehlerDifferential` `ModuleCat.carrier` `CommRingCat.carrier` `CommRing.toRing` `CommRingCat.commRing` `CategoryTheory.ConcreteCategory.hom` `ModuleCat` `ModuleCat.moduleCategory` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `d`	—	`ext`
`map_d` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CommRingCat` `CategoryTheory.Category.toCategoryStruct` `CommRingCat.instCategory`	`DFunLike.coe` `CommRingCat.KaehlerDifferential` `CategoryTheory.Functor.obj` `ModuleCat` `CommRingCat.carrier` `CommRing.toRing` `CommRingCat.commRing` `ModuleCat.moduleCategory` `ModuleCat.restrictScalars` `CommRingCat.Hom.hom` `ModuleCat.carrier` `CategoryTheory.ConcreteCategory.hom` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `map` `d` `RingHom` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier`	—	`IsScalarTower.of_algebraMap_eq'` `KaehlerDifferential.map_D` `IsScalarTower.of_compHom` `SMulCommClass.of_commMonoid` `IsScalarTower.right`

ModuleCat.Derivation

Definitions

Name	Category	Theorems
`d` 📖	CompOp	5 math math: `d_mul`, `desc_d`, `d_map`, `d_add`, `PresheafOfModules.Derivation'.app_apply`
`desc` 📖	CompOp	1 math math: `desc_d`
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`d_add` 📖	mathematical	—	`d` `CommRingCat.carrier` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `CommRingCat.commRing` `ModuleCat.carrier` `CommRing.toRing` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup`	—	`map_add` `AddMonoidHomClass.toAddHomClass` `Derivation.instAddMonoidHomClass`
`d_map` 📖	mathematical	—	`d` `DFunLike.coe` `CommRingCat.carrier` `CategoryTheory.ConcreteCategory.hom` `CommRingCat` `CommRingCat.instCategory` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `ModuleCat.carrier` `CommRing.toRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `ModuleCat.isAddCommGroup`	—	`Derivation.map_algebraMap`
`d_mul` 📖	mathematical	—	`d` `CommRingCat.carrier` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `CommRingCat.commRing` `ModuleCat.carrier` `CommRing.toRing` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `ModuleCat.isModule`	—	`Derivation.leibniz`
`desc_d` 📖	mathematical	—	`DFunLike.coe` `CommRingCat.KaehlerDifferential` `ModuleCat.carrier` `CommRingCat.carrier` `CommRing.toRing` `CommRingCat.commRing` `CategoryTheory.ConcreteCategory.hom` `ModuleCat` `ModuleCat.moduleCategory` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `desc` `CommRingCat.KaehlerDifferential.d` `d`	—	`Derivation.liftKaehlerDifferential_comp_D` `IsScalarTower.of_compHom`

---

← Back to Index