Presheaf

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

Statistics

Metric	Count
Definitions Derivation', mk, app, mk, Universal, desc, d, postcomp, derivation', isUniversal', relativeDifferentials', HasDifferentials	12
Theorems app_apply, d_app, mk_app, fac, postcomp_injective, congr_d, d_app, d_map, d_mul, d_one, ext, ext_iff, instSubsingletonUniversal, postcomp_d_apply, instHasDifferentials, relativeDifferentials'_map, relativeDifferentials'_map_d, relativeDifferentials'_obj, exists_universal_derivation	19
Total	31

PresheafOfModules

Definitions

Name	Category	Theorems
Derivation' 📖	CompOp	—
HasDifferentials 📖	CompData	1 math math: DifferentialsConstruction.instHasDifferentials

PresheafOfModules.Derivation

Definitions

Name	Category	Theorems
Universal 📖	CompData	2 math math: instSubsingletonUniversal, PresheafOfModules.HasDifferentials.exists_universal_derivation
d 📖	CompOp	9 math math: d_map, postcomp_d_apply, d_one, d_mul, congr_d, ext_iff, PresheafOfModules.Derivation'.d_app, d_app, PresheafOfModules.Derivation'.app_apply
postcomp 📖	CompOp	2 math math: Universal.fac, postcomp_d_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr_d 📖	mathematical	—	DFunLike.coe AddMonoidHom CommRingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CommRingCat CommRingCat.instCategory ModuleCat.carrier RingCat.carrier RingCat RingCat.instCategory CategoryTheory.Functor.comp CategoryTheory.forget₂ RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier Ring.toSemiring RingCat.ring RingCat.instConcreteCategoryRingHomCarrier CommRingCat.hasForgetToRingCat PresheafOfModules.obj AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup ModuleCat.isAddCommGroup AddMonoidHom.instFunLike d	—	—
d_app 📖	mathematical	—	DFunLike.coe AddMonoidHom CommRingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CommRingCat CommRingCat.instCategory CategoryTheory.Functor.op ModuleCat.carrier RingCat.carrier RingCat RingCat.instCategory CategoryTheory.Functor.comp CategoryTheory.forget₂ RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier Ring.toSemiring RingCat.ring RingCat.instConcreteCategoryRingHomCarrier CommRingCat.hasForgetToRingCat PresheafOfModules.obj AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup ModuleCat.isAddCommGroup AddMonoidHom.instFunLike d CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
d_map 📖	mathematical	—	DFunLike.coe AddMonoidHom CommRingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CommRingCat CommRingCat.instCategory ModuleCat.carrier RingCat.carrier RingCat RingCat.instCategory CategoryTheory.Functor.comp CategoryTheory.forget₂ RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier Ring.toSemiring RingCat.ring RingCat.instConcreteCategoryRingHomCarrier CommRingCat.hasForgetToRingCat PresheafOfModules.obj AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup ModuleCat.isAddCommGroup AddMonoidHom.instFunLike d CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map ModuleCat ModuleCat.moduleCategory ModuleCat.restrictScalars RingCat.Hom.hom LinearMap RingHom.id AddCommGroup.toAddCommMonoid ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier PresheafOfModules.map	—	—
d_mul 📖	mathematical	—	DFunLike.coe AddMonoidHom CommRingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CommRingCat CommRingCat.instCategory ModuleCat.carrier RingCat.carrier RingCat RingCat.instCategory CategoryTheory.Functor.comp CategoryTheory.forget₂ RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier Ring.toSemiring RingCat.ring RingCat.instConcreteCategoryRingHomCarrier CommRingCat.hasForgetToRingCat PresheafOfModules.obj AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup ModuleCat.isAddCommGroup AddMonoidHom.instFunLike d Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction PresheafOfModules.instModuleCarrierObjOppositeCommRingCatCarrierCarrierRingCatCompForget₂RingHomObj	—	—
d_one 📖	mathematical	—	DFunLike.coe AddMonoidHom CommRingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CommRingCat CommRingCat.instCategory ModuleCat.carrier RingCat.carrier RingCat RingCat.instCategory CategoryTheory.Functor.comp CategoryTheory.forget₂ RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier Ring.toSemiring RingCat.ring RingCat.instConcreteCategoryRingHomCarrier CommRingCat.hasForgetToRingCat PresheafOfModules.obj AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup ModuleCat.isAddCommGroup AddMonoidHom.instFunLike d AddMonoidWithOne.toOne NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	mul_one one_smul AddLeftCancelSemigroup.toIsLeftCancelAdd d_mul
ext 📖	—	d	—	—	—
ext_iff 📖	mathematical	—	d	—	ext
instSubsingletonUniversal 📖	mathematical	—	Universal	—	Universal.postcomp_injective Universal.fac
postcomp_d_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom CommRingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CommRingCat CommRingCat.instCategory ModuleCat.carrier RingCat.carrier RingCat RingCat.instCategory CategoryTheory.Functor.comp CategoryTheory.forget₂ RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier Ring.toSemiring RingCat.ring RingCat.instConcreteCategoryRingHomCarrier CommRingCat.hasForgetToRingCat PresheafOfModules.obj AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup AddMonoidHom.instFunLike d postcomp LinearMap RingHom.id ModuleCat.isModule LinearMap.instFunLike ModuleCat.Hom.hom PresheafOfModules.Hom.app	—	—

PresheafOfModules.Derivation'

Definitions

Name	Category	Theorems
app 📖	CompOp	2 math math: mk_app, app_apply
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
app_apply 📖	mathematical	—	ModuleCat.Derivation.d CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CommRingCat CommRingCat.instCategory PresheafOfModules.obj CategoryTheory.Functor.comp RingCat RingCat.instCategory CategoryTheory.forget₂ RingHom CommRingCat.carrier Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier RingCat.carrier Ring.toSemiring RingCat.ring RingCat.instConcreteCategoryRingHomCarrier CommRingCat.hasForgetToRingCat CategoryTheory.NatTrans.app app DFunLike.coe AddMonoidHom ModuleCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup ModuleCat.isAddCommGroup AddMonoidHom.instFunLike PresheafOfModules.Derivation.d CategoryTheory.Functor.id	—	—
d_app 📖	mathematical	—	DFunLike.coe AddMonoidHom CommRingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CommRingCat CommRingCat.instCategory ModuleCat.carrier RingCat.carrier RingCat RingCat.instCategory CategoryTheory.Functor.comp CategoryTheory.forget₂ RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier Ring.toSemiring RingCat.ring RingCat.instConcreteCategoryRingHomCarrier CommRingCat.hasForgetToRingCat PresheafOfModules.obj AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup ModuleCat.isAddCommGroup AddMonoidHom.instFunLike PresheafOfModules.Derivation.d CategoryTheory.Functor.id CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	PresheafOfModules.Derivation.d_app
mk_app 📖	mathematical	ModuleCat.Derivation.d CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CommRingCat CommRingCat.instCategory PresheafOfModules.obj CategoryTheory.Functor.comp RingCat RingCat.instCategory CategoryTheory.forget₂ RingHom CommRingCat.carrier Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier RingCat.carrier Ring.toSemiring RingCat.ring RingCat.instConcreteCategoryRingHomCarrier CommRingCat.hasForgetToRingCat CategoryTheory.NatTrans.app DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map ModuleCat ModuleCat.moduleCategory ModuleCat.restrictScalars RingCat.Hom.hom ModuleCat.carrier LinearMap RingHom.id AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier PresheafOfModules.map	app	—	—

PresheafOfModules.Derivation'.Universal

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

PresheafOfModules.Derivation.Universal

Definitions

Name	Category	Theorems
desc 📖	CompOp	1 math math: fac

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fac 📖	mathematical	—	PresheafOfModules.Derivation.postcomp desc	—	—
postcomp_injective 📖	—	PresheafOfModules.Derivation.postcomp	—	—	—

PresheafOfModules.DifferentialsConstruction

Definitions

Name	Category	Theorems
derivation' 📖	CompOp	—
isUniversal' 📖	CompOp	—
relativeDifferentials' 📖	CompOp	3 math math: relativeDifferentials'_map_d, relativeDifferentials'_obj, relativeDifferentials'_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasDifferentials 📖	mathematical	—	PresheafOfModules.HasDifferentials CategoryTheory.Functor.id	—	—
relativeDifferentials'_map 📖	mathematical	—	PresheafOfModules.map CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CommRingCat CommRingCat.instCategory RingCat RingCat.instCategory CategoryTheory.forget₂ RingHom CommRingCat.carrier Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier RingCat.carrier Ring.toSemiring RingCat.ring RingCat.instConcreteCategoryRingHomCarrier CommRingCat.hasForgetToRingCat relativeDifferentials' CommRingCat.KaehlerDifferential.map CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor.map	—	—
relativeDifferentials'_map_d 📖	mathematical	—	DFunLike.coe LinearMap CommRingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CommRingCat CommRingCat.instCategory Ring.toSemiring CommRing.toRing CommRingCat.commRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier PresheafOfModules.obj CategoryTheory.Functor.comp RingCat RingCat.instCategory CategoryTheory.forget₂ RingHom CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier RingCat.carrier RingCat.ring RingCat.instConcreteCategoryRingHomCarrier CommRingCat.hasForgetToRingCat relativeDifferentials' ModuleCat ModuleCat.moduleCategory ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule CommRingCat.KaehlerDifferential CategoryTheory.NatTrans.app LinearMap.instFunLike ModuleCat.Hom.hom PresheafOfModules.map CommRingCat.KaehlerDifferential.d CategoryTheory.ConcreteCategory.hom	—	CommRingCat.KaehlerDifferential.map_d CategoryTheory.NatTrans.naturality
relativeDifferentials'_obj 📖	mathematical	—	PresheafOfModules.obj CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CommRingCat CommRingCat.instCategory RingCat RingCat.instCategory CategoryTheory.forget₂ RingHom CommRingCat.carrier Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier RingCat.carrier Ring.toSemiring RingCat.ring RingCat.instConcreteCategoryRingHomCarrier CommRingCat.hasForgetToRingCat relativeDifferentials' CommRingCat.KaehlerDifferential CategoryTheory.Functor.obj CategoryTheory.NatTrans.app	—	—

PresheafOfModules.HasDifferentials

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_universal_derivation 📖	mathematical	—	PresheafOfModules CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CommRingCat CommRingCat.instCategory RingCat RingCat.instCategory CategoryTheory.forget₂ RingHom CommRingCat.carrier Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier RingCat.carrier Ring.toSemiring RingCat.ring RingCat.instConcreteCategoryRingHomCarrier CommRingCat.hasForgetToRingCat PresheafOfModules.Derivation PresheafOfModules.Derivation.Universal	—	—

---

← Back to Index