PullbackContinuous

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

Statistics

Metric	Count
Definitions adjunction, pullback, pullbackComp, pullbackId, pullbackIso, pullbackPushforwardAdjunction, sheafificationCompPullback	7
Theorems conjugateEquiv_pullbackComp_inv, conjugateEquiv_pullbackId_hom, instIsLeftAdjointPullback, instIsRightAdjointPushforward, instIsRightAdjointPushforwardCompSheafRingCatMapSheafPushforwardContinuous, instIsRightAdjointPushforwardIdSheafRingCat, pullback_assoc, pullback_comp_id, pullback_id_comp	9
Total	16

SheafOfModules

Definitions

Name	Category	Theorems
pullback 📖	CompOp	13 math math: pullbackPushforwardAdjunction_homEquiv_pullbackObjUnitToUnit, instIsLeftAdjointPullback, pullback_map_ιFree_comp_pullbackObjFreeIso_hom_assoc, pullbackObjFreeIso_hom_naturality_assoc, pullback_comp_id, conjugateEquiv_pullbackComp_inv, pullback_id_comp, pullback_assoc, instIsIsoPullbackObjUnitToUnitOfFinal, pullbackPushforwardAdjunction_homEquiv_symm_unitToPushforwardObjUnit, pullbackObjFreeIso_hom_naturality, conjugateEquiv_pullbackId_hom, pullback_map_ιFree_comp_pullbackObjFreeIso_hom
pullbackComp 📖	CompOp	4 math math: pullback_comp_id, conjugateEquiv_pullbackComp_inv, pullback_id_comp, pullback_assoc
pullbackId 📖	CompOp	3 math math: pullback_comp_id, pullback_id_comp, conjugateEquiv_pullbackId_hom
pullbackIso 📖	CompOp	—
pullbackPushforwardAdjunction 📖	CompOp	4 math math: pullbackPushforwardAdjunction_homEquiv_pullbackObjUnitToUnit, conjugateEquiv_pullbackComp_inv, pullbackPushforwardAdjunction_homEquiv_symm_unitToPushforwardObjUnit, conjugateEquiv_pullbackId_hom
sheafificationCompPullback 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conjugateEquiv_pullbackComp_inv 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor SheafOfModules instCategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category pullback CategoryTheory.Functor.comp CategoryTheory.CategoryStruct.comp CategoryTheory.Sheaf RingCat RingCat.instCategory CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.obj CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.Functor.map instIsRightAdjointPushforwardCompSheafRingCatMapSheafPushforwardContinuous pushforward EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.conjugateEquiv CategoryTheory.Adjunction.comp pullbackPushforwardAdjunction CategoryTheory.Iso.inv pullbackComp CategoryTheory.Iso.hom pushforwardComp	—	CategoryTheory.Adjunction.conjugateEquiv_leftAdjointCompIso_inv instIsRightAdjointPushforwardCompSheafRingCatMapSheafPushforwardContinuous
conjugateEquiv_pullbackId_hom 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor SheafOfModules instCategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category pullback CategoryTheory.Functor.id CategoryTheory.Functor.isContinuous_id CategoryTheory.CategoryStruct.id CategoryTheory.Sheaf RingCat RingCat.instCategory CategoryTheory.Sheaf.instCategorySheaf instIsRightAdjointPushforwardIdSheafRingCat pushforward EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.conjugateEquiv CategoryTheory.Adjunction.id pullbackPushforwardAdjunction CategoryTheory.Iso.hom pullbackId CategoryTheory.Iso.inv pushforwardId	—	CategoryTheory.Adjunction.conjugateEquiv_leftAdjointIdIso_hom CategoryTheory.Functor.isContinuous_id instIsRightAdjointPushforwardIdSheafRingCat
instIsLeftAdjointPullback 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint SheafOfModules instCategory pullback	—	CategoryTheory.Adjunction.isLeftAdjoint
instIsRightAdjointPushforward 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint SheafOfModules instCategory pushforward	—	CategoryTheory.Adjunction.isRightAdjoint CategoryTheory.Presheaf.instIsLocallyInjectiveOfIsIsoFunctorOpposite CategoryTheory.IsIso.id CategoryTheory.Presheaf.isLocallySurjective_of_iso
instIsRightAdjointPushforwardCompSheafRingCatMapSheafPushforwardContinuous 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint SheafOfModules instCategory pushforward CategoryTheory.Functor.comp 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.isRightAdjoint_of_iso CategoryTheory.Functor.isRightAdjoint_comp
instIsRightAdjointPushforwardIdSheafRingCat 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint SheafOfModules instCategory pushforward CategoryTheory.Functor.id CategoryTheory.Functor.isContinuous_id CategoryTheory.CategoryStruct.id CategoryTheory.Sheaf RingCat RingCat.instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf	—	CategoryTheory.Functor.isRightAdjoint_of_iso CategoryTheory.Functor.isContinuous_id CategoryTheory.Functor.isRightAdjoint_of_isEquivalence CategoryTheory.Functor.isEquivalence_refl
pullback_assoc 📖	mathematical	—	CategoryTheory.Iso.trans CategoryTheory.Functor SheafOfModules instCategory CategoryTheory.Functor.category CategoryTheory.Functor.comp pullback CategoryTheory.CategoryStruct.comp CategoryTheory.Sheaf RingCat RingCat.instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.obj CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.Functor.map instIsRightAdjointPushforwardCompSheafRingCatMapSheafPushforwardContinuous CategoryTheory.Functor.isoWhiskerLeft pullbackComp CategoryTheory.Iso.symm CategoryTheory.Functor.associator CategoryTheory.Functor.isoWhiskerRight	—	CategoryTheory.Adjunction.leftAdjointCompIso_assoc instIsRightAdjointPushforwardCompSheafRingCatMapSheafPushforwardContinuous pushforward_assoc
pullback_comp_id 📖	mathematical	—	pullbackComp CategoryTheory.Functor.id CategoryTheory.Functor.isContinuous_id CategoryTheory.Functor.instIsContinuousCompId CategoryTheory.CategoryStruct.id CategoryTheory.Sheaf RingCat RingCat.instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf instIsRightAdjointPushforwardIdSheafRingCat CategoryTheory.Iso.trans CategoryTheory.Functor SheafOfModules instCategory CategoryTheory.Functor.category CategoryTheory.Functor.comp pullback CategoryTheory.Functor.isoWhiskerLeft pullbackId CategoryTheory.Functor.rightUnitor	—	CategoryTheory.Adjunction.leftAdjointCompIso_comp_id CategoryTheory.Functor.isContinuous_id instIsRightAdjointPushforwardIdSheafRingCat CategoryTheory.Functor.instIsContinuousCompId pushforward_id_comp
pullback_id_comp 📖	mathematical	—	pullbackComp CategoryTheory.Functor.id CategoryTheory.Functor.isContinuous_id CategoryTheory.CategoryStruct.id CategoryTheory.Sheaf RingCat RingCat.instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf instIsRightAdjointPushforwardIdSheafRingCat CategoryTheory.Functor.instIsContinuousCompId_1 CategoryTheory.Iso.trans CategoryTheory.Functor SheafOfModules instCategory CategoryTheory.Functor.category CategoryTheory.Functor.comp pullback CategoryTheory.Functor.isoWhiskerRight pullbackId CategoryTheory.Functor.leftUnitor	—	CategoryTheory.Adjunction.leftAdjointCompIso_id_comp CategoryTheory.Functor.isContinuous_id instIsRightAdjointPushforwardIdSheafRingCat CategoryTheory.Functor.instIsContinuousCompId_1 pushforward_comp_id

SheafOfModules.PullbackConstruction

Definitions

Name	Category	Theorems
adjunction 📖	CompOp	—

---

← Back to Index