Documentation Verification Report

Pullback

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

Statistics

Metric	Count
Definitions `pullback`, `pullbackComp`, `pullbackId`, `pullbackObjIsDefined`, `pullbackPushforwardAdjunction`, `pushforwardCompCoyonedaFreeYonedaCorepresentableBy`	6
Theorems `instIsRightAdjointPushforward`, `instIsRightAdjointPushforwardCompFunctorOppositeRingCatWhiskerLeftOp`, `instIsRightAdjointPushforwardIdFunctorOppositeRingCat`, `pullbackObjIsDefined_eq_top`, `pullbackObjIsDefined_free_yoneda`, `pullback_assoc`, `pullback_comp_id`, `pullback_id_comp`	8
Total	14

PresheafOfModules

Definitions

Name	Category	Theorems
`pullback` 📖	CompOp	3 math math: `pullback_id_comp`, `pullback_comp_id`, `pullback_assoc`
`pullbackComp` 📖	CompOp	3 math math: `pullback_id_comp`, `pullback_comp_id`, `pullback_assoc`
`pullbackId` 📖	CompOp	2 math math: `pullback_id_comp`, `pullback_comp_id`
`pullbackObjIsDefined` 📖	CompOp	2 math math: `pullbackObjIsDefined_free_yoneda`, `pullbackObjIsDefined_eq_top`
`pullbackPushforwardAdjunction` 📖	CompOp	—
`pushforwardCompCoyonedaFreeYonedaCorepresentableBy` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsRightAdjointPushforward` 📖	mathematical	—	`CategoryTheory.Functor.IsRightAdjoint` `PresheafOfModules` `instCategory` `pushforward`	—	`CategoryTheory.Functor.isRightAdjoint_of_leftAdjointObjIsDefined_eq_top` `pullbackObjIsDefined_eq_top`
`instIsRightAdjointPushforwardCompFunctorOppositeRingCatWhiskerLeftOp` 📖	mathematical	—	`CategoryTheory.Functor.IsRightAdjoint` `PresheafOfModules` `instCategory` `pushforward` `CategoryTheory.Functor.comp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `RingCat` `RingCat.instCategory` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.op` `CategoryTheory.Functor.whiskerLeft`	—	`CategoryTheory.Functor.isRightAdjoint_of_iso` `CategoryTheory.Functor.isRightAdjoint_comp`
`instIsRightAdjointPushforwardIdFunctorOppositeRingCat` 📖	mathematical	—	`CategoryTheory.Functor.IsRightAdjoint` `PresheafOfModules` `instCategory` `pushforward` `CategoryTheory.Functor.id` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `RingCat` `RingCat.instCategory` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category`	—	`CategoryTheory.Functor.isRightAdjoint_of_iso` `CategoryTheory.Functor.isRightAdjoint_of_isEquivalence` `CategoryTheory.Functor.isEquivalence_refl`
`pullbackObjIsDefined_eq_top` 📖	mathematical	—	`pullbackObjIsDefined` `Top.top` `CategoryTheory.ObjectProperty` `PresheafOfModules` `CategoryTheory.Category.toCategoryStruct` `instCategory` `Pi.instTopForall` `BooleanAlgebra.toTop` `Prop.instBooleanAlgebra`	—	`CategoryTheory.Functor.leftAdjointObjIsDefined_of_isColimit` `hasLimit` `small_subtype` `small_Pi` `UnivLE.small` `univLE_of_max` `UnivLE.self` `hasColimitsOfShape` `AddCommGrpCat.hasColimitsOfShape` `CategoryTheory.Functor.leftAdjointObjIsDefined_colimit` `CategoryTheory.instSmallDiscrete` `pullbackObjIsDefined_free_yoneda`
`pullbackObjIsDefined_free_yoneda` 📖	mathematical	—	`pullbackObjIsDefined` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Functor.category` `PresheafOfModules` `instCategory` `free` `CategoryTheory.yoneda`	—	`CategoryTheory.Functor.CorepresentableBy.isCorepresentable`
`pullback_assoc` 📖	mathematical	—	`CategoryTheory.Iso.trans` `CategoryTheory.Functor` `PresheafOfModules` `instCategory` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `pullback` `CategoryTheory.CategoryStruct.comp` `Opposite` `CategoryTheory.Category.opposite` `RingCat` `RingCat.instCategory` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.op` `CategoryTheory.Functor.whiskerLeft` `instIsRightAdjointPushforwardCompFunctorOppositeRingCatWhiskerLeftOp` `CategoryTheory.Functor.isoWhiskerLeft` `pullbackComp` `CategoryTheory.Iso.symm` `CategoryTheory.Functor.associator` `CategoryTheory.Functor.isoWhiskerRight`	—	`CategoryTheory.Adjunction.leftAdjointCompIso_assoc` `instIsRightAdjointPushforwardCompFunctorOppositeRingCatWhiskerLeftOp` `pushforward_assoc`
`pullback_comp_id` 📖	mathematical	—	`pullbackComp` `CategoryTheory.Functor.id` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `RingCat` `RingCat.instCategory` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `instIsRightAdjointPushforwardIdFunctorOppositeRingCat` `CategoryTheory.Iso.trans` `PresheafOfModules` `instCategory` `CategoryTheory.Functor.comp` `pullback` `CategoryTheory.Functor.isoWhiskerLeft` `pullbackId` `CategoryTheory.Functor.rightUnitor`	—	`CategoryTheory.Adjunction.leftAdjointCompIso_comp_id` `instIsRightAdjointPushforwardIdFunctorOppositeRingCat` `pushforward_id_comp`
`pullback_id_comp` 📖	mathematical	—	`pullbackComp` `CategoryTheory.Functor.id` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `RingCat` `RingCat.instCategory` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `instIsRightAdjointPushforwardIdFunctorOppositeRingCat` `CategoryTheory.Iso.trans` `PresheafOfModules` `instCategory` `CategoryTheory.Functor.comp` `pullback` `CategoryTheory.Functor.isoWhiskerRight` `pullbackId` `CategoryTheory.Functor.leftUnitor`	—	`CategoryTheory.Adjunction.leftAdjointCompIso_id_comp` `instIsRightAdjointPushforwardIdFunctorOppositeRingCat` `pushforward_comp_id`

---

← Back to Index