PushforwardContinuous

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

Statistics

Metric	Count
Definitions over, overPushforwardOverAdj, pushforward, pushforwardComp, pushforwardCongr, pushforwardId, pushforwardNatIso, pushforwardNatTrans, pushforwardOver, pushforwardPushforwardAdj, pushforwardPushforwardEquivalence	11
Theorems instIsLeftAdjointOverOverRingCatPushforwardIdSheafOver, pushforwardComp_hom_app_val_app, pushforwardComp_inv_app_val_app, pushforwardCongr_hom_app_val_app, pushforwardCongr_inv_app_val_app, pushforwardCongr_symm, pushforwardNatIso_hom, pushforwardNatIso_inv, pushforwardNatTrans_app_val_app, pushforwardNatTrans_app_val_app_apply, pushforwardNatTrans_comp, pushforwardNatTrans_id, pushforwardPushforwardAdj_counit_app_val_app, pushforwardPushforwardAdj_unit_app_val_app, pushforwardPushforwardEquivalence_counit_app_val_app, pushforwardPushforwardEquivalence_unit_app_val_app, pushforward_assoc, pushforward_comp_id, pushforward_id_comp, pushforward_map_val, pushforward_obj_val	21
Total	32

SheafOfModules

Definitions

Name	Category	Theorems
over 📖	CompOp	3 math math: QuasicoherentData.localGeneratorsData_generators, QuasicoherentData.IsFinitePresentation.isFinite_presentation, LocalGeneratorsData.IsFiniteType.isFiniteType
overPushforwardOverAdj 📖	CompOp	—
pushforward 📖	CompOp	31 math math: pushforward_assoc, pushforwardNatIso_inv, pullbackPushforwardAdjunction_homEquiv_pullbackObjUnitToUnit, instIsRightAdjointPushforwardCompSheafRingCatMapSheafPushforwardContinuous, pushforwardComp_inv_app_val_app, pushforwardNatTrans_id, Presentation.quasicoherentData_presentation, pushforwardCongr_hom_app_val_app, pushforwardCongr_inv_app_val_app, conjugateEquiv_pullbackComp_inv, pushforwardPushforwardAdj_unit_app_val_app, pushforward_map_val, pushforwardComp_hom_app_val_app, instIsLeftAdjointOverOverRingCatPushforwardIdSheafOver, pushforwardCongr_symm, unitToPushforwardObjUnit_val_app_apply, pushforwardNatTrans_app_val_app, pullbackPushforwardAdjunction_homEquiv_symm_unitToPushforwardObjUnit, instIsRightAdjointPushforward, pushforward_comp_id, bijective_pushforwardSections, pushforwardPushforwardAdj_counit_app_val_app, conjugateEquiv_pullbackId_hom, pushforwardNatTrans_app_val_app_apply, pushforward_id_comp, pushforwardSections_coe, pushforwardSections_unitHomEquiv, instIsRightAdjointPushforwardIdSheafRingCat, pushforwardNatIso_hom, pushforward_obj_val, pushforwardNatTrans_comp
pushforwardComp 📖	CompOp	6 math math: pushforward_assoc, pushforwardComp_inv_app_val_app, conjugateEquiv_pullbackComp_inv, pushforwardComp_hom_app_val_app, pushforward_comp_id, pushforward_id_comp
pushforwardCongr 📖	CompOp	6 math math: pushforwardNatIso_inv, pushforwardNatTrans_id, pushforwardCongr_hom_app_val_app, pushforwardCongr_inv_app_val_app, pushforwardCongr_symm, pushforwardNatTrans_comp
pushforwardId 📖	CompOp	3 math math: pushforward_comp_id, conjugateEquiv_pullbackId_hom, pushforward_id_comp
pushforwardNatIso 📖	CompOp	2 math math: pushforwardNatIso_inv, pushforwardNatIso_hom
pushforwardNatTrans 📖	CompOp	6 math math: pushforwardNatIso_inv, pushforwardNatTrans_id, pushforwardNatTrans_app_val_app, pushforwardNatTrans_app_val_app_apply, pushforwardNatIso_hom, pushforwardNatTrans_comp
pushforwardOver 📖	CompOp	—
pushforwardPushforwardAdj 📖	CompOp	2 math math: pushforwardPushforwardAdj_unit_app_val_app, pushforwardPushforwardAdj_counit_app_val_app
pushforwardPushforwardEquivalence 📖	CompOp	2 math math: pushforwardPushforwardEquivalence_unit_app_val_app, pushforwardPushforwardEquivalence_counit_app_val_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsLeftAdjointOverOverRingCatPushforwardIdSheafOver 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint SheafOfModules instCategory CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.GrothendieckTopology.over CategoryTheory.Sheaf.over RingCat RingCat.instCategory pushforward CategoryTheory.Over.forget CategoryTheory.GrothendieckTopology.instIsContinuousOverForgetOver CategoryTheory.CategoryStruct.id CategoryTheory.Sheaf CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf	—	CategoryTheory.GrothendieckTopology.instIsContinuousOverForgetOver CategoryTheory.GrothendieckTopology.instIsContinuousOverStarOver
pushforwardComp_hom_app_val_app 📖	mathematical	—	DFunLike.coe PresheafOfModules.obj CategoryTheory.Sheaf.val RingCat RingCat.instCategory val CategoryTheory.Functor.obj SheafOfModules instCategory CategoryTheory.Functor.comp pushforward CategoryTheory.CategoryStruct.comp CategoryTheory.Sheaf CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.Functor.map ModuleCat.carrier RingCat.carrier Opposite CategoryTheory.Category.opposite 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 Hom.val CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category pushforwardComp	—	—
pushforwardComp_inv_app_val_app 📖	mathematical	—	DFunLike.coe PresheafOfModules.obj CategoryTheory.Sheaf.val RingCat RingCat.instCategory val CategoryTheory.Functor.obj SheafOfModules instCategory pushforward CategoryTheory.Functor.comp CategoryTheory.CategoryStruct.comp CategoryTheory.Sheaf CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.Functor.map ModuleCat.carrier RingCat.carrier Opposite CategoryTheory.Category.opposite 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 Hom.val CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category pushforwardComp	—	—
pushforwardCongr_hom_app_val_app 📖	mathematical	—	DFunLike.coe PresheafOfModules.obj CategoryTheory.Sheaf.val RingCat RingCat.instCategory val CategoryTheory.Functor.obj SheafOfModules instCategory pushforward ModuleCat.carrier RingCat.carrier Opposite CategoryTheory.Category.opposite 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 Hom.val CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category pushforwardCongr	—	—
pushforwardCongr_inv_app_val_app 📖	mathematical	—	DFunLike.coe PresheafOfModules.obj CategoryTheory.Sheaf.val RingCat RingCat.instCategory val CategoryTheory.Functor.obj SheafOfModules instCategory pushforward ModuleCat.carrier RingCat.carrier Opposite CategoryTheory.Category.opposite 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 Hom.val CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category pushforwardCongr	—	—
pushforwardCongr_symm 📖	mathematical	—	CategoryTheory.Iso.symm CategoryTheory.Functor SheafOfModules instCategory CategoryTheory.Functor.category pushforward pushforwardCongr Quiver.Hom CategoryTheory.Sheaf RingCat RingCat.instCategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.obj CategoryTheory.Functor.sheafPushforwardContinuous	—	—
pushforwardNatIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor SheafOfModules instCategory CategoryTheory.Functor.category pushforward CategoryTheory.CategoryStruct.comp CategoryTheory.Sheaf RingCat RingCat.instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.obj CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.NatTrans.app CategoryTheory.Functor.sheafPushforwardContinuousNatTrans pushforwardNatIso pushforwardNatTrans	—	—
pushforwardNatIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor SheafOfModules instCategory CategoryTheory.Functor.category pushforward CategoryTheory.CategoryStruct.comp CategoryTheory.Sheaf RingCat RingCat.instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.obj CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.NatTrans.app CategoryTheory.Functor.sheafPushforwardContinuousNatTrans CategoryTheory.Iso.hom pushforwardNatIso pushforwardNatTrans pushforwardCongr	—	—
pushforwardNatTrans_app_val_app 📖	mathematical	—	DFunLike.coe PresheafOfModules.obj CategoryTheory.Sheaf.val RingCat RingCat.instCategory val CategoryTheory.Functor.obj SheafOfModules instCategory pushforward CategoryTheory.CategoryStruct.comp CategoryTheory.Sheaf CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.NatTrans.app CategoryTheory.Functor.sheafPushforwardContinuousNatTrans ModuleCat.carrier RingCat.carrier Opposite CategoryTheory.Category.opposite 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 Hom.val pushforwardNatTrans Opposite.op Opposite.unop ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver PresheafOfModules.map	—	—
pushforwardNatTrans_app_val_app_apply 📖	mathematical	—	DFunLike.coe PresheafOfModules.obj CategoryTheory.Sheaf.val RingCat RingCat.instCategory val CategoryTheory.Functor.obj SheafOfModules instCategory pushforward CategoryTheory.CategoryStruct.comp CategoryTheory.Sheaf CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.NatTrans.app CategoryTheory.Functor.sheafPushforwardContinuousNatTrans ModuleCat.carrier RingCat.carrier Opposite CategoryTheory.Category.opposite 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 Hom.val pushforwardNatTrans Opposite.op Opposite.unop ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver PresheafOfModules.map	—	—
pushforwardNatTrans_comp 📖	mathematical	—	pushforwardNatTrans CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category SheafOfModules instCategory pushforward CategoryTheory.Sheaf RingCat RingCat.instCategory CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.obj CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.NatTrans.app CategoryTheory.Functor.sheafPushforwardContinuousNatTrans CategoryTheory.Iso.hom pushforwardCongr	—	CategoryTheory.NatTrans.ext' hom_ext PresheafOfModules.hom_ext ModuleCat.hom_ext LinearMap.ext RingHomCompTriple.ids CategoryTheory.Functor.map_comp PresheafOfModules.map_comp PresheafOfModules.comp_app
pushforwardNatTrans_id 📖	mathematical	—	pushforwardNatTrans CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Iso.hom SheafOfModules instCategory pushforward CategoryTheory.CategoryStruct.comp CategoryTheory.Sheaf RingCat RingCat.instCategory CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.obj CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.NatTrans.app CategoryTheory.Functor.sheafPushforwardContinuousNatTrans pushforwardCongr	—	CategoryTheory.NatTrans.ext' hom_ext PresheafOfModules.hom_ext ModuleCat.hom_ext LinearMap.ext CategoryTheory.Functor.map_id PresheafOfModules.map_id
pushforwardPushforwardAdj_counit_app_val_app 📖	mathematical	CategoryTheory.Functor.whiskerRight Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Functor.op CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.NatTrans.op CategoryTheory.Adjunction.counit CategoryTheory.Sheaf.val CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.Sheaf.Hom.val CategoryTheory.Functor.whiskerLeft CategoryTheory.Adjunction.unit CategoryTheory.CategoryStruct.id	DFunLike.coe PresheafOfModules.obj val SheafOfModules instCategory pushforward ModuleCat.carrier RingCat.carrier 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 Hom.val CategoryTheory.NatTrans.app pushforwardPushforwardAdj Opposite.op Opposite.unop ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver PresheafOfModules.map	—	—
pushforwardPushforwardAdj_unit_app_val_app 📖	mathematical	CategoryTheory.Functor.whiskerRight Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Functor.op CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.NatTrans.op CategoryTheory.Adjunction.counit CategoryTheory.Sheaf.val CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.Sheaf.Hom.val CategoryTheory.Functor.whiskerLeft CategoryTheory.Adjunction.unit CategoryTheory.CategoryStruct.id	DFunLike.coe PresheafOfModules.obj val SheafOfModules instCategory pushforward ModuleCat.carrier RingCat.carrier 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 Hom.val CategoryTheory.NatTrans.app pushforwardPushforwardAdj Opposite.op Opposite.unop ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver PresheafOfModules.map	—	—
pushforwardPushforwardEquivalence_counit_app_val_app 📖	mathematical	CategoryTheory.Functor.whiskerRight Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Functor.op CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.functor CategoryTheory.NatTrans.op CategoryTheory.Equivalence.counit CategoryTheory.Sheaf.val CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.Sheaf.Hom.val CategoryTheory.Functor.whiskerLeft CategoryTheory.Equivalence.unit CategoryTheory.CategoryStruct.id	DFunLike.coe PresheafOfModules.obj val SheafOfModules instCategory pushforwardPushforwardEquivalence ModuleCat.carrier RingCat.carrier 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 Hom.val CategoryTheory.NatTrans.app Opposite.op Opposite.unop ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver PresheafOfModules.map	—	—
pushforwardPushforwardEquivalence_unit_app_val_app 📖	mathematical	CategoryTheory.Functor.whiskerRight Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Functor.op CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.functor CategoryTheory.NatTrans.op CategoryTheory.Equivalence.counit CategoryTheory.Sheaf.val CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.Sheaf.Hom.val CategoryTheory.Functor.whiskerLeft CategoryTheory.Equivalence.unit CategoryTheory.CategoryStruct.id	DFunLike.coe PresheafOfModules.obj val SheafOfModules instCategory pushforwardPushforwardEquivalence ModuleCat.carrier RingCat.carrier 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 Hom.val CategoryTheory.NatTrans.app Opposite.op Opposite.unop ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver PresheafOfModules.map	—	—
pushforward_assoc 📖	mathematical	—	CategoryTheory.Iso.trans CategoryTheory.Functor SheafOfModules instCategory CategoryTheory.Functor.category CategoryTheory.Functor.comp pushforward CategoryTheory.CategoryStruct.comp CategoryTheory.Sheaf RingCat RingCat.instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.obj CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.Functor.map CategoryTheory.Functor.isoWhiskerLeft pushforwardComp CategoryTheory.Iso.symm CategoryTheory.Functor.associator CategoryTheory.Functor.isoWhiskerRight	—	CategoryTheory.Iso.ext CategoryTheory.NatTrans.ext' hom_ext PresheafOfModules.hom_ext ModuleCat.hom_ext LinearMap.ext
pushforward_comp_id 📖	mathematical	—	pushforwardComp CategoryTheory.Functor.id CategoryTheory.Functor.isContinuous_id CategoryTheory.CategoryStruct.id CategoryTheory.Sheaf RingCat RingCat.instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.instIsContinuousCompId_1 CategoryTheory.Iso.trans CategoryTheory.Functor SheafOfModules instCategory CategoryTheory.Functor.category CategoryTheory.Functor.comp pushforward CategoryTheory.Functor.isoWhiskerLeft pushforwardId CategoryTheory.Functor.rightUnitor	—	CategoryTheory.Iso.ext CategoryTheory.Functor.isContinuous_id CategoryTheory.Functor.instIsContinuousCompId_1 CategoryTheory.NatTrans.ext' hom_ext PresheafOfModules.hom_ext ModuleCat.hom_ext LinearMap.ext
pushforward_id_comp 📖	mathematical	—	pushforwardComp CategoryTheory.Functor.id CategoryTheory.Functor.isContinuous_id CategoryTheory.Functor.instIsContinuousCompId CategoryTheory.CategoryStruct.id CategoryTheory.Sheaf RingCat RingCat.instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Iso.trans CategoryTheory.Functor SheafOfModules instCategory CategoryTheory.Functor.category CategoryTheory.Functor.comp pushforward CategoryTheory.Functor.isoWhiskerRight pushforwardId CategoryTheory.Functor.leftUnitor	—	CategoryTheory.Iso.ext CategoryTheory.Functor.isContinuous_id CategoryTheory.Functor.instIsContinuousCompId CategoryTheory.NatTrans.ext' hom_ext PresheafOfModules.hom_ext ModuleCat.hom_ext LinearMap.ext
pushforward_map_val 📖	mathematical	—	Hom.val CategoryTheory.Functor.obj PresheafOfModules CategoryTheory.Sheaf.val RingCat RingCat.instCategory PresheafOfModules.instCategory PresheafOfModules.pushforward CategoryTheory.Sheaf.Hom.val CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.sheafPushforwardContinuous val CategoryTheory.Functor.map SheafOfModules instCategory pushforward	—	—
pushforward_obj_val 📖	mathematical	—	val CategoryTheory.Functor.obj SheafOfModules instCategory pushforward PresheafOfModules CategoryTheory.Sheaf.val RingCat RingCat.instCategory PresheafOfModules.instCategory PresheafOfModules.pushforward CategoryTheory.Sheaf.Hom.val CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.sheafPushforwardContinuous	—	—

---

← Back to Index