Documentation Verification Report

Generator

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

Statistics

Metric	Count
Definitions `freeYoneda`, `fromFreeYoneda`, `elementsMk`, `freeYoneda`, `freeYonedaCoproduct`, `freeYonedaCoproductMk`, `freeYonedaCoproductsCokernelCofork`, `freeYonedaEquiv`, `fromFreeYonedaCoproduct`, `isColimitFreeYonedaCoproductsCokernelCofork`, `toFreeYonedaCoproduct`, `ιFreeYonedaCoproduct`	12
Theorems `fromFreeYoneda_app_apply`, `instSmall`, `isDetecting`, `isSeparating`, `freeYonedaEquiv_comp`, `freeYonedaEquiv_symm_app`, `fromFreeYonedaCoproduct_app_mk`, `instEpiFromFreeYonedaCoproduct`, `toFreeYonedaCoproduct_fromFreeYonedaCoproduct`, `toFreeYonedaCoproduct_fromFreeYonedaCoproduct_assoc`, `wellPowered`, `ι_fromFreeYonedaCoproduct`, `ι_fromFreeYonedaCoproduct_apply`, `ι_fromFreeYonedaCoproduct_assoc`	14
Total	26

PresheafOfModules

Definitions

Name	Category	Theorems
`elementsMk` 📖	CompOp	—
`freeYoneda` 📖	CompOp	3 math math: `freeYoneda.isSeparating`, `freeYoneda.isDetecting`, `freeYoneda.instSmall`
`freeYonedaCoproduct` 📖	CompOp	7 math math: `toFreeYonedaCoproduct_fromFreeYonedaCoproduct`, `ι_fromFreeYonedaCoproduct`, `toFreeYonedaCoproduct_fromFreeYonedaCoproduct_assoc`, `ι_fromFreeYonedaCoproduct_assoc`, `instEpiFromFreeYonedaCoproduct`, `ι_fromFreeYonedaCoproduct_apply`, `fromFreeYonedaCoproduct_app_mk`
`freeYonedaCoproductMk` 📖	CompOp	1 math math: `fromFreeYonedaCoproduct_app_mk`
`freeYonedaCoproductsCokernelCofork` 📖	CompOp	—
`freeYonedaEquiv` 📖	CompOp	2 math math: `freeYonedaEquiv_symm_app`, `freeYonedaEquiv_comp`
`fromFreeYonedaCoproduct` 📖	CompOp	7 math math: `toFreeYonedaCoproduct_fromFreeYonedaCoproduct`, `ι_fromFreeYonedaCoproduct`, `toFreeYonedaCoproduct_fromFreeYonedaCoproduct_assoc`, `ι_fromFreeYonedaCoproduct_assoc`, `instEpiFromFreeYonedaCoproduct`, `ι_fromFreeYonedaCoproduct_apply`, `fromFreeYonedaCoproduct_app_mk`
`isColimitFreeYonedaCoproductsCokernelCofork` 📖	CompOp	—
`toFreeYonedaCoproduct` 📖	CompOp	2 math math: `toFreeYonedaCoproduct_fromFreeYonedaCoproduct`, `toFreeYonedaCoproduct_fromFreeYonedaCoproduct_assoc`
`ιFreeYonedaCoproduct` 📖	CompOp	3 math math: `ι_fromFreeYonedaCoproduct`, `ι_fromFreeYonedaCoproduct_assoc`, `ι_fromFreeYonedaCoproduct_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`freeYonedaEquiv_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `PresheafOfModules` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `free` `CategoryTheory.yoneda` `ModuleCat.carrier` `RingCat.carrier` `RingCat` `RingCat.instCategory` `Opposite.op` `RingCat.ring` `obj` `EquivLike.toFunLike` `Equiv.instEquivLike` `freeYonedaEquiv` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.ConcreteCategory.hom` `ModuleCat` `ModuleCat.moduleCategory` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `Hom.app`	—	—
`freeYonedaEquiv_symm_app` 📖	mathematical	—	`DFunLike.coe` `obj` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `PresheafOfModules` `instCategory` `free` `CategoryTheory.yoneda` `Opposite.op` `ModuleCat.carrier` `RingCat.carrier` `RingCat` `RingCat.instCategory` `RingCat.ring` `CategoryTheory.ConcreteCategory.hom` `ModuleCat` `ModuleCat.moduleCategory` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `Hom.app` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `freeYonedaEquiv` `ModuleCat.freeMk` `CategoryTheory.CategoryStruct.id` `Opposite.unop`	—	`ModuleCat.freeDesc_apply` `CategoryTheory.op_id` `CategoryTheory.Functor.map_id`
`fromFreeYonedaCoproduct_app_mk` 📖	mathematical	—	`DFunLike.coe` `obj` `freeYonedaCoproduct` `Opposite` `CategoryTheory.Functor.obj` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.comp` `Ab` `AddCommGrpCat.instCategory` `PresheafOfModules` `instCategory` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `toPresheaf` `CategoryTheory.forget` `AddMonoidHom` `AddCommGrpCat.carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGrpCat.str` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `ModuleCat.carrier` `RingCat.carrier` `RingCat` `RingCat.instCategory` `RingCat.ring` `CategoryTheory.ConcreteCategory.hom` `ModuleCat` `ModuleCat.moduleCategory` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `Hom.app` `fromFreeYonedaCoproduct` `freeYonedaCoproductMk`	—	`ι_fromFreeYonedaCoproduct_apply` `Elements.fromFreeYoneda_app_apply`
`instEpiFromFreeYonedaCoproduct` 📖	mathematical	—	`CategoryTheory.Epi` `PresheafOfModules` `instCategory` `freeYonedaCoproduct` `fromFreeYonedaCoproduct`	—	`epi_of_surjective`
`toFreeYonedaCoproduct_fromFreeYonedaCoproduct` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `PresheafOfModules` `CategoryTheory.Category.toCategoryStruct` `instCategory` `freeYonedaCoproduct` `CategoryTheory.Limits.kernel` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instPreadditive` `fromFreeYonedaCoproduct` `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` `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` `toFreeYonedaCoproduct` `instZeroHom`	—	`hasLimit` `small_subtype` `small_Pi` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.kernel.condition` `CategoryTheory.Limits.comp_zero`
`toFreeYonedaCoproduct_fromFreeYonedaCoproduct_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `PresheafOfModules` `CategoryTheory.Category.toCategoryStruct` `instCategory` `freeYonedaCoproduct` `CategoryTheory.Limits.kernel` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instPreadditive` `fromFreeYonedaCoproduct` `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` `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` `toFreeYonedaCoproduct` `instZeroHom`	—	`hasLimit` `small_subtype` `small_Pi` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `toFreeYonedaCoproduct_fromFreeYonedaCoproduct`
`wellPowered` 📖	mathematical	—	`CategoryTheory.WellPowered` `PresheafOfModules` `instCategory` `CategoryTheory.locallySmall_of_univLE` `UnivLE.self`	—	`CategoryTheory.wellPowered_of_isDetecting` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `hasFiniteLimits` `freeYoneda.instSmall` `CategoryTheory.locallySmall_of_univLE` `UnivLE.self` `freeYoneda.isDetecting`
`ι_fromFreeYonedaCoproduct` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `PresheafOfModules` `CategoryTheory.Category.toCategoryStruct` `instCategory` `Elements.freeYoneda` `freeYonedaCoproduct` `ιFreeYonedaCoproduct` `fromFreeYonedaCoproduct` `Elements.fromFreeYoneda`	—	`CategoryTheory.Limits.Sigma.ι_desc`
`ι_fromFreeYonedaCoproduct_apply` 📖	mathematical	—	`DFunLike.coe` `obj` `freeYonedaCoproduct` `ModuleCat.carrier` `RingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `RingCat` `RingCat.instCategory` `RingCat.ring` `CategoryTheory.ConcreteCategory.hom` `ModuleCat` `ModuleCat.moduleCategory` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `Hom.app` `fromFreeYonedaCoproduct` `Elements.freeYoneda` `ιFreeYonedaCoproduct` `Elements.fromFreeYoneda`	—	`CategoryTheory.Functor.congr_map` `ι_fromFreeYonedaCoproduct`
`ι_fromFreeYonedaCoproduct_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `PresheafOfModules` `CategoryTheory.Category.toCategoryStruct` `instCategory` `Elements.freeYoneda` `freeYonedaCoproduct` `ιFreeYonedaCoproduct` `fromFreeYonedaCoproduct` `Elements.fromFreeYoneda`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ι_fromFreeYonedaCoproduct`

PresheafOfModules.Elements

Definitions

Name	Category	Theorems
`freeYoneda` 📖	CompOp	4 math math: `PresheafOfModules.ι_fromFreeYonedaCoproduct`, `PresheafOfModules.ι_fromFreeYonedaCoproduct_assoc`, `fromFreeYoneda_app_apply`, `PresheafOfModules.ι_fromFreeYonedaCoproduct_apply`
`fromFreeYoneda` 📖	CompOp	4 math math: `PresheafOfModules.ι_fromFreeYonedaCoproduct`, `PresheafOfModules.ι_fromFreeYonedaCoproduct_assoc`, `fromFreeYoneda_app_apply`, `PresheafOfModules.ι_fromFreeYonedaCoproduct_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fromFreeYoneda_app_apply` 📖	mathematical	—	`DFunLike.coe` `PresheafOfModules.obj` `freeYoneda` `Opposite` `CategoryTheory.Functor.obj` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.comp` `Ab` `AddCommGrpCat.instCategory` `PresheafOfModules` `PresheafOfModules.instCategory` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `PresheafOfModules.toPresheaf` `CategoryTheory.forget` `AddMonoidHom` `AddCommGrpCat.carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGrpCat.str` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `ModuleCat.carrier` `RingCat.carrier` `RingCat` `RingCat.instCategory` `RingCat.ring` `CategoryTheory.ConcreteCategory.hom` `ModuleCat` `ModuleCat.moduleCategory` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `PresheafOfModules.Hom.app` `fromFreeYoneda` `ModuleCat.freeMk` `CategoryTheory.yoneda` `Opposite.unop` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`PresheafOfModules.freeYonedaEquiv_symm_app`

PresheafOfModules.freeYoneda

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instSmall` 📖	mathematical	—	`CategoryTheory.ObjectProperty.Small` `PresheafOfModules` `PresheafOfModules.instCategory` `PresheafOfModules.freeYoneda`	—	`CategoryTheory.ObjectProperty.instSmallOfObjOfSmall` `UnivLE.small` `UnivLE.self`
`isDetecting` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsDetecting` `PresheafOfModules` `PresheafOfModules.instCategory` `PresheafOfModules.freeYoneda`	—	`CategoryTheory.ObjectProperty.IsSeparating.isDetecting` `CategoryTheory.balanced_of_strongMonoCategory` `CategoryTheory.strongMonoCategory_of_regularMonoCategory` `CategoryTheory.regularMonoCategoryOfNormalMonoCategory` `PresheafOfModules.instIsNormalMonoCategory` `isSeparating`
`isSeparating` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsSeparating` `PresheafOfModules` `PresheafOfModules.instCategory` `PresheafOfModules.freeYoneda`	—	`PresheafOfModules.hom_ext` `ModuleCat.hom_ext` `LinearMap.ext` `Equiv.surjective`

---

← Back to Index