Presheaf

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

Statistics

Metric	Count
Definitions «term__*_», «term_|__», «term_|_ₕ_», «term_|_ₗ_⟪_⟫», Presheaf, comp, id, attrSheaf_restrict, presheafEquivOfIso, pullback, pullbackHomIsoPushforwardInv, pullbackInvIsoPushforwardHom, pullbackObjObjOfImageOpen, pushforward, pushforwardEq, pushforwardPullbackAdjunction, pushforwardToOfIso, restrict, restrictOpen, restrict_tac, restrict_tac?, toPushforwardOfIso, instCategoryPresheaf	23
Theorems 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, pushforwardEq_hom_app, pushforwardToOfIso_app, pushforward_eq', pushforward_map_app, pushforward_map_app', pushforward_obj_map, pushforward_obj_obj, restrict_restrict, toPushforwardOfIso_app	30
Total	53

AlgebraicGeometry

Definitions

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

TopCat

Definitions

Name	Category	Theorems
Presheaf 📖	CompOp	205 math math: Sheaf.pushforward_sheaf_of_sheaf, AlgebraicGeometry.PresheafedSpace.stalkMap_germ, Presheaf.locally_surjective_iff_surjective_on_stalks, 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, Sheaf.pushforward_map, instHasColimitsOfShapePresheaf, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app', 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, 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, 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, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_apply, 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, 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.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, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app'_assoc, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_assoc, 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, SkyscraperPresheafFunctor.map'_comp, Presheaf.pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk_assoc, 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, Sheaf.pushforward_obj_val, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_apply, Presheaf.stalkFunctor_map_germ_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, 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, AlgebraicGeometry.PresheafedSpace.ofRestrict_top_c, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality, AlgebraicGeometry.PresheafedSpace.stalkMap_germ_apply, Presheaf.stalkSpecializes_stalkFunctor_map, AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso_hom, 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.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, Sheaf.forget_full, AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit_map, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_assoc, Presheaf.presheafEquivOfIso_counitIso_inv_app_app, Presheaf.pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk, 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.LocallyRingedSpace.Γ_map_op, AlgebraicGeometry.PresheafedSpace.id_c, AlgebraicGeometry.SheafedSpace.congr_hom_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app', Presheaf.presheafEquivOfIso_functor_map_app, 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, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec_assoc, AlgebraicGeometry.SheafedSpace.congr_app, 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, skyscraperPresheafFunctor_map, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_apply, Presheaf.stalkPushforward.stalkPushforward_iso_of_isInducing, Presheaf.pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk_assoc, 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.stalkSpecializes_stalkPushforward_apply, Sheaf.pushforward_forget, Presheaf.pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk, 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	205 math math: Sheaf.pushforward_sheaf_of_sheaf, AlgebraicGeometry.PresheafedSpace.stalkMap_germ, Presheaf.locally_surjective_iff_surjective_on_stalks, 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, Sheaf.pushforward_map, instHasColimitsOfShapePresheaf, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app', 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, 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, 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, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_apply, 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, 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.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, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app'_assoc, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_assoc, 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, SkyscraperPresheafFunctor.map'_comp, Presheaf.pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk_assoc, 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, Sheaf.pushforward_obj_val, AlgebraicGeometry.LocallyRingedSpace.Γevaluation_naturality_apply, Presheaf.stalkFunctor_map_germ_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, 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, AlgebraicGeometry.PresheafedSpace.ofRestrict_top_c, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality, AlgebraicGeometry.PresheafedSpace.stalkMap_germ_apply, Presheaf.stalkSpecializes_stalkFunctor_map, AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso_hom, 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.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, Sheaf.forget_full, AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit_map, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_assoc, Presheaf.presheafEquivOfIso_counitIso_inv_app_app, Presheaf.pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk, 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.LocallyRingedSpace.Γ_map_op, AlgebraicGeometry.PresheafedSpace.id_c, AlgebraicGeometry.SheafedSpace.congr_hom_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app', Presheaf.presheafEquivOfIso_functor_map_app, 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, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec_assoc, AlgebraicGeometry.SheafedSpace.congr_app, 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, skyscraperPresheafFunctor_map, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_apply, Presheaf.stalkPushforward.stalkPushforward_iso_of_isInducing, Presheaf.pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk_assoc, 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.stalkSpecializes_stalkPushforward_apply, Sheaf.pushforward_forget, Presheaf.pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk, 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	11 math math: germ_stalkPullbackHom, germ_stalkPullbackInv_assoc, germToPullbackStalk_stalkPullbackHom, pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk_assoc, pullback_obj_obj_ext_iff, germ_stalkPullbackHom_assoc, germ_stalkPullbackInv, pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk, germToPullbackStalk_stalkPullbackHom_assoc, pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk_assoc, pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk
pullbackHomIsoPushforwardInv 📖	CompOp	—
pullbackInvIsoPushforwardHom 📖	CompOp	—
pullbackObjObjOfImageOpen 📖	CompOp	—
pushforward 📖	CompOp	149 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, 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, pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk_assoc, 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, 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.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.PresheafedSpace.pushforwardDiagramToColimit_map, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_assoc, pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk, 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', 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, 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, pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app'_assoc, AlgebraicGeometry.PresheafedSpace.restrict_top_presheaf, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app', AlgebraicGeometry.LocallyRingedSpace.comp_c_app, stalkSpecializes_stalkPushforward_apply, TopCat.Sheaf.pushforward_forget, pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk, 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	7 math math: germ_stalkPullbackHom, pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk_assoc, pullback_obj_obj_ext_iff, germ_stalkPullbackHom_assoc, pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk, pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk_assoc, pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk
pushforwardToOfIso 📖	CompOp	2 math math: pushforwardToOfIso_app, AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso_inv
restrict 📖	CompOp	2 math math: isLocallySurjective_iff, AlgebraicGeometry.Scheme.basicOpen_restrict
restrictOpen 📖	CompOp	6 math math: AlgebraicGeometry.RingedSpace.res_zero, map_restrict, restrictOpenCommRingCat_apply, AlgebraicGeometry.exists_eq_pow_mul_of_isAffineOpen, 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 CategoryTheory.Category.opposite Preorder.smallCategory 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
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
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