Stalks

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

Statistics

Metric	Count
Definitions germ, germToPullbackStalk, stalk, stalkCongr, stalkFunctor, stalkPullbackHom, stalkPullbackInv, stalkPullbackIso, stalkPushforward, stalkSpecializes, Γgerm	11
Theorems app_bijective_of_stalkFunctor_map_bijective, app_injective_iff_stalkFunctor_map_injective, app_injective_of_stalkFunctor_map_injective, app_isIso_of_stalkFunctor_map_iso, app_surjective_of_injective_of_locally_surjective, app_surjective_of_stalkFunctor_map_bijective, germToPullbackStalk_stalkPullbackHom, germToPullbackStalk_stalkPullbackHom_assoc, germ_eq, germ_eq_of_isBasis, germ_exist, germ_exist_of_isBasis, germ_ext, germ_res, germ_res', germ_res'_assoc, germ_res_apply, germ_res_apply', germ_res_assoc, germ_stalkPullbackHom, germ_stalkPullbackHom_assoc, germ_stalkPullbackInv, germ_stalkPullbackInv_assoc, germ_stalkSpecializes, germ_stalkSpecializes_apply, germ_stalkSpecializes_assoc, isIso_iff_stalkFunctor_map_iso, isIso_of_stalkFunctor_map_iso, map_germ_eq_Γgerm, map_germ_eq_Γgerm_assoc, mono_iff_stalk_mono, mono_of_stalk_mono, pullback_obj_obj_ext, pullback_obj_obj_ext_iff, pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk, pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk_assoc, pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk, pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk_assoc, section_ext, stalkCongr_hom, stalkCongr_inv, stalkFunctor_map_germ, stalkFunctor_map_germ_apply, stalkFunctor_map_germ_apply', stalkFunctor_map_germ_assoc, stalkFunctor_map_injective_of_app_injective, stalkFunctor_map_injective_of_isBasis, stalkFunctor_obj, stalkFunctor_preserves_mono, comp, id, stalkPushforward_iso_of_isInducing, stalkPushforward_germ, stalkPushforward_germ_apply, stalkPushforward_germ_assoc, stalkSpecializes_comp, stalkSpecializes_comp_apply, stalkSpecializes_comp_assoc, stalkSpecializes_refl, stalkSpecializes_stalkFunctor_map, stalkSpecializes_stalkFunctor_map_apply, stalkSpecializes_stalkFunctor_map_assoc, stalkSpecializes_stalkPushforward, stalkSpecializes_stalkPushforward_apply, stalkSpecializes_stalkPushforward_assoc, stalk_hom_ext, stalk_hom_ext_iff, stalk_mono_of_mono, Γgerm_res_apply	69
Total	80

TopCat.Presheaf

Definitions

Name	Category	Theorems
germ 📖	CompOp	129 math math: AlgebraicGeometry.Scheme.germ_stalkClosedPointTo, AlgebraicGeometry.Scheme.Hom.germ_stalkMap_assoc, AlgebraicGeometry.PresheafedSpace.stalkMap_germ, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec_fromSpecStalk_assoc, germ_stalkPullbackHom, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ, AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ_assoc, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ_assoc, AlgebraicGeometry.Scheme.mem_basicOpen', germ_exist_of_isBasis, AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_inv_app, smoothSheafCommRing.eval_germ, germ_stalkSpecializes_apply, germ_res', stalkPushforward_germ_apply, StalkSkyscraperPresheafAdjunctionAuxs.germ_fromStalk, AlgebraicGeometry.Scheme.exists_germ_injective, germ_res_apply, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec_fromSpecStalk, germ_stalkPullbackInv_assoc, AlgebraicGeometry.PresheafedSpace.stalkMap_germ_assoc, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv, AlgebraicGeometry.IsAffineOpen.ideal_le_iff, TopCat.stalkToFiber_germ, germ_stalkSpecializes_assoc, AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom_apply, AlgebraicGeometry.Scheme.Hom.germ_stalkMap_apply, stalkPushforward_germ_assoc, AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_hom_app, stalk_open_algebraMap, AlgebraicGeometry.Scheme.fromSpecStalk_appTop, germ_ext, AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ, map_germ_eq_Γgerm, AlgebraicGeometry.germ_comp_stalkToFiberRingHom, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ, germ_res_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, germToPullbackStalk_stalkPullbackHom, AlgebraicGeometry.Spec.germ_stalkMapIso_hom_assoc, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv_assoc, smoothSheafCommRing.evalHom_germ, AlgebraicGeometry.germ_stalkClosedPointIso_hom_assoc, AlgebraicGeometry.Scheme.stalkMap_germ_assoc, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ_apply, map_germ_eq_Γgerm_assoc, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom, stalk_hom_ext_iff, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ_apply, AlgebraicGeometry.germ_injective_of_isIntegral, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_assoc, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ_apply, pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk_assoc, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ_apply, AlgebraicGeometry.germ_stalkClosedPointIso_hom, stalkFunctor_map_germ_apply, germ_res_apply', StalkSkyscraperPresheafAdjunctionAuxs.germ_fromStalk_assoc, germ_exist, germ_res, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv, AlgebraicGeometry.PresheafedSpace.stalkMap_germ_apply, stalkPushforward_germ, AlgebraicGeometry.ΓSpecIso_hom_stalkClosedPointIso_inv, germ_skyscraperPresheafStalkOfSpecializes_hom_assoc, germ_stalkPullbackHom_assoc, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv, smoothSheaf.eval_germ, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_apply, germ_stalkPullbackInv, AlgebraicGeometry.IsAffineOpen.primeIdealOf_eq_map_closedPoint, AlgebraicGeometry.Scheme.stalkMap_germ_apply, AlgebraicGeometry.Scheme.Hom.germ_stalkMap, AlgebraicGeometry.StructureSheaf.algebraMap_germ_assoc, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom_assoc, AlgebraicGeometry.StructureSheaf.algebraMap_germ, AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_toSpecΓ, AlgebraicGeometry.stalkToFiberRingHom_germ, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_assoc, AlgebraicGeometry.Scheme.IsGermInjectiveAt.cond, pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv_assoc, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_apply, germ_res'_assoc, AlgebraicGeometry.StructureSheaf.toOpen_germ, AlgebraicGeometry.Proj.stalkIso'_germ, AlgebraicGeometry.Scheme.mem_basicOpen_top, AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_toSpecΓ_assoc, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ, AlgebraicGeometry.germ_eq_zero_of_pow_mul_eq_zero, AlgebraicGeometry.Scheme.fromSpecStalk_app, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_base_apply, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_germ, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ_assoc, AlgebraicGeometry.Scheme.germ_residue_assoc, Γgerm_res_apply, AlgebraicGeometry.Scheme.mem_basicOpen'', germ_stalkSpecializes, AlgebraicGeometry.Scheme.germ_residue, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ, AlgebraicGeometry.Spec.germ_stalkMapIso_hom, AlgebraicGeometry.Spec.fromSpecStalk_eq, stalkFunctor_map_germ, germToPullbackStalk_stalkPullbackHom_assoc, AlgebraicGeometry.Scheme.exists_le_and_germ_injective, PresheafOfModules.germ_ringCat_smul, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ_assoc, PresheafOfModules.germ_smul, submonoidPresheafOfStalk_obj, stalkFunctor_map_germ_apply', AlgebraicGeometry.Proj.stalkIso'_symm_mk, pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk_assoc, AlgebraicGeometry.RingedSpace.mem_basicOpen, AlgebraicGeometry.StructureSheaf.algebraMap_germ_apply, AlgebraicGeometry.Scheme.stalkMap_germ, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ_assoc, stalkFunctor_map_germ_assoc, pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk, germ_skyscraperPresheafStalkOfSpecializes_hom, StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf_app, AlgebraicGeometry.RingedSpace.mem_basicOpen', AlgebraicGeometry.Scheme.mem_basicOpen, AlgebraicGeometry.Scheme.Spec_fromSpecStalk, AlgebraicGeometry.IsAffineOpen.ideal_ext_iff, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ, AlgebraicGeometry.IsAffineOpen.mem_ideal_iff
germToPullbackStalk 📖	CompOp	8 math math: germ_stalkPullbackInv_assoc, germToPullbackStalk_stalkPullbackHom, pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk_assoc, germ_stalkPullbackInv, pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk, germToPullbackStalk_stalkPullbackHom_assoc, pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk_assoc, pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk
stalk 📖	CompOp	358 math math: AlgebraicGeometry.Scheme.toSpecΓ_apply, smoothSheafCommRing.ι_forgetStalk_inv, AlgebraicGeometry.Scheme.fromSpecStalk_closedPoint, AlgebraicGeometry.StructureSheaf.instIsScalarTowerCarrierStalkCommRingCatStructurePresheafInCommRingCatCarrierAbPresheafOpensCarrierTopModuleStructurePresheaf, AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv_assoc, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo, AlgebraicGeometry.Scheme.Hom.germ_stalkMap_assoc, AlgebraicGeometry.Scheme.Spec_map_stalkMap_fromSpecStalk, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.stalk_iso, AlgebraicGeometry.PresheafedSpace.stalkMap_germ, instNontrivialCarrierStalkCommRingCatPresheafSmoothSheafCommRing, AlgebraicGeometry.surjectiveOnStalks_iff, AlgebraicGeometry.instIsDomainCarrierStalkCommRingCatPresheafOfIsIntegral, smoothSheafCommRing.nonunits_stalk, germ_stalkPullbackHom, AlgebraicGeometry.LocallyRingedSpace.notMem_prime_iff_unit_in_stalk, stalkSpecializes_stalkPushforward, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ, AlgebraicGeometry.StructureSheaf.IsLocalization.to_stalk, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_point, AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ_assoc, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ_assoc, AlgebraicGeometry.Scheme.mem_basicOpen', StalkSkyscraperPresheafAdjunctionAuxs.counit_app, AlgebraicGeometry.HasRingHomProperty.stalkMap, germ_exist_of_isBasis, AlgebraicGeometry.Scheme.stalkSpecializes_stalkMap, AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_inv_app, AlgebraicGeometry.Scheme.Spec_map_stalkSpecializes_fromSpecStalk, AlgebraicGeometry.isField_stalk_of_closure_mem_irreducibleComponents, AlgebraicGeometry.Scheme.stalkMap_congr_assoc, smoothSheafCommRing.eval_germ, AlgebraicGeometry.localRingHom_comp_stalkIso_apply, AlgebraicGeometry.Scheme.instIsOverFromSpecStalkOfMem, AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap, AlgebraicGeometry.IsAffineOpen.fromSpecStalk_closedPoint, germ_stalkSpecializes_apply, AlgebraicGeometry.StructureSheaf.instAtPrimeCarrierStalkCommRingCatStructurePresheafInCommRingCatAsIdeal, AlgebraicGeometry.StructureSheaf.toStalk_stalkSpecializes_assoc, AlgebraicGeometry.Scheme.Opens.stalkIso_inv, smoothSheafCommRing.instLocalRing_stalk, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom_assoc, AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem_compHom, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_point_assoc, germ_res', AlgebraicGeometry.functionField_isScalarTower, stalkPushforward_germ_apply, StalkSkyscraperPresheafAdjunctionAuxs.germ_fromStalk, stalkToFiber_injective, AlgebraicGeometry.Scheme.exists_germ_injective, AlgebraicGeometry.IsOpenImmersion.iff_isIso_stalkMap, AlgebraicGeometry.Scheme.Cover.instIsIsoCommRingCatStalkMapFromGlued, germ_res_apply, germ_stalkPullbackInv_assoc, AlgebraicGeometry.SpecToEquivOfLocalRing_apply_snd_coe, AlgebraicGeometry.PresheafedSpace.stalkMap_germ_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.stalk_iso, AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, AlgebraicGeometry.isIso_iff_isIso_stalkMap, AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr, AlgebraicGeometry.StructureSheaf.toStalk_stalkSpecializes, AlgebraicGeometry.RingedSpace.mem_top_basicOpen, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv, AlgebraicGeometry.Scheme.range_fromSpecStalk, AlgebraicGeometry.IsAffineOpen.ideal_le_iff, AlgebraicGeometry.stalkToFiberRingHom_homogeneousLocalizationToStalk, AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom_assoc, AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_ι_assoc, germ_stalkSpecializes_assoc, AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom_apply, AlgebraicGeometry.Scheme.Hom.germ_stalkMap_apply, TopCat.stalkToFiber_injective, stalkPushforward_germ_assoc, AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_hom_app, stalkFunctor_obj, stalk_open_algebraMap, smoothSheafCommRing.forgetStalk_inv_comp_eval_assoc, AlgebraicGeometry.Scheme.fromSpecStalk_appTop, germ_ext, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_point_assoc, AlgebraicGeometry.Scheme.stalkMap_congr_point_assoc, smoothSheafCommRing.forgetStalk_inv_comp_eval, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_assoc, AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ, map_germ_eq_Γgerm, AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap_apply, AlgebraicGeometry.Scheme.Spec_map_stalkMap_fromSpecStalk_assoc, AlgebraicGeometry.LocallyRingedSpace.isLocalHomStalkMap, AlgebraicGeometry.LocallyRingedSpace.coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, smoothSheafCommRing.forgetStalk_inv_comp_eval_apply, AlgebraicGeometry.Spec_map_localization_isIso, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom_aux, AlgebraicGeometry.Scheme.stalkClosedPointTo_fromSpecStalk, smoothSheafCommRing.isUnit_stalk_iff, AlgebraicGeometry.Scheme.stalkMap_hom_inv_assoc, AlgebraicGeometry.germ_comp_stalkToFiberRingHom, AlgebraicGeometry.PresheafedSpace.stalkMap.congr, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, AlgebraicGeometry.Scheme.residue_descResidueField, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ, AlgebraicGeometry.Scheme.SpecMap_stalkSpecializes_fromSpecStalk, AlgebraicGeometry.Scheme.descResidueField_fromSpecResidueField, germ_res_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, AlgebraicGeometry.LocallyRingedSpace.stalkMap_id, germToPullbackStalk_stalkPullbackHom, AlgebraicGeometry.Spec.germ_stalkMapIso_hom_assoc, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv_assoc, AlgebraicGeometry.formallySmooth_stalkMap_iff, AlgebraicGeometry.isIso_stalkMap_coprodSpec, smoothSheafCommRing.evalHom_germ, AlgebraicGeometry.LocallyRingedSpace.residue_comp_residueFieldMap_eq_stalkMap_comp_residue, stalkCongr_hom, AlgebraicGeometry.PresheafedSpace.ofRestrict_stalkMap_isIso, AlgebraicGeometry.germ_stalkClosedPointIso_hom_assoc, smoothSheafCommRing.forgetStalk_hom_comp_evalHom_assoc, AlgebraicGeometry.Scheme.stalkMap_germ_assoc, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ_apply, AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom_apply, map_germ_eq_Γgerm_assoc, AlgebraicGeometry.Scheme.stalkMap_congr_hom_assoc, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom, AlgebraicGeometry.Scheme.stalkSpecializes_stalkMap_apply, AlgebraicGeometry.Scheme.stalkMap_id, AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom_assoc, stalk_hom_ext_iff, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ_apply, TopCat.stalkToFiber_surjective, AlgebraicGeometry.germ_injective_of_isIntegral, AlgebraicGeometry.PresheafedSpace.stalkMap.id, AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk_assoc, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_assoc, AlgebraicGeometry.stalkMap_toStalk, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom, AlgebraicGeometry.isOpenImmersion_iff_stalk, AlgebraicGeometry.LocallyRingedSpace.Hom.prop, AlgebraicGeometry.SurjectiveOnStalks.surj_on_stalks, AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap_assoc, AlgebraicGeometry.Spec.fromSpecStalk_eq', AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ_apply, AlgebraicGeometry.IsClosedImmersion.Spec_map_residue, AlgebraicGeometry.SurjectiveOnStalks.stalkMap_surjective, AlgebraicGeometry.Scheme.SpecMap_stalkSpecializes_fromSpecStalk_assoc, AlgebraicGeometry.PresheafedSpace.stalkMap.isIso, pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk_assoc, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ_apply, AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv, AlgebraicGeometry.Scheme.stalkMap_congr_hom, stalkSpecializes_stalkFunctor_map_assoc, smoothSheafCommRing.ι_forgetStalk_inv_apply, AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_ι, AlgebraicGeometry.instIsFractionRingCarrierStalkCommRingCatPresheafFunctionField, AlgebraicGeometry.germ_stalkClosedPointIso_hom, AlgebraicGeometry.SpecToEquivOfLocalRing_apply_fst, StalkSkyscraperPresheafAdjunctionAuxs.unit_app, AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierOfCarrierStalkAbPresheafPrimeComplAsIdealHomToStalk, AlgebraicGeometry.Scheme.stalkMap_comp, smoothSheafCommRing.eval_surjective, AlgebraicGeometry.Scheme.residue_surjective, AlgebraicGeometry.over_def, AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom_assoc, smoothSheafCommRing.forgetStalk_hom_comp_evalHom, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_stalk_isLocalHom, stalkFunctor_map_germ_apply, germ_res_apply', stalkSpecializes_comp, AlgebraicGeometry.StructureSheaf.toStalk_stalkSpecializes_apply, StalkSkyscraperPresheafAdjunctionAuxs.germ_fromStalk_assoc, AlgebraicGeometry.Scheme.instIsOverMapStalkSpecializesCommRingCatPresheaf, smoothSheafCommRing.ι_forgetStalk_inv_assoc, germ_exist, germ_res, AlgebraicGeometry.LocallyOfFiniteType.stalkMap, AlgebraicGeometry.LocallyRingedSpace.ofRestrict_stalkMap_isIso, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv, AlgebraicGeometry.Scheme.stalkMap_congr_point, AlgebraicGeometry.Scheme.stalkMap_hom_inv, AlgebraicGeometry.PresheafedSpace.stalkMap_germ_apply, stalkSpecializes_stalkFunctor_map, AlgebraicGeometry.Scheme.stalkMap_hom_inv_apply, AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_iff, AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap_apply, AlgebraicGeometry.LocallyRingedSpace.isLocalHomStalkMap', AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv, AlgebraicGeometry.Scheme.Spec_map_stalkSpecializes_fromSpecStalk_assoc, stalkPushforward_germ, AlgebraicGeometry.ΓSpecIso_hom_stalkClosedPointIso_inv, germ_skyscraperPresheafStalkOfSpecializes_hom_assoc, germ_stalkPullbackHom_assoc, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_apply, AlgebraicGeometry.IsOpenImmersion.instIsIsoCommRingCatStalkMap, AlgebraicGeometry.Scheme.isLocalHom_stalkClosedPointTo', germ_stalkPullbackInv, AlgebraicGeometry.stalkMap_toStalk_apply, AlgebraicGeometry.IsAffineOpen.primeIdealOf_eq_map_closedPoint, AlgebraicGeometry.stalkMap_injective_of_isOpenMap_of_injective, AlgebraicGeometry.Scheme.stalkMap_germ_apply, AlgebraicGeometry.LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf, AlgebraicGeometry.Scheme.Hom.germ_stalkMap, AlgebraicGeometry.StructureSheaf.algebraMap_germ_assoc, instNontrivialStalkPresheafSmoothSheaf, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.stalk_iso, AlgebraicGeometry.Flat.stalkMap, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom_assoc, AlgebraicGeometry.Scheme.Hom.stalkMap_comp, AlgebraicGeometry.StructureSheaf.algebraMap_germ, AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheafPrimeComplAsIdealToStalkₗ, AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_toSpecΓ, AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap_apply, smoothSheafCommRing.ι_forgetStalk_hom_apply, AlgebraicGeometry.stalkToFiberRingHom_germ, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_ofRestrict, smoothSheafCommRing.ι_forgetStalk_hom_assoc, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_assoc, AlgebraicGeometry.instIsPreimmersionFromSpecStalk, AlgebraicGeometry.isIso_SpecMap_stakMap_localization, AlgebraicGeometry.Scheme.residue_residueFieldMap_assoc, AlgebraicGeometry.Scheme.Spec_fromSpecStalk', AlgebraicGeometry.FormallyUnramified.stalkMap, AlgebraicGeometry.Scheme.IsGermInjectiveAt.cond, pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk, AlgebraicGeometry.PresheafedSpace.stalkMap.congr_hom, AlgebraicGeometry.Scheme.residue_residueFieldCongr, AlgebraicGeometry.IsOpenImmersion.iff_stalk_iso, AlgebraicGeometry.Scheme.residue_residueFieldMap, AlgebraicGeometry.LocallyRingedSpace.isLocalRing, AlgebraicGeometry.StructureSheaf.stalkAlgebra_map, AlgebraicGeometry.PresheafedSpace.stalkMap.comp, AlgebraicGeometry.Scheme.stalkMap_inv_hom_apply, stalkSpecializes_comp_assoc, AlgebraicGeometry.Scheme.SpecMap_residue_apply, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv_assoc, AlgebraicGeometry.Scheme.instIsPreimmersionMapResidue, AlgebraicGeometry.Scheme.Hom.mem_smoothLocus, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_apply, germ_res'_assoc, AlgebraicGeometry.StructureSheaf.toOpen_germ, AlgebraicGeometry.Proj.stalkIso'_germ, AlgebraicGeometry.IsAffineOpen.fromSpecStalk_isPreimmersion, AlgebraicGeometry.Scheme.mem_basicOpen_top, stalkSpecializes_comp_apply, AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_toSpecΓ_assoc, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp, AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv_apply, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ, AlgebraicGeometry.Scheme.stalkMap_inv_hom, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc, AlgebraicGeometry.germ_eq_zero_of_pow_mul_eq_zero, AlgebraicGeometry.Scheme.fromSpecStalk_app, AlgebraicGeometry.IsAffineOpen.isLocalization_stalk, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_base_apply, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv_assoc, smoothSheafCommRing.ι_forgetStalk_hom, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_germ, AlgebraicGeometry.Flat.iff_flat_stalkMap, AlgebraicGeometry.isIso_iff_stalk_iso, AlgebraicGeometry.Scheme.instIsOverMapStalkMapOverInferInstanceOverClass, AlgebraicGeometry.SpecToEquivOfLocalRing_symm_apply, AlgebraicGeometry.Scheme.Hom.stalkMap_congr, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec, AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap, AlgebraicGeometry.IsAffineOpen.isLocalization_stalk', AlgebraicGeometry.Scheme.residue_residueFieldCongr_assoc, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ_assoc, AlgebraicGeometry.Scheme.germ_residue_assoc, Γgerm_res_apply, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_assoc, AlgebraicGeometry.Scheme.mem_basicOpen'', AlgebraicGeometry.stalkClosedPointIso_inv, AlgebraicGeometry.Scheme.stalkMap_inv_hom_assoc, smoothSheaf.eval_surjective, AlgebraicGeometry.IsClosedImmersion.SpecMap_residue, germ_stalkSpecializes, AlgebraicGeometry.Scheme.residue_descResidueField_assoc, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_hom_assoc, AlgebraicGeometry.Scheme.germ_residue, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ, AlgebraicGeometry.Spec.germ_stalkMapIso_hom, AlgebraicGeometry.HasRingHomProperty.stalkMap_of_respectsIso, AlgebraicGeometry.Spec.fromSpecStalk_eq, stalkSpecializes_refl, stalkSpecializes_stalkFunctor_map_apply, AlgebraicGeometry.Scheme.Hom.stalkMap_id, stalkFunctor_map_germ, AlgebraicGeometry.Scheme.isLocalHom_stalkClosedPointTo, germToPullbackStalk_stalkPullbackHom_assoc, stalkToFiber_surjective, AlgebraicGeometry.SpecToEquivOfLocalRing_eq_iff, AlgebraicGeometry.Scheme.exists_le_and_germ_injective, PresheafOfModules.germ_ringCat_smul, AlgebraicGeometry.LocallyRingedSpace.toStalk_stalkMap_toΓSpec, AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk, AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap_assoc, AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom_apply, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_ofRestrict, AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv_assoc, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ_assoc, PresheafOfModules.germ_smul, AlgebraicGeometry.LocallyRingedSpace.isLocalHom_stalkMap_congr, stalkSpecializes_stalkPushforward_assoc, stalkPushforward.comp, AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap_assoc, smoothSheafCommRing.forgetStalk_hom_comp_evalHom_apply, AlgebraicGeometry.instIsNoetherianRingCarrierStalkCommRingCatPresheafOfIsLocallyNoetherian, AlgebraicGeometry.isReduced_stalk_of_isReduced, AlgebraicGeometry.Scheme.Hom.instIsLocalHomCarrierStalkCommRingCatPresheafCoeContinuousMapCarrierCarrierHomTopCatBaseRingHomHomStalkMap, submonoidPresheafOfStalk_obj, AlgebraicGeometry.LocallyRingedSpace.stalkMap_comp, stalkFunctor_map_germ_apply', AlgebraicGeometry.StructureSheaf.algebraMap_pushforward_stalk, AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv_apply, AlgebraicGeometry.Scheme.stalkClosedPointTo_comp, AlgebraicGeometry.Scheme.Spec_map_residue_apply, AlgebraicGeometry.Proj.stalkIso'_symm_mk, stalkPushforward.stalkPushforward_iso_of_isInducing, AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk, pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk_assoc, AlgebraicGeometry.LocallyRingedSpace.isLocalHomValStalkMap, AlgebraicGeometry.localRingHom_comp_stalkIso, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_point, AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom, AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso, AlgebraicGeometry.RingedSpace.mem_basicOpen, AlgebraicGeometry.Scheme.instEpiCommRingCatResidue, AlgebraicGeometry.StructureSheaf.algebraMap_germ_apply, AlgebraicGeometry.Scheme.stalkMap_germ, AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ_assoc, AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso_apply, stalkFunctor_map_germ_assoc, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_hom, AlgebraicGeometry.Scheme.Hom.isOpen_smoothLocus, AlgebraicGeometry.Spec_stalkClosedPointIso, AlgebraicGeometry.Scheme.stalkSpecializes_stalkMap_assoc, stalkSpecializes_stalkPushforward_apply, pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk, AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem_toPartialMap, germ_skyscraperPresheafStalkOfSpecializes_hom, AlgebraicGeometry.Scheme.stalkMap_congr, stalkCongr_inv, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom, AlgebraicGeometry.PresheafedSpace.stalkMap.congr_point, StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf_app, AlgebraicGeometry.RingedSpace.mem_basicOpen', AlgebraicGeometry.Scheme.mem_basicOpen, AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk_assoc, AlgebraicGeometry.Scheme.Spec_fromSpecStalk, AlgebraicGeometry.homogeneousLocalizationToStalk_stalkToFiberRingHom, AlgebraicGeometry.IsAffineOpen.ideal_ext_iff, AlgebraicGeometry.Scheme.Hom.stalkMap_surjective, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ, AlgebraicGeometry.IsAffineOpen.mem_ideal_iff, AlgebraicGeometry.Scheme.toSpecΓ_base
stalkCongr 📖	CompOp	30 math math: AlgebraicGeometry.Scheme.Hom.stalkMap_congr_point, AlgebraicGeometry.Scheme.stalkMap_congr_assoc, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom_assoc, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_point_assoc, AlgebraicGeometry.Scheme.stalkMap_congr_point_assoc, AlgebraicGeometry.Scheme.stalkClosedPointTo_fromSpecStalk, AlgebraicGeometry.Scheme.stalkMap_hom_inv_assoc, stalkCongr_hom, AlgebraicGeometry.Scheme.stalkMap_congr_hom_assoc, AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv, AlgebraicGeometry.Scheme.stalkMap_congr_hom, AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom_assoc, AlgebraicGeometry.Scheme.stalkMap_congr_point, AlgebraicGeometry.Scheme.stalkMap_hom_inv, AlgebraicGeometry.Scheme.stalkMap_hom_inv_apply, AlgebraicGeometry.Scheme.residue_residueFieldCongr, AlgebraicGeometry.Scheme.stalkMap_inv_hom_apply, AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv_apply, AlgebraicGeometry.Scheme.stalkMap_inv_hom, AlgebraicGeometry.Scheme.Hom.stalkMap_congr, AlgebraicGeometry.Scheme.residue_residueFieldCongr_assoc, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_assoc, AlgebraicGeometry.Scheme.stalkMap_inv_hom_assoc, AlgebraicGeometry.SpecToEquivOfLocalRing_eq_iff, AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom_apply, AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv_assoc, AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom, AlgebraicGeometry.Scheme.stalkMap_congr, stalkCongr_inv, AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom
stalkFunctor 📖	CompOp	25 math math: locally_surjective_iff_surjective_on_stalks, StalkSkyscraperPresheafAdjunctionAuxs.counit_app, AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_inv_app, stalkFunctor_map_injective_of_app_injective, AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_hom_app, stalkFunctor_obj, stalkFunctor_map_injective_of_isBasis, stalk_mono_of_mono, instIsLeftAdjointPresheafStalkFunctor, AlgebraicGeometry.Scheme.Hom.stalkFunctor_toImage_injective, stalkSpecializes_stalkFunctor_map_assoc, StalkSkyscraperPresheafAdjunctionAuxs.unit_app, stalkFunctor_map_germ_apply, stalkFunctor_preserves_mono, stalkSpecializes_stalkFunctor_map, stalkPushforward.id, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc, stalkSpecializes_stalkFunctor_map_apply, stalkFunctor_map_germ, app_injective_iff_stalkFunctor_map_injective, isIso_iff_stalkFunctor_map_iso, stalkFunctor_map_germ_apply', mono_iff_stalk_mono, stalkFunctor_map_germ_assoc
stalkPullbackHom 📖	CompOp	4 math math: germ_stalkPullbackHom, germToPullbackStalk_stalkPullbackHom, germ_stalkPullbackHom_assoc, germToPullbackStalk_stalkPullbackHom_assoc
stalkPullbackInv 📖	CompOp	2 math math: germ_stalkPullbackInv_assoc, germ_stalkPullbackInv
stalkPullbackIso 📖	CompOp	—
stalkPushforward 📖	CompOp	9 math math: stalkSpecializes_stalkPushforward, stalkPushforward_germ_apply, stalkPushforward_germ_assoc, stalkPushforward_germ, stalkPushforward.id, stalkSpecializes_stalkPushforward_assoc, stalkPushforward.comp, stalkPushforward.stalkPushforward_iso_of_isInducing, stalkSpecializes_stalkPushforward_apply
stalkSpecializes 📖	CompOp	47 math math: AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv_assoc, stalkSpecializes_stalkPushforward, AlgebraicGeometry.Scheme.stalkSpecializes_stalkMap, AlgebraicGeometry.Scheme.Spec_map_stalkSpecializes_fromSpecStalk, AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap, germ_stalkSpecializes_apply, AlgebraicGeometry.StructureSheaf.toStalk_stalkSpecializes_assoc, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_point_assoc, AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap, AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr, AlgebraicGeometry.StructureSheaf.toStalk_stalkSpecializes, AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom_assoc, germ_stalkSpecializes_assoc, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_assoc, AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap_apply, AlgebraicGeometry.Scheme.SpecMap_stalkSpecializes_fromSpecStalk, stalkCongr_hom, AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom_apply, AlgebraicGeometry.Scheme.stalkSpecializes_stalkMap_apply, AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap_assoc, AlgebraicGeometry.Scheme.SpecMap_stalkSpecializes_fromSpecStalk_assoc, stalkSpecializes_stalkFunctor_map_assoc, stalkSpecializes_comp, AlgebraicGeometry.StructureSheaf.toStalk_stalkSpecializes_apply, AlgebraicGeometry.Scheme.instIsOverMapStalkSpecializesCommRingCatPresheaf, stalkSpecializes_stalkFunctor_map, AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap_apply, AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv, AlgebraicGeometry.Scheme.Spec_map_stalkSpecializes_fromSpecStalk_assoc, AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap_apply, stalkSpecializes_comp_assoc, stalkSpecializes_comp_apply, AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap, germ_stalkSpecializes, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_hom_assoc, stalkSpecializes_refl, stalkSpecializes_stalkFunctor_map_apply, AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap_assoc, stalkSpecializes_stalkPushforward_assoc, AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap_assoc, AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv_apply, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_point, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_hom, AlgebraicGeometry.Scheme.stalkSpecializes_stalkMap_assoc, stalkSpecializes_stalkPushforward_apply, stalkCongr_inv
Γgerm 📖	CompOp	12 math math: AlgebraicGeometry.Scheme.toSpecΓ_apply, AlgebraicGeometry.LocallyRingedSpace.notMem_prime_iff_unit_in_stalk, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, AlgebraicGeometry.RingedSpace.mem_top_basicOpen, map_germ_eq_Γgerm, AlgebraicGeometry.LocallyRingedSpace.coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, map_germ_eq_Γgerm_assoc, Γgerm_res_apply, AlgebraicGeometry.LocallyRingedSpace.toStalk_stalkMap_toΓSpec, AlgebraicGeometry.Scheme.toSpecΓ_base

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
app_bijective_of_stalkFunctor_map_bijective 📖	mathematical	Function.Bijective CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf stalkFunctor CategoryTheory.Sheaf.val TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map CategoryTheory.Sheaf.Hom.val	Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.NatTrans.app	—	app_injective_of_stalkFunctor_map_injective app_surjective_of_stalkFunctor_map_bijective
app_injective_iff_stalkFunctor_map_injective 📖	mathematical	—	CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf stalkFunctor CategoryTheory.Sheaf.val TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.NatTrans.app	—	app_injective_of_stalkFunctor_map_injective stalkFunctor_map_injective_of_app_injective
app_injective_of_stalkFunctor_map_injective 📖	mathematical	CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf stalkFunctor CategoryTheory.Sheaf.val TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map	Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.NatTrans.app	—	section_ext stalkFunctor_map_germ_apply
app_isIso_of_stalkFunctor_map_iso 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf stalkFunctor TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike CategoryTheory.Sheaf.val Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology CategoryTheory.Functor.map CategoryTheory.Sheaf.Hom.val	Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.NatTrans.app	—	CategoryTheory.isIso_iff_bijective app_bijective_of_stalkFunctor_map_bijective CategoryTheory.Functor.map_isIso CategoryTheory.isIso_of_reflects_iso
app_surjective_of_injective_of_locally_surjective 📖	—	CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf stalkFunctor CategoryTheory.Sheaf.val TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map CategoryTheory.Sheaf.Hom.val Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.NatTrans.app Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—	section_ext inf_le_left stalkFunctor_map_germ_apply CategoryTheory.NatTrans.naturality CategoryTheory.ConcreteCategory.comp_apply CategoryTheory.Functor.map_comp TopCat.Sheaf.existsUnique_gluing' TopCat.Sheaf.eq_of_locally_eq' Subtype.forall'
app_surjective_of_stalkFunctor_map_bijective 📖	mathematical	Function.Bijective CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf stalkFunctor CategoryTheory.Sheaf.val TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map CategoryTheory.Sheaf.Hom.val	Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.NatTrans.app	—	app_surjective_of_injective_of_locally_surjective germ_exist germ_eq stalkFunctor_map_germ_apply CategoryTheory.ConcreteCategory.comp_apply CategoryTheory.NatTrans.naturality
germToPullbackStalk_stalkPullbackHom 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.Presheaf TopCat.instCategoryPresheaf pullback Opposite.op stalk DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier germToPullbackStalk stalkPullbackHom germ	—	pullback_obj_obj_ext pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk_assoc germ_stalkPullbackHom germ_res
germToPullbackStalk_stalkPullbackHom_assoc 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.Presheaf TopCat.instCategoryPresheaf pullback Opposite.op stalk DFunLike.coe ContinuousMap ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory TopCat.instConcreteCategoryContinuousMapCarrier germToPullbackStalk stalkPullbackHom germ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' germToPullbackStalk_stalkPullbackHom
germ_eq 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op stalk CategoryTheory.ConcreteCategory.hom germ	CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff CategoryTheory.isFilteredOrEmpty_op_of_isCofilteredOrEmpty CategoryTheory.IsCofiltered.toIsCofilteredOrEmpty CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits CategoryTheory.isFiltered_op_of_isCofiltered
germ_eq_of_isBasis 📖	mathematical	TopologicalSpace.Opens.IsBasis TopCat.carrier TopCat.str TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op stalk CategoryTheory.ConcreteCategory.hom germ	CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.homOfLE	—	germ_eq TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open TopologicalSpace.Opens.is_open' HasSubset.Subset.trans Set.instIsTransSubset CategoryTheory.Functor.map_comp DFunLike.congr_arg
germ_exist 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op stalk CategoryTheory.ConcreteCategory.hom germ	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.Types.jointly_surjective CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder
germ_exist_of_isBasis 📖	mathematical	TopologicalSpace.Opens.IsBasis TopCat.carrier TopCat.str	DFunLike.coe CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op stalk CategoryTheory.ConcreteCategory.hom germ	—	germ_exist TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open TopologicalSpace.Opens.is_open' CategoryTheory.ConcreteCategory.comp_apply germ_res'
germ_ext 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	stalk germ	—	germ_res CategoryTheory.ConcreteCategory.comp_apply
germ_res 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op stalk CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver germ Quiver.Hom.le	—	CategoryTheory.Limits.colimit.w CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize
germ_res' 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op stalk CategoryTheory.Functor.map germ Quiver.Hom.le Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver	—	CategoryTheory.Limits.colimit.w CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize
germ_res'_assoc 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op CategoryTheory.Functor.map stalk germ Quiver.Hom.le Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' germ_res'
germ_res_apply 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike	DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op stalk CategoryTheory.ConcreteCategory.hom germ CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom.le	—	CategoryTheory.ConcreteCategory.comp_apply germ_res
germ_res_apply' 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike	DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op stalk CategoryTheory.ConcreteCategory.hom germ CategoryTheory.Functor.map Quiver.Hom.le Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.ConcreteCategory.comp_apply germ_res'
germ_res_assoc 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver stalk germ Quiver.Hom.le	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' germ_res
germ_stalkPullbackHom 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op stalk TopCat.Presheaf TopCat.instCategoryPresheaf pullback germ stalkPullbackHom CategoryTheory.Functor.id CategoryTheory.Functor.comp pushforward CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit pushforwardPullbackAdjunction TopologicalSpace.Opens.map	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.ι_colimMap_assoc CategoryTheory.Functor.map_id CategoryTheory.Limits.colimit.ι_pre CategoryTheory.Category.id_comp
germ_stalkPullbackHom_assoc 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op stalk germ TopCat.Presheaf TopCat.instCategoryPresheaf pullback stalkPullbackHom pushforward CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Adjunction.unit pushforwardPullbackAdjunction TopologicalSpace.Opens.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' germ_stalkPullbackHom
germ_stalkPullbackInv 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.Presheaf TopCat.instCategoryPresheaf pullback Opposite.op stalk DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier germ stalkPullbackInv germToPullbackStalk	—	CategoryTheory.Limits.colimit.ι_desc
germ_stalkPullbackInv_assoc 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.Presheaf TopCat.instCategoryPresheaf pullback Opposite.op stalk germ DFunLike.coe ContinuousMap ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory TopCat.instConcreteCategoryContinuousMapCarrier stalkPullbackInv germToPullbackStalk	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' germ_stalkPullbackInv
germ_stalkSpecializes 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike Specializes	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op stalk germ stalkSpecializes Specializes.mem_open SetLike.coe TopologicalSpace.Opens.isOpen	—	CategoryTheory.Limits.colimit.ι_desc
germ_stalkSpecializes_apply 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike Specializes	DFunLike.coe stalk CategoryTheory.ConcreteCategory.hom stalkSpecializes CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op germ Specializes.mem_open SetLike.coe TopologicalSpace.Opens.isOpen	—	Specializes.mem_open TopologicalSpace.Opens.isOpen CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise germ_stalkSpecializes
germ_stalkSpecializes_assoc 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike Specializes	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op stalk germ stalkSpecializes Specializes.mem_open SetLike.coe TopologicalSpace.Opens.isOpen	—	Specializes.mem_open TopologicalSpace.Opens.isOpen CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' germ_stalkSpecializes
isIso_iff_stalkFunctor_map_iso 📖	mathematical	—	CategoryTheory.IsIso TopCat.Sheaf TopCat.instCategorySheaf CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf stalkFunctor CategoryTheory.Sheaf.val TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology CategoryTheory.Functor.map CategoryTheory.Sheaf.Hom.val	—	CategoryTheory.Functor.map_isIso isIso_of_stalkFunctor_map_iso
isIso_of_stalkFunctor_map_iso 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf stalkFunctor CategoryTheory.Sheaf.val TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology CategoryTheory.Functor.map CategoryTheory.Sheaf.Hom.val	TopCat.Sheaf TopCat.instCategorySheaf	—	app_isIso_of_stalkFunctor_map_iso CategoryTheory.NatIso.isIso_of_isIso_app CategoryTheory.isIso_of_fully_faithful TopCat.Sheaf.forget_full TopCat.Sheaf.forgetFaithful
map_germ_eq_Γgerm 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder stalk CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver germ Γgerm	—	germ_res
map_germ_eq_Γgerm_assoc 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver stalk germ Γgerm	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_germ_eq_Γgerm
mono_iff_stalk_mono 📖	mathematical	—	CategoryTheory.Mono TopCat.Sheaf TopCat.instCategorySheaf CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf stalkFunctor CategoryTheory.Sheaf.val TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology CategoryTheory.Functor.map CategoryTheory.Sheaf.Hom.val	—	stalk_mono_of_mono mono_of_stalk_mono
mono_of_stalk_mono 📖	mathematical	CategoryTheory.Mono CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf stalkFunctor CategoryTheory.Sheaf.val TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology CategoryTheory.Functor.map CategoryTheory.Sheaf.Hom.val	TopCat.Sheaf TopCat.instCategorySheaf	—	CategoryTheory.Sheaf.Hom.mono_iff_presheaf_mono CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder CategoryTheory.NatTrans.mono_iff_mono_app CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits CategoryTheory.ConcreteCategory.mono_iff_injective_of_preservesPullback CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits app_injective_of_stalkFunctor_map_injective
pullback_obj_obj_ext 📖	—	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 CategoryTheory.Functor.id Opposite.op CategoryTheory.Functor.comp pullback pushforward CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit pushforwardPullbackAdjunction Opposite.unop CategoryTheory.Functor.map CategoryTheory.Functor.op TopologicalSpace.Opens.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.homOfLE	—	—	CategoryTheory.Limits.IsColimit.hom_ext CategoryTheory.Functor.instHasLeftKanExtension CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.Category.assoc CategoryTheory.leOfHom CategoryTheory.Functor.lanAdjunction_unit
pullback_obj_obj_ext_iff 📖	mathematical	—	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 CategoryTheory.Functor.id Opposite.op CategoryTheory.Functor.comp pullback pushforward CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit pushforwardPullbackAdjunction Opposite.unop CategoryTheory.Functor.map CategoryTheory.Functor.op TopologicalSpace.Opens.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.homOfLE	—	pullback_obj_obj_ext
pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike Opposite.unop DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.Presheaf TopCat.instCategoryPresheaf CategoryTheory.Functor.id CategoryTheory.Functor.comp pullback pushforward stalk CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit pushforwardPullbackAdjunction germToPullbackStalk TopologicalSpace.Opens.map germ	—	le_refl CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk
pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk_assoc 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike Opposite.unop DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.Presheaf TopCat.instCategoryPresheaf pushforward pullback CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Adjunction.unit pushforwardPullbackAdjunction stalk germToPullbackStalk TopologicalSpace.Opens.map germ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk
pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens.map	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite CategoryTheory.Category.opposite TopCat.Presheaf TopCat.instCategoryPresheaf CategoryTheory.Functor.id Opposite.op CategoryTheory.Functor.comp pullback pushforward stalk DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit pushforwardPullbackAdjunction CategoryTheory.Functor.map CategoryTheory.Functor.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.homOfLE germToPullbackStalk germ	—	CategoryTheory.Functor.lanAdjunction_unit CategoryTheory.Functor.instHasLeftKanExtension CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.Category.assoc CategoryTheory.Limits.IsColimit.fac
pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk_assoc 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens.map	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite CategoryTheory.Category.opposite Opposite.op TopCat.Presheaf TopCat.instCategoryPresheaf pushforward pullback CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Adjunction.unit pushforwardPullbackAdjunction CategoryTheory.Functor.map CategoryTheory.Functor.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.homOfLE stalk DFunLike.coe ContinuousMap ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory TopCat.instConcreteCategoryContinuousMapCarrier germToPullbackStalk germ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk
section_ext 📖	—	DFunLike.coe CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.Sheaf.presheaf Opposite.op stalk CategoryTheory.ConcreteCategory.hom germ	—	—	TopCat.Sheaf.eq_of_locally_eq' Preorder.subsingleton_hom germ_eq
stalkCongr_hom 📖	mathematical	Inseparable TopCat.carrier TopCat.str	CategoryTheory.Iso.hom stalk stalkCongr stalkSpecializes	—	—
stalkCongr_inv 📖	mathematical	Inseparable TopCat.carrier TopCat.str	CategoryTheory.Iso.inv stalk stalkCongr stalkSpecializes	—	—
stalkFunctor_map_germ 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op stalk TopCat.Presheaf TopCat.instCategoryPresheaf stalkFunctor germ CategoryTheory.Functor.map CategoryTheory.NatTrans.app	—	CategoryTheory.Limits.colimit.ι_map CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize
stalkFunctor_map_germ_apply 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike	DFunLike.coe CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf stalkFunctor CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op stalk germ CategoryTheory.NatTrans.app	—	CategoryTheory.ConcreteCategory.comp_apply stalkFunctor_map_germ
stalkFunctor_map_germ_apply' 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike	DFunLike.coe CategoryTheory.ToHom stalk CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map TopCat.Presheaf TopCat.instCategoryPresheaf stalkFunctor CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op germ CategoryTheory.NatTrans.app	—	stalkFunctor_map_germ_apply
stalkFunctor_map_germ_assoc 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op stalk germ TopCat.Presheaf TopCat.instCategoryPresheaf stalkFunctor CategoryTheory.Functor.map CategoryTheory.NatTrans.app	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' stalkFunctor_map_germ
stalkFunctor_map_injective_of_app_injective 📖	mathematical	CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app	TopCat.Presheaf TopCat.instCategoryPresheaf stalkFunctor CategoryTheory.Functor.map	—	germ_exist germ_eq stalkFunctor_map_germ_apply CategoryTheory.ConcreteCategory.comp_apply CategoryTheory.NatTrans.naturality germ_res_apply
stalkFunctor_map_injective_of_isBasis 📖	mathematical	TopologicalSpace.Opens.IsBasis TopCat.carrier TopCat.str CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app	TopCat.Presheaf TopCat.instCategoryPresheaf stalkFunctor CategoryTheory.Functor.map	—	germ_exist_of_isBasis germ_eq_of_isBasis stalkFunctor_map_germ_apply germ_res_apply' CategoryTheory.NatTrans.naturality_apply
stalkFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf stalkFunctor stalk	—	—
stalkFunctor_preserves_mono 📖	mathematical	—	CategoryTheory.Functor.PreservesMonomorphisms TopCat.Sheaf TopCat.instCategorySheaf CategoryTheory.Functor.comp TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Sheaf.forget stalkFunctor	—	CategoryTheory.ConcreteCategory.mono_of_injective app_injective_iff_stalkFunctor_map_injective CategoryTheory.ConcreteCategory.mono_iff_injective_of_preservesPullback CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.NatTrans.mono_iff_mono_app CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits CategoryTheory.presheaf_mono_of_mono CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder
stalkPushforward_germ 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.Presheaf TopCat.instCategoryPresheaf pushforward Opposite.op stalk germ stalkPushforward TopologicalSpace.Opens.map	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.ι_colimMap_assoc CategoryTheory.Functor.map_id CategoryTheory.Limits.colimit.ι_pre CategoryTheory.Category.id_comp
stalkPushforward_germ_apply 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	stalk CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf pushforward stalkPushforward Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op TopologicalSpace.Opens.map germ	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise stalkPushforward_germ
stalkPushforward_germ_assoc 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.Presheaf TopCat.instCategoryPresheaf pushforward Opposite.op stalk germ stalkPushforward TopologicalSpace.Opens.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' stalkPushforward_germ
stalkSpecializes_comp 📖	mathematical	Specializes TopCat.carrier TopCat.str	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct stalk stalkSpecializes Specializes.trans	—	stalk_hom_ext Specializes.trans Specializes.mem_open TopologicalSpace.Opens.isOpen germ_stalkSpecializes_assoc germ_stalkSpecializes
stalkSpecializes_comp_apply 📖	mathematical	Specializes TopCat.carrier TopCat.str	DFunLike.coe stalk CategoryTheory.ConcreteCategory.hom stalkSpecializes Specializes.trans	—	Specializes.trans CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise stalkSpecializes_comp
stalkSpecializes_comp_assoc 📖	mathematical	Specializes TopCat.carrier TopCat.str	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct stalk stalkSpecializes Specializes.trans	—	Specializes.trans CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' stalkSpecializes_comp
stalkSpecializes_refl 📖	mathematical	—	stalkSpecializes specializes_refl TopCat.carrier TopCat.str CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct stalk	—	stalk_hom_ext specializes_refl Specializes.mem_open TopologicalSpace.Opens.isOpen germ_stalkSpecializes CategoryTheory.Category.comp_id
stalkSpecializes_stalkFunctor_map 📖	mathematical	Specializes TopCat.carrier TopCat.str	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct stalk CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf stalkFunctor stalkSpecializes CategoryTheory.Functor.map	—	stalk_hom_ext Specializes.mem_open TopologicalSpace.Opens.isOpen germ_stalkSpecializes_assoc stalkFunctor_map_germ stalkFunctor_map_germ_assoc germ_stalkSpecializes
stalkSpecializes_stalkFunctor_map_apply 📖	mathematical	Specializes TopCat.carrier TopCat.str	DFunLike.coe stalk CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map TopCat.Presheaf TopCat.instCategoryPresheaf stalkFunctor stalkSpecializes	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise stalkSpecializes_stalkFunctor_map
stalkSpecializes_stalkFunctor_map_assoc 📖	mathematical	Specializes TopCat.carrier TopCat.str	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct stalk stalkSpecializes CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf stalkFunctor CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' stalkSpecializes_stalkFunctor_map
stalkSpecializes_stalkPushforward 📖	mathematical	Specializes TopCat.carrier TopCat.str	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct stalk CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf pushforward DFunLike.coe ContinuousMap ContinuousMap.instFunLike TopCat.Hom.hom stalkSpecializes ContinuousMap.map_specializes stalkPushforward CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory TopCat.instConcreteCategoryContinuousMapCarrier	—	stalk_hom_ext ContinuousMap.map_specializes Specializes.mem_open TopologicalSpace.Opens.isOpen germ_stalkSpecializes_assoc stalkPushforward_germ stalkPushforward_germ_assoc germ_stalkSpecializes
stalkSpecializes_stalkPushforward_apply 📖	mathematical	Specializes TopCat.carrier TopCat.str	DFunLike.coe stalk CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf pushforward ContinuousMap ContinuousMap.instFunLike TopCat.Hom.hom CategoryTheory.ConcreteCategory.hom stalkPushforward stalkSpecializes ContinuousMap.map_specializes	—	ContinuousMap.map_specializes CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise stalkSpecializes_stalkPushforward
stalkSpecializes_stalkPushforward_assoc 📖	mathematical	Specializes TopCat.carrier TopCat.str	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct stalk CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf pushforward DFunLike.coe ContinuousMap ContinuousMap.instFunLike TopCat.Hom.hom stalkSpecializes ContinuousMap.map_specializes stalkPushforward	—	ContinuousMap.map_specializes CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' stalkSpecializes_stalkPushforward
stalk_hom_ext 📖	—	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 Opposite.op stalk germ	—	—	CategoryTheory.Limits.colimit.hom_ext CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
stalk_hom_ext_iff 📖	mathematical	—	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 Opposite.op stalk germ	—	stalk_hom_ext
stalk_mono_of_mono 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf stalkFunctor CategoryTheory.Sheaf.val TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology CategoryTheory.Functor.map CategoryTheory.Sheaf.Hom.val	—	CategoryTheory.Functor.map_mono stalkFunctor_preserves_mono
Γgerm_res_apply 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike	DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op stalk CategoryTheory.ConcreteCategory.hom germ Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Γgerm	—	germ_res_apply

TopCat.Presheaf.stalkPushforward

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	—	TopCat.Presheaf.stalkPushforward CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory TopCat.Presheaf.stalk CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	—	TopCat.Presheaf.stalk_hom_ext CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.ι_colimMap_assoc CategoryTheory.Functor.map_id CategoryTheory.Limits.colimit.ι_pre CategoryTheory.Category.id_comp CategoryTheory.Category.assoc CategoryTheory.Limits.colimit.ι_pre_assoc
id 📖	mathematical	—	TopCat.Presheaf.stalkPushforward CategoryTheory.CategoryStruct.id TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory CategoryTheory.Functor.map TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.stalkFunctor CategoryTheory.Functor.obj TopCat.Presheaf.pushforward CategoryTheory.Iso.hom TopCat.Presheaf.Pushforward.id	—	TopCat.Presheaf.stalk_hom_ext CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.ι_colimMap_assoc CategoryTheory.Functor.map_id CategoryTheory.Limits.colimit.ι_pre CategoryTheory.Category.id_comp CategoryTheory.Limits.ι_colimMap
stalkPushforward_iso_of_isInducing 📖	mathematical	Topology.IsInducing TopCat.carrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.IsIso TopCat.Presheaf.stalk CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward TopCat.Presheaf.stalkPushforward	—	CategoryTheory.Functor.Final.comp_hasColimit CategoryTheory.Functor.final_op_of_initial CategoryTheory.Functor.initial_of_adjunction CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize TopCat.Presheaf.stalk_hom_ext TopCat.Presheaf.stalkPushforward_germ CategoryTheory.Limits.colimit.ι_pre CategoryTheory.Iso.isIso_hom

---

← Back to Index