Opens

📁 Source: Mathlib/Topology/Category/TopCat/Opens.lean

Statistics

Metric	Count
Definitions adjunction, functor, botLE, inclusion', inclusionTopIso, infLELeft, infLERight, leMapTop, leSupr, leTop, map, mapComp, mapId, mapIso, mapMapIso, instFunLike, toTopCat, adjunction, functor, functorObj, opensGI	21
Theorems coe_functor_obj, functorFullOfMono, functor_faithful, adjunction_counit_app_self, adjunction_counit_map_functor, apply_def, apply_mk, coe_id, coe_inclusion', comp_apply, functor_map_eq_inf, functor_obj_map_obj, id_apply, inclusion'_hom_apply, inclusion'_map_eq_top, inclusion'_top_functor, infLELeft_apply, infLELeft_apply_mk, isOpenEmbedding, isOpenEmbedding_obj_top, leSupr_apply_mk, mapComp_hom_app, mapComp_inv_app, mapId_hom_app, mapId_inv_app, mapIso_hom_app, mapIso_inv_app, mapIso_refl, mapMapIso_counitIso, mapMapIso_functor, mapMapIso_inverse, mapMapIso_unitIso, map_coe, map_comp_eq, map_comp_map, map_comp_obj, map_comp_obj', map_comp_obj_unop, map_eq, map_functor_eq, map_functor_eq', map_homOfLE, map_iSup, map_id_eq, map_id_obj, map_id_obj', map_id_obj_unop, map_obj, map_top, mem_map, op_map_comp_obj, op_map_id_obj, set_range_inclusion', toTopCat_map, val_apply, functor_map, functor_obj, le_functorObj_iff, map_functorObj, mem_functorObj_iff, functor_obj_injective	61
Total	82

IsOpenMap

Definitions

Name	Category	Theorems
adjunction 📖	CompOp	6 math math: AlgebraicGeometry.SheafedSpace.ofRestrict_hom_c_app, TopologicalSpace.Opens.adjunction_counit_map_functor, TopologicalSpace.Opens.adjunction_counit_app_self, AlgebraicGeometry.Scheme.ofRestrict_toLRSHom_c_app, AlgebraicGeometry.Scheme.ofRestrict_app, AlgebraicGeometry.PresheafedSpace.ofRestrict_c_app
functor 📖	CompOp	56 math math: AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen, AlgebraicGeometry.LocallyRingedSpace.restrict_presheaf_obj, Topology.IsOpenEmbedding.functor_isContinuous, AlgebraicGeometry.Scheme.restrictFunctorΓ_inv_app, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ_assoc, AlgebraicGeometry.Scheme.Opens.topIso_inv, TopologicalSpace.Opens.map_functor_eq', functorNhds_obj_coe, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_c_app, functor_faithful, TopologicalSpace.Opens.isOpenEmbedding_obj_top, functorFullOfMono, AlgebraicGeometry.IsAffineOpen.isoSpec_inv, TopologicalSpace.Opens.inclusion'_top_functor, TopologicalSpace.Opens.map_functor_eq, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict_invApp_apply, AlgebraicGeometry.Scheme.restrict_presheaf_obj, AlgebraicGeometry.PresheafedSpace.GlueData.ι_image_preimage_eq, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ, TopologicalSpace.Opens.functor_obj_map_obj, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.image_preimage_is_empty, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ_apply, AlgebraicGeometry.SheafedSpace.ofRestrict_hom_c_app, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app', AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ_apply, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ_apply, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ_apply, AlgebraicGeometry.Scheme.restrictFunctorΓ_hom_app, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_hom_c_app, TopologicalSpace.Opens.adjunction_counit_map_functor, TopologicalSpace.Opens.adjunction_counit_app_self, coverPreserving, AlgebraicGeometry.Scheme.ofRestrict_toLRSHom_c_app, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso, AlgebraicGeometry.LocallyRingedSpace.restrict_presheaf_map, functorNhds_map, Topology.IsOpenEmbedding.functor_obj_injective, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc, TopologicalSpace.Opens.functor_map_eq_inf, AlgebraicGeometry.Scheme.Opens.mem_basicOpen_toScheme, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ_assoc, AlgebraicGeometry.PresheafedSpace.restrict_presheaf, AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp_π, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ, coe_functor_obj, AlgebraicGeometry.Scheme.Opens.topIso_hom, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ_assoc, AlgebraicGeometry.Scheme.ofRestrict_app, Topology.IsOpenEmbedding.compatiblePreserving, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ_assoc, TopCat.Presheaf.isSheaf_of_isOpenEmbedding, AlgebraicGeometry.PresheafedSpace.ofRestrict_c_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.ofRestrict_invApp_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_functor_obj 📖	mathematical	IsOpenMap TopCat.carrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder functor Set.image	—	—
functorFullOfMono 📖	mathematical	IsOpenMap TopCat.carrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.Functor.Full TopologicalSpace.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder functor	—	TopCat.mono_iff_injective
functor_faithful 📖	mathematical	IsOpenMap TopCat.carrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.Functor.Faithful TopologicalSpace.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder functor	—	Preorder.subsingleton_hom

TopologicalSpace.Opens

Definitions

Name	Category	Theorems
botLE 📖	CompOp	—
inclusion' 📖	CompOp	59 math math: AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_injective, inclusion'_hom_apply, AlgebraicGeometry.Scheme.restrictFunctorΓ_inv_app, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_fromSpec, coe_inclusion', AlgebraicGeometry.Scheme.Opens.topIso_inv, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_preimage_basicOpen, TopCat.GlueData.ι_fromOpenSubsetsGlue, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_hom_apply_asIdeal, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_surjective, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, TopCat.GlueData.ι_fromOpenSubsetsGlue_apply, TopCat.GlueData.ofOpenSubsets_toGlueData_t, isOpenEmbedding_obj_top, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, AlgebraicGeometry.IsAffineOpen.isoSpec_inv, inclusion'_top_functor, map_functor_eq, AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, AlgebraicGeometry.ProjIsoSpecTopComponent.fromSpec_toSpec, isOpenEmbedding, AlgebraicGeometry.PresheafedSpace.restrictTopIso_hom, AlgebraicGeometry.Scheme.restrictFunctorΓ_hom_app, set_range_inclusion', AlgebraicGeometry.SheafedSpace.restrictTopIso_inv, inclusion'_map_eq_top, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq, adjunction_counit_map_functor, AlgebraicGeometry.Scheme.local_affine, adjunction_counit_app_self, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_isIso, AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply, AlgebraicGeometry.PresheafedSpace.ofRestrict_top_c, AlgebraicGeometry.PresheafedSpace.toRestrictTop_c, AlgebraicGeometry.ProjectiveSpectrum.Proj.isIso_toSpec, functor_map_eq_inf, TopologicalSpace.OpenNhds.isOpenEmbedding, TopCat.GlueData.ofOpenSubsets_toGlueData_V, TopCat.GlueData.ofOpenSubsets_toGlueData_f, AlgebraicGeometry.Scheme.Opens.mem_basicOpen_toScheme, AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq_comap, AlgebraicGeometry.PresheafedSpace.toRestrictTop_base, AlgebraicGeometry.Scheme.affineBasisCover_map_range, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_basicOpen, AlgebraicGeometry.Scheme.affineOpenCover_X, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen, AlgebraicGeometry.Scheme.Opens.topIso_hom, AlgebraicGeometry.PresheafedSpace.restrictTopIso_inv, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, AlgebraicGeometry.Scheme.Opens.eq_presheaf_map_eqToHom, AlgebraicGeometry.PresheafedSpace.restrict_top_presheaf, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_bijective, AlgebraicGeometry.SheafedSpace.restrictTopIso_hom
inclusionTopIso 📖	CompOp	4 math math: inclusion'_top_functor, AlgebraicGeometry.PresheafedSpace.toRestrictTop_c, AlgebraicGeometry.PresheafedSpace.toRestrictTop_base, AlgebraicGeometry.PresheafedSpace.restrict_top_presheaf
infLELeft 📖	CompOp	2 math math: infLELeft_apply_mk, infLELeft_apply
infLERight 📖	CompOp	—
leMapTop 📖	CompOp	—
leSupr 📖	CompOp	4 math math: TopCat.Presheaf.SheafConditionEqualizerProducts.res_π, leSupr_apply_mk, TopCat.Sheaf.eq_of_locally_eq_iff, TopCat.Presheaf.SheafConditionEqualizerProducts.res_π_apply
leTop 📖	CompOp	—
map 📖	CompOp	403 math math: AlgebraicGeometry.Γ_map_morphismRestrict, AlgebraicGeometry.Scheme.Modules.pushforward_obj_presheaf_map, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst_assoc, AlgebraicGeometry.Proj.fromOfGlobalSections_resLE, AlgebraicGeometry.Scheme.map_PrimeSpectrum_basicOpen_of_affine, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo, map_id_obj_unop, AlgebraicGeometry.Scheme.Hom.opensRange_pullbackSnd, AlgebraicGeometry.Scheme.Hom.germ_stalkMap_assoc, map_coe, AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inter, AlgebraicGeometry.PresheafedSpace.stalkMap_germ, AlgebraicGeometry.Scheme.Hom.app_invApp'_assoc, AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_comp, AlgebraicGeometry.Scheme.app_eq, AlgebraicGeometry.opensCone_pt, AlgebraicGeometry.morphismRestrict_base_coe, AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality, TopCat.Presheaf.germ_stalkPullbackHom, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_counit_app_app, AlgebraicGeometry.instGeometricallyIrreducibleMorphismRestrict, AlgebraicGeometry.Scheme.Hom.exists_isIso_morphismRestrict_toNormalization, AlgebraicGeometry.morphismRestrict_ι_assoc, AlgebraicGeometry.Scheme.Modules.pushforwardCongr_hom_app_app, AlgebraicGeometry.exists_isAffineOpen_preimage_eq, AlgebraicGeometry.Scheme.Modules.pushforward_obj_obj, AlgebraicGeometry.Scheme.Hom.preimage_bot, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp, TopologicalSpace.OpenNhds.inclusionMapIso_hom, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_preimage_basicOpen, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app_assoc, AlgebraicGeometry.Scheme.Hom.resLE_eq_morphismRestrict, AlgebraicGeometry.Scheme.inv_app, AlgebraicGeometry.image_morphismRestrict_preimage, map_functor_eq', AlgebraicGeometry.SpecMap_preimage_basicOpen, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_apply, map_obj, AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen, AlgebraicGeometry.Scheme.Hom.preimage_le_preimage_of_le, AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι_assoc, TopologicalSpace.OpenNhds.inclusionMapIso_inv, AlgebraicGeometry.Scheme.congr_app, AlgebraicGeometry.IsZariskiLocalAtTarget.restrict, AlgebraicGeometry.Scheme.preimage_comp, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι, AlgebraicGeometry.IsFinite.instMorphismRestrict, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app', TopCat.Presheaf.pushforwardToOfIso_app, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, map_comp_obj_unop, TopCat.Presheaf.stalkPushforward_germ_apply, AlgebraicGeometry.Scheme.Hom.preimage_top, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd_assoc, AlgebraicGeometry.Scheme.Hom.toNormalization_app_preimage, AlgebraicGeometry.Scheme.Hom.toImage_app_injective, AlgebraicGeometry.Scheme.Hom.id_preimage, AlgebraicGeometry.Flat.instMorphismRestrict, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app', AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_ker_glueDataObjι, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_c_app, AlgebraicGeometry.instQuasiCompactMorphismRestrict, AlgebraicGeometry.Scheme.eqToHom_c_app, TopCat.GlueData.ofOpenSubsets_toGlueData_t, AlgebraicGeometry.PresheafedSpace.componentwiseDiagram_map, AlgebraicGeometry.PresheafedSpace.stalkMap_germ_assoc, AlgebraicGeometry.Scheme.Hom.image_preimage_le, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app, AlgebraicGeometry.Scheme.Opens.isoOfLE_hom_ι_assoc, AlgebraicGeometry.Scheme.Hom.fromNormalization_preimage, AlgebraicGeometry.Scheme.Hom.iSup_preimage_eq_top, AlgebraicGeometry.SurjectiveOnStalks.iff_of_isAffine, AlgebraicGeometry.SheafedSpace.comp_hom_c_app, AlgebraicGeometry.IsIntegralHom.isIntegral_app, AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf, AlgebraicGeometry.PresheafedSpace.comp_c_app, AlgebraicGeometry.Scheme.IdealSheafData.ideal_map, AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd, AlgebraicGeometry.IsImmersion.instMorphismRestrict, AlgebraicGeometry.Scheme.Hom.comp_app, mapId_hom_app, AlgebraicGeometry.IsOpenImmersion.range_pullback_fst_of_right, mapComp_hom_app, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app_assoc, AlgebraicGeometry.Scheme.Hom.ι_toNormalization, AlgebraicGeometry.Scheme.Hom.congr_app, AlgebraicGeometry.Scheme.Hom.preimage_iSup, map_id_obj', AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality_assoc, AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom_apply, AlgebraicGeometry.Scheme.Hom.germ_stalkMap_apply, AlgebraicGeometry.Scheme.preimage_basicOpen_top, AlgebraicGeometry.Scheme.Hom.app_appIso_inv_assoc, AlgebraicGeometry.IsAffineOpen.basicOpen_fromSpec_app, TopologicalSpace.OpenNhds.map_obj, TopCat.Presheaf.stalkPushforward_germ_assoc, AlgebraicGeometry.Scheme.opensRange_homOfLE, TopCat.Presheaf.pushforward_map_app, map_homOfLE, AlgebraicGeometry.isIso_morphismRestrict_iff_isIso_app, AlgebraicGeometry.morphismRestrict_base, AlgebraicGeometry.Scheme.ι_image_homOfLE_le_ι_image, AlgebraicGeometry.Scheme.Hom.preimage_image_eq, inclusion'_top_functor, AlgebraicGeometry.isBasis_preimage_isAffineOpen, AlgebraicGeometry.Scheme.Hom.app_surjective, TopCat.Presheaf.presheafEquivOfIso_inverse_obj_map, TopCat.Presheaf.pushforwardEq_hom_app, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_apply, AlgebraicGeometry.Scheme.Spec_map_presheaf_map_eqToHom, map_functor_eq, map_id_obj, AlgebraicGeometry.Scheme.Hom.mem_preimage, AlgebraicGeometry.SheafedSpace.comp_c_app, AlgebraicGeometry.liftCoborder_app, AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_basicOpen, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_assoc, AlgebraicGeometry.Scheme.Hom.preimage_smoothLocus_eq, AlgebraicGeometry.PresheafedSpace.GlueData.ι_image_preimage_eq, AlgebraicGeometry.opensDiagram_map, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_presheafMap, AlgebraicGeometry.Scheme.Hom.app_eq, AlgebraicGeometry.morphismRestrict_ι, AlgebraicGeometry.Scheme.Hom.preimageIso_inv_ι, map_comp_map, AlgebraicGeometry.Scheme.Hom.preimage_basicOpen_top, functor_obj_map_obj, map_comp_obj', mapMapIso_functor, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.image_preimage_is_empty, AlgebraicGeometry.HasAffineProperty.restrict, AlgebraicGeometry.opensDiagramι_app, mapIso_inv_app, TopCat.Presheaf.presheafEquivOfIso_unitIso_hom_app_app, AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app, AlgebraicGeometry.Scheme.Hom.ker_apply, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app'_assoc, AlgebraicGeometry.instIsIsoSchemeMorphismRestrict, AlgebraicGeometry.Scheme.stalkMap_germ_assoc, AlgebraicGeometry.SheafedSpace.ofRestrict_hom_c_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.inv_invApp, AlgebraicGeometry.Scheme.Hom.appIso_inv_app, AlgebraicGeometry.Scheme.Hom.liftCoborder_preimage, op_map_id_obj, AlgebraicGeometry.Scheme.Hom.opensRange_pullbackFst, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι_assoc, mapMapIso_unitIso, AlgebraicGeometry.instLocallyQuasiFiniteMorphismRestrict, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app', AlgebraicGeometry.Scheme.Hom.comp_app_assoc, AlgebraicGeometry.Scheme.comp_app, AlgebraicGeometry.Scheme.Hom.finite_app, AlgebraicGeometry.instGeometricallyReducedMorphismRestrict, AlgebraicGeometry.exists_preimage_eq, AlgebraicGeometry.Scheme.evaluation_naturality, AlgebraicGeometry.Scheme.Hom.ideal_ker_le, AlgebraicGeometry.Scheme.Hom.appIso_hom', AlgebraicGeometry.Scheme.homOfLE_appTop, TopCat.Presheaf.pushforward_obj_obj, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self, AlgebraicGeometry.isClosedImmersion_iff_isAffineHom, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_inv_app'_assoc, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_assoc, AlgebraicGeometry.Scheme.Hom.preimage_basicOpen, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app, AlgebraicGeometry.Scheme.Hom.app_invApp', AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp, map_eq, AlgebraicGeometry.morphismRestrict_comp, AlgebraicGeometry.IsProper.instMorphismRestrict, TopCat.Presheaf.pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk_assoc, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top, AlgebraicGeometry.Scheme.Opens.isoOfLE_hom_ι, AlgebraicGeometry.opensDiagram_obj, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app_assoc, mapMapIso_inverse, AlgebraicGeometry.Spec.sheafedSpaceMap_hom_c_app, AlgebraicGeometry.morphismRestrict_app', AlgebraicGeometry.Scheme.evaluation_naturality_apply, AlgebraicGeometry.opensCone_π_app, AlgebraicGeometry.IsOpenImmersion.opensEquiv_symm_apply, mapId_inv_app, AlgebraicGeometry.PresheafedSpace.comp_c_app_assoc, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_hom_c_app, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp, AlgebraicGeometry.targetAffineLocally_affineAnd_iff, inclusion'_map_eq_top, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd, adjunction_counit_map_functor, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_subschemeCover_map, AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι, AlgebraicGeometry.affinePreimage, AlgebraicGeometry.Scheme.Hom.preimageIso_inv_ι_assoc, AlgebraicGeometry.isAffineHom_iff, compatiblePreserving_opens_map, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app, adjunction_counit_app_self, mem_map, AlgebraicGeometry.instLocallyOfFiniteTypeMorphismRestrict, AlgebraicGeometry.IsIntegralHom.instMorphismRestrict, TopCat.Presheaf.pullback_obj_obj_ext_iff, AlgebraicGeometry.Scheme.ofRestrict_toLRSHom_c_app, AlgebraicGeometry.Scheme.Hom.preimage_sup, AlgebraicGeometry.Scheme.preimage_opensRange_toSpecΓ, AlgebraicGeometry.instIsOpenImmersionMorphismRestrict, AlgebraicGeometry.Scheme.Opens.ι_preimage_self, AlgebraicGeometry.instQuasiSeparatedMorphismRestrict, AlgebraicGeometry.HasAffineProperty.iff_of_iSup_eq_top, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality, AlgebraicGeometry.PresheafedSpace.stalkMap_germ_apply, map_comp_eq, AlgebraicGeometry.Scheme.homOfLE_app, AlgebraicGeometry.Scheme.Hom.comp_preimage, AlgebraicGeometry.Scheme.Hom.naturality_assoc, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_glueDataObjMap, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self_apply, TopCat.Presheaf.pushforward_map_app', TopCat.Presheaf.pushforward_obj_map, AlgebraicGeometry.Scheme.Hom.isIso_app, AlgebraicGeometry.IsAffineOpen.ι_basicOpen_preimage, map_iSup, TopCat.Presheaf.presheafEquivOfIso_unitIso_inv_app_app, AlgebraicGeometry.morphismRestrict_appTop, AlgebraicGeometry.Scheme.Hom.exists_mem_and_isIso_morphismRestrict_toNormalization, TopCat.Presheaf.stalkPushforward_germ, AlgebraicGeometry.SheafedSpace.comp_hom_c_app', AlgebraicGeometry.Scheme.Hom.preimage_opensRange, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen, TopCat.Presheaf.germ_stalkPullbackHom_assoc, TopCat.Presheaf.presheafEquivOfIso_functor_obj_obj, AlgebraicGeometry.PresheafedSpace.componentwiseDiagram_obj, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_apply, AlgebraicGeometry.HasAffineProperty.affineAnd_iff, AlgebraicGeometry.IsOpenImmersion.app_eq_appIso_inv_app_of_comp_eq, AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι_app, AlgebraicGeometry.IsOpenImmersion.ΓIso_inv, AlgebraicGeometry.IsOpenImmersion.range_pullback_snd_of_left, AlgebraicGeometry.Scheme.Opens.isoOfLE_inv_ι, AlgebraicGeometry.Scheme.Hom.ι_toNormalization_assoc, AlgebraicGeometry.IsLocalAtTarget.restrict, Topology.IsInducing.map_functorObj, AlgebraicGeometry.Scheme.Hom.fromNormalization_app_assoc, AlgebraicGeometry.Proj.fromOfGlobalSections_morphismRestrict, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app_apply, AlgebraicGeometry.Scheme.stalkMap_germ_apply, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc, AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatAppObjOpensOpensFunctor, AlgebraicGeometry.Scheme.ker_morphismRestrict_ideal, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι, AlgebraicGeometry.Scheme.Hom.germ_stalkMap, AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app, AlgebraicGeometry.Scheme.Hom.preimage_iSup_eq_top, functor_map_eq_inf, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_unit_app_app, AlgebraicGeometry.IsLocalAtTarget.iff_of_iSup_eq_top, AlgebraicGeometry.Scheme.Hom.isIntegral_app, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.isIntegralHom_iff, TopCat.GlueData.ofOpenSubsets_toGlueData_V, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app, TopCat.GlueData.ofOpenSubsets_toGlueData_f, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom, AlgebraicGeometry.Scheme.Hom.coe_preimage, AlgebraicGeometry.Scheme.preimage_eq_top_of_closedPoint_mem, AlgebraicGeometry.Proj.awayι_preimage_basicOpen, AlgebraicGeometry.IsFinite.finite_app, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_assoc, AlgebraicGeometry.IsIntegralHom.integral_app, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp_app_assoc, TopCat.Presheaf.presheafEquivOfIso_counitIso_inv_app_app, AlgebraicGeometry.IsAffineOpen.preimage_of_isIso, AlgebraicGeometry.instIsClosedImmersionMorphismRestrict, AlgebraicGeometry.Scheme.Hom.preimage_inf, op_map_comp_obj, AlgebraicGeometry.isPullback_morphismRestrict, AlgebraicGeometry.Scheme.Hom.appIso_hom, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_apply, AlgebraicGeometry.Scheme.evaluation_naturality_assoc, AlgebraicGeometry.IsAffineOpen.preimage_of_isOpenImmersion, AlgebraicGeometry.targetAffineLocally_affineAnd_iff', AlgebraicGeometry.quasiCompact_iff_forall_isAffineOpen, AlgebraicGeometry.instSmoothMorphismRestrict, AlgebraicGeometry.Scheme.Opens.ι_app_self, mapComp_inv_app, AlgebraicGeometry.Scheme.Hom.naturality, AlgebraicGeometry.exists_isFinite_morphismRestrict_of_finite_preimage_singleton, AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.to_basicOpen, map_comp_obj, AlgebraicGeometry.IsOpenImmersion.image_preimage_eq_preimage_image_of_isPullback, AlgebraicGeometry.LocallyRingedSpace.preimage_basicOpen, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst_assoc, mapIso_hom_app, AlgebraicGeometry.Scheme.fromSpecStalk_app, AlgebraicGeometry.instGeometricallyIntegralMorphismRestrict, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app_surjective, AlgebraicGeometry.Scheme.preimage_zeroLocus, AlgebraicGeometry.PresheafedSpace.congr_app, TopCat.Presheaf.presheafEquivOfIso_counitIso_hom_app_app, AlgebraicGeometry.affineOpensRestrict_symm_apply_coe, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_snd_of_left, AlgebraicGeometry.IsIntegralHom.hasAffineProperty, AlgebraicGeometry.Scheme.Hom.preimage_mono, AlgebraicGeometry.Scheme.SpecMap_presheaf_map_eqToHom, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict, AlgebraicGeometry.isFinite_iff, TopCat.Presheaf.presheafEquivOfIso_inverse_obj_obj, instIsContinuousOpensCarrierMapGrothendieckTopology, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_fst_of_right, AlgebraicGeometry.IsOpenImmersion.range_pullbackFst, AlgebraicGeometry.Scheme.Opens.ι_app, AlgebraicGeometry.Scheme.Modules.pushforwardCongr_inv_app_app, AlgebraicGeometry.Scheme.Hom.isCompact_preimage, AlgebraicGeometry.instUniversallyClosedMorphismRestrict, AlgebraicGeometry.SheafedSpace.congr_hom_app, AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatApp, AlgebraicGeometry.Scheme.Hom.inv_image, map_top, AlgebraicGeometry.IsPreimmersion.instMorphismRestrict, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app', AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp_π, TopCat.Presheaf.presheafEquivOfIso_functor_map_app, Topology.IsInducing.le_functorObj_iff, AlgebraicGeometry.exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimage, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_hom, AlgebraicGeometry.IsSeparated.instMorphismRestrict, mapMapIso_counitIso, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_apply, AlgebraicGeometry.quasiCompact_iff_forall_affine, AlgebraicGeometry.instLocallyOfFinitePresentationMorphismRestrict, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen', AlgebraicGeometry.IsAffineOpen.app_basicOpen_eq_away_map, AlgebraicGeometry.Scheme.preimage_basicOpen, AlgebraicGeometry.Scheme.Opens.instIsIsoCommRingCatAppLEιTopToScheme, AlgebraicGeometry.IsAffineHom.isAffine_preimage, TopCat.Presheaf.toPushforwardOfIso_app, AlgebraicGeometry.IsAffineOpen.ΓSpecIso_hom_fromSpec_app, AlgebraicGeometry.Scheme.comp_app_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_assoc, AlgebraicGeometry.morphismRestrict_app, AlgebraicGeometry.Scheme.Hom.toImage_app, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_invApp, coverPreserving_opens_map, AlgebraicGeometry.Scheme.ofRestrict_app, AlgebraicGeometry.SheafedSpace.congr_app, AlgebraicGeometry.Scheme.OpenCover.restrict_X, AlgebraicGeometry.IsAffineOpen.fromSpec_app_of_le, AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen, AlgebraicGeometry.Scheme.Hom.app_appIso_inv, AlgebraicGeometry.Scheme.Hom.normalizationObjIso_hom_val, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app, AlgebraicGeometry.Scheme.Hom.appLE_eq_app, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp_app_assoc, AlgebraicGeometry.IsOpenImmersion.app_eq_invApp_app_of_comp_eq_aux, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.colimitDesc_preimage, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_invApp, TopologicalSpace.OpenNhds.inclusionMapIso_inv_app, AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_apply, AlgebraicGeometry.sourceAffineLocally_morphismRestrict, AlgebraicGeometry.Etale.instMorphismRestrict, AlgebraicGeometry.Scheme.IdealSheafData.ideal_map_of_isAffineHom, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_inv_app'_assoc, AlgebraicGeometry.Scheme.Modules.pushforward_map_app, AlgebraicGeometry.Scheme.Hom.inv_app, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app', AlgebraicGeometry.Scheme.Hom.isQuasiSeparated_preimage, AlgebraicGeometry.Scheme.Hom.app_injective, AlgebraicGeometry.Scheme.exists_isOpenCover_and_isAffine, AlgebraicGeometry.LocallyRingedSpace.comp_c_app, TopCat.Presheaf.presheafEquivOfIso_functor_obj_map, AlgebraicGeometry.Scheme.stalkMap_germ, AlgebraicGeometry.Proj.fromOfGlobalSections_preimage_basicOpen, TopCat.Presheaf.presheafEquivOfIso_inverse_map_app, TopologicalSpace.OpenNhds.inclusionMapIso_hom_app, mapIso_refl, AlgebraicGeometry.Scheme.Hom.fromNormalization_app, AlgebraicGeometry.Scheme.Hom.eqToHom_app, instRepresentablyFlatOpensCarrierMap, TopCat.Presheaf.pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk, AlgebraicGeometry.IsOpenImmersion.lift_app, AlgebraicGeometry.isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange, AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv_symm_apply_coe, AlgebraicGeometry.SheafedSpace.comp_c_app', AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_apply, AlgebraicGeometry.PresheafedSpace.ofRestrict_c_app, AlgebraicGeometry.IsAffineOpen.preimage, AlgebraicGeometry.Scheme.Opens.isoOfLE_inv_ι_assoc, AlgebraicGeometry.Spec.map_app, AlgebraicGeometry.morphismRestrict_id, map_id_eq, AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ
mapComp 📖	CompOp	2 math math: mapComp_hom_app, mapComp_inv_app
mapId 📖	CompOp	2 math math: mapId_hom_app, mapId_inv_app
mapIso 📖	CompOp	3 math math: mapIso_inv_app, mapIso_hom_app, mapIso_refl
mapMapIso 📖	CompOp	10 math math: mapMapIso_functor, TopCat.Presheaf.presheafEquivOfIso_unitIso_hom_app_app, mapMapIso_unitIso, mapMapIso_inverse, TopCat.Presheaf.presheafEquivOfIso_unitIso_inv_app_app, TopCat.Presheaf.presheafEquivOfIso_counitIso_inv_app_app, TopCat.Presheaf.presheafEquivOfIso_counitIso_hom_app_app, TopCat.Presheaf.presheafEquivOfIso_functor_map_app, mapMapIso_counitIso, TopCat.Presheaf.presheafEquivOfIso_inverse_map_app
toTopCat 📖	CompOp	67 math math: AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_injective, inclusion'_hom_apply, AlgebraicGeometry.Scheme.restrictFunctorΓ_inv_app, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_fromSpec, coe_inclusion', AlgebraicGeometry.Scheme.Opens.topIso_inv, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_preimage_basicOpen, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_hom_apply_asIdeal, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_surjective, TopCat.GlueData.ofOpenSubsets_toGlueData_U, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, TopCat.GlueData.ofOpenSubsets_toGlueData_t, isOpenEmbedding_obj_top, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, AlgebraicGeometry.IsAffineOpen.isoSpec_inv, inclusion'_top_functor, TopCat.GlueData.instIsIsoT, TopCat.presheafToTop_obj, map_functor_eq, AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, AlgebraicGeometry.ProjIsoSpecTopComponent.fromSpec_toSpec, isOpenEmbedding, AlgebraicGeometry.PresheafedSpace.restrictTopIso_hom, TopCat.GlueData.MkCore.t_inv, AlgebraicGeometry.Scheme.restrictFunctorΓ_hom_app, set_range_inclusion', AlgebraicGeometry.SheafedSpace.restrictTopIso_inv, inclusion'_map_eq_top, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq, adjunction_counit_map_functor, AlgebraicGeometry.Scheme.local_affine, adjunction_counit_app_self, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_isIso, AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply, AlgebraicGeometry.PresheafedSpace.ofRestrict_top_c, TopCat.GlueData.MkCore.t_id, AlgebraicGeometry.PresheafedSpace.toRestrictTop_c, AlgebraicGeometry.ProjectiveSpectrum.Proj.isIso_toSpec, functor_map_eq_inf, TopologicalSpace.OpenNhds.isOpenEmbedding, TopCat.GlueData.ofOpenSubsets_toGlueData_V, TopCat.GlueData.ofOpenSubsets_toGlueData_f, AlgebraicGeometry.Scheme.Opens.mem_basicOpen_toScheme, AlgebraicGeometry.Scheme.Opens.ι_app_self, AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, TopCat.GlueData.MkCore.t_inter, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq_comap, AlgebraicGeometry.Scheme.homOfLE_base, AlgebraicGeometry.PresheafedSpace.toRestrictTop_base, AlgebraicGeometry.Scheme.affineBasisCover_map_range, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_basicOpen, toTopCat_map, AlgebraicGeometry.Scheme.affineOpenCover_X, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen, AlgebraicGeometry.Scheme.Opens.topIso_hom, AlgebraicGeometry.PresheafedSpace.restrictTopIso_inv, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, TopCat.GlueData.MkCore.cocycle, AlgebraicGeometry.Scheme.Opens.eq_presheaf_map_eqToHom, AlgebraicGeometry.PresheafedSpace.restrict_top_presheaf, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_bijective, AlgebraicGeometry.SheafedSpace.restrictTopIso_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjunction_counit_app_self 📖	mathematical	—	CategoryTheory.NatTrans.app TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder CategoryTheory.Functor.comp CategoryTheory.Functor.obj TopCat TopCat.instCategory toTopCat map inclusion' IsOpenMap.functor Topology.IsOpenEmbedding.isOpenMap DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier isOpenEmbedding CategoryTheory.Functor.id CategoryTheory.Adjunction.counit IsOpenMap.adjunction CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct	—	Topology.IsOpenEmbedding.isOpenMap isOpenEmbedding Preorder.subsingleton_hom
adjunction_counit_map_functor 📖	mathematical	—	CategoryTheory.NatTrans.app TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder CategoryTheory.Functor.comp CategoryTheory.Functor.obj TopCat TopCat.instCategory toTopCat map inclusion' IsOpenMap.functor Topology.IsOpenEmbedding.isOpenMap DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier isOpenEmbedding CategoryTheory.Functor.id CategoryTheory.Adjunction.counit IsOpenMap.adjunction CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct	—	Topology.IsOpenEmbedding.isOpenMap isOpenEmbedding Preorder.subsingleton_hom
apply_def 📖	mathematical	—	DFunLike.coe Quiver.Hom TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Preorder.smallCategory PartialOrder.toPreorder instPartialOrder SetLike.instMembership instSetLike opensHom.instFunLike Quiver.Hom.le	—	—
apply_mk 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership instSetLike	DFunLike.coe Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Preorder.smallCategory PartialOrder.toPreorder instPartialOrder opensHom.instFunLike Quiver.Hom.le	—	—
coe_id 📖	mathematical	—	DFunLike.coe Quiver.Hom TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Preorder.smallCategory PartialOrder.toPreorder instPartialOrder SetLike.instMembership instSetLike opensHom.instFunLike	—	—
coe_inclusion' 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder TopCat TopCat.instCategory toTopCat CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier inclusion' SetLike.instMembership instSetLike	—	—
comp_apply 📖	mathematical	—	DFunLike.coe Quiver.Hom TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Preorder.smallCategory PartialOrder.toPreorder instPartialOrder SetLike.instMembership instSetLike opensHom.instFunLike CategoryTheory.CategoryStruct.comp	—	—
functor_map_eq_inf 📖	mathematical	—	CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder TopCat TopCat.instCategory toTopCat IsOpenMap.functor inclusion' Topology.IsOpenEmbedding.isOpenMap DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier isOpenEmbedding map SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	ext Topology.IsOpenEmbedding.isOpenMap isOpenEmbedding Set.image_congr Set.image_preimage_eq_inter_range set_range_inclusion'
functor_obj_map_obj 📖	mathematical	IsOpenMap TopCat.carrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.Functor.obj TopologicalSpace.Opens Preorder.smallCategory PartialOrder.toPreorder instPartialOrder IsOpenMap.functor map SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	ext Set.ext
id_apply 📖	mathematical	—	DFunLike.coe Quiver.Hom TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Preorder.smallCategory PartialOrder.toPreorder instPartialOrder SetLike.instMembership instSetLike opensHom.instFunLike	—	—
inclusion'_hom_apply 📖	mathematical	—	DFunLike.coe ContinuousMap TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership instSetLike instTopologicalSpaceSubtype ContinuousMap.instFunLike TopCat.Hom.hom CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder instPartialOrder TopCat TopCat.instCategory toTopCat inclusion'	—	—
inclusion'_map_eq_top 📖	mathematical	—	CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder TopCat TopCat.instCategory toTopCat map inclusion' Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	ext Subtype.coe_preimage_self
inclusion'_top_functor 📖	mathematical	—	IsOpenMap.functor CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder TopCat TopCat.instCategory toTopCat Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder inclusion' Topology.IsOpenEmbedding.isOpenMap DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier isOpenEmbedding map CategoryTheory.Iso.inv inclusionTopIso	—	CategoryTheory.Functor.ext Topology.IsOpenEmbedding.isOpenMap isOpenEmbedding ext Set.ext Preorder.subsingleton_hom
infLELeft_apply 📖	mathematical	—	DFunLike.coe Quiver.Hom TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Preorder.smallCategory PartialOrder.toPreorder instPartialOrder SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice SetLike.instMembership instSetLike opensHom.instFunLike infLELeft inf_le_left	—	—
infLELeft_apply_mk 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership instSetLike SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	DFunLike.coe Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Preorder.smallCategory PartialOrder.toPreorder instPartialOrder opensHom.instFunLike infLELeft inf_le_left	—	—
isOpenEmbedding 📖	mathematical	—	Topology.IsOpenEmbedding TopCat.carrier CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder TopCat TopCat.instCategory toTopCat DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier inclusion'	—	IsOpen.isOpenEmbedding_subtypeVal is_open'
isOpenEmbedding_obj_top 📖	mathematical	—	CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder TopCat TopCat.instCategory toTopCat IsOpenMap.functor inclusion' Topology.IsOpenEmbedding.isOpenMap DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier isOpenEmbedding Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	ext Topology.IsOpenEmbedding.isOpenMap isOpenEmbedding Set.image_univ Subtype.range_coe
leSupr_apply_mk 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership instSetLike	DFunLike.coe Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Preorder.smallCategory PartialOrder.toPreorder instPartialOrder iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice opensHom.instFunLike leSupr le_iSup	—	—
mapComp_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder map CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category mapComp CategoryTheory.eqToHom CategoryTheory.Functor.obj map_comp_obj	—	—
mapComp_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder CategoryTheory.Functor.comp map CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category mapComp CategoryTheory.eqToHom CategoryTheory.Functor.obj	—	—
mapId_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder map CategoryTheory.CategoryStruct.id TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category mapId CategoryTheory.eqToHom CategoryTheory.Functor.obj map_id_obj	—	—
mapId_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder CategoryTheory.Functor.id map CategoryTheory.CategoryStruct.id TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category mapId CategoryTheory.eqToHom CategoryTheory.Functor.obj	—	—
mapIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder map CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category mapIso CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
mapIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder map CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category mapIso CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
mapIso_refl 📖	mathematical	—	mapIso CategoryTheory.Iso.refl CategoryTheory.Functor TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder CategoryTheory.Functor.category map	—	—
mapMapIso_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder mapMapIso CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.comp map CategoryTheory.Iso.inv TopCat TopCat.instCategory CategoryTheory.Iso.hom CategoryTheory.Functor.id CategoryTheory.eqToIso CategoryTheory.Functor.obj	—	—
mapMapIso_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder mapMapIso map CategoryTheory.Iso.hom TopCat TopCat.instCategory	—	—
mapMapIso_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder mapMapIso map CategoryTheory.Iso.inv TopCat TopCat.instCategory	—	—
mapMapIso_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder mapMapIso CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.id CategoryTheory.Functor.comp map CategoryTheory.Iso.hom TopCat TopCat.instCategory CategoryTheory.Iso.inv CategoryTheory.eqToIso CategoryTheory.Functor.obj	—	—
map_coe 📖	mathematical	—	SetLike.coe TopologicalSpace.Opens TopCat.carrier TopCat.str instSetLike CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder instPartialOrder map Set.preimage DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	—	—
map_comp_eq 📖	mathematical	—	map CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory CategoryTheory.Functor.comp TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder	—	—
map_comp_map 📖	mathematical	—	CategoryTheory.Functor.map TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder map CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory CategoryTheory.Functor.obj	—	—
map_comp_obj 📖	mathematical	—	CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder map CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory	—	—
map_comp_obj' 📖	mathematical	IsOpen TopCat.carrier TopCat.str	CategoryTheory.Functor.obj TopologicalSpace.Opens Preorder.smallCategory PartialOrder.toPreorder instPartialOrder map CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory	—	—
map_comp_obj_unop 📖	mathematical	—	CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder map CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory Opposite.unop	—	—
map_eq 📖	mathematical	—	map	—	—
map_functor_eq 📖	mathematical	—	CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder TopCat TopCat.instCategory toTopCat map inclusion' IsOpenMap.functor Topology.IsOpenEmbedding.isOpenMap DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier isOpenEmbedding	—	map_functor_eq' isOpenEmbedding
map_functor_eq' 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.Functor.obj TopologicalSpace.Opens Preorder.smallCategory PartialOrder.toPreorder instPartialOrder map IsOpenMap.functor Topology.IsOpenEmbedding.isOpenMap	—	ext Topology.IsOpenEmbedding.isOpenMap Set.preimage_image_eq Topology.IsEmbedding.injective Topology.IsOpenEmbedding.toIsEmbedding
map_homOfLE 📖	mathematical	TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.toLE PartialOrder.toPreorder instPartialOrder	CategoryTheory.Functor.map Preorder.smallCategory map CategoryTheory.homOfLE CategoryTheory.Functor.obj	—	—
map_iSup 📖	mathematical	—	CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder map iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	ext Set.ext coe_iSup Set.preimage_iUnion
map_id_eq 📖	mathematical	—	map CategoryTheory.CategoryStruct.id TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory CategoryTheory.Functor.id TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder	—	—
map_id_obj 📖	mathematical	—	CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder map CategoryTheory.CategoryStruct.id TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory	—	—
map_id_obj' 📖	mathematical	IsOpen TopCat.carrier TopCat.str	CategoryTheory.Functor.obj TopologicalSpace.Opens Preorder.smallCategory PartialOrder.toPreorder instPartialOrder map CategoryTheory.CategoryStruct.id TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory	—	—
map_id_obj_unop 📖	mathematical	—	CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder map CategoryTheory.CategoryStruct.id TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory Opposite.unop	—	map_id_obj
map_obj 📖	mathematical	IsOpen TopCat.carrier TopCat.str	CategoryTheory.Functor.obj TopologicalSpace.Opens Preorder.smallCategory PartialOrder.toPreorder instPartialOrder map Set.preimage DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier IsOpen.preimage TopCat.Hom.hom ContinuousMap.continuous	—	—
map_top 📖	mathematical	—	CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder map Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—
mem_map 📖	mathematical	—	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership instSetLike CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder instPartialOrder map DFunLike.coe ContinuousMap ContinuousMap.instFunLike TopCat.Hom.hom	—	—
op_map_comp_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder instPartialOrder CategoryTheory.Functor.op map CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory	—	—
op_map_id_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder instPartialOrder CategoryTheory.Functor.op map CategoryTheory.CategoryStruct.id TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory	—	map_id_obj
set_range_inclusion' 📖	mathematical	—	Set.range TopCat.carrier CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.str Preorder.smallCategory PartialOrder.toPreorder instPartialOrder TopCat TopCat.instCategory toTopCat DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier inclusion' SetLike.coe instSetLike	—	Set.ext
toTopCat_map 📖	mathematical	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership instSetLike	DFunLike.coe CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder instPartialOrder TopCat TopCat.instCategory toTopCat CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier CategoryTheory.Functor.map Quiver.Hom.le	—	—
val_apply 📖	mathematical	—	TopCat.carrier TopologicalSpace.Opens TopCat.str SetLike.instMembership instSetLike DFunLike.coe Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Preorder.smallCategory PartialOrder.toPreorder instPartialOrder opensHom.instFunLike	—	—

TopologicalSpace.Opens.opensHom

Definitions

Name	Category	Theorems
instFunLike 📖	CompOp	15 math math: TopCat.PrelocalPredicate.res, TopologicalSpace.Opens.id_apply, TopCat.presheafToType_map, TopologicalSpace.Opens.comp_apply, TopologicalSpace.Opens.infLELeft_apply_mk, TopologicalSpace.Opens.coe_id, TopCat.presheafToTypes_map, TopCat.subpresheafToTypes_map_coe, TopologicalSpace.Opens.leSupr_apply_mk, AlgebraicGeometry.StructureSheaf.res_apply, TopologicalSpace.Opens.apply_mk, TopologicalSpace.Opens.infLELeft_apply, TopologicalSpace.Opens.apply_def, AlgebraicGeometry.Proj.res_apply, TopologicalSpace.Opens.val_apply

Topology.IsInducing

Definitions

Name	Category	Theorems
adjunction 📖	CompOp	—
functor 📖	CompOp	4 math math: functorNhds_obj_coe, functor_obj, functorNhds_map, functor_map
functorObj 📖	CompOp	5 math math: mem_functorObj_iff, map_functorObj, functor_obj, le_functorObj_iff, functor_map
opensGI 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
functor_map 📖	mathematical	Topology.IsInducing TopCat.carrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.Functor.map TopologicalSpace.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder functor CategoryTheory.homOfLE functorObj	—	—
functor_obj 📖	mathematical	Topology.IsInducing TopCat.carrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.Functor.obj TopologicalSpace.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder functor functorObj	—	—
le_functorObj_iff 📖	mathematical	Topology.IsInducing TopCat.carrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	TopologicalSpace.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder functorObj CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens.map	—	isOpen_iff mem_functorObj_iff TopologicalSpace.Opens.mem_sSup IsOpen.union TopologicalSpace.Opens.is_open' TopologicalSpace.Opens.ext Set.union_eq_right Set.mem_union_left
map_functorObj 📖	mathematical	Topology.IsInducing TopCat.carrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.Functor.obj TopologicalSpace.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map functorObj	—	le_antisymm isOpen_iff TopologicalSpace.Opens.mem_sSup
mem_functorObj_iff 📖	mathematical	Topology.IsInducing TopCat.carrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike functorObj	—	map_functorObj

Topology.IsOpenEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
functor_obj_injective 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	TopologicalSpace.Opens CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder IsOpenMap.functor isOpenMap	—	isOpenMap TopologicalSpace.Opens.ext Set.image_injective Topology.IsEmbedding.injective toIsEmbedding

---

← Back to Index