Presheaf

📁 Source: Mathlib/Topology/Sheaves/Presheaf.lean

Statistics

Metric	Count
Definitions «term__*_», «term_|__», «term_|_ₕ_», «term_|_ₗ_⟪_⟫», pullbackIso, pullbackObjIso, Presheaf, comp, id, attrSheaf_restrict, presheafEquivOfIso, pullback, pullbackHomIsoPushforwardInv, pullbackInvIsoPushforwardHom, pullbackObjObjOfImageOpen, pullbackPushforwardAdjunction, pushforward, pushforwardEq, pushforwardPullbackAdjunction, pushforwardToOfIso, restrict, restrictOpen, restrict_tac, restrict_tac?, toPushforwardOfIso, instCategoryPresheaf	26
Theorems pullbackIso_hom_app_app, pullbackIso_inv_app_app, pullbackObjIso_hom_app, pullbackObjIso_hom_naturality, pullbackObjIso_inv_app, comp_eq, comp_hom_app, comp_inv_app, id_eq, id_hom_app, id_inv_app, comp_app, ext, ext_iff, id_pushforward, map_restrict, presheafEquivOfIso_counitIso_hom_app_app, presheafEquivOfIso_counitIso_inv_app_app, presheafEquivOfIso_functor_map_app, presheafEquivOfIso_functor_obj_map, presheafEquivOfIso_functor_obj_obj, presheafEquivOfIso_inverse_map_app, presheafEquivOfIso_inverse_obj_map, presheafEquivOfIso_inverse_obj_obj, presheafEquivOfIso_unitIso_hom_app_app, presheafEquivOfIso_unitIso_inv_app_app, pullbackObjObjOfImageOpen_hom_naturality, pushforwardEq_hom_app, pushforwardToOfIso_app, pushforward_eq', pushforward_map_app, pushforward_map_app', pushforward_obj_map, pushforward_obj_obj, restrict_restrict, restrict_self, toPushforwardOfIso_app	37
Total	63

AlgebraicGeometry

Definitions

Name	Category	Theorems
«term__*_» 📖	CompOp	—
«term_|__» 📖	CompOp	—
«term_|_ₕ_» 📖	CompOp	—
«term_|_ₗ_⟪_⟫» 📖	CompOp	—

IsOpenMap

Definitions

Name	Category	Theorems
pullbackIso 📖	CompOp	2 math math: pullbackIso_hom_app_app, pullbackIso_inv_app_app
pullbackObjIso 📖	CompOp	3 math math: pullbackObjIso_hom_app, pullbackObjIso_hom_naturality, pullbackObjIso_inv_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pullbackIso_hom_app_app 📖	mathematical	IsOpenMap TopCat.carrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pullback CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.op functor CategoryTheory.Iso.hom pullbackIso Opposite.op Opposite.unop TopCat.Presheaf.pullbackObjObjOfImageOpen	—	—
pullbackIso_inv_app_app 📖	mathematical	IsOpenMap TopCat.carrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.op functor TopCat.Presheaf.pullback CategoryTheory.Iso.inv pullbackIso Opposite.op Opposite.unop TopCat.Presheaf.pullbackObjObjOfImageOpen	—	—
pullbackObjIso_hom_app 📖	mathematical	IsOpenMap TopCat.carrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pullback CategoryTheory.Functor.comp CategoryTheory.Functor.op functor CategoryTheory.Iso.hom pullbackObjIso Opposite.op Opposite.unop TopCat.Presheaf.pullbackObjObjOfImageOpen	—	—
pullbackObjIso_hom_naturality 📖	mathematical	IsOpenMap TopCat.carrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.CategoryStruct.comp TopCat.Presheaf CategoryTheory.Category.toCategoryStruct TopCat.instCategoryPresheaf CategoryTheory.Functor.obj TopCat.Presheaf.pullback CategoryTheory.Functor.comp Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.op functor CategoryTheory.Functor.map CategoryTheory.Iso.hom pullbackObjIso CategoryTheory.Functor.whiskerLeft	—	TopCat.Presheaf.ext CategoryTheory.Limits.IsColimit.hom_ext CategoryTheory.Functor.instHasLeftKanExtension CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize IsOpen.preimage ContinuousMap.continuous CategoryTheory.Category.assoc CategoryTheory.NatTrans.naturality CategoryTheory.NatTrans.congr_app Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom_assoc CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom
pullbackObjIso_inv_app 📖	mathematical	IsOpenMap TopCat.carrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.comp CategoryTheory.Functor.op functor CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pullback CategoryTheory.Iso.inv pullbackObjIso Opposite.op Opposite.unop TopCat.Presheaf.pullbackObjObjOfImageOpen	—	—

TopCat

Definitions

Name	Category	Theorems
Presheaf 📖	CompOp	229 math math: Sheaf.pushforward_sheaf_of_sheaf, AlgebraicGeometry.PresheafedSpace.stalkMap_germ, Presheaf.locally_surjective_iff_surjective_on_stalks, IsOpenMap.pullbackIso_hom_app_app, Presheaf.Pushforward.id_inv_app, Presheaf.germ_stalkPullbackHom, Presheaf.stalkSpecializes_stalkPushforward, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp, Sheaf.forgetFaithful, AlgebraicGeometry.PresheafedSpace.isoOfComponents_inv, AlgebraicGeometry.Scheme.Modules.instPreservesLimitsPresheafAbCarrierCommRingCatToPresheaf, StalkSkyscraperPresheafAdjunctionAuxs.counit_app, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app_assoc, smoothSheafCommRing.ι_evalHom_apply, AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_inv_app, Presheaf.stalkFunctor_map_injective_of_app_injective, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_apply, Presheaf.Pushforward.comp_eq, IsOpenMap.pullbackObjIso_hom_app, Sheaf.pushforward_map, instHasColimitsOfShapePresheaf, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app', IsOpenMap.pullbackObjIso_hom_naturality, Presheaf.pushforwardToOfIso_app, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, Presheaf.stalkPushforward_germ_apply, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_eq, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app', AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_c_app, Presheaf.germ_stalkPullbackInv_assoc, Sheaf.exact_iff_stalkFunctor_map_exact, AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_hom_π, AlgebraicGeometry.PresheafedSpace.componentwiseDiagram_map, AlgebraicGeometry.PresheafedSpace.stalkMap_germ_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app, AlgebraicGeometry.SheafedSpace.comp_hom_c_app, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isIso_of_subset, AlgebraicGeometry.PresheafedSpace.isoOfComponents_hom, AlgebraicGeometry.PresheafedSpace.comp_c_app, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app_assoc, instIsLeftAdjointSheafCompPresheafForgetStalkFunctor, AlgebraicGeometry.LocallyRingedSpace.Γ_Spec_left_triangle, Presheaf.comp_app, AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom_apply, Presheaf.stalkPushforward_germ_assoc, Presheaf.pushforward_map_app, AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_hom_app, Presheaf.stalkFunctor_obj, Presheaf.presheafEquivOfIso_inverse_obj_map, Presheaf.pushforwardEq_hom_app, AlgebraicGeometry.Scheme.Modules.toPresheaf_obj, AlgebraicGeometry.Scheme.Modules.instFaithfulPresheafAbCarrierCommRingCatToPresheaf, AlgebraicGeometry.PresheafedSpace.Γ_map_op, Presheaf.pullbackObjObjOfImageOpen_hom_naturality, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_apply, instAdditivePresheafStalkFunctor, Sheaf.extend_hom_app, AlgebraicGeometry.SheafedSpace.comp_c_app, AlgebraicGeometry.SheafedSpace.id_hom_c_app, Presheaf.stalkFunctor_map_injective_of_isBasis, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom_aux, IsOpenMap.pullbackIso_inv_app_app, smoothSheafCommRing.ι_evalHom, Presheaf.germToPullbackStalk_stalkPullbackHom, Presheaf.pushforward_eq', instHasColimitsOfSizePresheafOfHasColimits, Presheaf.presheafEquivOfIso_unitIso_hom_app_app, AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app'_assoc, AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.desc_c_naturality, AlgebraicGeometry.Scheme.Modules.toPresheaf_map, skyscraperPresheafFunctor_obj, AlgebraicGeometry.SheafedSpace.ofRestrict_hom_c_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_invApp, Presheaf.stalk_mono_of_mono, instIsLeftAdjointPresheafStalkFunctor, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app', instHasLimitsOfShapePresheaf, AlgebraicGeometry.ΓSpec.left_triangle, Presheaf.pushforward_obj_obj, AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso_inv, IsOpenMap.pullbackObjIso_inv_app, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app'_assoc, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_assoc, Presheaf.pullbackPushforwardAdjunction_unit_pullback_map_germToPullbackStalk, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom, Sheaf.isZero_iff_stalkFunctor_obj_isZero, AlgebraicGeometry.Scheme.Hom.stalkFunctor_toImage_injective, AlgebraicGeometry.LocallyRingedSpace.Hom.ext_iff, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp, SkyscraperPresheafFunctor.map'_comp, Presheaf.instMonoCommRingCatToTotalQuotientPresheafPresheaf, Presheaf.stalkSpecializes_stalkFunctor_map_assoc, AlgebraicGeometry.SheafedSpace.Γ_map, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app_assoc, StalkSkyscraperPresheafAdjunctionAuxs.unit_app, AlgebraicGeometry.Spec.sheafedSpaceMap_hom_c_app, Presheaf.Pushforward.comp_inv_app, Presheaf.epi_toLocalizationPresheaf, AlgebraicGeometry.PresheafedSpace.comp_c_app_assoc, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_hom_c_app, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp, limit_isSheaf, Sheaf.pushforward_obj_val, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_apply, Presheaf.stalkFunctor_map_germ_apply, Presheaf.stalkFunctor_map_unit_toSheafify_isIso, AlgebraicGeometry.PresheafedSpace.map_id_c_app, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_app_isLocalHom, AlgebraicGeometry.PresheafedSpace.c_isIso_of_iso, Presheaf.Pushforward.id_hom_app, Presheaf.stalkFunctor_preserves_mono, Presheaf.pullback_obj_obj_ext_iff, AlgebraicGeometry.Scheme.ofRestrict_toLRSHom_c_app, Presheaf.id_pushforward, Presheaf.Pushforward.id_eq, Presheaf.IsFlasque.pushforward_isFlasque, AlgebraicGeometry.PresheafedSpace.ofRestrict_top_c, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality, AlgebraicGeometry.PresheafedSpace.stalkMap_germ_apply, Presheaf.stalkSpecializes_stalkFunctor_map, AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso_hom, AlgebraicGeometry.PresheafedSpace.colimit_presheaf, Presheaf.pushforward_map_app', skyscraperPresheaf_eq_pushforward, Presheaf.pushforward_obj_map, Presheaf.presheafEquivOfIso_unitIso_inv_app_app, Presheaf.stalkPushforward_germ, AlgebraicGeometry.SheafedSpace.comp_hom_c_app', Presheaf.stalkPushforward.id, Presheaf.germ_stalkPullbackHom_assoc, AlgebraicGeometry.LocallyRingedSpace.Γ_map, Presheaf.presheafEquivOfIso_functor_obj_obj, AlgebraicGeometry.Proj.germ_map_sectionInBasicOpen, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_apply, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso, AlgebraicGeometry.PresheafedSpace.toRestrictTop_c, Presheaf.germ_stalkPullbackInv, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app_apply, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app, CategoryTheory.Functor.mapPresheaf_map_c, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso', AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app, AlgebraicGeometry.Proj.sheafedSpaceMap_hom_c_app_hom_apply_coe, Sheaf.forget_full, AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit_map, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_assoc, Presheaf.presheafEquivOfIso_counitIso_inv_app_app, AlgebraicGeometry.PresheafedSpace.Γ_map, AlgebraicGeometry.SheafedSpace.id_hom_c, AlgebraicGeometry.SheafedSpace.id_c_app, AlgebraicGeometry.Scheme.emptyTo_c_app, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_assoc, AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit_obj, AlgebraicGeometry.LocallyRingedSpace.preimage_basicOpen, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp, smoothSheafCommRing.ι_evalHom_assoc, Presheaf.Pushforward.comp_hom_app, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc, AlgebraicGeometry.PresheafedSpace.congr_app, Presheaf.presheafEquivOfIso_counitIso_hom_app_app, AlgebraicGeometry.PresheafedSpace.id_c_app, AlgebraicGeometry.SheafedSpace.id_c, Presheaf.presheafEquivOfIso_inverse_obj_obj, AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_inv_ι_app, AlgebraicGeometry.LocallyRingedSpace.Γ_map_op, Sheaf.instPreservesFiniteLimitsCompPresheafForgetStalkFunctor, AlgebraicGeometry.PresheafedSpace.id_c, AlgebraicGeometry.SheafedSpace.congr_hom_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app', Presheaf.presheafEquivOfIso_functor_map_app, Presheaf.pullbackPushforwardAdjunction_unit_pullback_map_germToPullbackStalk_assoc, AlgebraicGeometry.Scheme.Modules.instReflectsIsomorphismsPresheafAbCarrierCommRingCatToPresheaf, Presheaf.stalkSpecializes_stalkFunctor_map_apply, Presheaf.stalkFunctor_map_germ, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality, Presheaf.germToPullbackStalk_stalkPullbackHom_assoc, Presheaf.toPushforwardOfIso_app, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_assoc, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_invApp, AlgebraicGeometry.PresheafedSpace.comp_c, instHasLimitsPresheaf, Presheaf.app_injective_iff_stalkFunctor_map_injective, isSheaf_of_isLimit, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec_assoc, AlgebraicGeometry.SheafedSpace.congr_app, Presheaf.pullbackPushforwardAdjunction_unit_app_app_germToPullbackStalk_assoc, Presheaf.isIso_iff_stalkFunctor_map_iso, Presheaf.stalkSpecializes_stalkPushforward_assoc, Presheaf.stalkPushforward.comp, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_assoc, AlgebraicGeometry.PresheafedSpace.map_comp_c_app, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, Presheaf.stalkFunctor_map_germ_apply', AlgebraicGeometry.StructureSheaf.algebraMap_pushforward_stalk, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_invApp, Sheaf.instAdditivePresheafForget, skyscraperPresheafFunctor_map, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_apply, Presheaf.stalkPushforward.stalkPushforward_iso_of_isInducing, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app'_assoc, AlgebraicGeometry.PresheafedSpace.restrict_top_presheaf, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app', Presheaf.mono_iff_stalk_mono, AlgebraicGeometry.LocallyRingedSpace.comp_c_app, Presheaf.presheafEquivOfIso_functor_obj_map, Presheaf.presheafEquivOfIso_inverse_map_app, Presheaf.stalkFunctor_map_germ_assoc, Presheaf.pullbackPushforwardAdjunction_unit_app_app_germToPullbackStalk, AlgebraicGeometry.PresheafedSpace.colimitCocone_ι_app_c, Presheaf.stalkSpecializes_stalkPushforward_apply, Sheaf.pushforward_forget, Presheaf.sections_exact_of_exact, instIsRightAdjointPresheafSkyscraperPresheafFunctorOfHasColimits, AlgebraicGeometry.SheafedSpace.Γ_map_op, SkyscraperPresheafFunctor.map'_id, AlgebraicGeometry.SheafedSpace.comp_c_app', AlgebraicGeometry.PresheafedSpace.ofRestrict_c_app, AlgebraicGeometry.LocallyRingedSpace.comp_c, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ
instCategoryPresheaf 📖	CompOp	229 math math: Sheaf.pushforward_sheaf_of_sheaf, AlgebraicGeometry.PresheafedSpace.stalkMap_germ, Presheaf.locally_surjective_iff_surjective_on_stalks, IsOpenMap.pullbackIso_hom_app_app, Presheaf.Pushforward.id_inv_app, Presheaf.germ_stalkPullbackHom, Presheaf.stalkSpecializes_stalkPushforward, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp, Sheaf.forgetFaithful, AlgebraicGeometry.PresheafedSpace.isoOfComponents_inv, AlgebraicGeometry.Scheme.Modules.instPreservesLimitsPresheafAbCarrierCommRingCatToPresheaf, StalkSkyscraperPresheafAdjunctionAuxs.counit_app, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app_assoc, smoothSheafCommRing.ι_evalHom_apply, AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_inv_app, Presheaf.stalkFunctor_map_injective_of_app_injective, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_apply, Presheaf.Pushforward.comp_eq, IsOpenMap.pullbackObjIso_hom_app, Sheaf.pushforward_map, instHasColimitsOfShapePresheaf, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app', IsOpenMap.pullbackObjIso_hom_naturality, Presheaf.pushforwardToOfIso_app, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, Presheaf.stalkPushforward_germ_apply, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_eq, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app', AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_c_app, Presheaf.germ_stalkPullbackInv_assoc, Sheaf.exact_iff_stalkFunctor_map_exact, AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_hom_π, AlgebraicGeometry.PresheafedSpace.componentwiseDiagram_map, AlgebraicGeometry.PresheafedSpace.stalkMap_germ_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app, AlgebraicGeometry.SheafedSpace.comp_hom_c_app, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isIso_of_subset, AlgebraicGeometry.PresheafedSpace.isoOfComponents_hom, AlgebraicGeometry.PresheafedSpace.comp_c_app, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app_assoc, instIsLeftAdjointSheafCompPresheafForgetStalkFunctor, AlgebraicGeometry.LocallyRingedSpace.Γ_Spec_left_triangle, Presheaf.comp_app, AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom_apply, Presheaf.stalkPushforward_germ_assoc, Presheaf.pushforward_map_app, AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_hom_app, Presheaf.stalkFunctor_obj, Presheaf.presheafEquivOfIso_inverse_obj_map, Presheaf.pushforwardEq_hom_app, AlgebraicGeometry.Scheme.Modules.toPresheaf_obj, AlgebraicGeometry.Scheme.Modules.instFaithfulPresheafAbCarrierCommRingCatToPresheaf, AlgebraicGeometry.PresheafedSpace.Γ_map_op, Presheaf.pullbackObjObjOfImageOpen_hom_naturality, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_apply, instAdditivePresheafStalkFunctor, Sheaf.extend_hom_app, AlgebraicGeometry.SheafedSpace.comp_c_app, AlgebraicGeometry.SheafedSpace.id_hom_c_app, Presheaf.stalkFunctor_map_injective_of_isBasis, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom_aux, IsOpenMap.pullbackIso_inv_app_app, smoothSheafCommRing.ι_evalHom, Presheaf.germToPullbackStalk_stalkPullbackHom, Presheaf.pushforward_eq', instHasColimitsOfSizePresheafOfHasColimits, Presheaf.presheafEquivOfIso_unitIso_hom_app_app, AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app'_assoc, AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.desc_c_naturality, AlgebraicGeometry.Scheme.Modules.toPresheaf_map, skyscraperPresheafFunctor_obj, AlgebraicGeometry.SheafedSpace.ofRestrict_hom_c_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_invApp, Presheaf.stalk_mono_of_mono, instIsLeftAdjointPresheafStalkFunctor, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app', instHasLimitsOfShapePresheaf, AlgebraicGeometry.ΓSpec.left_triangle, Presheaf.pushforward_obj_obj, AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso_inv, IsOpenMap.pullbackObjIso_inv_app, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app'_assoc, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_assoc, Presheaf.pullbackPushforwardAdjunction_unit_pullback_map_germToPullbackStalk, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom, Sheaf.isZero_iff_stalkFunctor_obj_isZero, AlgebraicGeometry.Scheme.Hom.stalkFunctor_toImage_injective, AlgebraicGeometry.LocallyRingedSpace.Hom.ext_iff, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp, SkyscraperPresheafFunctor.map'_comp, Presheaf.instMonoCommRingCatToTotalQuotientPresheafPresheaf, Presheaf.stalkSpecializes_stalkFunctor_map_assoc, AlgebraicGeometry.SheafedSpace.Γ_map, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app_assoc, StalkSkyscraperPresheafAdjunctionAuxs.unit_app, AlgebraicGeometry.Spec.sheafedSpaceMap_hom_c_app, Presheaf.Pushforward.comp_inv_app, Presheaf.epi_toLocalizationPresheaf, AlgebraicGeometry.PresheafedSpace.comp_c_app_assoc, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_hom_c_app, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp, limit_isSheaf, Sheaf.pushforward_obj_val, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_apply, Presheaf.stalkFunctor_map_germ_apply, Presheaf.stalkFunctor_map_unit_toSheafify_isIso, AlgebraicGeometry.PresheafedSpace.map_id_c_app, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_app_isLocalHom, AlgebraicGeometry.PresheafedSpace.c_isIso_of_iso, Presheaf.Pushforward.id_hom_app, Presheaf.stalkFunctor_preserves_mono, Presheaf.pullback_obj_obj_ext_iff, AlgebraicGeometry.Scheme.ofRestrict_toLRSHom_c_app, Presheaf.id_pushforward, Presheaf.Pushforward.id_eq, Presheaf.IsFlasque.pushforward_isFlasque, AlgebraicGeometry.PresheafedSpace.ofRestrict_top_c, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality, AlgebraicGeometry.PresheafedSpace.stalkMap_germ_apply, Presheaf.stalkSpecializes_stalkFunctor_map, AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso_hom, AlgebraicGeometry.PresheafedSpace.colimit_presheaf, Presheaf.pushforward_map_app', skyscraperPresheaf_eq_pushforward, Presheaf.pushforward_obj_map, Presheaf.presheafEquivOfIso_unitIso_inv_app_app, Presheaf.stalkPushforward_germ, AlgebraicGeometry.SheafedSpace.comp_hom_c_app', Presheaf.stalkPushforward.id, Presheaf.germ_stalkPullbackHom_assoc, AlgebraicGeometry.LocallyRingedSpace.Γ_map, Presheaf.presheafEquivOfIso_functor_obj_obj, AlgebraicGeometry.Proj.germ_map_sectionInBasicOpen, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_apply, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso, AlgebraicGeometry.PresheafedSpace.toRestrictTop_c, Presheaf.germ_stalkPullbackInv, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app_apply, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app, CategoryTheory.Functor.mapPresheaf_map_c, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso', AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app, AlgebraicGeometry.Proj.sheafedSpaceMap_hom_c_app_hom_apply_coe, Sheaf.forget_full, AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit_map, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_assoc, Presheaf.presheafEquivOfIso_counitIso_inv_app_app, AlgebraicGeometry.PresheafedSpace.Γ_map, AlgebraicGeometry.SheafedSpace.id_hom_c, AlgebraicGeometry.SheafedSpace.id_c_app, AlgebraicGeometry.Scheme.emptyTo_c_app, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_assoc, AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit_obj, AlgebraicGeometry.LocallyRingedSpace.preimage_basicOpen, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp, smoothSheafCommRing.ι_evalHom_assoc, Presheaf.Pushforward.comp_hom_app, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc, AlgebraicGeometry.PresheafedSpace.congr_app, Presheaf.presheafEquivOfIso_counitIso_hom_app_app, AlgebraicGeometry.PresheafedSpace.id_c_app, AlgebraicGeometry.SheafedSpace.id_c, Presheaf.presheafEquivOfIso_inverse_obj_obj, AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_inv_ι_app, AlgebraicGeometry.LocallyRingedSpace.Γ_map_op, Sheaf.instPreservesFiniteLimitsCompPresheafForgetStalkFunctor, AlgebraicGeometry.PresheafedSpace.id_c, AlgebraicGeometry.SheafedSpace.congr_hom_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app', Presheaf.presheafEquivOfIso_functor_map_app, Presheaf.pullbackPushforwardAdjunction_unit_pullback_map_germToPullbackStalk_assoc, AlgebraicGeometry.Scheme.Modules.instReflectsIsomorphismsPresheafAbCarrierCommRingCatToPresheaf, Presheaf.stalkSpecializes_stalkFunctor_map_apply, Presheaf.stalkFunctor_map_germ, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality, Presheaf.germToPullbackStalk_stalkPullbackHom_assoc, Presheaf.toPushforwardOfIso_app, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_assoc, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_invApp, AlgebraicGeometry.PresheafedSpace.comp_c, instHasLimitsPresheaf, Presheaf.app_injective_iff_stalkFunctor_map_injective, isSheaf_of_isLimit, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec_assoc, AlgebraicGeometry.SheafedSpace.congr_app, Presheaf.pullbackPushforwardAdjunction_unit_app_app_germToPullbackStalk_assoc, Presheaf.isIso_iff_stalkFunctor_map_iso, Presheaf.stalkSpecializes_stalkPushforward_assoc, Presheaf.stalkPushforward.comp, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_assoc, AlgebraicGeometry.PresheafedSpace.map_comp_c_app, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, Presheaf.stalkFunctor_map_germ_apply', AlgebraicGeometry.StructureSheaf.algebraMap_pushforward_stalk, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_invApp, Sheaf.instAdditivePresheafForget, skyscraperPresheafFunctor_map, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_apply, Presheaf.stalkPushforward.stalkPushforward_iso_of_isInducing, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app'_assoc, AlgebraicGeometry.PresheafedSpace.restrict_top_presheaf, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app', Presheaf.mono_iff_stalk_mono, AlgebraicGeometry.LocallyRingedSpace.comp_c_app, Presheaf.presheafEquivOfIso_functor_obj_map, Presheaf.presheafEquivOfIso_inverse_map_app, Presheaf.stalkFunctor_map_germ_assoc, Presheaf.pullbackPushforwardAdjunction_unit_app_app_germToPullbackStalk, AlgebraicGeometry.PresheafedSpace.colimitCocone_ι_app_c, Presheaf.stalkSpecializes_stalkPushforward_apply, Sheaf.pushforward_forget, Presheaf.sections_exact_of_exact, instIsRightAdjointPresheafSkyscraperPresheafFunctorOfHasColimits, AlgebraicGeometry.SheafedSpace.Γ_map_op, SkyscraperPresheafFunctor.map'_id, AlgebraicGeometry.SheafedSpace.comp_c_app', AlgebraicGeometry.PresheafedSpace.ofRestrict_c_app, AlgebraicGeometry.LocallyRingedSpace.comp_c, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ

TopCat.Presheaf

Definitions

Name	Category	Theorems
attrSheaf_restrict 📖	CompOp	—
presheafEquivOfIso 📖	CompOp	10 math math: presheafEquivOfIso_inverse_obj_map, presheafEquivOfIso_unitIso_hom_app_app, presheafEquivOfIso_unitIso_inv_app_app, presheafEquivOfIso_functor_obj_obj, presheafEquivOfIso_counitIso_inv_app_app, presheafEquivOfIso_counitIso_hom_app_app, presheafEquivOfIso_inverse_obj_obj, presheafEquivOfIso_functor_map_app, presheafEquivOfIso_functor_obj_map, presheafEquivOfIso_inverse_map_app
pullback 📖	CompOp	17 math math: IsOpenMap.pullbackIso_hom_app_app, germ_stalkPullbackHom, IsOpenMap.pullbackObjIso_hom_app, IsOpenMap.pullbackObjIso_hom_naturality, germ_stalkPullbackInv_assoc, pullbackObjObjOfImageOpen_hom_naturality, IsOpenMap.pullbackIso_inv_app_app, germToPullbackStalk_stalkPullbackHom, IsOpenMap.pullbackObjIso_inv_app, pullbackPushforwardAdjunction_unit_pullback_map_germToPullbackStalk, pullback_obj_obj_ext_iff, germ_stalkPullbackHom_assoc, germ_stalkPullbackInv, pullbackPushforwardAdjunction_unit_pullback_map_germToPullbackStalk_assoc, germToPullbackStalk_stalkPullbackHom_assoc, pullbackPushforwardAdjunction_unit_app_app_germToPullbackStalk_assoc, pullbackPushforwardAdjunction_unit_app_app_germToPullbackStalk
pullbackHomIsoPushforwardInv 📖	CompOp	—
pullbackInvIsoPushforwardHom 📖	CompOp	—
pullbackObjObjOfImageOpen 📖	CompOp	5 math math: IsOpenMap.pullbackIso_hom_app_app, IsOpenMap.pullbackObjIso_hom_app, pullbackObjObjOfImageOpen_hom_naturality, IsOpenMap.pullbackIso_inv_app_app, IsOpenMap.pullbackObjIso_inv_app
pullbackPushforwardAdjunction 📖	CompOp	7 math math: germ_stalkPullbackHom, pullbackPushforwardAdjunction_unit_pullback_map_germToPullbackStalk, pullback_obj_obj_ext_iff, germ_stalkPullbackHom_assoc, pullbackPushforwardAdjunction_unit_pullback_map_germToPullbackStalk_assoc, pullbackPushforwardAdjunction_unit_app_app_germToPullbackStalk_assoc, pullbackPushforwardAdjunction_unit_app_app_germToPullbackStalk
pushforward 📖	CompOp	152 math math: TopCat.Sheaf.pushforward_sheaf_of_sheaf, AlgebraicGeometry.PresheafedSpace.stalkMap_germ, Pushforward.id_inv_app, germ_stalkPullbackHom, stalkSpecializes_stalkPushforward, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp, AlgebraicGeometry.PresheafedSpace.isoOfComponents_inv, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app_assoc, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_apply, Pushforward.comp_eq, TopCat.Sheaf.pushforward_map, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app', pushforwardToOfIso_app, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, stalkPushforward_germ_apply, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_eq, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app', AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_c_app, AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_hom_π, AlgebraicGeometry.PresheafedSpace.componentwiseDiagram_map, AlgebraicGeometry.PresheafedSpace.stalkMap_germ_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app, AlgebraicGeometry.SheafedSpace.comp_hom_c_app, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isIso_of_subset, AlgebraicGeometry.PresheafedSpace.isoOfComponents_hom, AlgebraicGeometry.PresheafedSpace.comp_c_app, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app_assoc, AlgebraicGeometry.LocallyRingedSpace.Γ_Spec_left_triangle, AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom_apply, stalkPushforward_germ_assoc, pushforward_map_app, pushforwardEq_hom_app, AlgebraicGeometry.PresheafedSpace.Γ_map_op, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_apply, AlgebraicGeometry.SheafedSpace.comp_c_app, AlgebraicGeometry.SheafedSpace.id_hom_c_app, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom_aux, pushforward_eq', AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app'_assoc, AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.desc_c_naturality, AlgebraicGeometry.SheafedSpace.ofRestrict_hom_c_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_invApp, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app', AlgebraicGeometry.ΓSpec.left_triangle, pushforward_obj_obj, AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso_inv, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app'_assoc, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_assoc, pullbackPushforwardAdjunction_unit_pullback_map_germToPullbackStalk, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom, AlgebraicGeometry.Scheme.Hom.stalkFunctor_toImage_injective, AlgebraicGeometry.LocallyRingedSpace.Hom.ext_iff, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp, AlgebraicGeometry.SheafedSpace.Γ_map, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app_assoc, AlgebraicGeometry.Spec.sheafedSpaceMap_hom_c_app, Pushforward.comp_inv_app, AlgebraicGeometry.PresheafedSpace.comp_c_app_assoc, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_hom_c_app, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp, TopCat.Sheaf.pushforward_obj_val, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_apply, AlgebraicGeometry.PresheafedSpace.map_id_c_app, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_app_isLocalHom, AlgebraicGeometry.PresheafedSpace.c_isIso_of_iso, Pushforward.id_hom_app, pullback_obj_obj_ext_iff, AlgebraicGeometry.Scheme.ofRestrict_toLRSHom_c_app, id_pushforward, Pushforward.id_eq, IsFlasque.pushforward_isFlasque, AlgebraicGeometry.PresheafedSpace.ofRestrict_top_c, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality, AlgebraicGeometry.PresheafedSpace.stalkMap_germ_apply, AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso_hom, pushforward_map_app', skyscraperPresheaf_eq_pushforward, pushforward_obj_map, stalkPushforward_germ, AlgebraicGeometry.SheafedSpace.comp_hom_c_app', stalkPushforward.id, germ_stalkPullbackHom_assoc, AlgebraicGeometry.LocallyRingedSpace.Γ_map, AlgebraicGeometry.Proj.germ_map_sectionInBasicOpen, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_apply, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso, AlgebraicGeometry.PresheafedSpace.toRestrictTop_c, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app_apply, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app, CategoryTheory.Functor.mapPresheaf_map_c, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso', AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app, AlgebraicGeometry.Proj.sheafedSpaceMap_hom_c_app_hom_apply_coe, AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit_map, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_assoc, AlgebraicGeometry.PresheafedSpace.Γ_map, AlgebraicGeometry.SheafedSpace.id_hom_c, AlgebraicGeometry.SheafedSpace.id_c_app, AlgebraicGeometry.Scheme.emptyTo_c_app, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_assoc, AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit_obj, AlgebraicGeometry.LocallyRingedSpace.preimage_basicOpen, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp, Pushforward.comp_hom_app, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc, AlgebraicGeometry.PresheafedSpace.congr_app, AlgebraicGeometry.PresheafedSpace.id_c_app, AlgebraicGeometry.SheafedSpace.id_c, AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_inv_ι_app, AlgebraicGeometry.LocallyRingedSpace.Γ_map_op, AlgebraicGeometry.SheafedSpace.congr_hom_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app', pullbackPushforwardAdjunction_unit_pullback_map_germToPullbackStalk_assoc, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality, toPushforwardOfIso_app, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_assoc, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_invApp, AlgebraicGeometry.PresheafedSpace.comp_c, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec_assoc, AlgebraicGeometry.SheafedSpace.congr_app, pullbackPushforwardAdjunction_unit_app_app_germToPullbackStalk_assoc, stalkSpecializes_stalkPushforward_assoc, stalkPushforward.comp, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_assoc, AlgebraicGeometry.PresheafedSpace.map_comp_c_app, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, AlgebraicGeometry.StructureSheaf.algebraMap_pushforward_stalk, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_invApp, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_apply, stalkPushforward.stalkPushforward_iso_of_isInducing, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app'_assoc, AlgebraicGeometry.PresheafedSpace.restrict_top_presheaf, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app', AlgebraicGeometry.LocallyRingedSpace.comp_c_app, pullbackPushforwardAdjunction_unit_app_app_germToPullbackStalk, stalkSpecializes_stalkPushforward_apply, TopCat.Sheaf.pushforward_forget, AlgebraicGeometry.SheafedSpace.Γ_map_op, AlgebraicGeometry.SheafedSpace.comp_c_app', AlgebraicGeometry.PresheafedSpace.ofRestrict_c_app, AlgebraicGeometry.LocallyRingedSpace.comp_c, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ
pushforwardEq 📖	CompOp	4 math math: pushforwardEq_hom_app, AlgebraicGeometry.PresheafedSpace.map_id_c_app, AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit_map, AlgebraicGeometry.PresheafedSpace.map_comp_c_app
pushforwardPullbackAdjunction 📖	CompOp	—
pushforwardToOfIso 📖	CompOp	2 math math: pushforwardToOfIso_app, AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso_inv
restrict 📖	CompOp	1 math math: AlgebraicGeometry.Scheme.basicOpen_restrict
restrictOpen 📖	CompOp	11 math math: AlgebraicGeometry.exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux, AlgebraicGeometry.exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux_aux, AlgebraicGeometry.RingedSpace.res_zero, restrict_self, isLocallySurjective_iff, map_restrict, restrictOpenCommRingCat_apply, AlgebraicGeometry.exists_eq_pow_mul_of_isAffineOpen, restrict_sum, restrict_restrict, AlgebraicGeometry.exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated
restrict_tac 📖	CompOp	—
restrict_tac? 📖	CompOp	—
toPushforwardOfIso 📖	CompOp	2 math math: AlgebraicGeometry.PresheafedSpace.isoOfComponents_inv, toPushforwardOfIso_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.CategoryStruct.comp TopCat.Presheaf CategoryTheory.Category.toCategoryStruct TopCat.instCategoryPresheaf CategoryTheory.Functor.obj	—	—
ext 📖	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op	—	—	CategoryTheory.NatTrans.ext
ext_iff 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op	—	ext
id_pushforward 📖	mathematical	—	pushforward CategoryTheory.CategoryStruct.id TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory CategoryTheory.Functor.id TopCat.Presheaf TopCat.instCategoryPresheaf	—	—
map_restrict 📖	mathematical	TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder	DFunLike.coe CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app restrictOpen	—	CategoryTheory.ConcreteCategory.comp_apply CategoryTheory.NatTrans.naturality
presheafEquivOfIso_counitIso_hom_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.whiskeringLeft CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.op CategoryTheory.Equivalence.symm TopologicalSpace.Opens.mapMapIso CategoryTheory.Equivalence.inverse CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Equivalence.counitIso TopCat.Presheaf TopCat.instCategoryPresheaf presheafEquivOfIso CategoryTheory.Functor.map Opposite.op TopologicalSpace.Opens.map CategoryTheory.Iso.inv TopCat TopCat.instCategory Opposite.unop CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.eqToHom_op CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
presheafEquivOfIso_counitIso_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Functor.whiskeringLeft CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.op CategoryTheory.Equivalence.symm TopologicalSpace.Opens.mapMapIso CategoryTheory.Equivalence.inverse CategoryTheory.Iso.inv CategoryTheory.Equivalence.counitIso TopCat.Presheaf TopCat.instCategoryPresheaf presheafEquivOfIso CategoryTheory.Functor.map Opposite.op TopologicalSpace.Opens.map TopCat TopCat.instCategory CategoryTheory.Iso.hom Opposite.unop CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.eqToHom_op CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
presheafEquivOfIso_functor_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.op CategoryTheory.Equivalence.symm TopologicalSpace.Opens.mapMapIso CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.functor TopCat.Presheaf TopCat.instCategoryPresheaf presheafEquivOfIso Opposite.op CategoryTheory.Functor.obj TopologicalSpace.Opens.map CategoryTheory.Iso.hom TopCat TopCat.instCategory Opposite.unop	—	—
presheafEquivOfIso_functor_obj_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.functor TopCat.Presheaf TopCat.instCategoryPresheaf presheafEquivOfIso Opposite.op TopologicalSpace.Opens.map CategoryTheory.Iso.hom TopCat TopCat.instCategory Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom.unop	—	—
presheafEquivOfIso_functor_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.functor TopCat.Presheaf TopCat.instCategoryPresheaf presheafEquivOfIso Opposite.op TopologicalSpace.Opens.map CategoryTheory.Iso.hom TopCat TopCat.instCategory Opposite.unop	—	—
presheafEquivOfIso_inverse_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.op CategoryTheory.Equivalence.symm TopologicalSpace.Opens.mapMapIso CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.inverse TopCat.Presheaf TopCat.instCategoryPresheaf presheafEquivOfIso Opposite.op CategoryTheory.Functor.obj TopologicalSpace.Opens.map CategoryTheory.Iso.inv TopCat TopCat.instCategory Opposite.unop	—	—
presheafEquivOfIso_inverse_obj_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.inverse TopCat.Presheaf TopCat.instCategoryPresheaf presheafEquivOfIso Opposite.op TopologicalSpace.Opens.map CategoryTheory.Iso.inv TopCat TopCat.instCategory Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom.unop	—	—
presheafEquivOfIso_inverse_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.inverse TopCat.Presheaf TopCat.instCategoryPresheaf presheafEquivOfIso Opposite.op TopologicalSpace.Opens.map CategoryTheory.Iso.inv TopCat TopCat.instCategory Opposite.unop	—	—
presheafEquivOfIso_unitIso_hom_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Functor.whiskeringLeft CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.op CategoryTheory.Equivalence.symm TopologicalSpace.Opens.mapMapIso CategoryTheory.Equivalence.functor CategoryTheory.Iso.hom CategoryTheory.Equivalence.unitIso TopCat.Presheaf TopCat.instCategoryPresheaf presheafEquivOfIso CategoryTheory.Functor.map Opposite.op TopologicalSpace.Opens.map TopCat TopCat.instCategory CategoryTheory.Iso.inv Opposite.unop CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.eqToHom_op CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
presheafEquivOfIso_unitIso_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.whiskeringLeft CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.op CategoryTheory.Equivalence.symm TopologicalSpace.Opens.mapMapIso CategoryTheory.Equivalence.functor CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Equivalence.unitIso TopCat.Presheaf TopCat.instCategoryPresheaf presheafEquivOfIso CategoryTheory.Functor.map Opposite.op TopologicalSpace.Opens.map CategoryTheory.Iso.hom TopCat TopCat.instCategory Opposite.unop CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.eqToHom_op CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
pullbackObjObjOfImageOpen_hom_naturality 📖	mathematical	IsOpen TopCat.carrier TopCat.str Set.image DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.Presheaf TopCat.instCategoryPresheaf pullback Opposite.op Set.image DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier SetLike.coe TopologicalSpace.Opens.instSetLike CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.homOfLE CategoryTheory.Iso.hom pullbackObjObjOfImageOpen IsOpenMap.functorMap	—	CategoryTheory.Limits.IsColimit.hom_ext CategoryTheory.Functor.instHasLeftKanExtension CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize IsOpen.preimage ContinuousMap.continuous CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom_assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom CategoryTheory.Limits.coconeOfDiagramTerminal_ι_app
pushforwardEq_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf pushforward CategoryTheory.Iso.hom pushforwardEq CategoryTheory.Functor.map CategoryTheory.Functor.op TopologicalSpace.Opens.map CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.eqToHom_op
pushforwardToOfIso_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf pushforward CategoryTheory.Iso.inv TopCat TopCat.instCategory pushforwardToOfIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.op TopologicalSpace.Opens.map Opposite.unop CategoryTheory.Iso.hom CategoryTheory.Functor.map CategoryTheory.Functor.op CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite	—	CategoryTheory.Adjunction.homEquiv_counit presheafEquivOfIso_counitIso_hom_app_app
pushforward_eq' 📖	mathematical	—	CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf pushforward	—	—
pushforward_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.comp CategoryTheory.Functor.op TopologicalSpace.Opens.map CategoryTheory.Functor.map TopCat.Presheaf TopCat.instCategoryPresheaf pushforward Opposite.op CategoryTheory.Functor.obj Opposite.unop	—	—
pushforward_map_app' 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf pushforward CategoryTheory.Functor.map Opposite.op TopologicalSpace.Opens.map Opposite.unop	—	—
pushforward_obj_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf pushforward Opposite.op TopologicalSpace.Opens.map Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom.unop	—	—
pushforward_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.Presheaf TopCat.instCategoryPresheaf pushforward Opposite.op TopologicalSpace.Opens.map Opposite.unop	—	—
restrict_restrict 📖	mathematical	TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder	restrictOpen	—	CategoryTheory.ConcreteCategory.comp_apply CategoryTheory.Functor.map_comp
restrict_self 📖	mathematical	—	restrictOpen	—	CategoryTheory.Functor.map_id CategoryTheory.id_apply
toPushforwardOfIso_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf pushforward CategoryTheory.Iso.inv TopCat TopCat.instCategory toPushforwardOfIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.op TopologicalSpace.Opens.map CategoryTheory.Iso.hom Opposite.op Opposite.unop CategoryTheory.Functor.map CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite	—	CategoryTheory.Adjunction.homEquiv_unit presheafEquivOfIso_unitIso_hom_app_app

TopCat.Presheaf.Pushforward

Definitions

Name	Category	Theorems
comp 📖	CompOp	3 math math: comp_inv_app, AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit_map, comp_hom_app
id 📖	CompOp	4 math math: id_inv_app, AlgebraicGeometry.PresheafedSpace.map_id_c_app, id_hom_app, TopCat.Presheaf.stalkPushforward.id

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_eq 📖	mathematical	—	CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory	—	—
comp_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory CategoryTheory.Iso.hom comp CategoryTheory.CategoryStruct.id	—	—
comp_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory CategoryTheory.Iso.inv comp CategoryTheory.CategoryStruct.id	—	—
id_eq 📖	mathematical	—	CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.CategoryStruct.id TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory	—	—
id_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.CategoryStruct.id TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory CategoryTheory.Iso.hom id	—	—
id_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.CategoryStruct.id TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory CategoryTheory.Iso.inv id	—	—

---

← Back to Index