Documentation Verification Report

Generators

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

Statistics

Metric	Count
Definitions `Generators`, `GeneratingSections`, `I`, `IsFiniteType`, `equivOfIso`, `ofEpi`, `s`, `π`, `IsFiniteType`, `LocalGeneratorsData`, `I`, `IsFiniteType`, `X`, `generators`, `localGeneratorsDataOfIsFiniteType`	15
Theorems `finite`, `epi`, `ofEpi_I`, `ofEpi_s`, `ofEpi_π`, `opEpi_comp`, `opEpi_id`, `exists_localGeneratorsData`, `isFiniteType`, `coversTop`	10
Total	25

Algebra

Definitions

Name	Category	Theorems
`Generators` 📖	CompData	1 math math: `FiniteType.iff_exists_generators`

SheafOfModules

Definitions

Name	Category	Theorems
`GeneratingSections` 📖	CompData	—
`IsFiniteType` 📖	CompData	1 math math: `instIsFiniteTypeOfIsFinitePresentation`
`LocalGeneratorsData` 📖	CompData	—
`localGeneratorsDataOfIsFiniteType` 📖	CompOp	—

SheafOfModules.GeneratingSections

Definitions

Name	Category	Theorems
`I` 📖	CompOp	14 math math: `ofEpi_I`, `epi`, `IsFiniteType.finite`, `SheafOfModules.Presentation.map_relations_I`, `SheafOfModules.Presentation.mapRelations_mapGenerators`, `SheafOfModules.relationsOfIsCokernelFree_I`, `SheafOfModules.Presentation.of_isIso_relations`, `SheafOfModules.Presentation.mapRelations_mapGenerators_assoc`, `ofEpi_π`, `SheafOfModules.relationsOfIsCokernelFree_s`, `SheafOfModules.Presentation.map_generators_I`, `SheafOfModules.Presentation.IsFinite.finite_relations`, `SheafOfModules.Presentation.map_π_eq`, `SheafOfModules.generatorsOfIsCokernelFree_I`
`IsFiniteType` 📖	CompData	2 math math: `SheafOfModules.Presentation.IsFinite.isFiniteType_generators`, `SheafOfModules.LocalGeneratorsData.IsFiniteType.isFiniteType`
`equivOfIso` 📖	CompOp	—
`ofEpi` 📖	CompOp	7 math math: `ofEpi_I`, `opEpi_comp`, `SheafOfModules.Presentation.of_isIso_relations`, `SheafOfModules.Presentation.of_isIso_generators`, `ofEpi_π`, `ofEpi_s`, `opEpi_id`
`s` 📖	CompOp	5 math math: `epi`, `SheafOfModules.Presentation.map_relations_I`, `SheafOfModules.relationsOfIsCokernelFree_s`, `ofEpi_s`, `SheafOfModules.generatorsOfIsCokernelFree_s`
`π` 📖	CompOp	10 math math: `SheafOfModules.Presentation.map_relations_I`, `SheafOfModules.Presentation.mapRelations_mapGenerators`, `SheafOfModules.relationsOfIsCokernelFree_I`, `SheafOfModules.Presentation.of_isIso_relations`, `SheafOfModules.Presentation.mapRelations_mapGenerators_assoc`, `ofEpi_π`, `SheafOfModules.relationsOfIsCokernelFree_s`, `SheafOfModules.generatorsOfIsCokernelFree_π`, `SheafOfModules.Presentation.IsFinite.finite_relations`, `SheafOfModules.Presentation.map_π_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epi` 📖	mathematical	—	`CategoryTheory.Epi` `SheafOfModules` `SheafOfModules.instCategory` `SheafOfModules.free` `I` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `SheafOfModules.freeHomEquiv` `s`	—	—
`ofEpi_I` 📖	mathematical	—	`I` `ofEpi`	—	—
`ofEpi_s` 📖	mathematical	—	`s` `ofEpi` `SheafOfModules.sectionsMap`	—	—
`ofEpi_π` 📖	mathematical	—	`π` `ofEpi` `CategoryTheory.CategoryStruct.comp` `SheafOfModules` `CategoryTheory.Category.toCategoryStruct` `SheafOfModules.instCategory` `SheafOfModules.free` `I`	—	`SheafOfModules.freeHomEquiv_symm_comp`
`opEpi_comp` 📖	mathematical	—	`ofEpi` `CategoryTheory.CategoryStruct.comp` `SheafOfModules` `CategoryTheory.Category.toCategoryStruct` `SheafOfModules.instCategory` `CategoryTheory.epi_comp`	—	`CategoryTheory.epi_comp`
`opEpi_id` 📖	mathematical	—	`ofEpi` `CategoryTheory.CategoryStruct.id` `SheafOfModules` `CategoryTheory.Category.toCategoryStruct` `SheafOfModules.instCategory` `CategoryTheory.instEpiId`	—	`CategoryTheory.instEpiId`

SheafOfModules.GeneratingSections.IsFiniteType

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite` 📖	mathematical	—	`Finite` `SheafOfModules.GeneratingSections.I`	—	—

SheafOfModules.IsFiniteType

Theorems

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

SheafOfModules.LocalGeneratorsData

Definitions

Name	Category	Theorems
`I` 📖	CompOp	2 math math: `coversTop`, `SheafOfModules.QuasicoherentData.localGeneratorsData_I`
`IsFiniteType` 📖	CompData	2 math math: `SheafOfModules.IsFiniteType.exists_localGeneratorsData`, `SheafOfModules.QuasicoherentData.instIsFiniteTypeLocalGeneratorsDataOfIsFinitePresentation`
`X` 📖	CompOp	3 math math: `SheafOfModules.QuasicoherentData.localGeneratorsData_X`, `coversTop`, `IsFiniteType.isFiniteType`
`generators` 📖	CompOp	2 math math: `SheafOfModules.QuasicoherentData.localGeneratorsData_generators`, `IsFiniteType.isFiniteType`

Theorems

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

SheafOfModules.LocalGeneratorsData.IsFiniteType

Theorems

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

---

← Back to Index