Sheafify

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

Statistics

Metric	Count
Definitions smul, SMulCandidate, mk', x, instUniqueSMulCandidate, smul, smulCandidate, sheafify, sheafifyHomEquiv, sheafifyHomEquiv', sheafifyMap, toSheafify	12
Theorems isCompatible_map_smul, isCompatible_map_smul_aux, h, add_smul, app_eq_of_isLocallyInjective, instNonemptySMulCandidate, instSubsingletonSMulCandidate, map_smul, map_smul_eq, mul_smul, one_smul, smul_add, smul_zero, zero_smul, comp_toPresheaf_map_sheafifyHomEquiv'_symm_hom, instIsLocallyInjectiveToSheafify, instIsLocallySurjectiveToSheafify, sheafifyMap_val, toPresheaf_map_toSheafify, toSheafify_app_apply, toSheafify_app_apply'	21
Total	33

CategoryTheory.Presieve.FamilyOfElements

Definitions

Name	Category	Theorems
smul 📖	CompOp	1 math math: isCompatible_map_smul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCompatible_map_smul 📖	mathematical	CategoryTheory.Presheaf.IsSeparated AddCommGrpCat AddCommGrpCat.instCategory AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier IsAmalgamation CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.types CategoryTheory.forget RingHom RingCat.carrier Semiring.toNonAssocSemiring Ring.toSemiring RingCat.ring RingHom.instFunLike RingCat.instConcreteCategoryRingHomCarrier map CategoryTheory.Functor.whiskerRight Ab PresheafOfModules.presheaf	Compatible smul	—	RingCat.comp_apply CategoryTheory.NatTrans.naturality CategoryTheory.Functor.map_comp CategoryTheory.NatTrans.naturality_apply CategoryTheory.ConcreteCategory.comp_apply CategoryTheory.op_comp isCompatible_map_smul_aux
isCompatible_map_smul_aux 📖	mathematical	CategoryTheory.Presheaf.IsSeparated AddCommGrpCat AddCommGrpCat.instCategory AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory Opposite.op RingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring Ring.toSemiring RingCat.ring RingHom.instFunLike RingCat.instConcreteCategoryRingHomCarrier CategoryTheory.NatTrans.app CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite Ab PresheafOfModules.presheaf	PresheafOfModules.obj 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 SMulZeroClass.toSMul AddZero.toZero DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	PresheafOfModules.Sheafify.app_eq_of_isLocallyInjective CategoryTheory.Functor.map_comp RingCat.comp_apply CategoryTheory.NatTrans.naturality AddCommGrpCat.coe_comp CategoryTheory.NatTrans.naturality_apply PresheafOfModules.map_smul

PresheafOfModules

Definitions

Name	Category	Theorems
sheafify 📖	CompOp	7 math math: instIsLocallySurjectiveToSheafify, toSheafify_app_apply', toPresheaf_map_toSheafify, sheafifyMap_val, comp_toPresheaf_map_sheafifyHomEquiv'_symm_hom, instIsLocallyInjectiveToSheafify, toSheafify_app_apply
sheafifyHomEquiv 📖	CompOp	—
sheafifyHomEquiv' 📖	CompOp	1 math math: comp_toPresheaf_map_sheafifyHomEquiv'_symm_hom
sheafifyMap 📖	CompOp	2 math math: sheafification_map, sheafifyMap_val
toSheafify 📖	CompOp	5 math math: instIsLocallySurjectiveToSheafify, toSheafify_app_apply', toPresheaf_map_toSheafify, instIsLocallyInjectiveToSheafify, toSheafify_app_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_toPresheaf_map_sheafifyHomEquiv'_symm_hom 📖	mathematical	CategoryTheory.Presheaf.IsSheaf Ab AddCommGrpCat.instCategory presheaf CategoryTheory.Sheaf.val RingCat RingCat.instCategory	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category AddCommGrpCat CategoryTheory.Functor.obj PresheafOfModules instCategory toPresheaf CategoryTheory.Functor.map SheafOfModules.val sheafify DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver restrictScalars EquivLike.toFunLike Equiv.instEquivLike Equiv.symm sheafifyHomEquiv'	—	CategoryTheory.Functor.congr_map Equiv.apply_symm_apply
instIsLocallyInjectiveToSheafify 📖	mathematical	—	IsLocallyInjective CategoryTheory.Functor.obj PresheafOfModules CategoryTheory.Sheaf.val RingCat RingCat.instCategory instCategory restrictScalars SheafOfModules.val sheafify toSheafify	—	—
instIsLocallySurjectiveToSheafify 📖	mathematical	—	IsLocallySurjective CategoryTheory.Functor.obj PresheafOfModules CategoryTheory.Sheaf.val RingCat RingCat.instCategory instCategory restrictScalars SheafOfModules.val sheafify toSheafify	—	—
sheafifyMap_val 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite Ab AddCommGrpCat.instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj PresheafOfModules instCategory toPresheaf CategoryTheory.Sheaf.val AddCommGrpCat CategoryTheory.Functor.map presheaf CategoryTheory.Sheaf.Hom.val	SheafOfModules.Hom.val sheafify sheafifyMap homMk RingCat RingCat.instCategory SheafOfModules.val	—	—
toPresheaf_map_toSheafify 📖	mathematical	—	CategoryTheory.Functor.map PresheafOfModules instCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite Ab AddCommGrpCat.instCategory CategoryTheory.Functor.category toPresheaf CategoryTheory.Functor.obj CategoryTheory.Sheaf.val RingCat RingCat.instCategory restrictScalars SheafOfModules.val sheafify toSheafify	—	—
toSheafify_app_apply 📖	mathematical	—	DFunLike.coe LinearMap RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory Ring.toSemiring RingCat.ring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier obj PresheafOfModules CategoryTheory.Sheaf.val instCategory restrictScalars SheafOfModules.val sheafify AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.Hom.hom Hom.app toSheafify Ab AddCommGrpCat.instCategory presheaf AddCommGrpCat AddCommGrpCat.carrier CategoryTheory.ConcreteCategory.hom AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier CategoryTheory.NatTrans.app	—	—
toSheafify_app_apply' 📖	mathematical	—	DFunLike.coe LinearMap RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory Ring.toSemiring RingCat.ring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier obj ModuleCat CategoryTheory.Sheaf.val ModuleCat.moduleCategory ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.NatTrans.app SheafOfModules.val sheafify AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule PresheafOfModules instCategory restrictScalars LinearMap.instFunLike ModuleCat.Hom.hom Hom.app toSheafify Ab AddCommGrpCat.instCategory presheaf AddCommGrpCat AddCommGrpCat.carrier CategoryTheory.ConcreteCategory.hom AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier	—	—

PresheafOfModules.Sheafify

Definitions

Name	Category	Theorems
SMulCandidate 📖	CompData	2 math math: instSubsingletonSMulCandidate, instNonemptySMulCandidate
instUniqueSMulCandidate 📖	CompOp	—
smul 📖	CompOp	8 math math: add_smul, map_smul_eq, smul_add, one_smul, zero_smul, smul_zero, map_smul, mul_smul
smulCandidate 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_smul 📖	mathematical	—	smul RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Sheaf.val Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing RingCat.ring AddCommGrpCat.carrier AddCommGrpCat AddCommGrpCat.instCategory AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid AddCommGrpCat.str	—	CategoryTheory.GrothendieckTopology.intersection_covering CategoryTheory.Presheaf.imageSieve_mem CategoryTheory.Sheaf.isSeparated CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.Functor.corepresentable_preservesLimit AddCommGrpCat.forget_isCorepresentable AddMonoidHom.map_add map_smul_eq map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass add_smul AddMonoidHom.instAddMonoidHomClass
app_eq_of_isLocallyInjective 📖	mathematical	CategoryTheory.Presheaf.IsSeparated AddCommGrpCat AddCommGrpCat.instCategory AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory Opposite.op RingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring Ring.toSemiring RingCat.ring RingHom.instFunLike RingCat.instConcreteCategoryRingHomCarrier CategoryTheory.NatTrans.app Ab PresheafOfModules.presheaf	ModuleCat.carrier PresheafOfModules.obj SMulZeroClass.toSMul AddZero.toZero ModuleCat.isAddCommGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid ModuleCat.isModule	—	CategoryTheory.GrothendieckTopology.intersection_covering CategoryTheory.Presheaf.equalizerSieve_mem CategoryTheory.NatTrans.naturality_apply PresheafOfModules.map_smul
instNonemptySMulCandidate 📖	mathematical	—	SMulCandidate	—	CategoryTheory.GrothendieckTopology.intersection_covering CategoryTheory.Presheaf.imageSieve_mem CategoryTheory.Presieve.FamilyOfElements.restrict_map CategoryTheory.Presieve.isAmalgamation_restrict CategoryTheory.Presieve.FamilyOfElements.isAmalgamation_map_localPreimage CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.Functor.corepresentable_preservesLimit AddCommGrpCat.forget_isCorepresentable CategoryTheory.Presheaf.IsSheaf.isSheafFor CategoryTheory.Sheaf.cond CategoryTheory.Presieve.FamilyOfElements.isCompatible_map_smul CategoryTheory.Sheaf.isSeparated CategoryTheory.Presieve.IsSheafFor.isAmalgamation
instSubsingletonSMulCandidate 📖	mathematical	—	SMulCandidate	—	CategoryTheory.GrothendieckTopology.intersection_covering CategoryTheory.Presheaf.imageSieve_mem CategoryTheory.Sheaf.isSeparated CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.Functor.corepresentable_preservesLimit AddCommGrpCat.forget_isCorepresentable
map_smul 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Sheaf.val AddCommGrpCat.carrier CategoryTheory.ConcreteCategory.hom AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier CategoryTheory.Functor.map smul RingCat RingCat.instCategory RingCat.carrier RingHom Semiring.toNonAssocSemiring Ring.toSemiring RingCat.ring RingHom.instFunLike RingCat.instConcreteCategoryRingHomCarrier	—	CategoryTheory.GrothendieckTopology.intersection_covering CategoryTheory.Presheaf.imageSieve_mem CategoryTheory.Sheaf.isSeparated CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.Functor.corepresentable_preservesLimit AddCommGrpCat.forget_isCorepresentable CategoryTheory.ConcreteCategory.comp_apply CategoryTheory.Functor.map_comp map_smul_eq RingCat.comp_apply
map_smul_eq 📖	mathematical	DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Sheaf.val RingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring Ring.toSemiring RingCat.ring RingHom.instFunLike RingCat.instConcreteCategoryRingHomCarrier CategoryTheory.NatTrans.app CategoryTheory.Functor.map Ab AddCommGrpCat.instCategory PresheafOfModules.presheaf AddCommGrpCat AddCommGrpCat.carrier AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier	smul ModuleCat.carrier PresheafOfModules.obj SMulZeroClass.toSMul AddZero.toZero ModuleCat.isAddCommGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid ModuleCat.isModule	—	SMulCandidate.h
mul_smul 📖	mathematical	—	smul RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Sheaf.val Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing RingCat.ring	—	CategoryTheory.GrothendieckTopology.intersection_covering CategoryTheory.Presheaf.imageSieve_mem CategoryTheory.Sheaf.isSeparated CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.Functor.corepresentable_preservesLimit AddCommGrpCat.forget_isCorepresentable map_smul_eq map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass SemigroupAction.mul_smul
one_smul 📖	mathematical	—	smul RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Sheaf.val AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne RingCat.ring	—	CategoryTheory.Sheaf.isSeparated CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.Functor.corepresentable_preservesLimit AddCommGrpCat.forget_isCorepresentable CategoryTheory.Presheaf.imageSieve_mem map_smul_eq map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass one_smul
smul_add 📖	mathematical	—	smul AddCommGrpCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Sheaf.val AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid AddCommGrpCat.str	—	CategoryTheory.GrothendieckTopology.intersection_covering CategoryTheory.Presheaf.imageSieve_mem CategoryTheory.Sheaf.isSeparated CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.Functor.corepresentable_preservesLimit AddCommGrpCat.forget_isCorepresentable AddMonoidHom.map_add map_smul_eq map_add AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass smul_add
smul_zero 📖	mathematical	—	smul AddCommGrpCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Sheaf.val NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddCommGrpCat.str	—	CategoryTheory.Sheaf.isSeparated CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.Functor.corepresentable_preservesLimit AddCommGrpCat.forget_isCorepresentable CategoryTheory.Presheaf.imageSieve_mem AddMonoidHom.map_zero map_smul_eq map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass smul_zero
zero_smul 📖	mathematical	—	smul RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Sheaf.val MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing RingCat.ring AddCommGrpCat.carrier AddCommGrpCat AddCommGrpCat.instCategory NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddCommGrpCat.str	—	CategoryTheory.Sheaf.isSeparated CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.Functor.corepresentable_preservesLimit AddCommGrpCat.forget_isCorepresentable CategoryTheory.Presheaf.imageSieve_mem map_smul_eq map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass zero_smul AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass AddMonoidHom.map_zero

PresheafOfModules.Sheafify.SMulCandidate

Definitions

Name	Category	Theorems
mk' 📖	CompOp	—
x 📖	CompOp	1 math math: h

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
h 📖	mathematical	DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Sheaf.val RingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring Ring.toSemiring RingCat.ring RingHom.instFunLike RingCat.instConcreteCategoryRingHomCarrier CategoryTheory.NatTrans.app CategoryTheory.Functor.map Ab AddCommGrpCat.instCategory PresheafOfModules.presheaf AddCommGrpCat AddCommGrpCat.carrier AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier	x ModuleCat.carrier PresheafOfModules.obj SMulZeroClass.toSMul AddZero.toZero ModuleCat.isAddCommGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid ModuleCat.isModule	—	—

---

← Back to Index