Documentation Verification Report

Stalk

📁 Source: Mathlib/Algebra/Category/ModuleCat/Stalk.lean

Statistics

Metric	Count
Definitions `smul`, `filteredColimitsModule`, `instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier`, `instModuleCarrierStalkRingCatCarrierAbPresheafOpensCarrier`	4
Theorems `ι_smul`, `germ_ringCat_smul`, `germ_smul`	3
Total	7

CategoryTheory.Limits

Definitions

Name	Category	Theorems
`filteredColimitsModule` 📖	CompOp	—

CategoryTheory.Limits.IsColimit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ι_smul` 📖	mathematical	`DFunLike.coe` `CategoryTheory.Functor.obj` `Ab` `AddCommGrpCat.instCategory` `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` `RingCat.carrier` `RingCat` `RingCat.instCategory` `SMulZeroClass.toSMul` `AddZero.toZero` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `RingCat.ring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingCat.instConcreteCategoryRingHomCarrier`	`CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι` `module`	—	`AddEquiv.eq_symm_apply` `comp_coconePointUniqueUpToIso_hom` `CategoryTheory.IsFiltered.toIsFilteredOrEmpty` `CategoryTheory.IsFilteredOrEmpty.cocone_maps` `CategoryTheory.Functor.ιColimitType_eq_of_map_eq_map`

CategoryTheory.Limits.colimit

Definitions

Name	Category	Theorems
`smul` 📖	CompOp	—

PresheafOfModules

Definitions

Name	Category	Theorems
`instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier` 📖	CompOp	2 math math: `AlgebraicGeometry.StructureSheaf.instIsScalarTowerCarrierStalkCommRingCatStructurePresheafInCommRingCatCarrierAbPresheafOpensCarrierTopModuleStructurePresheaf`, `germ_smul`
`instModuleCarrierStalkRingCatCarrierAbPresheafOpensCarrier` 📖	CompOp	1 math math: `germ_ringCat_smul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`germ_ringCat_smul` 📖	mathematical	`TopCat.carrier` `TopologicalSpace.Opens` `TopCat.str` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike`	`DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `Ab` `AddCommGrpCat.instCategory` `presheaf` `Opposite.op` `TopCat.Presheaf.stalk` `AddCommGrpCat.hasColimitsOfSize` `UnivLE.self` `AddCommGrpCat.carrier` `CategoryTheory.ConcreteCategory.hom` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGrpCat.str` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `TopCat.Presheaf.germ` `RingCat.carrier` `RingCat` `RingCat.instCategory` `ModuleCat.carrier` `RingCat.ring` `obj` `SMulZeroClass.toSMul` `AddZero.toZero` `ModuleCat.isAddCommGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `ModuleCat.isModule` `RingCat.Colimits.hasColimits_ringCat` `instModuleCarrierStalkRingCatCarrierAbPresheafOpensCarrier` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingCat.instConcreteCategoryRingHomCarrier`	—	`CategoryTheory.Limits.IsColimit.ι_smul` `CategoryTheory.isFiltered_op_of_isCofiltered` `CategoryTheory.isCofiltered_of_directed_ge_nonempty` `SemilatticeInf.instIsCodirectedOrder` `map_smul` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits` `CategoryTheory.Limits.hasFilteredColimitsOfSize_of_hasColimitsOfSize` `RingCat.Colimits.hasColimits_ringCat` `AddCommGrpCat.hasColimit` `Opposite.small` `UnivLE.small` `univLE_of_max` `UnivLE.self`
`germ_smul` 📖	mathematical	`TopCat.carrier` `TopologicalSpace.Opens` `TopCat.str` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike`	`DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `Ab` `AddCommGrpCat.instCategory` `presheaf` `CategoryTheory.Functor.comp` `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` `Opposite.op` `TopCat.Presheaf.stalk` `AddCommGrpCat.hasColimitsOfSize` `UnivLE.self` `AddCommGrpCat.carrier` `CategoryTheory.ConcreteCategory.hom` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGrpCat.str` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `TopCat.Presheaf.germ` `ModuleCat.carrier` `obj` `SMulZeroClass.toSMul` `AddZero.toZero` `ModuleCat.isAddCommGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `ModuleCat.isModule` `CommRingCat.Colimits.hasColimits_commRingCat` `instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier`	—	`CategoryTheory.Limits.IsColimit.ι_smul` `CategoryTheory.isFiltered_op_of_isCofiltered` `CategoryTheory.isCofiltered_of_directed_ge_nonempty` `SemilatticeInf.instIsCodirectedOrder` `map_smul` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits` `CategoryTheory.Limits.hasFilteredColimitsOfSize_of_hasColimitsOfSize` `CommRingCat.Colimits.hasColimits_commRingCat` `CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit` `CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits` `CommRingCat.FilteredColimits.forget₂Ring_preservesFilteredColimits` `AddCommGrpCat.hasColimit` `Opposite.small` `UnivLE.small` `univLE_of_max` `UnivLE.self`

---

← Back to Index