Quasicoherent

📁 Source: Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean

Statistics

Metric	Count
Definitions IsFinitePresentation, IsQuasicoherent, generators, isColimit, map, mapGenerators, mapRelations, of_isIso, quasicoherentData, relations, QuasicoherentData, I, IsFinitePresentation, X, bind, localGeneratorsData, presentation, shrink, generatorsOfIsCokernelFree, isFinitePresentation, isQuasicoherent, presentationOfIsCokernelFree, quasicoherentDataOfIsFinitePresentation, relationsOfIsCokernelFree	24
Theorems exists_quasicoherentData, nonempty_quasicoherentData, of_coversTop, finite_relations, isFiniteType_generators, isQuasicoherent, mapRelations_mapGenerators, mapRelations_mapGenerators_assoc, map_generators_I, map_relations_I, map_π_eq, of_isIso_generators, of_isIso_relations, quasicoherentData_I, quasicoherentData_X, quasicoherentData_presentation, isFinite_presentation, coversTop, instIsFiniteTypeLocalGeneratorsDataOfIsFinitePresentation, isQuasicoherent, localGeneratorsData_I, localGeneratorsData_X, localGeneratorsData_generators, generatorsOfIsCokernelFree_I, generatorsOfIsCokernelFree_s, generatorsOfIsCokernelFree_π, instIsFiniteTypeOfIsFinitePresentation, instIsQuasicoherentOfIsFinitePresentation, instPreservesColimitsOfSize, presentationOfIsCokernelFree_generators, presentationOfIsCokernelFree_relations, relationsOfIsCokernelFree_I, relationsOfIsCokernelFree_s	33
Total	57

SheafOfModules

Definitions

Name	Category	Theorems
IsFinitePresentation 📖	CompData	—
IsQuasicoherent 📖	CompData	4 math math: Presentation.isQuasicoherent, QuasicoherentData.isQuasicoherent, instIsQuasicoherentOfIsFinitePresentation, AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde
QuasicoherentData 📖	CompData	1 math math: IsQuasicoherent.nonempty_quasicoherentData
generatorsOfIsCokernelFree 📖	CompOp	7 math math: presentationOfIsCokernelFree_generators, Presentation.map_relations_I, relationsOfIsCokernelFree_I, relationsOfIsCokernelFree_s, generatorsOfIsCokernelFree_π, generatorsOfIsCokernelFree_s, generatorsOfIsCokernelFree_I
isFinitePresentation 📖	CompOp	—
isQuasicoherent 📖	CompOp	—
presentationOfIsCokernelFree 📖	CompOp	2 math math: presentationOfIsCokernelFree_generators, presentationOfIsCokernelFree_relations
quasicoherentDataOfIsFinitePresentation 📖	CompOp	—
relationsOfIsCokernelFree 📖	CompOp	3 math math: presentationOfIsCokernelFree_relations, relationsOfIsCokernelFree_I, relationsOfIsCokernelFree_s

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
generatorsOfIsCokernelFree_I 📖	mathematical	CategoryTheory.CategoryStruct.comp SheafOfModules CategoryTheory.Category.toCategoryStruct instCategory free CategoryTheory.instHasWeakSheafifyOfHasSheafify AddCommGrpCat AddCommGrpCat.instCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive	GeneratingSections.I generatorsOfIsCokernelFree	—	CategoryTheory.instHasWeakSheafifyOfHasSheafify
generatorsOfIsCokernelFree_s 📖	mathematical	CategoryTheory.CategoryStruct.comp SheafOfModules CategoryTheory.Category.toCategoryStruct instCategory free CategoryTheory.instHasWeakSheafifyOfHasSheafify AddCommGrpCat AddCommGrpCat.instCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive	GeneratingSections.s generatorsOfIsCokernelFree DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike freeHomEquiv	—	CategoryTheory.instHasWeakSheafifyOfHasSheafify
generatorsOfIsCokernelFree_π 📖	mathematical	CategoryTheory.CategoryStruct.comp SheafOfModules CategoryTheory.Category.toCategoryStruct instCategory free CategoryTheory.instHasWeakSheafifyOfHasSheafify AddCommGrpCat AddCommGrpCat.instCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive	GeneratingSections.π generatorsOfIsCokernelFree	—	CategoryTheory.instHasWeakSheafifyOfHasSheafify Equiv.symm_apply_apply
instIsFiniteTypeOfIsFinitePresentation 📖	mathematical	CategoryTheory.GrothendieckTopology.HasSheafCompose CategoryTheory.Over CategoryTheory.instCategoryOver RingCat RingCat.instCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.GrothendieckTopology.over CategoryTheory.forget₂ RingHom RingCat.carrier Semiring.toNonAssocSemiring Ring.toSemiring RingCat.ring RingHom.instFunLike RingCat.instConcreteCategoryRingHomCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier RingCat.hasForgetToAddCommGrp CategoryTheory.HasWeakSheafify CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective	IsFiniteType	—	IsFinitePresentation.exists_quasicoherentData QuasicoherentData.instIsFiniteTypeLocalGeneratorsDataOfIsFinitePresentation
instIsQuasicoherentOfIsFinitePresentation 📖	mathematical	CategoryTheory.GrothendieckTopology.HasSheafCompose CategoryTheory.Over CategoryTheory.instCategoryOver RingCat RingCat.instCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.GrothendieckTopology.over CategoryTheory.forget₂ RingHom RingCat.carrier Semiring.toNonAssocSemiring Ring.toSemiring RingCat.ring RingHom.instFunLike RingCat.instConcreteCategoryRingHomCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier RingCat.hasForgetToAddCommGrp CategoryTheory.HasWeakSheafify CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective	IsQuasicoherent	—	IsFinitePresentation.exists_quasicoherentData
instPreservesColimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfSize SheafOfModules instCategory	—	CategoryTheory.Limits.preservesColimitsOfSize_shrink
presentationOfIsCokernelFree_generators 📖	mathematical	CategoryTheory.CategoryStruct.comp SheafOfModules CategoryTheory.Category.toCategoryStruct instCategory free CategoryTheory.instHasWeakSheafifyOfHasSheafify AddCommGrpCat AddCommGrpCat.instCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive	Presentation.generators presentationOfIsCokernelFree generatorsOfIsCokernelFree	—	CategoryTheory.instHasWeakSheafifyOfHasSheafify
presentationOfIsCokernelFree_relations 📖	mathematical	CategoryTheory.CategoryStruct.comp SheafOfModules CategoryTheory.Category.toCategoryStruct instCategory free CategoryTheory.instHasWeakSheafifyOfHasSheafify AddCommGrpCat AddCommGrpCat.instCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive	Presentation.relations presentationOfIsCokernelFree relationsOfIsCokernelFree	—	CategoryTheory.instHasWeakSheafifyOfHasSheafify hasLimit small_subtype small_Pi UnivLE.small univLE_of_max UnivLE.self AddCommGrpCat.hasLimitsOfShape
relationsOfIsCokernelFree_I 📖	mathematical	CategoryTheory.CategoryStruct.comp SheafOfModules CategoryTheory.Category.toCategoryStruct instCategory free CategoryTheory.instHasWeakSheafifyOfHasSheafify AddCommGrpCat AddCommGrpCat.instCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive	GeneratingSections.I CategoryTheory.Limits.kernel generatorsOfIsCokernelFree GeneratingSections.π hasLimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair small_subtype small_Pi CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Functor.comp ModuleCat RingCat.carrier Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Sheaf.val RingCat.ring ModuleCat.moduleCategory evaluation CategoryTheory.forget LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier UnivLE.small univLE_of_max UnivLE.self Set Set.instMembership CategoryTheory.Functor.sections AddCommGrpCat.hasLimitsOfShape relationsOfIsCokernelFree	—	CategoryTheory.instHasWeakSheafifyOfHasSheafify hasLimit small_subtype small_Pi UnivLE.small univLE_of_max UnivLE.self AddCommGrpCat.hasLimitsOfShape
relationsOfIsCokernelFree_s 📖	mathematical	CategoryTheory.CategoryStruct.comp SheafOfModules CategoryTheory.Category.toCategoryStruct instCategory free CategoryTheory.instHasWeakSheafifyOfHasSheafify AddCommGrpCat AddCommGrpCat.instCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive	GeneratingSections.s CategoryTheory.Limits.kernel GeneratingSections.I generatorsOfIsCokernelFree GeneratingSections.π hasLimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair small_subtype small_Pi CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Functor.comp ModuleCat RingCat.carrier Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Sheaf.val RingCat.ring ModuleCat.moduleCategory evaluation CategoryTheory.forget LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier UnivLE.small univLE_of_max UnivLE.self Set Set.instMembership CategoryTheory.Functor.sections AddCommGrpCat.hasLimitsOfShape relationsOfIsCokernelFree DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike freeHomEquiv CategoryTheory.Limits.kernel.lift	—	CategoryTheory.instHasWeakSheafifyOfHasSheafify hasLimit small_subtype small_Pi UnivLE.small univLE_of_max UnivLE.self AddCommGrpCat.hasLimitsOfShape

SheafOfModules.IsFinitePresentation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_quasicoherentData 📖	mathematical	CategoryTheory.GrothendieckTopology.HasSheafCompose CategoryTheory.Over CategoryTheory.instCategoryOver RingCat RingCat.instCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.GrothendieckTopology.over CategoryTheory.forget₂ RingHom RingCat.carrier Semiring.toNonAssocSemiring Ring.toSemiring RingCat.ring RingHom.instFunLike RingCat.instConcreteCategoryRingHomCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier RingCat.hasForgetToAddCommGrp CategoryTheory.HasWeakSheafify CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective	SheafOfModules.QuasicoherentData.IsFinitePresentation	—	—

SheafOfModules.IsQuasicoherent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nonempty_quasicoherentData 📖	mathematical	CategoryTheory.GrothendieckTopology.HasSheafCompose CategoryTheory.Over CategoryTheory.instCategoryOver RingCat RingCat.instCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.GrothendieckTopology.over CategoryTheory.forget₂ RingHom RingCat.carrier Semiring.toNonAssocSemiring Ring.toSemiring RingCat.ring RingHom.instFunLike RingCat.instConcreteCategoryRingHomCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier RingCat.hasForgetToAddCommGrp CategoryTheory.HasWeakSheafify CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective	SheafOfModules.QuasicoherentData	—	—
of_coversTop 📖	—	CategoryTheory.GrothendieckTopology.HasSheafCompose CategoryTheory.Over CategoryTheory.instCategoryOver RingCat RingCat.instCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.GrothendieckTopology.over CategoryTheory.forget₂ RingHom RingCat.carrier Semiring.toNonAssocSemiring Ring.toSemiring RingCat.ring RingHom.instFunLike RingCat.instConcreteCategoryRingHomCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier RingCat.hasForgetToAddCommGrp CategoryTheory.HasSheafify CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective CategoryTheory.GrothendieckTopology.CoversTop SheafOfModules.IsQuasicoherent CategoryTheory.Sheaf.over CategoryTheory.instHasWeakSheafifyOfHasSheafify SheafOfModules.over	—	—	CategoryTheory.instHasWeakSheafifyOfHasSheafify SheafOfModules.QuasicoherentData.isQuasicoherent nonempty_quasicoherentData

SheafOfModules.Presentation

Definitions

Name	Category	Theorems
generators 📖	CompOp	11 math math: SheafOfModules.presentationOfIsCokernelFree_generators, SheafOfModules.QuasicoherentData.localGeneratorsData_generators, IsFinite.isFiniteType_generators, map_relations_I, mapRelations_mapGenerators, of_isIso_relations, of_isIso_generators, mapRelations_mapGenerators_assoc, map_generators_I, IsFinite.finite_relations, map_π_eq
isColimit 📖	CompOp	1 math math: map_relations_I
map 📖	CompOp	4 math math: quasicoherentData_presentation, map_relations_I, map_generators_I, map_π_eq
mapGenerators 📖	CompOp	3 math math: map_relations_I, mapRelations_mapGenerators, mapRelations_mapGenerators_assoc
mapRelations 📖	CompOp	3 math math: map_relations_I, mapRelations_mapGenerators, mapRelations_mapGenerators_assoc
of_isIso 📖	CompOp	2 math math: of_isIso_relations, of_isIso_generators
quasicoherentData 📖	CompOp	3 math math: quasicoherentData_presentation, quasicoherentData_I, quasicoherentData_X
relations 📖	CompOp	6 math math: SheafOfModules.presentationOfIsCokernelFree_relations, map_relations_I, mapRelations_mapGenerators, of_isIso_relations, mapRelations_mapGenerators_assoc, IsFinite.finite_relations

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isQuasicoherent 📖	mathematical	CategoryTheory.GrothendieckTopology.HasSheafCompose CategoryTheory.Over CategoryTheory.instCategoryOver RingCat RingCat.instCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.GrothendieckTopology.over CategoryTheory.forget₂ RingHom RingCat.carrier Semiring.toNonAssocSemiring Ring.toSemiring RingCat.ring RingHom.instFunLike RingCat.instConcreteCategoryRingHomCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier RingCat.hasForgetToAddCommGrp CategoryTheory.HasSheafify CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective	SheafOfModules.IsQuasicoherent CategoryTheory.instHasWeakSheafifyOfHasSheafify	—	CategoryTheory.instHasWeakSheafifyOfHasSheafify
mapRelations_mapGenerators 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SheafOfModules CategoryTheory.Category.toCategoryStruct SheafOfModules.instCategory SheafOfModules.free CategoryTheory.instHasWeakSheafifyOfHasSheafify AddCommGrpCat AddCommGrpCat.instCategory SheafOfModules.GeneratingSections.I CategoryTheory.Limits.kernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms SheafOfModules.instPreadditive generators SheafOfModules.GeneratingSections.π SheafOfModules.hasLimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero small_subtype small_Pi CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Functor.comp ModuleCat RingCat.carrier Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Sheaf.val RingCat.ring ModuleCat.moduleCategory SheafOfModules.evaluation CategoryTheory.forget LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier UnivLE.small univLE_of_max UnivLE.self Set Set.instMembership CategoryTheory.Functor.sections AddCommGrpCat.hasLimitsOfShape relations mapRelations mapGenerators	—	CategoryTheory.instHasWeakSheafifyOfHasSheafify SheafOfModules.hasLimit small_subtype small_Pi UnivLE.small univLE_of_max UnivLE.self AddCommGrpCat.hasLimitsOfShape CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.Limits.kernel.condition CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_initial_object CategoryTheory.Abelian.hasZeroObject CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits CategoryTheory.Limits.PreservesColimitsOfSize0.preservesFiniteColimits SheafOfModules.instPreservesColimitsOfSize CategoryTheory.Limits.comp_zero
mapRelations_mapGenerators_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SheafOfModules CategoryTheory.Category.toCategoryStruct SheafOfModules.instCategory SheafOfModules.free CategoryTheory.instHasWeakSheafifyOfHasSheafify AddCommGrpCat AddCommGrpCat.instCategory SheafOfModules.GeneratingSections.I CategoryTheory.Limits.kernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms SheafOfModules.instPreadditive generators SheafOfModules.GeneratingSections.π SheafOfModules.hasLimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero small_subtype small_Pi CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Functor.comp ModuleCat RingCat.carrier Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Sheaf.val RingCat.ring ModuleCat.moduleCategory SheafOfModules.evaluation CategoryTheory.forget LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier UnivLE.small univLE_of_max UnivLE.self Set Set.instMembership CategoryTheory.Functor.sections AddCommGrpCat.hasLimitsOfShape relations mapRelations mapGenerators	—	CategoryTheory.instHasWeakSheafifyOfHasSheafify SheafOfModules.hasLimit small_subtype small_Pi UnivLE.small univLE_of_max UnivLE.self AddCommGrpCat.hasLimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapRelations_mapGenerators
map_generators_I 📖	mathematical	—	SheafOfModules.GeneratingSections.I CategoryTheory.instHasWeakSheafifyOfHasSheafify AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Functor.obj SheafOfModules SheafOfModules.instCategory generators map	—	CategoryTheory.instHasWeakSheafifyOfHasSheafify
map_relations_I 📖	mathematical	—	SheafOfModules.GeneratingSections.I CategoryTheory.instHasWeakSheafifyOfHasSheafify AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Limits.kernel SheafOfModules SheafOfModules.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms SheafOfModules.instPreadditive SheafOfModules.free CategoryTheory.Functor.obj SheafOfModules.generatorsOfIsCokernelFree generators SheafOfModules.GeneratingSections.π relations mapRelations mapGenerators mapRelations_mapGenerators DFunLike.coe Equiv CategoryTheory.Limits.IsColimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor.comp CategoryTheory.Limits.parallelPair CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm SheafOfModules.freeHomEquiv SheafOfModules.GeneratingSections.s CategoryTheory.Limits.kernel.ι CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Functor.mapCocone CategoryTheory.Limits.CokernelCofork.ofπ CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso CategoryTheory.Limits.parallelPairIsoMk SheafOfModules.mapFree CategoryTheory.Limits.Cocones.ext CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category CategoryTheory.Limits.Cocones.precompose CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Iso.refl CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.isColimitOfPreserves isColimit SheafOfModules.hasLimit small_subtype small_Pi CategoryTheory.types ModuleCat RingCat.carrier Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Sheaf.val RingCat.ring ModuleCat.moduleCategory SheafOfModules.evaluation CategoryTheory.forget LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier UnivLE.small univLE_of_max UnivLE.self Set Set.instMembership CategoryTheory.Functor.sections AddCommGrpCat.hasLimitsOfShape map	—	CategoryTheory.instHasWeakSheafifyOfHasSheafify mapRelations_mapGenerators SheafOfModules.hasLimit small_subtype small_Pi UnivLE.small univLE_of_max UnivLE.self AddCommGrpCat.hasLimitsOfShape
map_π_eq 📖	mathematical	—	SheafOfModules.GeneratingSections.π CategoryTheory.instHasWeakSheafifyOfHasSheafify AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Functor.obj SheafOfModules SheafOfModules.instCategory generators map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct SheafOfModules.free SheafOfModules.GeneratingSections.I CategoryTheory.Iso.inv SheafOfModules.mapFree CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.map	—	CategoryTheory.instHasWeakSheafifyOfHasSheafify CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape Equiv.symm_apply_eq
of_isIso_generators 📖	mathematical	—	generators CategoryTheory.instHasWeakSheafifyOfHasSheafify AddCommGrpCat AddCommGrpCat.instCategory of_isIso SheafOfModules.GeneratingSections.ofEpi	—	CategoryTheory.instHasWeakSheafifyOfHasSheafify
of_isIso_relations 📖	mathematical	—	relations CategoryTheory.instHasWeakSheafifyOfHasSheafify AddCommGrpCat AddCommGrpCat.instCategory of_isIso SheafOfModules.GeneratingSections.ofEpi CategoryTheory.Limits.kernel SheafOfModules SheafOfModules.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms SheafOfModules.instPreadditive SheafOfModules.free SheafOfModules.GeneratingSections.I generators SheafOfModules.GeneratingSections.π CategoryTheory.Iso.hom CategoryTheory.Iso.trans CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.symm CategoryTheory.Limits.kernelCompMono CategoryTheory.eqToIso	—	CategoryTheory.instHasWeakSheafifyOfHasSheafify
quasicoherentData_I 📖	mathematical	CategoryTheory.GrothendieckTopology.HasSheafCompose CategoryTheory.Over CategoryTheory.instCategoryOver RingCat RingCat.instCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.GrothendieckTopology.over CategoryTheory.forget₂ RingHom RingCat.carrier Semiring.toNonAssocSemiring Ring.toSemiring RingCat.ring RingHom.instFunLike RingCat.instConcreteCategoryRingHomCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier RingCat.hasForgetToAddCommGrp CategoryTheory.HasSheafify CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective	SheafOfModules.QuasicoherentData.I CategoryTheory.instHasWeakSheafifyOfHasSheafify quasicoherentData	—	CategoryTheory.instHasWeakSheafifyOfHasSheafify
quasicoherentData_X 📖	mathematical	CategoryTheory.GrothendieckTopology.HasSheafCompose CategoryTheory.Over CategoryTheory.instCategoryOver RingCat RingCat.instCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.GrothendieckTopology.over CategoryTheory.forget₂ RingHom RingCat.carrier Semiring.toNonAssocSemiring Ring.toSemiring RingCat.ring RingHom.instFunLike RingCat.instConcreteCategoryRingHomCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier RingCat.hasForgetToAddCommGrp CategoryTheory.HasSheafify CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective	SheafOfModules.QuasicoherentData.X CategoryTheory.instHasWeakSheafifyOfHasSheafify quasicoherentData	—	CategoryTheory.instHasWeakSheafifyOfHasSheafify
quasicoherentData_presentation 📖	mathematical	CategoryTheory.GrothendieckTopology.HasSheafCompose CategoryTheory.Over CategoryTheory.instCategoryOver RingCat RingCat.instCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.GrothendieckTopology.over CategoryTheory.forget₂ RingHom RingCat.carrier Semiring.toNonAssocSemiring Ring.toSemiring RingCat.ring RingHom.instFunLike RingCat.instConcreteCategoryRingHomCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier RingCat.hasForgetToAddCommGrp CategoryTheory.HasSheafify CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective	SheafOfModules.QuasicoherentData.presentation CategoryTheory.instHasWeakSheafifyOfHasSheafify quasicoherentData map CategoryTheory.Sheaf.over SheafOfModules.pushforward CategoryTheory.Over.forget CategoryTheory.GrothendieckTopology.instIsContinuousOverForgetOver CategoryTheory.CategoryStruct.id CategoryTheory.Sheaf CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Iso.refl SheafOfModules SheafOfModules.instCategory CategoryTheory.Functor.obj SheafOfModules.unit	—	CategoryTheory.instHasWeakSheafifyOfHasSheafify CategoryTheory.GrothendieckTopology.instIsContinuousOverForgetOver

SheafOfModules.Presentation.IsFinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_relations 📖	mathematical	—	Finite SheafOfModules.GeneratingSections.I CategoryTheory.Limits.kernel SheafOfModules SheafOfModules.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms SheafOfModules.instPreadditive SheafOfModules.free SheafOfModules.Presentation.generators SheafOfModules.GeneratingSections.π SheafOfModules.hasLimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero small_subtype small_Pi CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Functor.comp ModuleCat RingCat.carrier Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Sheaf.val RingCat.ring ModuleCat.moduleCategory SheafOfModules.evaluation CategoryTheory.forget LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier UnivLE.small univLE_of_max UnivLE.self Set Set.instMembership CategoryTheory.Functor.sections AddCommGrpCat.hasLimitsOfShape SheafOfModules.Presentation.relations	—	—
isFiniteType_generators 📖	mathematical	—	SheafOfModules.GeneratingSections.IsFiniteType SheafOfModules.Presentation.generators	—	—

SheafOfModules.QuasicoherentData

Definitions

Name	Category	Theorems
I 📖	CompOp	3 math math: coversTop, localGeneratorsData_I, SheafOfModules.Presentation.quasicoherentData_I
IsFinitePresentation 📖	CompData	1 math math: SheafOfModules.IsFinitePresentation.exists_quasicoherentData
X 📖	CompOp	5 math math: localGeneratorsData_generators, coversTop, IsFinitePresentation.isFinite_presentation, localGeneratorsData_X, SheafOfModules.Presentation.quasicoherentData_X
bind 📖	CompOp	—
localGeneratorsData 📖	CompOp	4 math math: localGeneratorsData_generators, instIsFiniteTypeLocalGeneratorsDataOfIsFinitePresentation, localGeneratorsData_X, localGeneratorsData_I
presentation 📖	CompOp	3 math math: localGeneratorsData_generators, IsFinitePresentation.isFinite_presentation, SheafOfModules.Presentation.quasicoherentData_presentation
shrink 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coversTop 📖	mathematical	CategoryTheory.GrothendieckTopology.HasSheafCompose CategoryTheory.Over CategoryTheory.instCategoryOver RingCat RingCat.instCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.GrothendieckTopology.over CategoryTheory.forget₂ RingHom RingCat.carrier Semiring.toNonAssocSemiring Ring.toSemiring RingCat.ring RingHom.instFunLike RingCat.instConcreteCategoryRingHomCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier RingCat.hasForgetToAddCommGrp CategoryTheory.HasWeakSheafify CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective	CategoryTheory.GrothendieckTopology.CoversTop I X	—	—
instIsFiniteTypeLocalGeneratorsDataOfIsFinitePresentation 📖	mathematical	CategoryTheory.GrothendieckTopology.HasSheafCompose CategoryTheory.Over CategoryTheory.instCategoryOver RingCat RingCat.instCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.GrothendieckTopology.over CategoryTheory.forget₂ RingHom RingCat.carrier Semiring.toNonAssocSemiring Ring.toSemiring RingCat.ring RingHom.instFunLike RingCat.instConcreteCategoryRingHomCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier RingCat.hasForgetToAddCommGrp CategoryTheory.HasWeakSheafify CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective	SheafOfModules.LocalGeneratorsData.IsFiniteType localGeneratorsData	—	SheafOfModules.Presentation.IsFinite.isFiniteType_generators IsFinitePresentation.isFinite_presentation
isQuasicoherent 📖	mathematical	CategoryTheory.GrothendieckTopology.HasSheafCompose CategoryTheory.Over CategoryTheory.instCategoryOver RingCat RingCat.instCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.GrothendieckTopology.over CategoryTheory.forget₂ RingHom RingCat.carrier Semiring.toNonAssocSemiring Ring.toSemiring RingCat.ring RingHom.instFunLike RingCat.instConcreteCategoryRingHomCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier RingCat.hasForgetToAddCommGrp CategoryTheory.HasWeakSheafify CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective	SheafOfModules.IsQuasicoherent	—	—
localGeneratorsData_I 📖	mathematical	CategoryTheory.GrothendieckTopology.HasSheafCompose CategoryTheory.Over CategoryTheory.instCategoryOver RingCat RingCat.instCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.GrothendieckTopology.over CategoryTheory.forget₂ RingHom RingCat.carrier Semiring.toNonAssocSemiring Ring.toSemiring RingCat.ring RingHom.instFunLike RingCat.instConcreteCategoryRingHomCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier RingCat.hasForgetToAddCommGrp CategoryTheory.HasWeakSheafify CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective	SheafOfModules.LocalGeneratorsData.I localGeneratorsData I	—	—
localGeneratorsData_X 📖	mathematical	CategoryTheory.GrothendieckTopology.HasSheafCompose CategoryTheory.Over CategoryTheory.instCategoryOver RingCat RingCat.instCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.GrothendieckTopology.over CategoryTheory.forget₂ RingHom RingCat.carrier Semiring.toNonAssocSemiring Ring.toSemiring RingCat.ring RingHom.instFunLike RingCat.instConcreteCategoryRingHomCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier RingCat.hasForgetToAddCommGrp CategoryTheory.HasWeakSheafify CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective	SheafOfModules.LocalGeneratorsData.X localGeneratorsData X	—	—
localGeneratorsData_generators 📖	mathematical	CategoryTheory.GrothendieckTopology.HasSheafCompose CategoryTheory.Over CategoryTheory.instCategoryOver RingCat RingCat.instCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.GrothendieckTopology.over CategoryTheory.forget₂ RingHom RingCat.carrier Semiring.toNonAssocSemiring Ring.toSemiring RingCat.ring RingHom.instFunLike RingCat.instConcreteCategoryRingHomCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier RingCat.hasForgetToAddCommGrp CategoryTheory.HasWeakSheafify CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective	SheafOfModules.LocalGeneratorsData.generators localGeneratorsData SheafOfModules.Presentation.generators X CategoryTheory.Sheaf.over SheafOfModules.over presentation	—	—

SheafOfModules.QuasicoherentData.IsFinitePresentation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isFinite_presentation 📖	mathematical	CategoryTheory.GrothendieckTopology.HasSheafCompose CategoryTheory.Over CategoryTheory.instCategoryOver RingCat RingCat.instCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.GrothendieckTopology.over CategoryTheory.forget₂ RingHom RingCat.carrier Semiring.toNonAssocSemiring Ring.toSemiring RingCat.ring RingHom.instFunLike RingCat.instConcreteCategoryRingHomCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier RingCat.hasForgetToAddCommGrp CategoryTheory.HasWeakSheafify CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective	SheafOfModules.Presentation.IsFinite SheafOfModules.QuasicoherentData.X CategoryTheory.Sheaf.over SheafOfModules.over SheafOfModules.QuasicoherentData.presentation	—	—

---

← Back to Index