Pushforward

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

Statistics

Metric	Count
Definitions pushforward, pushforwardComp, pushforwardCompToPresheaf, pushforwardId, pushforward₀, pushforward₀CompToPresheaf, pushforward₀_obj	7
Theorems pushforward_assoc, pushforward_comp_id, pushforward_id_comp, pushforward_map_app_apply, pushforward_map_app_apply', pushforward_obj_map_apply, pushforward_obj_map_apply', pushforward_obj_obj, pushforward₀_obj_map, pushforward₀_obj_obj_carrier, pushforward₀_obj_obj_isAddCommGroup, pushforward₀_obj_obj_isModule	12
Total	19

PresheafOfModules

Definitions

Name	Category	Theorems
pushforward 📖	CompOp	13 math math: instIsRightAdjointPushforwardCompFunctorOppositeRingCatWhiskerLeftOp, pushforward_map_app_apply, pushforward_map_app_apply', pushforward_obj_map_apply, SheafOfModules.pushforward_map_val, pushforward_obj_obj, pushforward_assoc, pushforward_obj_map_apply', instIsRightAdjointPushforward, pushforward_id_comp, SheafOfModules.pushforward_obj_val, instIsRightAdjointPushforwardIdFunctorOppositeRingCat, pushforward_comp_id
pushforwardComp 📖	CompOp	3 math math: pushforward_assoc, pushforward_id_comp, pushforward_comp_id
pushforwardCompToPresheaf 📖	CompOp	—
pushforwardId 📖	CompOp	2 math math: pushforward_id_comp, pushforward_comp_id
pushforward₀ 📖	CompOp	2 math math: pushforward_map_app_apply', pushforward_obj_map_apply'
pushforward₀CompToPresheaf 📖	CompOp	—
pushforward₀_obj 📖	CompOp	5 math math: pushforward₀_obj_obj_carrier, pushforward₀_obj_obj_isAddCommGroup, pushforward_obj_obj, pushforward₀_obj_obj_isModule, pushforward₀_obj_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pushforward_assoc 📖	mathematical	—	CategoryTheory.Iso.trans CategoryTheory.Functor PresheafOfModules instCategory CategoryTheory.Functor.category CategoryTheory.Functor.comp pushforward CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.op CategoryTheory.Functor.whiskerLeft CategoryTheory.Functor.isoWhiskerLeft pushforwardComp CategoryTheory.Iso.symm CategoryTheory.Functor.associator CategoryTheory.Functor.isoWhiskerRight	—	CategoryTheory.Iso.ext CategoryTheory.NatTrans.ext' hom_ext ModuleCat.hom_ext LinearMap.ext
pushforward_comp_id 📖	mathematical	—	pushforwardComp CategoryTheory.Functor.id CategoryTheory.CategoryStruct.id CategoryTheory.Functor Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Iso.trans PresheafOfModules instCategory CategoryTheory.Functor.comp pushforward CategoryTheory.Functor.isoWhiskerLeft pushforwardId CategoryTheory.Functor.rightUnitor	—	CategoryTheory.Iso.ext CategoryTheory.NatTrans.ext' hom_ext ModuleCat.hom_ext LinearMap.ext
pushforward_id_comp 📖	mathematical	—	pushforwardComp CategoryTheory.Functor.id CategoryTheory.CategoryStruct.id CategoryTheory.Functor Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Iso.trans PresheafOfModules instCategory CategoryTheory.Functor.comp pushforward CategoryTheory.Functor.isoWhiskerRight pushforwardId CategoryTheory.Functor.leftUnitor	—	CategoryTheory.Iso.ext CategoryTheory.NatTrans.ext' hom_ext ModuleCat.hom_ext LinearMap.ext
pushforward_map_app_apply 📖	mathematical	—	DFunLike.coe LinearMap RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory Ring.toSemiring RingCat.ring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier obj PresheafOfModules instCategory pushforward AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.Hom.hom Hom.app CategoryTheory.Functor.map Opposite.op Opposite.unop CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory ModuleCat.instConcreteCategoryLinearMapIdCarrier	—	—
pushforward_map_app_apply' 📖	mathematical	—	DFunLike.coe LinearMap RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory Ring.toSemiring RingCat.ring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier ModuleCat CategoryTheory.Functor.comp CategoryTheory.Functor.op ModuleCat.moduleCategory ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.NatTrans.app obj PresheafOfModules instCategory pushforward₀ AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule pushforward Opposite.op Opposite.unop LinearMap.instFunLike ModuleCat.Hom.hom Hom.app CategoryTheory.Functor.map CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier	—	—
pushforward_obj_map_apply 📖	mathematical	—	DFunLike.coe LinearMap RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory Ring.toSemiring RingCat.ring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier obj PresheafOfModules instCategory pushforward ModuleCat ModuleCat.moduleCategory ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.Hom.hom map Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom.unop CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier	—	—
pushforward_obj_map_apply' 📖	mathematical	—	DFunLike.coe LinearMap RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory Ring.toSemiring RingCat.ring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier ModuleCat CategoryTheory.Functor.comp CategoryTheory.Functor.op ModuleCat.moduleCategory ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.NatTrans.app obj PresheafOfModules instCategory pushforward₀ CategoryTheory.Functor.map AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule pushforward Opposite.op Opposite.unop LinearMap.instFunLike ModuleCat.Hom.hom map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom.unop CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier	—	—
pushforward_obj_obj 📖	mathematical	—	obj CategoryTheory.Functor.obj PresheafOfModules instCategory pushforward ModuleCat RingCat.carrier Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory Opposite.op Opposite.unop RingCat.ring ModuleCat.moduleCategory ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.op pushforward₀_obj	—	—
pushforward₀_obj_map 📖	mathematical	—	map CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Functor.op pushforward₀_obj CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	—
pushforward₀_obj_obj_carrier 📖	mathematical	—	ModuleCat.carrier RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Functor.comp CategoryTheory.Functor.op RingCat.ring obj pushforward₀_obj	—	—
pushforward₀_obj_obj_isAddCommGroup 📖	mathematical	—	ModuleCat.isAddCommGroup RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Functor.comp CategoryTheory.Functor.op RingCat.ring obj pushforward₀_obj	—	—
pushforward₀_obj_obj_isModule 📖	mathematical	—	ModuleCat.isModule RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Functor.comp CategoryTheory.Functor.op RingCat.ring obj pushforward₀_obj	—	—

---

← Back to Index