Documentation Verification Report

Pullback

📁 Source: Mathlib/CategoryTheory/Shift/Pullback.lean

Statistics

Metric	Count
Definitions `commShiftPullback`, `natIsoComp`, `natIsoId`, `PullbackShift`, `adjunction`, `functor`, `natTrans`, `instCategoryPullbackShift`, `instHasShiftPullbackShift`, `instPreadditivePullbackShift`, `pullbackShiftIso`	11
Theorems `commShiftPullback`, `commShiftPullback_iso_eq`, `commShiftPullback`, `instCommShiftPullbackShiftHomFunctorNatIsoComp`, `instCommShiftPullbackShiftHomFunctorNatIsoId`, `adjunction_counit`, `adjunction_unit`, `instAdditivePullbackShiftShiftFunctorOfCoeAddMonoidHom`, `instHasZeroObjectPullbackShift`, `pullbackShiftFunctorAdd'_hom_app`, `pullbackShiftFunctorAdd'_inv_app`, `pullbackShiftFunctorZero'_hom_app`, `pullbackShiftFunctorZero'_inv_app`, `pullbackShiftFunctorZero_hom_app`, `pullbackShiftFunctorZero_inv_app`	15
Total	26

CategoryTheory

Definitions

Name	Category	Theorems
`PullbackShift` 📖	CompOp	19 math math: `PullbackShift.adjunction_counit`, `NatTrans.instCommShiftPullbackShiftHomFunctorNatIsoComp`, `NatTrans.instCommShiftPullbackShiftHomFunctorNatIsoId`, `pullbackShiftFunctorZero_inv_app`, `PullbackShift.adjunction_unit`, `NatTrans.commShiftPullback`, `Adjunction.commShiftPullback`, `pullbackShiftFunctorZero'_hom_app`, `pullbackShiftFunctorZero_hom_app`, `Functor.commShiftPullback_iso_eq`, `pullbackShiftFunctorAdd'_hom_app`, `instAdditivePullbackShiftShiftFunctorOfCoeAddMonoidHom`, `instHasZeroObjectPullbackShift`, `pullbackShiftFunctorZero'_inv_app`, `CommShift₂Setup.z_zero₂`, `pullbackShiftFunctorAdd'_inv_app`, `CommShift₂Setup.z_zero₁`, `CommShift₂Setup.hε`, `CommShift₂Setup.int_z`
`instCategoryPullbackShift` 📖	CompOp	19 math math: `PullbackShift.adjunction_counit`, `NatTrans.instCommShiftPullbackShiftHomFunctorNatIsoComp`, `NatTrans.instCommShiftPullbackShiftHomFunctorNatIsoId`, `pullbackShiftFunctorZero_inv_app`, `PullbackShift.adjunction_unit`, `NatTrans.commShiftPullback`, `Adjunction.commShiftPullback`, `pullbackShiftFunctorZero'_hom_app`, `pullbackShiftFunctorZero_hom_app`, `Functor.commShiftPullback_iso_eq`, `pullbackShiftFunctorAdd'_hom_app`, `instAdditivePullbackShiftShiftFunctorOfCoeAddMonoidHom`, `instHasZeroObjectPullbackShift`, `pullbackShiftFunctorZero'_inv_app`, `CommShift₂Setup.z_zero₂`, `pullbackShiftFunctorAdd'_inv_app`, `CommShift₂Setup.z_zero₁`, `CommShift₂Setup.hε`, `CommShift₂Setup.int_z`
`instHasShiftPullbackShift` 📖	CompOp	16 math math: `NatTrans.instCommShiftPullbackShiftHomFunctorNatIsoComp`, `NatTrans.instCommShiftPullbackShiftHomFunctorNatIsoId`, `pullbackShiftFunctorZero_inv_app`, `NatTrans.commShiftPullback`, `Adjunction.commShiftPullback`, `pullbackShiftFunctorZero'_hom_app`, `pullbackShiftFunctorZero_hom_app`, `Functor.commShiftPullback_iso_eq`, `pullbackShiftFunctorAdd'_hom_app`, `instAdditivePullbackShiftShiftFunctorOfCoeAddMonoidHom`, `pullbackShiftFunctorZero'_inv_app`, `CommShift₂Setup.z_zero₂`, `pullbackShiftFunctorAdd'_inv_app`, `CommShift₂Setup.z_zero₁`, `CommShift₂Setup.hε`, `CommShift₂Setup.int_z`
`instPreadditivePullbackShift` 📖	CompOp	2 math math: `instAdditivePullbackShiftShiftFunctorOfCoeAddMonoidHom`, `CommShift₂Setup.int_z`
`pullbackShiftIso` 📖	CompOp	7 math math: `pullbackShiftFunctorZero_inv_app`, `pullbackShiftFunctorZero'_hom_app`, `pullbackShiftFunctorZero_hom_app`, `Functor.commShiftPullback_iso_eq`, `pullbackShiftFunctorAdd'_hom_app`, `pullbackShiftFunctorZero'_inv_app`, `pullbackShiftFunctorAdd'_inv_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instAdditivePullbackShiftShiftFunctorOfCoeAddMonoidHom` 📖	mathematical	—	`Functor.Additive` `PullbackShift` `instCategoryPullbackShift` `instPreadditivePullbackShift` `shiftFunctor` `instHasShiftPullbackShift`	—	—
`instHasZeroObjectPullbackShift` 📖	mathematical	—	`Limits.HasZeroObject` `PullbackShift` `instCategoryPullbackShift`	—	—
`pullbackShiftFunctorAdd'_hom_app` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike`	`NatTrans.app` `PullbackShift` `instCategoryPullbackShift` `shiftFunctor` `instHasShiftPullbackShift` `Functor.comp` `Iso.hom` `Functor` `Functor.category` `shiftFunctorAdd'` `CategoryStruct.comp` `Category.toCategoryStruct` `Functor.obj` `pullbackShiftIso` `Iso.inv` `Functor.map`	—	`cancel_epi` `epi_of_strongEpi` `strongEpi_of_isIso` `NatIso.inv_app_isIso` `Iso.inv_hom_id_app` `pullbackShiftFunctorAdd'_inv_app` `Category.assoc` `Iso.inv_hom_id_app_assoc` `Iso.hom_inv_id_app_assoc` `Functor.map_comp` `Iso.hom_inv_id_app` `Functor.map_id`
`pullbackShiftFunctorAdd'_inv_app` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike`	`NatTrans.app` `PullbackShift` `instCategoryPullbackShift` `Functor.comp` `shiftFunctor` `instHasShiftPullbackShift` `Iso.inv` `Functor` `Functor.category` `shiftFunctorAdd'` `CategoryStruct.comp` `Category.toCategoryStruct` `Functor.obj` `Functor.map` `Iso.hom` `pullbackShiftIso`	—	`NatTrans.naturality_assoc` `Functor.map_id` `Category.id_comp` `shiftFunctorAdd'_eq_shiftFunctorAdd` `AddMonoidHom.map_add` `Discrete.addMonoidalFunctor_μ` `eqToHom_map`
`pullbackShiftFunctorZero'_hom_app` 📖	mathematical	—	`NatTrans.app` `PullbackShift` `instCategoryPullbackShift` `shiftFunctor` `instHasShiftPullbackShift` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Functor.id` `Iso.hom` `Functor` `Functor.category` `shiftFunctorZero` `CategoryStruct.comp` `Category.toCategoryStruct` `Functor.obj` `DFunLike.coe` `AddMonoidHom` `AddMonoidHom.instFunLike` `pullbackShiftIso` `shiftFunctorZero'`	—	`cancel_epi` `epi_of_strongEpi` `strongEpi_of_isIso` `NatIso.inv_app_isIso` `Iso.inv_hom_id_app` `pullbackShiftFunctorZero'_inv_app` `Category.assoc` `Iso.inv_hom_id_app_assoc`
`pullbackShiftFunctorZero'_inv_app` 📖	mathematical	—	`NatTrans.app` `PullbackShift` `instCategoryPullbackShift` `Functor.id` `shiftFunctor` `instHasShiftPullbackShift` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Iso.inv` `Functor` `Functor.category` `shiftFunctorZero` `CategoryStruct.comp` `Category.toCategoryStruct` `Functor.obj` `DFunLike.coe` `AddMonoidHom` `AddMonoidHom.instFunLike` `shiftFunctorZero'` `pullbackShiftIso`	—	`pullbackShiftFunctorZero_inv_app` `Functor.congr_obj` `eqToHom_app` `Category.assoc` `Category.comp_id`
`pullbackShiftFunctorZero_hom_app` 📖	mathematical	—	`NatTrans.app` `PullbackShift` `instCategoryPullbackShift` `shiftFunctor` `instHasShiftPullbackShift` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Functor.id` `Iso.hom` `Functor` `Functor.category` `shiftFunctorZero` `CategoryStruct.comp` `Category.toCategoryStruct` `Functor.obj` `pullbackShiftIso`	—	`cancel_epi` `epi_of_strongEpi` `strongEpi_of_isIso` `NatIso.inv_app_isIso` `Iso.inv_hom_id_app` `pullbackShiftFunctorZero_inv_app` `Category.assoc` `Iso.inv_hom_id_app_assoc`
`pullbackShiftFunctorZero_inv_app` 📖	mathematical	—	`NatTrans.app` `PullbackShift` `instCategoryPullbackShift` `Functor.id` `shiftFunctor` `instHasShiftPullbackShift` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Iso.inv` `Functor` `Functor.category` `shiftFunctorZero` `CategoryStruct.comp` `Category.toCategoryStruct` `Functor.obj` `pullbackShiftIso`	—	`AddMonoidHom.map_zero` `eqToHom_map`

CategoryTheory.Adjunction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commShiftPullback` 📖	mathematical	—	`CommShift` `CategoryTheory.PullbackShift` `CategoryTheory.instCategoryPullbackShift` `CategoryTheory.PullbackShift.functor` `CategoryTheory.PullbackShift.adjunction` `CategoryTheory.instHasShiftPullbackShift` `CategoryTheory.Functor.commShiftPullback`	—	`CategoryTheory.NatTrans.CommShift.comp` `CategoryTheory.NatTrans.instCommShiftPullbackShiftHomFunctorNatIsoId` `CategoryTheory.NatTrans.commShiftPullback` `CommShift.commShift_unit` `CategoryTheory.NatTrans.instCommShiftPullbackShiftHomFunctorNatIsoComp` `CategoryTheory.NatTrans.CommShift.of_iso_inv` `CommShift.commShift_counit`

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`commShiftPullback` 📖	CompOp	5 math math: `CategoryTheory.NatTrans.instCommShiftPullbackShiftHomFunctorNatIsoComp`, `CategoryTheory.NatTrans.instCommShiftPullbackShiftHomFunctorNatIsoId`, `CategoryTheory.NatTrans.commShiftPullback`, `CategoryTheory.Adjunction.commShiftPullback`, `commShiftPullback_iso_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commShiftPullback_iso_eq` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike`	`CommShift.commShiftIso` `CategoryTheory.PullbackShift` `CategoryTheory.instCategoryPullbackShift` `CategoryTheory.PullbackShift.functor` `CategoryTheory.instHasShiftPullbackShift` `commShiftPullback` `CategoryTheory.Iso.trans` `CategoryTheory.Functor` `category` `comp` `CategoryTheory.shiftFunctor` `isoWhiskerRight` `CategoryTheory.pullbackShiftIso` `isoWhiskerLeft` `CategoryTheory.Iso.symm`	—	—

CategoryTheory.NatTrans

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commShiftPullback` 📖	mathematical	—	`CommShift` `CategoryTheory.PullbackShift` `CategoryTheory.instCategoryPullbackShift` `CategoryTheory.PullbackShift.functor` `CategoryTheory.PullbackShift.natTrans` `CategoryTheory.instHasShiftPullbackShift` `CategoryTheory.Functor.commShiftPullback`	—	`ext'` `CategoryTheory.Functor.commShiftPullback_iso_eq` `CategoryTheory.Category.assoc` `naturality_assoc` `naturality`
`instCommShiftPullbackShiftHomFunctorNatIsoComp` 📖	mathematical	—	`CommShift` `CategoryTheory.PullbackShift` `CategoryTheory.instCategoryPullbackShift` `CategoryTheory.PullbackShift.functor` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `PullbackShift.natIsoComp` `CategoryTheory.instHasShiftPullbackShift` `CategoryTheory.Functor.commShiftPullback` `CategoryTheory.Functor.CommShift.comp`	—	`ext'` `CategoryTheory.Functor.commShiftPullback_iso_eq` `CategoryTheory.Functor.commShiftIso_comp_hom_app` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.id_comp` `CategoryTheory.Iso.inv_hom_id_app`
`instCommShiftPullbackShiftHomFunctorNatIsoId` 📖	mathematical	—	`CommShift` `CategoryTheory.PullbackShift` `CategoryTheory.instCategoryPullbackShift` `CategoryTheory.Functor.id` `CategoryTheory.PullbackShift.functor` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `PullbackShift.natIsoId` `CategoryTheory.instHasShiftPullbackShift` `CategoryTheory.Functor.CommShift.id` `CategoryTheory.Functor.commShiftPullback`	—	`ext'` `CategoryTheory.Functor.whiskerRight_id'` `CategoryTheory.Category.comp_id` `CategoryTheory.Functor.commShiftIso_id_hom_app` `CategoryTheory.Functor.commShiftPullback_iso_eq` `CategoryTheory.Category.id_comp` `CategoryTheory.Iso.hom_inv_id_app`

CategoryTheory.NatTrans.PullbackShift

Definitions

Name	Category	Theorems
`natIsoComp` 📖	CompOp	3 math math: `CategoryTheory.PullbackShift.adjunction_counit`, `CategoryTheory.NatTrans.instCommShiftPullbackShiftHomFunctorNatIsoComp`, `CategoryTheory.PullbackShift.adjunction_unit`
`natIsoId` 📖	CompOp	3 math math: `CategoryTheory.PullbackShift.adjunction_counit`, `CategoryTheory.NatTrans.instCommShiftPullbackShiftHomFunctorNatIsoId`, `CategoryTheory.PullbackShift.adjunction_unit`

CategoryTheory.PullbackShift

Definitions

Name	Category	Theorems
`adjunction` 📖	CompOp	3 math math: `adjunction_counit`, `adjunction_unit`, `CategoryTheory.Adjunction.commShiftPullback`
`functor` 📖	CompOp	7 math math: `adjunction_counit`, `CategoryTheory.NatTrans.instCommShiftPullbackShiftHomFunctorNatIsoComp`, `CategoryTheory.NatTrans.instCommShiftPullbackShiftHomFunctorNatIsoId`, `adjunction_unit`, `CategoryTheory.NatTrans.commShiftPullback`, `CategoryTheory.Adjunction.commShiftPullback`, `CategoryTheory.Functor.commShiftPullback_iso_eq`
`natTrans` 📖	CompOp	3 math math: `adjunction_counit`, `adjunction_unit`, `CategoryTheory.NatTrans.commShiftPullback`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjunction_counit` 📖	mathematical	—	`CategoryTheory.Adjunction.counit` `CategoryTheory.PullbackShift` `CategoryTheory.instCategoryPullbackShift` `functor` `adjunction` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.Iso.inv` `CategoryTheory.NatTrans.PullbackShift.natIsoComp` `natTrans` `CategoryTheory.NatTrans.PullbackShift.natIsoId`	—	—
`adjunction_unit` 📖	mathematical	—	`CategoryTheory.Adjunction.unit` `CategoryTheory.PullbackShift` `CategoryTheory.instCategoryPullbackShift` `functor` `adjunction` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.NatTrans.PullbackShift.natIsoId` `natTrans` `CategoryTheory.NatTrans.PullbackShift.natIsoComp`	—	—

---

← Back to Index