OpenImmersion

📁 Source: Mathlib/AlgebraicGeometry/OpenImmersion.lean

Statistics

Metric	Count
Definitions IsOpenImmersion, forgetCreatesPullbackOfLeft, forgetCreatesPullbackOfRight, isoOfRangeEq, isoRestrict, opensEquiv, ΓIso, ΓIsoTop, scheme, toScheme, toSchemeHom, appIso, opensFunctor, opensRange, ofRestrict, restrict, stalkMapIsoOfIsPullback, «term_''ᵁ_»	18
Theorems app_eq_appIso_inv_app_of_comp_eq, app_eq_invApp_app_of_comp_eq_aux, app_ΓIso_hom, app_ΓIso_hom_apply, app_ΓIso_hom_assoc, comp, comp_lift, comp_lift_assoc, hasLimit_cospan_forget_of_left, hasLimit_cospan_forget_of_left', hasLimit_cospan_forget_of_right, hasLimit_cospan_forget_of_right', hasPullback_of_left, hasPullback_of_right, iff_isIso_stalkMap, iff_stalk_iso, image_preimage_eq_preimage_image_of_isPullback, instFstScheme, instHasOfPostcompPropertyScheme, instIsIsoCommRingCatStalkMap, instIsOpenImmersionMapSchemeLocallyRingedSpaceForgetToLocallyRingedSpace, instLift, instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace, instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace_1, instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop, instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop_1, instPreservesLimitSchemeWalkingCospanCospanForget, instPreservesLimitSchemeWalkingCospanCospanForget_1, instSndScheme, instπWalkingCospanSchemeCospanOne, isIso, isOpen_range, isPullback, isPullback_lift_id, isoOfRangeEq_hom_fac, isoOfRangeEq_hom_fac_assoc, isoOfRangeEq_inv_fac, isoOfRangeEq_inv_fac_assoc, le_monomorphisms, lift_app, lift_fac, lift_fac_assoc, lift_uniq, map_ΓIso_hom, map_ΓIso_inv, map_ΓIso_inv_apply, map_ΓIso_inv_assoc, mono, ofRestrict, of_comp, of_isIso, of_isIso_stalkMap, of_isLocalization, of_stalk_iso, opensEquiv_apply_coe, opensEquiv_symm_apply, opensRange_pullback_fst_of_right, opensRange_pullback_snd_of_left, range_pullbackFst, range_pullbackSnd, range_pullback_fst_of_right, range_pullback_snd_of_left, range_pullback_to_base_of_left, range_pullback_to_base_of_right, to_iso, ΓIso_inv, scheme_eq_of_locallyRingedSpace_eq, scheme_toScheme, toSchemeHom_isOpenImmersion, toSchemeHom_toPshHom, toScheme_toLocallyRingedSpace, appIso_hom, appIso_hom', appIso_inv_app, appIso_inv_appLE, appIso_inv_appLE_assoc, appIso_inv_app_apply, appIso_inv_app_assoc, appIso_inv_app_presheafMap, appIso_inv_naturality, appIso_inv_naturality_assoc, appLE_appIso_inv, appLE_appIso_inv_apply, appLE_appIso_inv_assoc, app_appIso_inv, app_appIso_inv_assoc, app_invApp', app_invApp'_assoc, apply_mem_image_iff, coe_image, coe_opensRange, comp_appIso, comp_image, id_appIso, id_image, image_iSup, image_iSup₂, image_injective, image_le_image_iff, image_le_image_of_le, image_le_opensRange, image_mono, image_preimage_eq_opensRange_inf, image_preimage_eq_opensRange_inter, image_preimage_le, image_top_eq_opensRange, instIsContinuousOpensOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, instIsIsoCommRingCatAppObjOpensOpensFunctor, inv_image, isIso_app, isOpenEmbedding, map_mem_image_iff, mem_opensRange, opensFunctor_map_homOfLE, opensRange_comp, opensRange_comp_of_isIso, opensRange_of_isIso, opensRange_pullbackFst, opensRange_pullbackSnd, preimage_image_eq, preimage_opensRange, basic_open_isOpenImmersion, exists_affine_mem_range_and_range_subset, image_basicOpen, image_zeroLocus, instIsOpenImmersionMapOfHomAwayAlgebraMap, isOpenImmersion_SpecMap_localizationAway, ofRestrict_app, ofRestrict_appIso, ofRestrict_appLE, ofRestrict_toLRSHom_base, ofRestrict_toLRSHom_c_app, restrict_carrier, restrict_presheaf_map, restrict_presheaf_obj, restrict_toPresheafedSpace, isIso_iff_isIso_stalkMap, isIso_iff_isOpenImmersion, isIso_iff_isOpenImmersion_and_epi_base, isIso_iff_stalk_iso, isIso_of_isOpenImmersion_of_opensRange_eq_top, isOpenImmersion_isMultiplicative, isOpenImmersion_isStableUnderComposition, isOpenImmersion_respectsIso, isOpenImmersion_stableUnderBaseChange	145
Total	163

AlgebraicGeometry

Definitions

Name	Category	Theorems
IsOpenImmersion 📖	CompOp	296 math math: Scheme.Pullback.gluedLiftPullbackMap_snd, IsOpenImmersion.of_openCover_source, descendsAlong_isOpenImmersion_surjective_inf_flat_inf_quasicompact', Scheme.AffineOpenCover.openCover_f, Scheme.Cover.RelativeGluingData.cover_X, Scheme.Cover.gluedCoverT'_snd_snd_assoc, Scheme.Pullback.gluedLiftPullbackMap_snd_assoc, instIsAffineXSchemeFiniteSubcover, instIsLocallyArtinianXScheme, Scheme.Cover.LocallyDirected.ofIsBasisOpensRange_le_iff, Scheme.affineBasisCover_is_basis, Scheme.Pullback.openCoverOfLeftRight_f, Scheme.OpenCover.map_glueMorphismsOverOfLocallyDirected_left_assoc, IsOpenImmersion.instLift, Scheme.Pullback.t'_snd_fst_fst_assoc, Proj.mapAffineOpenCover_I₀, isOpenImmersion_isStableUnderComposition, Scheme.Cover.glued_cover_cocycle_fst, sigmaOpenCover_X, Scheme.Hom.iUnion_support_ker_openCover_map_comp, Scheme.Pullback.openCoverOfBase_I₀, Algebra.FormallyUnramified.isOpenImmersion_SpecMap_lmul, Scheme.OpenCover.finiteSubcover_f, Scheme.Pullback.openCoverOfBase_f, Scheme.Pullback.openCoverOfRight_I₀, Scheme.basic_open_isOpenImmersion, Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_snd_assoc, isNoetherian_iff_of_finite_affine_openCover, ExistsHomHomCompEqCompAux.exists_eq, Scheme.Cover.ColimitGluingData.isPullback, Scheme.openCoverOfIsOpenCover_I₀, instIsOpenImmersionLeftSchemeDiscretePUnitMapWalkingSpanOverTopMorphismPropertySpan, ExistsHomHomCompEqCompAux.h𝒰S, Scheme.Cover.glued_cover_cocycle, Scheme.affineOpenCover_I₀, Scheme.Cover.gluedCover_t, Scheme.Pullback.t_fst_snd_assoc, Scheme.Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι, Scheme.Cover.RelativeGluingData.cover_I₀, sourceLocalClosure.iff_forall_exists, Scheme.Cover.gluedCover_U, Scheme.OpenCover.map_glueMorphismsOfLocallyDirected_assoc, IsOpenImmersion.iff_isIso_stalkMap, Scheme.isOpenImmersion_SpecMap_localizationAway, Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom, Scheme.exists_affine_mem_range_and_range_subset, Scheme.instIsOpenImmersionMapOfHomAwayAlgebraMap, Scheme.affineOpenCover_idx, Scheme.Hom.fromNormalization_preimage, HasRingHomProperty.respects_isOpenImmersion, Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap, Scheme.OpenCover.map_glueMorphismsOverOfLocallyDirected_left, Scheme.OpenCover.map_glueMorphismsOfLocallyDirected, Scheme.Pullback.left_affine_comp_pullback_hasPullback, IsLocalAtSource.iff_of_openCover, Scheme.Hom.ι_toNormalization, Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst_assoc, Scheme.Cover.ColimitGluingData.transitionCocone_pt, Scheme.Pullback.cocycle, Scheme.Pullback.pullbackP1Iso_hom_snd, Scheme.GlueData.openCover_f, instIsAffineXSchemeAffineCover, isLocallyNoetherian_iff_of_affine_openCover, Scheme.Cover.ColimitGluingData.transitionMap_id, Scheme.directedAffineCover_f, Scheme.pullback_map_isOpenImmersion, Scheme.Pullback.t'_fst_fst_snd_assoc, Scheme.Cover.gluedCover_V, IsOpenImmersion.of_forall_source_exists, HasAffineProperty.iff_of_openCover, IsOpenImmersion.instπWalkingCospanSchemeCospanOne, Scheme.Cover.ι_fromGlued_assoc, Scheme.GlueData.f_open, Scheme.OpenCover.isOpenCover_opensRange, Scheme.Cover.RelativeGluingData.ι_toBase, Scheme.openCoverOfIsOpenCover_f, Scheme.Cover.gluedCoverT'_fst_fst, IsOpenImmersion.comp, Scheme.Pullback.pullbackFstιToV_fst_assoc, Scheme.IsLocallyDirected.openCover_f, QuasiCompactCover.exists_hom, Scheme.IdealSheafData.subschemeCover_map_subschemeι, Scheme.Cover.gluedCoverT'_snd_fst, Scheme.isAffine_affineBasisCover, Scheme.Pullback.t_snd, Scheme.directedAffineCover_I₀, Scheme.Cover.RelativeGluingData.ι_toBase_assoc, Scheme.Pullback.gluing_J, Scheme.Cover.RelativeGluingData.equifibered, Scheme.Pullback.gluing_f, Scheme.Pullback.pullbackP1Iso_hom_fst_assoc, IsOpenImmersion.of_stalk_iso, Scheme.AffineOpenCover.instIsOpenImmersionF, ExistsHomHomCompEqCompAux.h𝒰X, isOpenImmersion_stableUnderBaseChange, sourceLocalClosure.instIsZariskiLocalAtSourceIsOpenImmersionOfRespectsIsoOfRespectsLeftScheme, hasOfPostcompProperty_isOpenImmersion_of_morphismRestrict, Scheme.Pullback.pullbackP1Iso_hom_ι_assoc, Scheme.OpenCover.restrict_f, Scheme.Pullback.pullbackFstιToV_fst, Scheme.OpenCover.iSup_opensRange, Scheme.GlueData.ι_isOpenImmersion, FormallyUnramified.isOpenImmersion_diagonal, Scheme.Pullback.pullbackP1Iso_inv_snd_assoc, Scheme.Pullback.t_fst_fst, instIsOpenImmersionCompSchemeιQuasiFiniteLocusToNormalization, Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι, Scheme.LocalRepresentability.glueData_openCover_map, Scheme.Pullback.openCoverOfRight_f, Scheme.Pullback.t'_snd_snd, Scheme.Hom.iInf_ker_openCover_map_comp, Scheme.Cover.LocallyDirected.ofIsBasisOpensRange_trans, isOpenImmersion_SpecMap_iff_of_surjective, instIsOpenImmersionInrScheme, instIsOpenImmersionToNormalizationOfLocallyQuasiFiniteOfLocallyOfFiniteType, Scheme.Cover.gluedCover_J, Scheme.Cover.ColimitGluingData.transitionCocone_ι_app, isIso_iff_isOpenImmersion_and_surjective, Scheme.Opens.instIsOpenImmersionι, isIso_iff_isOpenImmersion, isOpenImmersion_isMultiplicative, Scheme.Cover.glued_cover_cocycle_snd, Scheme.openCoverOfIsOpenCover_X, Scheme.instIsOpenImmersionToSpecΓOfIsQuasiAffine, Scheme.affineOpenCoverOfSpanRangeEqTop_X_carrier, IsImmersion.isImmersion_iff_exists, IsLocalAtSource.respectsLeft_isOpenImmersion, Scheme.Pullback.pullbackP1Iso_inv_fst, isLocalIso_iff, Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom_assoc, Scheme.Pullback.pullbackP1Iso_inv_fst_assoc, QuasiCompactCover.inst, isOpenImmersion_iff_stalk, Scheme.Pullback.t'_snd_fst_fst, Scheme.GlueData.openCover_X, Scheme.directedAffineCover_X, Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι_assoc, Scheme.Pullback.gluing_U, Scheme.Pullback.t'_fst_fst_fst, isOpenImmersion_of_isEmpty, instIsOpenImmersionMapScheme, isOpenImmersion_respectsIso, Scheme.AffineZariskiSite.directedCover_X, IsOpenImmersion.of_isIso, Scheme.OpenCover.instIsOpenImmersionTrans, Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap_assoc, IsOpenImmersion.instHasOfPostcompPropertyScheme, Scheme.IdealSheafData.opensRange_subschemeCover_map, Scheme.Pullback.cocycle_fst_fst_snd, isIso_iff_isOpenImmersion_and_epi_base, instRespectsSchemeLocallyQuasiFiniteIsOpenImmersion, Scheme.Pullback.openCoverOfRight_X, Scheme.Cover.gluedCoverT'_snd_fst_assoc, Scheme.Cover.ι_glueMorphisms, IsZariskiLocalAtSource.respectsLeft_isOpenImmersion, Scheme.AffineZariskiSite.directedCover_f, instIsOpenImmersionMapSchemeCompOverOverTopMorphismPropertyForgetForget, Proj.affineOpenCover_f, Scheme.IsLocallyDirected.openCover_I₀, isOpenImmersion_eq_inf, instIsOpenImmersionMorphismRestrict, Scheme.Cover.ι_glueMorphisms_assoc, instIsOpenImmersionLeftSchemeDiscretePUnitιOverTopMorphismProperty, IsZariskiLocalAtSource.iff_of_openCover, Scheme.Hom.iInf_ker_openCover_map_comp_apply, instIsOpenImmersionInlScheme, Scheme.IsLocallyDirected.openCover_X, Scheme.Cover.RelativeGluingData.cover_f, Scheme.Pullback.openCoverOfBase_X, isOpenImmersion_sigmaDesc, Scheme.Pullback.pullbackP1Iso_hom_snd_assoc, Scheme.Pullback.cocycle_fst_fst_fst, Scheme.Pullback.openCoverOfBase'_f, instIsOpenImmersionMapWalkingSpanSchemeSpan, Scheme.Cover.gluedCover_f, Scheme.Pullback.t_fst_snd, Scheme.Hom.ι_toNormalization_assoc, IsOpenImmersion.of_flat_of_mono, Scheme.Pullback.gluedLiftPullbackMap_fst_assoc, instIsOpenImmersionMapOfHomForallEvalRingHom, IsLocalAtTarget.iff_of_openCover, Scheme.IdealSheafData.isOpenImmersion_glueDataObjMap, Scheme.directedAffineCover_trans, Scheme.Pullback.t'_snd_fst_snd, Scheme.IsLocallyDirected.instIsOpenImmersionι, instIsOpenImmersionSigmaSpec, Scheme.AffineZariskiSite.opensRange_relativeGluingData_map, Scheme.Cover.ColimitGluingData.prop_trans, Scheme.Pullback.cocycle_snd_fst_fst, Scheme.Pullback.pullbackP1Iso_inv_snd, Scheme.Cover.gluedCoverT'_fst_snd_assoc, instIsOpenImmersionAppOverSchemeOpensDiagramι, Scheme.Cover.ColimitGluingData.trans_app_left, Scheme.Pullback.t'_fst_fst_snd, instIsOpenImmersionHomOfLE, Scheme.affineBasisCover_obj, Scheme.Cover.ColimitGluingData.transitionMap_comp, sigmaOpenCover_I₀, isomorphisms_eq_isOpenImmersion_inf_surjective, Scheme.Pullback.cocycle_fst_snd, Scheme.IdealSheafData.subSchemeCover_map_inclusion_assoc, instIsAffineXSchemeCoverOfIsIsoIsOpenImmersionId, Scheme.OpenCover.finiteSubcover_X, IsOpenImmersion.iff_stalk_iso, Scheme.Hom.ι_fromNormalization_assoc, IsLocalIso.exists_isOpenImmersion, Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_map, Scheme.Pullback.pullbackP1Iso_hom_ι, IsOpenImmersion.of_isIso_stalkMap, Scheme.IdealSheafData.subSchemeCover_map_inclusion, Scheme.Pullback.openCoverOfLeftRight_I₀, Scheme.affineOpenCoverOfSpanRangeEqTop_idx, Scheme.Pullback.t'_snd_snd_assoc, Scheme.instHasPullbacksIsOpenImmersion, Scheme.Cover.gluedCoverT'_snd_snd, IsOpenImmersion.of_comp, IsZariskiLocalAtTarget.iff_of_openCover, Scheme.affineOpenCoverOfSpanRangeEqTop_f, instIsLocallyNoetherianXScheme, sigmaOpenCover_f, Scheme.LocalRepresentability.instIsOpenImmersionToGlued, Scheme.instIsLocalAtTargetIsomorphismsZariskiPrecoverage, Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_map_assoc, isLocallyArtinian_iff_openCover, Scheme.AffineOpenCover.openCover_I₀, Scheme.Pullback.t'_fst_snd_assoc, Scheme.OpenCover.restrict_I₀, Scheme.Pullback.openCoverOfLeft_I₀, IsImmersion.instIsOpenImmersionToImageOfQuasiCompact, Scheme.Pullback.pullbackFstιToV_snd_assoc, Scheme.instIsOpenImmersionF, Scheme.affineOpenCover_f, Proj.mapAffineOpenCover_f, Scheme.Pullback.t'_fst_snd, Scheme.Cover.gluedCoverT'_fst_snd, Scheme.Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin, Scheme.IsLocallyDirected.exists_of_pullback_V_V, Scheme.AffineZariskiSite.PreservesLocalization.opensRange_map, Scheme.Pullback.pullbackFstιToV_snd, Scheme.Pullback.t'_fst_fst_fst_assoc, isOpenImmersion_isZariskiLocalAtTarget, instHasOfPostcompPropertySchemeIsOpenImmersionOfIsStableUnderBaseChange, Scheme.Cover.RelativeGluingData.preimage_toBase_eq_range_ι, Scheme.affineBasisCover_map_range, IsAffineOpen.isOpenImmersion_fromSpec, Scheme.Hom.instIsLocallyDirectedI₀DirectedCoverCompFunctorNormalizationGlueDataForget, instRespectsSchemeSmoothIsOpenImmersion, Scheme.Pullback.cocycle_snd_snd, IsOpenImmersion.le_monomorphisms, Scheme.Hom.ι_fromNormalization, IsOpenImmersion.of_isLocalization, Scheme.Pullback.t_snd_assoc, Scheme.GlueData.openCover_I₀, Flat.instRespectsSchemeIsOpenImmersion, Proj.instIsOpenImmersionAwayι, isLocallyNoetherian_iff_openCover, Scheme.affineOpenCover_X, IsOpenImmersion.ofRestrict, IsLocalIso.eq_sourceLocalClosure_isOpenImmersion, Scheme.Cover.instIsOpenImmersionFromGlued, Scheme.Pullback.cocycle_snd_fst_snd, Scheme.Cover.ColimitGluingData.functor_map, IsImmersion.isImmersion_iff_exists_of_quasiCompact, HasRingHomProperty.iff_of_source_openCover, Scheme.Pullback.openCoverOfLeft_f, Scheme.OpenCover.restrict_X, Scheme.affineOneHypercover_toPreOneHypercover_toPreZeroHypercover, Scheme.Pullback.t_fst_fst_assoc, Scheme.Pullback.pullbackP1Iso_hom_fst, Scheme.openCoverBasicOpenTop_f, Scheme.Cover.gluedCoverT'_fst_fst_assoc, Scheme.OpenCover.instIsOpenImmersionMapI₀FunctorOfLocallyDirected, Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_snd, Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst, Scheme.affineOpenCoverOfSpanRangeEqTop_I₀, Scheme.AffineZariskiSite.PreservesLocalization.colimitDesc_preimage, Scheme.Cover.ColimitGluingData.functor_obj, Scheme.Pullback.openCoverOfLeftRight_X, Scheme.Pullback.lift_comp_ι, Scheme.Cover.ColimitGluingData.relativeGluingData_natTrans_app, Scheme.isAffine_affineCover, Scheme.AffineZariskiSite.directedCover_I₀, IsOpenImmersion.instSndScheme, Scheme.AffineOpenCover.openCover_X, IsOpenImmersion.instFstScheme, Scheme.AffineZariskiSite.PreservesLocalization.isOpenImmersion, PresheafedSpace.IsOpenImmersion.toSchemeHom_isOpenImmersion, Scheme.Pullback.openCoverOfLeft_X, Scheme.Cover.RelativeGluingData.instIsOpenImmersionMapI₀Functor, Scheme.Cover.RelativeGluingData.isPullback_natTrans_ι_toBase, Scheme.Pullback.diagonalCover_map, Scheme.Pullback.t'_snd_fst_snd_assoc, Scheme.Cover.ι_fromGlued, Scheme.instIsJointlySurjectivePreservingIsOpenImmersion, Scheme.Pullback.gluedLiftPullbackMap_fst, Scheme.isAffine_affineOpenCover
«term_''ᵁ_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIso_iff_isIso_stalkMap 📖	mathematical	—	CategoryTheory.IsIso Scheme Scheme.instCategory TopCat TopCat.instCategory PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier Scheme.Hom.stalkMap	—	CommRingCat.Colimits.hasColimits_commRingCat isIso_iff_isOpenImmersion_and_epi_base IsOpenImmersion.iff_isIso_stalkMap Topology.IsEmbedding.injective Topology.IsOpenEmbedding.toIsEmbedding TopCat.epi_iff_surjective Topology.IsOpenEmbedding.continuous Topology.IsOpenEmbedding.isOpenMap CategoryTheory.Iso.isIso_hom CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso Homeomorph.isOpenEmbedding
isIso_iff_isOpenImmersion 📖	mathematical	—	CategoryTheory.IsIso Scheme Scheme.instCategory IsOpenImmersion CategoryTheory.Epi TopCat TopCat.instCategory PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom'	—	isIso_iff_isOpenImmersion_and_epi_base
isIso_iff_isOpenImmersion_and_epi_base 📖	mathematical	—	CategoryTheory.IsIso Scheme Scheme.instCategory IsOpenImmersion CategoryTheory.Epi TopCat TopCat.instCategory PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom'	—	IsOpenImmersion.of_isIso CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso Scheme.Hom.isIso_base IsOpenImmersion.isIso
isIso_iff_stalk_iso 📖	mathematical	—	CategoryTheory.IsIso Scheme Scheme.instCategory TopCat TopCat.instCategory PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier Scheme.Hom.stalkMap	—	isIso_iff_isIso_stalkMap
isIso_of_isOpenImmersion_of_opensRange_eq_top 📖	mathematical	Scheme.Hom.opensRange Top.top Scheme.Opens OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	CategoryTheory.IsIso Scheme Scheme.instCategory	—	isIso_iff_isOpenImmersion_and_epi_base TopCat.epi_iff_surjective Set.range_eq_univ TopologicalSpace.Opens.ext_iff
isOpenImmersion_isMultiplicative 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative Scheme Scheme.instCategory IsOpenImmersion	—	IsOpenImmersion.of_isIso CategoryTheory.IsIso.id isOpenImmersion_isStableUnderComposition
isOpenImmersion_isStableUnderComposition 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderComposition Scheme Scheme.instCategory IsOpenImmersion	—	LocallyRingedSpace.IsOpenImmersion.comp
isOpenImmersion_respectsIso 📖	mathematical	—	CategoryTheory.MorphismProperty.RespectsIso Scheme Scheme.instCategory IsOpenImmersion	—	CategoryTheory.MorphismProperty.respectsIso_of_isStableUnderComposition isOpenImmersion_isStableUnderComposition IsOpenImmersion.of_isIso
isOpenImmersion_stableUnderBaseChange 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange Scheme Scheme.instCategory IsOpenImmersion	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange.mk' isOpenImmersion_respectsIso IsOpenImmersion.instFstScheme

AlgebraicGeometry.IsOpenImmersion

Definitions

Name	Category	Theorems
forgetCreatesPullbackOfLeft 📖	CompOp	—
forgetCreatesPullbackOfRight 📖	CompOp	—
isoOfRangeEq 📖	CompOp	4 math math: isoOfRangeEq_inv_fac_assoc, isoOfRangeEq_hom_fac, isoOfRangeEq_hom_fac_assoc, isoOfRangeEq_inv_fac
isoRestrict 📖	CompOp	—
opensEquiv 📖	CompOp	2 math math: opensEquiv_apply_coe, opensEquiv_symm_apply
ΓIso 📖	CompOp	7 math math: map_ΓIso_inv_assoc, ΓIso_inv, app_ΓIso_hom_assoc, map_ΓIso_inv, app_ΓIso_hom, app_ΓIso_hom_apply, map_ΓIso_hom
ΓIsoTop 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
app_eq_appIso_inv_app_of_comp_eq 📖	mathematical	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory	AlgebraicGeometry.Scheme.Hom.app CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.Scheme.Hom.opensFunctor TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.Iso.inv AlgebraicGeometry.Scheme.Hom.appIso CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.eqToHom app_eq_invApp_app_of_comp_eq_aux	—	app_eq_invApp_app_of_comp_eq_aux AlgebraicGeometry.Scheme.Hom.comp_app CategoryTheory.Category.assoc AlgebraicGeometry.Scheme.Hom.preimage_image_eq AlgebraicGeometry.Scheme.Hom.appIso_inv_app_assoc AlgebraicGeometry.Scheme.Hom.naturality_assoc CategoryTheory.Functor.map_comp CategoryTheory.op_comp Quiver.Hom.unop_op CategoryTheory.eqToHom_map CategoryTheory.eqToHom_trans CategoryTheory.eqToHom_op CategoryTheory.eqToHom_refl CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
app_eq_invApp_app_of_comp_eq_aux 📖	mathematical	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory	CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.Scheme.Hom.opensFunctor	—	AlgebraicGeometry.Scheme.Hom.preimage_image_eq
app_ΓIso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.Scheme.Hom.opensRange AlgebraicGeometry.Scheme.Hom.app CategoryTheory.Iso.hom ΓIso CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver SemilatticeInf.toPartialOrder CategoryTheory.homOfLE inf_le_right	—	inf_le_right map_ΓIso_inv CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
app_ΓIso_hom_apply 📖	mathematical	—	DFunLike.coe RingHom CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.Scheme.Hom.opensRange Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CategoryTheory.ConcreteCategory.hom CommRingCat.instConcreteCategoryRingHomCarrier CategoryTheory.Iso.hom ΓIso AlgebraicGeometry.Scheme.Hom.app CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SemilatticeInf.toPartialOrder CategoryTheory.homOfLE inf_le_right	—	inf_le_right CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise app_ΓIso_hom
app_ΓIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' AlgebraicGeometry.Scheme.Hom.app SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.Scheme.Hom.opensRange CategoryTheory.Iso.hom ΓIso CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver SemilatticeInf.toPartialOrder CategoryTheory.homOfLE inf_le_right	—	inf_le_right CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' app_ΓIso_hom
comp 📖	mathematical	—	AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory	—	AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.comp
comp_lift 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace Set.instHasSubset Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory lift HasSubset.Subset.trans Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace Set.instHasSubset Set.instIsTransSubset Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	—	HasSubset.Subset.trans Set.instIsTransSubset CategoryTheory.cancel_mono mono CategoryTheory.Category.assoc lift_fac
comp_lift_assoc 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace Set.instHasSubset Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory lift HasSubset.Subset.trans Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace Set.instHasSubset Set.instIsTransSubset Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	—	HasSubset.Subset.trans Set.instIsTransSubset CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_lift
hasLimit_cospan_forget_of_left 📖	mathematical	—	CategoryTheory.Limits.HasLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory CategoryTheory.Functor.comp AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.cospan AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace	—	CategoryTheory.Limits.hasLimit_iff_of_iso
hasLimit_cospan_forget_of_left' 📖	mathematical	—	CategoryTheory.Limits.HasLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory CategoryTheory.Limits.cospan CategoryTheory.Functor.obj CategoryTheory.Functor.comp AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace CategoryTheory.Limits.WalkingCospan.left CategoryTheory.Limits.WalkingCospan.right CategoryTheory.Limits.WalkingCospan.one CategoryTheory.Functor.map CategoryTheory.Limits.WalkingCospan.Hom.inl CategoryTheory.Limits.WalkingCospan.Hom.inr	—	AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.hasPullback_of_left instIsOpenImmersionMapSchemeLocallyRingedSpaceForgetToLocallyRingedSpace
hasLimit_cospan_forget_of_right 📖	mathematical	—	CategoryTheory.Limits.HasLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory CategoryTheory.Functor.comp AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.cospan AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace	—	CategoryTheory.Limits.hasLimit_iff_of_iso
hasLimit_cospan_forget_of_right' 📖	mathematical	—	CategoryTheory.Limits.HasLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory CategoryTheory.Limits.cospan CategoryTheory.Functor.obj CategoryTheory.Functor.comp AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace CategoryTheory.Limits.WalkingCospan.left CategoryTheory.Limits.WalkingCospan.right CategoryTheory.Limits.WalkingCospan.one CategoryTheory.Functor.map CategoryTheory.Limits.WalkingCospan.Hom.inl CategoryTheory.Limits.WalkingCospan.Hom.inr	—	AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.hasPullback_of_right instIsOpenImmersionMapSchemeLocallyRingedSpaceForgetToLocallyRingedSpace
hasPullback_of_left 📖	mathematical	—	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory	—	CategoryTheory.hasLimit_of_created hasLimit_cospan_forget_of_left
hasPullback_of_right 📖	mathematical	—	CategoryTheory.Limits.HasPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory	—	CategoryTheory.hasLimit_of_created hasLimit_cospan_forget_of_right
iff_isIso_stalkMap 📖	mathematical	—	AlgebraicGeometry.IsOpenImmersion Topology.IsOpenEmbedding TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.IsIso TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.Scheme.Hom.stalkMap	—	CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open of_isIso_stalkMap
iff_stalk_iso 📖	mathematical	—	AlgebraicGeometry.IsOpenImmersion Topology.IsOpenEmbedding TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.IsIso TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.Scheme.Hom.stalkMap	—	iff_isIso_stalkMap
image_preimage_eq_preimage_image_of_isPullback 📖	mathematical	CategoryTheory.IsPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory	CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.Scheme.Hom.opensFunctor TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' TopologicalSpace.Opens TopCat.str	—	TopologicalSpace.Opens.ext Set.ext CategoryTheory.CommSq.w CategoryTheory.IsPullback.toCommSq hasPullback_of_left Eq.ge range_pullbackSnd CategoryTheory.IsPullback.isoPullback_inv_snd
instFstScheme 📖	mathematical	—	AlgebraicGeometry.IsOpenImmersion CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory hasPullback_of_right CategoryTheory.Limits.pullback.fst	—	hasPullback_of_right CategoryTheory.Limits.hasPullback_symmetry CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd comp of_isIso CategoryTheory.Iso.isIso_hom instSndScheme
instHasOfPostcompPropertyScheme 📖	mathematical	—	CategoryTheory.MorphismProperty.HasOfPostcompProperty AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.IsOpenImmersion	—	of_comp
instIsIsoCommRingCatStalkMap 📖	mathematical	—	CategoryTheory.IsIso CommRingCat CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' AlgebraicGeometry.Scheme.Hom.stalkMap	—	—
instIsOpenImmersionMapSchemeLocallyRingedSpaceForgetToLocallyRingedSpace 📖	mathematical	—	AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion CategoryTheory.Functor.obj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace CategoryTheory.Functor.map	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso
instLift 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace Set.instHasSubset Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	AlgebraicGeometry.IsOpenImmersion lift	—	of_comp lift_fac
instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace	—	CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit hasLimit_cospan_forget_of_left
instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace_1 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace	—	CategoryTheory.Limits.preservesPullback_symmetry instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace
instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory TopCat TopCat.instCategory CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan AlgebraicGeometry.Scheme.forgetToTop	—	CategoryTheory.Limits.comp_preservesLimit instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace CategoryTheory.Limits.preservesLimit_of_iso_diagram AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToTop_preservesPullback_of_left
instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop_1 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory TopCat TopCat.instCategory CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan AlgebraicGeometry.Scheme.forgetToTop	—	CategoryTheory.Limits.preservesPullback_symmetry instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop
instPreservesLimitSchemeWalkingCospanCospanForget 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.types CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan AlgebraicGeometry.Scheme.forget	—	CategoryTheory.Limits.comp_preservesLimit instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits TopCat.forget_preservesLimits
instPreservesLimitSchemeWalkingCospanCospanForget_1 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.types CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan AlgebraicGeometry.Scheme.forget	—	CategoryTheory.Limits.comp_preservesLimit instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop_1 CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits TopCat.forget_preservesLimits
instSndScheme 📖	mathematical	—	AlgebraicGeometry.IsOpenImmersion CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory hasPullback_of_left CategoryTheory.Limits.pullback.snd	—	hasPullback_of_left AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.hasPullback_of_left instIsOpenImmersionMapSchemeLocallyRingedSpaceForgetToLocallyRingedSpace instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace CategoryTheory.Limits.PreservesPullback.iso_hom_snd AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.comp AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.of_isIso CategoryTheory.Iso.isIso_hom AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullback_snd_of_left
instπWalkingCospanSchemeCospanOne 📖	mathematical	—	AlgebraicGeometry.IsOpenImmersion CategoryTheory.Limits.limit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.cospan hasPullback_of_right CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingCospan.one CategoryTheory.Limits.limit.π	—	hasPullback_of_right CategoryTheory.Limits.limit.w comp instFstScheme
isIso 📖	mathematical	—	CategoryTheory.IsIso AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory	—	CategoryTheory.isIso_of_reflects_iso AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.to_iso CategoryTheory.reflectsIsomorphisms_comp CategoryTheory.reflectsIsomorphisms_of_full_and_faithful AlgebraicGeometry.Scheme.instFullLocallyRingedSpaceForgetToLocallyRingedSpace AlgebraicGeometry.Scheme.instFaithfulLocallyRingedSpaceForgetToLocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instReflectsIsomorphismsSheafedSpaceCommRingCatForgetToSheafedSpace AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_full AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_faithful
isOpen_range 📖	mathematical	—	IsOpen TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	—	Topology.IsOpenEmbedding.isOpen_range AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open
isPullback 📖	mathematical	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' AlgebraicGeometry.Scheme.Hom.opensRange	CategoryTheory.IsPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory	—	hasPullback_of_left instSndScheme range_pullbackSnd CategoryTheory.cancel_mono mono CategoryTheory.Category.assoc CategoryTheory.Limits.pullback.condition isoOfRangeEq_inv_fac_assoc CategoryTheory.IsPullback.paste_horiz CategoryTheory.IsPullback.of_horiz_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.IsIso.id isoOfRangeEq_inv_fac CategoryTheory.Category.comp_id CategoryTheory.IsPullback.of_hasPullback
isPullback_lift_id 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace Set.instHasSubset Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	CategoryTheory.IsPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory lift CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Category.comp_id lift_fac CategoryTheory.IsPullback.paste_horiz CategoryTheory.IsPullback.of_id_snd CategoryTheory.IsKernelPair.id_of_mono mono
isoOfRangeEq_hom_fac 📖	mathematical	Set.range TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Iso.hom isoOfRangeEq	—	lift_fac le_of_eq
isoOfRangeEq_hom_fac_assoc 📖	mathematical	Set.range TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Iso.hom isoOfRangeEq	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoOfRangeEq_hom_fac
isoOfRangeEq_inv_fac 📖	mathematical	Set.range TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Iso.inv isoOfRangeEq	—	lift_fac le_of_eq
isoOfRangeEq_inv_fac_assoc 📖	mathematical	Set.range TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Iso.inv isoOfRangeEq	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoOfRangeEq_inv_fac
le_monomorphisms 📖	mathematical	—	CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra AlgebraicGeometry.IsOpenImmersion CategoryTheory.MorphismProperty.monomorphisms	—	CategoryTheory.MorphismProperty.monomorphisms.infer_property mono
lift_app 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace Set.instHasSubset Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	AlgebraicGeometry.Scheme.Hom.app lift CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.Scheme.Hom.opensFunctor TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.Iso.inv AlgebraicGeometry.Scheme.Hom.appIso CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.eqToHom app_eq_invApp_app_of_comp_eq_aux Quiver.Hom AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory lift_fac	—	app_eq_appIso_inv_app_of_comp_eq lift_fac
lift_fac 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace Set.instHasSubset Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory lift	—	AlgebraicGeometry.Scheme.Hom.ext' AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift_fac
lift_fac_assoc 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace Set.instHasSubset Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory lift	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_fac
lift_uniq 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace Set.instHasSubset Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory	lift	—	AlgebraicGeometry.Scheme.Hom.ext' AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift_uniq
map_ΓIso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.Scheme.Hom.opensRange AlgebraicGeometry.Scheme.Hom.app CategoryTheory.Iso.hom ΓIso CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver SemilatticeInf.toPartialOrder CategoryTheory.homOfLE inf_le_right	—	app_ΓIso_hom
map_ΓIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.Scheme.Hom.opensRange AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver SemilatticeInf.toPartialOrder CategoryTheory.homOfLE inf_le_right CategoryTheory.Iso.inv ΓIso AlgebraicGeometry.Scheme.Hom.app	—	inf_le_right LE.le.trans ΓIso_inv AlgebraicGeometry.Scheme.Hom.map_appLE AlgebraicGeometry.Scheme.Hom.appLE_eq_app
map_ΓIso_inv_apply 📖	mathematical	—	DFunLike.coe RingHom CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.Scheme.Hom.opensRange AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CategoryTheory.ConcreteCategory.hom CommRingCat.instConcreteCategoryRingHomCarrier AlgebraicGeometry.Scheme.Hom.appLE CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SemilatticeInf.toPartialOrder CategoryTheory.homOfLE inf_le_right AlgebraicGeometry.Scheme.Hom.app	—	inf_le_right ΓIso_inv CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise map_ΓIso_inv
map_ΓIso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.Scheme.Hom.opensRange CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver SemilatticeInf.toPartialOrder CategoryTheory.homOfLE inf_le_right AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.Iso.inv ΓIso AlgebraicGeometry.Scheme.Hom.app	—	inf_le_right CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_ΓIso_inv
mono 📖	mathematical	—	CategoryTheory.Mono AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory	—	CategoryTheory.Functor.mono_of_mono_map CategoryTheory.reflectsMonomorphisms_of_reflectsLimitsOfShape CategoryTheory.Limits.ReflectsFiniteLimits.reflects CategoryTheory.Limits.instReflectsFiniteLimitsOfReflectsLimits CategoryTheory.Limits.fullyFaithful_reflectsLimits AlgebraicGeometry.Scheme.instFullLocallyRingedSpaceForgetToLocallyRingedSpace AlgebraicGeometry.Scheme.instFaithfulLocallyRingedSpaceForgetToLocallyRingedSpace
ofRestrict 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier TopCat.of AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	AlgebraicGeometry.IsOpenImmersion AlgebraicGeometry.Scheme.restrict AlgebraicGeometry.Scheme.ofRestrict	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict
of_comp 📖	mathematical	—	AlgebraicGeometry.IsOpenImmersion	—	of_isIso_stalkMap Topology.IsOpenEmbedding.of_comp AlgebraicGeometry.Scheme.Hom.isOpenEmbedding CategoryTheory.IsIso.of_isIso_comp_left CommRingCat.Colimits.hasColimits_commRingCat instIsIsoCommRingCatStalkMap AlgebraicGeometry.Scheme.Hom.stalkMap_comp
of_isIso 📖	mathematical	—	AlgebraicGeometry.IsOpenImmersion	—	AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.of_isIso AlgebraicGeometry.Scheme.Hom.isIso_toLRSHom
of_isIso_stalkMap 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.IsIso TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.Scheme.Hom.stalkMap	AlgebraicGeometry.IsOpenImmersion	—	CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.SheafedSpace.IsOpenImmersion.of_stalk_iso CommRingCat.hasLimits CommRingCat.forgetReflectIsos CommRingCat.forget_preservesLimits CommRingCat.FilteredColimits.forget_preservesFilteredColimits
of_isLocalization 📖	mathematical	—	AlgebraicGeometry.IsOpenImmersion AlgebraicGeometry.Spec CommRingCat.of AlgebraicGeometry.Spec.map CommRingCat.ofHom algebraMap CommRing.toCommSemiring CommSemiring.toSemiring	—	AlgHomClass.toRingHomClass AlgHom.algHomClass Localization.isLocalization AlgHom.comp_algebraMap CommRingCat.ofHom_comp AlgebraicGeometry.Spec.map_comp AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass comp AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.of_isIso AlgebraicGeometry.Scheme.Hom.isIso_toLRSHom AlgebraicGeometry.instIsIsoSchemeMapOfCommRingCat AlgebraicGeometry.Scheme.instIsOpenImmersionMapOfHomAwayAlgebraMap
of_stalk_iso 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.IsIso TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.Scheme.Hom.stalkMap	AlgebraicGeometry.IsOpenImmersion	—	of_isIso_stalkMap
opensEquiv_apply_coe 📖	mathematical	—	AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.Scheme.Hom.opensRange DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike opensEquiv CategoryTheory.Functor.obj Preorder.smallCategory AlgebraicGeometry.Scheme.Hom.opensFunctor	—	—
opensEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.Scheme.Hom.opensRange EquivLike.toFunLike Equiv.instEquivLike Equiv.symm opensEquiv CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	—	—
opensRange_pullback_fst_of_right 📖	mathematical	—	AlgebraicGeometry.Scheme.Hom.opensRange CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory hasPullback_of_right CategoryTheory.Limits.pullback.fst instFstScheme CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	—	AlgebraicGeometry.Scheme.Hom.opensRange_pullbackFst
opensRange_pullback_snd_of_left 📖	mathematical	—	AlgebraicGeometry.Scheme.Hom.opensRange CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory hasPullback_of_left CategoryTheory.Limits.pullback.snd instSndScheme CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	—	AlgebraicGeometry.Scheme.Hom.opensRange_pullbackSnd
range_pullbackFst 📖	mathematical	—	Set.range TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory hasPullback_of_right DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.Limits.pullback.fst SetLike.coe AlgebraicGeometry.Scheme.Opens TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map AlgebraicGeometry.Scheme.Hom.opensRange	—	hasPullback_of_right CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits TopCat.topCat_hasLimits instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop_1 CategoryTheory.Limits.PreservesPullback.iso_hom_fst TopCat.coe_comp Set.range_comp Set.range_eq_univ TopCat.epi_iff_surjective CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom Set.preimage_univ TopCat.pullback_fst_image_snd_preimage Set.image_univ
range_pullbackSnd 📖	mathematical	—	Set.range TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory hasPullback_of_left DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.Limits.pullback.snd SetLike.coe AlgebraicGeometry.Scheme.Opens TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map AlgebraicGeometry.Scheme.Hom.opensRange	—	hasPullback_of_left CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits TopCat.topCat_hasLimits instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop CategoryTheory.Limits.PreservesPullback.iso_hom_snd TopCat.coe_comp Set.range_comp Set.range_eq_univ TopCat.epi_iff_surjective CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom Set.preimage_univ TopCat.pullback_snd_image_fst_preimage Set.image_univ
range_pullback_fst_of_right 📖	mathematical	—	Set.range TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory hasPullback_of_right DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.Limits.pullback.fst SetLike.coe AlgebraicGeometry.Scheme.Opens TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map AlgebraicGeometry.Scheme.Hom.opensRange	—	range_pullbackFst
range_pullback_snd_of_left 📖	mathematical	—	Set.range TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory hasPullback_of_left DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.Limits.pullback.snd SetLike.coe AlgebraicGeometry.Scheme.Opens TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map AlgebraicGeometry.Scheme.Hom.opensRange	—	range_pullbackSnd
range_pullback_to_base_of_left 📖	mathematical	—	Set.range TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory hasPullback_of_left DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback.fst Set Set.instInter	—	hasPullback_of_left CategoryTheory.Limits.pullback.condition AlgebraicGeometry.Scheme.Hom.comp_base TopCat.coe_comp Set.range_comp range_pullbackSnd IsOpen.preimage ContinuousMap.continuous TopologicalSpace.Opens.is_open' TopologicalSpace.Opens.map_obj Set.image_preimage_eq_inter_range TopologicalSpace.Opens.carrier_eq_coe AlgebraicGeometry.Scheme.Hom.coe_opensRange
range_pullback_to_base_of_right 📖	mathematical	—	Set.range TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory hasPullback_of_right DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback.fst Set Set.instInter	—	hasPullback_of_right AlgebraicGeometry.Scheme.Hom.comp_base TopCat.coe_comp Set.range_comp range_pullbackFst IsOpen.preimage ContinuousMap.continuous TopologicalSpace.Opens.is_open' TopologicalSpace.Opens.map_obj Set.image_preimage_eq_inter_range Set.inter_comm TopologicalSpace.Opens.carrier_eq_coe AlgebraicGeometry.Scheme.Hom.coe_opensRange
to_iso 📖	mathematical	—	CategoryTheory.IsIso AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory	—	isIso
ΓIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CommRingCat CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.Scheme.Hom.opensRange ΓIso AlgebraicGeometry.Scheme.Hom.appLE	—	LE.le.trans Eq.ge AlgebraicGeometry.Scheme.Hom.preimage_image_eq CategoryTheory.eqToHom_op AlgebraicGeometry.Scheme.Hom.appIso_hom' AlgebraicGeometry.Scheme.Hom.map_appLE

AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion

Definitions

Name	Category	Theorems
scheme 📖	CompOp	—

AlgebraicGeometry.PresheafedSpace.IsOpenImmersion

Definitions

Name	Category	Theorems
toScheme 📖	CompOp	4 math math: toScheme_toLocallyRingedSpace, scheme_toScheme, toSchemeHom_toPshHom, toSchemeHom_isOpenImmersion
toSchemeHom 📖	CompOp	2 math math: toSchemeHom_toPshHom, toSchemeHom_isOpenImmersion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
scheme_eq_of_locallyRingedSpace_eq 📖	—	AlgebraicGeometry.Scheme.toLocallyRingedSpace	—	—	TopologicalSpace.OpenNhds.isOpenEmbedding
scheme_toScheme 📖	mathematical	—	toScheme AlgebraicGeometry.SheafedSpace.toPresheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.Hom.toPshHom AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' AlgebraicGeometry.instIsOpenImmersionCommRingCatOfIsOpenImmersion	—	scheme_eq_of_locallyRingedSpace_eq AlgebraicGeometry.instIsOpenImmersionCommRingCatOfIsOpenImmersion locallyRingedSpace_toLocallyRingedSpace
toSchemeHom_isOpenImmersion 📖	mathematical	—	AlgebraicGeometry.IsOpenImmersion toScheme toSchemeHom	—	—
toSchemeHom_toPshHom 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.Hom.toPshHom CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace toScheme AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' toSchemeHom	—	—
toScheme_toLocallyRingedSpace 📖	mathematical	—	AlgebraicGeometry.Scheme.toLocallyRingedSpace toScheme toLocallyRingedSpace	—	—

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
ofRestrict 📖	CompOp	7 math math: ofRestrict_appIso, ofRestrict_toLRSHom_base, ofRestrict_appLE, ofRestrict_toLRSHom_c_app, restrict_presheaf_map, AlgebraicGeometry.IsOpenImmersion.ofRestrict, ofRestrict_app
restrict 📖	CompOp	10 math math: ofRestrict_appIso, restrict_toPresheafedSpace, ofRestrict_toLRSHom_base, ofRestrict_appLE, restrict_presheaf_obj, ofRestrict_toLRSHom_c_app, restrict_presheaf_map, restrict_carrier, AlgebraicGeometry.IsOpenImmersion.ofRestrict, ofRestrict_app
stalkMapIsoOfIsPullback 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basic_open_isOpenImmersion 📖	mathematical	—	AlgebraicGeometry.IsOpenImmersion AlgebraicGeometry.Spec CommRingCat.of Localization.Away CommRingCat.carrier CommRing.toCommMonoid CommRingCat.commRing OreLocalization.instCommRing Submonoid.powers CommMonoid.toMonoid OreLocalization.oreSetComm AlgebraicGeometry.Spec.map CommRingCat.ofHom algebraMap CommRing.toCommSemiring OreLocalization.instSemiring Ring.toSemiring CommRing.toRing OreLocalization.instAlgebra Algebra.id	—	isOpenImmersion_SpecMap_localizationAway
exists_affine_mem_range_and_range_subset 📖	mathematical	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	CommRingCat Quiver.Hom AlgebraicGeometry.Scheme CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.Spec AlgebraicGeometry.IsOpenImmersion TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace Set Set.instMembership Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' Set.instHasSubset SetLike.coe Opens TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	—	TopologicalSpace.OpenNhds.isOpenEmbedding local_affine CategoryTheory.Iso.hom_inv_id TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open PrimeSpectrum.isBasis_basic_opens TopologicalSpace.Opens.is_open' AlgebraicGeometry.IsOpenImmersion.comp isOpenImmersion_SpecMap_localizationAway AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.comp AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.of_isIso CategoryTheory.Iso.isIso_inv AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.ofRestrict Hom.comp_base TopCat.coe_comp Set.range_comp PrimeSpectrum.localization_away_comap_range Localization.isLocalization Set.image_subset_iff
image_basicOpen 📖	mathematical	—	CategoryTheory.Functor.obj Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier Hom.opensFunctor basicOpen DFunLike.coe Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op CommRingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier CategoryTheory.Iso.inv Hom.appIso	—	preimage_basicOpen inf_eq_right LE.le.trans basicOpen_le Eq.ge Hom.preimage_image_eq basicOpen_res Hom.appIso_inv_app_apply Hom.image_preimage_eq_opensRange_inf Set.Subset.trans Set.image_subset_range
image_zeroLocus 📖	mathematical	—	Set.image TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' zeroLocus Set Set.instInter CategoryTheory.Functor.obj Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier Hom.opensFunctor CommRingCat.carrier Opposite TopologicalSpace.Opens CategoryTheory.Category.opposite AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.Hom.hom CategoryTheory.Iso.inv Hom.appIso Set.range	—	Set.ext Set.image_congr Function.Injective.mem_set_image Topology.IsEmbedding.injective Topology.IsOpenEmbedding.toIsEmbedding Hom.isOpenEmbedding Set.image_subset_range
instIsOpenImmersionMapOfHomAwayAlgebraMap 📖	mathematical	—	AlgebraicGeometry.IsOpenImmersion AlgebraicGeometry.Spec CommRingCat.of Localization.Away CommRing.toCommMonoid OreLocalization.instCommRing Submonoid.powers CommMonoid.toMonoid OreLocalization.oreSetComm AlgebraicGeometry.Spec.map CommRingCat.ofHom algebraMap CommRing.toCommSemiring OreLocalization.instSemiring Ring.toSemiring CommRing.toRing OreLocalization.instAlgebra Algebra.id	—	isOpenImmersion_SpecMap_localizationAway
isOpenImmersion_SpecMap_localizationAway 📖	mathematical	—	AlgebraicGeometry.IsOpenImmersion AlgebraicGeometry.Spec CommRingCat.of Localization.Away CommRingCat.carrier CommRing.toCommMonoid CommRingCat.commRing OreLocalization.instCommRing Submonoid.powers CommMonoid.toMonoid OreLocalization.oreSetComm AlgebraicGeometry.Spec.map CommRingCat.ofHom algebraMap CommRing.toCommSemiring OreLocalization.instSemiring Ring.toSemiring CommRing.toRing OreLocalization.instAlgebra Algebra.id	—	AlgebraicGeometry.SheafedSpace.IsOpenImmersion.of_stalk_iso CommRingCat.hasLimits CommRingCat.Colimits.hasColimits_commRingCat CommRingCat.forgetReflectIsos CommRingCat.forget_preservesLimits CommRingCat.FilteredColimits.forget_preservesFilteredColimits AlgebraicGeometry.isIso_SpecMap_stakMap_localization PrimeSpectrum.localization_away_isOpenEmbedding Localization.isLocalization
ofRestrict_app 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier TopCat.of AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	Hom.app restrict ofRestrict CategoryTheory.Functor.map Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op TopCat.of AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp TopologicalSpace.Opens.map IsOpenMap.functor Topology.IsOpenEmbedding.isOpenMap DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Adjunction.counit IsOpenMap.adjunction	—	—
ofRestrict_appIso 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier TopCat.of AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	Hom.appIso restrict ofRestrict AlgebraicGeometry.IsOpenImmersion.ofRestrict CategoryTheory.Iso.refl CommRingCat CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier Hom.opensFunctor	—	CategoryTheory.Iso.ext AlgebraicGeometry.IsOpenImmersion.ofRestrict Eq.ge Hom.preimage_image_eq Hom.appIso_hom' ofRestrict_appLE CategoryTheory.Functor.map_id
ofRestrict_appLE 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier TopCat.of AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier Opens restrict Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' ofRestrict	Hom.appLE restrict ofRestrict CategoryTheory.Functor.map Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op Opens CategoryTheory.Functor.obj AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier Hom.opensFunctor AlgebraicGeometry.IsOpenImmersion.ofRestrict Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.homOfLE	—	AlgebraicGeometry.IsOpenImmersion.ofRestrict Topology.IsOpenEmbedding.isOpenMap CategoryTheory.Functor.map_comp
ofRestrict_toLRSHom_base 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier TopCat.of AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	AlgebraicGeometry.PresheafedSpace.Hom.base CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.LocallyRingedSpace.restrict toLocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom restrict ofRestrict	—	—
ofRestrict_toLRSHom_c_app 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier TopCat.of AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Functor.obj TopCat.Presheaf AlgebraicGeometry.PresheafedSpace.restrict TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.c AlgebraicGeometry.LocallyRingedSpace.restrict AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom restrict ofRestrict CategoryTheory.Functor.map Opposite.op Topology.IsOpenEmbedding.functor TopologicalSpace.Opens.map Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct IsOpenMap.functor CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit IsOpenMap.adjunction	—	—
restrict_carrier 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier TopCat.of AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace restrict	—	—
restrict_presheaf_map 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier TopCat.of AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.Functor.map Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace restrict TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op Opens CategoryTheory.Functor.obj AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier Hom.opensFunctor ofRestrict AlgebraicGeometry.IsOpenImmersion.ofRestrict Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.homOfLE	—	—
restrict_presheaf_obj 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier TopCat.of AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CommRingCat CommRingCat.instCategory AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace restrict AlgebraicGeometry.PresheafedSpace.carrier Opposite.op Topology.IsOpenEmbedding.functor Opposite.unop	—	—
restrict_toPresheafedSpace 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier TopCat.of AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	AlgebraicGeometry.SheafedSpace.toPresheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace restrict AlgebraicGeometry.PresheafedSpace.restrict	—	—

AlgebraicGeometry.Scheme.Hom

Definitions

Name	Category	Theorems
appIso 📖	CompOp	27 math math: AlgebraicGeometry.Scheme.ofRestrict_appIso, app_invApp'_assoc, AlgebraicGeometry.Scheme.ker_ideal_of_isPullback_of_isOpenImmersion, app_appIso_inv_assoc, appIso_inv_app_presheafMap, AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_of_isOpenImmersion, appIso_inv_app, AlgebraicGeometry.Scheme.Opens.ι_appIso, appIso_inv_naturality, appIso_hom', appLE_appIso_inv, app_invApp', AlgebraicGeometry.Scheme.image_basicOpen, appIso_inv_naturality_assoc, comp_appIso, appIso_inv_appLE_assoc, appIso_inv_app_assoc, id_appIso, appLE_appIso_inv_assoc, AlgebraicGeometry.IsOpenImmersion.app_eq_appIso_inv_app_of_comp_eq, appIso_hom, appLE_appIso_inv_apply, appIso_inv_app_apply, AlgebraicGeometry.Scheme.image_zeroLocus, app_appIso_inv, AlgebraicGeometry.IsOpenImmersion.lift_app, appIso_inv_appLE
opensFunctor 📖	CompOp	114 math math: AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen, AlgebraicGeometry.Γ_map_morphismRestrict, image_preimage_eq_opensRange_inter, AlgebraicGeometry.Scheme.ofRestrict_appIso, app_invApp'_assoc, instIsContinuousOpensOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_counit_app_app, AlgebraicGeometry.Scheme.Opens.mem_ι_image_iff, AlgebraicGeometry.Scheme.Opens.topIso_inv, opensFunctor_map_homOfLE, AlgebraicGeometry.image_morphismRestrict_preimage, AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_inv_app, image_le_image_of_le, image_preimage_le, image_top_eq_opensRange, AlgebraicGeometry.Scheme.ker_ideal_of_isPullback_of_isOpenImmersion, image_preimage_eq_opensRange_inf, image_iSup₂, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv, AlgebraicGeometry.Scheme.ofRestrict_appLE, AlgebraicGeometry.IsAffineOpen.isoSpec_inv, app_appIso_inv_assoc, AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_hom_app, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen_topIso_inv, AlgebraicGeometry.Scheme.ι_image_homOfLE_le_ι_image, preimage_image_eq, AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_obj, AlgebraicGeometry.liftCoborder_app, AlgebraicGeometry.morphismRestrict_appLE, appIso_inv_app_presheafMap, AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_hom_app_app, apply_mem_image_iff, AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_inv_app_app, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv_assoc, AlgebraicGeometry.Scheme.Modules.restrict_map, image_mono, AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_of_isOpenImmersion, appIso_inv_app, liftCoborder_preimage, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom, AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_inv_app_app, AlgebraicGeometry.affineOpensRestrict_apply_coe_coe, AlgebraicGeometry.Scheme.Opens.ι_appIso, appIso_inv_naturality, appIso_hom', AlgebraicGeometry.Scheme.homOfLE_appTop, AlgebraicGeometry.IsOpenImmersion.opensEquiv_apply_coe, appLE_appIso_inv, isAffineOpen_iff_of_isOpenImmersion, app_invApp', AlgebraicGeometry.Scheme.image_basicOpen, AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion, AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_hom_app_app, AlgebraicGeometry.Scheme.Modules.restrictFunctorId_inv_app_app, AlgebraicGeometry.morphismRestrict_app', appIso_inv_naturality_assoc, comp_appIso, appIso_inv_appLE_assoc, appIso_inv_app_assoc, AlgebraicGeometry.Scheme.Opens.ι_appTop, map_mem_image_iff, AlgebraicGeometry.Scheme.map_basicOpen, AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv_apply_coe_coe, id_appIso, appLE_appIso_inv_assoc, image_iSup, AlgebraicGeometry.Scheme.homOfLE_app, AlgebraicGeometry.Scheme.homOfLE_appLE, AlgebraicGeometry.morphismRestrict_appTop, AlgebraicGeometry.IsOpenImmersion.app_eq_appIso_inv_app_of_comp_eq, isoImage_inv_ι, isoImage_inv_ι_assoc, instIsIsoCommRingCatAppObjOpensOpensFunctor, AlgebraicGeometry.Scheme.ker_morphismRestrict_ideal, AlgebraicGeometry.Scheme.Modules.restrict_obj, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_unit_app_app, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom_assoc, coe_image, AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_map, resLE_preimage, le_preimage_resLE_iff, appIso_hom, image_le_opensRange, appLE_appIso_inv_apply, AlgebraicGeometry.Scheme.Opens.ι_app_self, image_injective, AlgebraicGeometry.Scheme.restrict_presheaf_map, AlgebraicGeometry.IsOpenImmersion.image_preimage_eq_preimage_image_of_isPullback, AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen', AlgebraicGeometry.Scheme.map_basicOpen_map, AlgebraicGeometry.IsAffineOpen.fromSpec_image_basicOpen, AlgebraicGeometry.Scheme.Opens.ι_image_le, AlgebraicGeometry.Scheme.Opens.ι_appLE, comp_image, resLE_appLE, AlgebraicGeometry.Scheme.Opens.ι_app, isoImage_hom_ι, inv_image, opensRange_comp, appIso_inv_app_apply, AlgebraicGeometry.morphismRestrict_app, AlgebraicGeometry.Scheme.Opens.ι_image_top, AlgebraicGeometry.Scheme.Modules.restrictFunctorId_hom_app_app, AlgebraicGeometry.Scheme.image_zeroLocus, isoImage_hom_ι_assoc, AlgebraicGeometry.Scheme.Opens.topIso_hom, image_le_image_iff, app_appIso_inv, AlgebraicGeometry.IsOpenImmersion.app_eq_invApp_app_of_comp_eq_aux, AlgebraicGeometry.Scheme.Opens.eq_presheaf_map_eqToHom, le_resLE_preimage_iff, AlgebraicGeometry.IsOpenImmersion.lift_app, appIso_inv_appLE, id_image
opensRange 📖	CompOp	61 math math: opensRange_pullbackSnd, image_preimage_eq_opensRange_inter, AlgebraicGeometry.Scheme.Cover.LocallyDirected.ofIsBasisOpensRange_le_iff, mem_opensRange, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι, AlgebraicGeometry.IsAffineOpen.opensRange_fromSpec, image_top_eq_opensRange, fromNormalization_preimage, image_preimage_eq_opensRange_inf, AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd, AlgebraicGeometry.isAffineOpen_opensRange, AlgebraicGeometry.IsOpenImmersion.range_pullback_fst_of_right, AlgebraicGeometry.Scheme.Opens.opensRange_ι, AlgebraicGeometry.Scheme.opensRange_homOfLE, AlgebraicGeometry.coe_opensRestrict_symm_apply, AlgebraicGeometry.Scheme.OpenCover.isOpenCover_opensRange, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_assoc, isoOpensRange_hom_ι_assoc, isoOpensRange_hom_ι, AlgebraicGeometry.Scheme.IsLocallyDirected.homOfLE_tAux, AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange, AlgebraicGeometry.Scheme.Cover.LocallyDirected.ofIsBasisOpensRange_trans, opensRange_pullbackFst, AlgebraicGeometry.disjoint_opensRange_sigmaι, AlgebraicGeometry.Scheme.IsLocallyDirected.fst_inv_eq_snd_inv, AlgebraicGeometry.IsOpenImmersion.opensEquiv_apply_coe, appLE_appIso_inv, AlgebraicGeometry.IsOpenImmersion.opensEquiv_symm_apply, AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv_apply_coe_coe, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_subschemeCover_map, AlgebraicGeometry.Scheme.preimage_opensRange_toSpecΓ, appLE_appIso_inv_assoc, AlgebraicGeometry.Proj.opensRange_awayι, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_glueDataObjMap, preimage_opensRange, AlgebraicGeometry.IsOpenImmersion.ΓIso_inv, AlgebraicGeometry.IsOpenImmersion.range_pullback_snd_of_left, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_assoc, AlgebraicGeometry.isCompl_opensRange_inl_inr, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv, AlgebraicGeometry.Scheme.AffineZariskiSite.opensRange_relativeGluingData_map, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_apply, image_le_opensRange, appLE_appIso_inv_apply, isoOpensRange_inv_comp_assoc, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_snd_of_left, AlgebraicGeometry.Scheme.IsLocallyDirected.exists_of_pullback_V_V, AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.opensRange_map, AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_fst_of_right, AlgebraicGeometry.IsOpenImmersion.range_pullbackFst, opensRange_comp_of_isIso, opensRange_comp, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_hom, opensRange_of_isIso, AlgebraicGeometry.Scheme.IsLocallyDirected.homOfLE_tAux_assoc, AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.colimitDesc_preimage, isoOpensRange_inv_comp, coe_opensRange, AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv_symm_apply_coe, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
appIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CommRingCat CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor appIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' app CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.eqToHom preimage_image_eq	—	AlgebraicGeometry.instIsOpenImmersionCommRingCatOfIsOpenImmersion AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.instIsIsoInvApp preimage_image_eq AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_invApp CategoryTheory.eqToHom_op
appIso_hom' 📖	mathematical	—	CategoryTheory.Iso.hom CommRingCat CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor appIso appLE Eq.ge TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' preimage_image_eq	—	appIso_hom
appIso_inv_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' CategoryTheory.Iso.inv appIso app CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.eqToHom preimage_image_eq	—	AlgebraicGeometry.instIsOpenImmersionCommRingCatOfIsOpenImmersion preimage_image_eq AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app CategoryTheory.eqToHom_op
appIso_inv_appLE 📖	mathematical	AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' opensFunctor	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor CategoryTheory.Iso.inv appIso appLE CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.homOfLE	—	preimage_image_eq appIso_inv_app_assoc CategoryTheory.eqToHom_op CategoryTheory.Functor.map_comp
appIso_inv_appLE_assoc 📖	mathematical	AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' opensFunctor	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor CategoryTheory.Iso.inv appIso appLE CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.homOfLE	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' appIso_inv_appLE
appIso_inv_app_apply 📖	mathematical	—	DFunLike.coe RingHom CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CategoryTheory.ConcreteCategory.hom CommRingCat.instConcreteCategoryRingHomCarrier app CategoryTheory.Iso.inv appIso CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom preimage_image_eq	—	preimage_image_eq CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise appIso_inv_app
appIso_inv_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor CategoryTheory.Iso.inv appIso TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' app CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.eqToHom preimage_image_eq	—	preimage_image_eq CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' appIso_inv_app
appIso_inv_app_presheafMap 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor CategoryTheory.Iso.inv appIso TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' app CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.eqToHom preimage_image_eq CategoryTheory.CategoryStruct.id	—	preimage_image_eq appIso_inv_app_assoc CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_id
appIso_inv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor CategoryTheory.Functor.map CategoryTheory.Iso.inv appIso CategoryTheory.Functor.op	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_naturality AlgebraicGeometry.instIsOpenImmersionCommRingCatOfIsOpenImmersion
appIso_inv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens CategoryTheory.Functor.map AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor CategoryTheory.Iso.inv appIso CategoryTheory.Functor.op	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' appIso_inv_naturality
appLE_appIso_inv 📖	mathematical	AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom'	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor appLE CategoryTheory.Iso.inv appIso CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.homOfLE LE.le.trans TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' image_mono SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice opensRange Preorder.toLE inf_le_right image_preimage_eq_opensRange_inf	—	LE.le.trans image_mono inf_le_right image_preimage_eq_opensRange_inf Set.image_preimage_subset CategoryTheory.Category.assoc appIso_inv_naturality app_appIso_inv_assoc CategoryTheory.Functor.map_comp
appLE_appIso_inv_apply 📖	mathematical	AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom'	DFunLike.coe RingHom CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CategoryTheory.ConcreteCategory.hom CommRingCat.instConcreteCategoryRingHomCarrier CategoryTheory.Iso.inv appIso appLE CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.homOfLE LE.le.trans TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' image_mono SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice opensRange Preorder.toLE inf_le_right image_preimage_eq_opensRange_inf	—	LE.le.trans image_mono inf_le_right image_preimage_eq_opensRange_inf CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise appLE_appIso_inv
appLE_appIso_inv_assoc 📖	mathematical	AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom'	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens appLE AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor CategoryTheory.Iso.inv appIso CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.homOfLE LE.le.trans TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' image_mono SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice opensRange Preorder.toLE inf_le_right image_preimage_eq_opensRange_inf	—	LE.le.trans image_mono inf_le_right image_preimage_eq_opensRange_inf CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' appLE_appIso_inv
app_appIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' opensFunctor app CategoryTheory.Iso.inv appIso CategoryTheory.Functor.map Quiver.Hom.op Set CategoryTheory.CategoryStruct.toQuiver OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.image DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier Set.preimage TopologicalSpace.Opens.carrier CategoryTheory.homOfLE Set.image_preimage_subset	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp AlgebraicGeometry.instIsOpenImmersionCommRingCatOfIsOpenImmersion
app_appIso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' app opensFunctor CategoryTheory.Iso.inv appIso CategoryTheory.Functor.map Quiver.Hom.op Set CategoryTheory.CategoryStruct.toQuiver OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.image DFunLike.coe ContinuousMap CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier Set.preimage TopologicalSpace.Opens.carrier CategoryTheory.homOfLE Set.image_preimage_subset	—	Set.image_preimage_subset CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' app_appIso_inv
app_invApp' 📖	mathematical	AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensRange	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' opensFunctor app CategoryTheory.Iso.inv appIso CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.eqToHom TopologicalSpace.Opens.ext	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp AlgebraicGeometry.instIsOpenImmersionCommRingCatOfIsOpenImmersion
app_invApp'_assoc 📖	mathematical	AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensRange	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' app opensFunctor CategoryTheory.Iso.inv appIso CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.eqToHom TopologicalSpace.Opens.ext	—	TopologicalSpace.Opens.ext CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' app_invApp'
apply_mem_image_iff 📖	mathematical	—	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Scheme.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder opensFunctor DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom'	—	Function.Injective.mem_set_image Topology.IsEmbedding.injective Topology.IsOpenEmbedding.toIsEmbedding isOpenEmbedding
coe_image 📖	mathematical	—	SetLike.coe AlgebraicGeometry.Scheme.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder opensFunctor Set.image DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom'	—	—
coe_opensRange 📖	mathematical	—	SetLike.coe TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.instSetLike opensRange Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom'	—	—
comp_appIso 📖	mathematical	—	appIso CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.IsOpenImmersion.comp CategoryTheory.Iso.trans CommRingCat CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor CategoryTheory.Functor.mapIso CategoryTheory.Iso.op CategoryTheory.eqToIso	—	CategoryTheory.Iso.ext AlgebraicGeometry.IsOpenImmersion.comp LE.le.trans preimage_image_eq le_rfl appIso_hom app_eq_appLE CategoryTheory.eqToHom_op appLE_map appLE_comp_appLE map_appLE
comp_image 📖	mathematical	—	CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.IsOpenImmersion.comp	—	TopologicalSpace.Opens.ext AlgebraicGeometry.IsOpenImmersion.comp Set.image_comp
id_appIso 📖	mathematical	—	appIso CategoryTheory.CategoryStruct.id AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.of_isIso AlgebraicGeometry.Scheme.toLocallyRingedSpace toLRSHom isIso_toLRSHom CategoryTheory.IsIso.id CategoryTheory.Functor.mapIso Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor CategoryTheory.Iso.op CategoryTheory.eqToIso	—	CategoryTheory.Iso.ext AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.of_isIso isIso_toLRSHom CategoryTheory.IsIso.id CommRingCat.hom_ext RingHom.ext preimage_image_eq appIso_hom CategoryTheory.eqToHom_op CategoryTheory.Category.id_comp
id_image 📖	mathematical	—	CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor CategoryTheory.CategoryStruct.id AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.of_isIso toLRSHom isIso_toLRSHom CategoryTheory.IsIso.id	—	TopologicalSpace.Opens.ext AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.of_isIso isIso_toLRSHom CategoryTheory.IsIso.id Set.image_id
image_iSup 📖	mathematical	—	CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice	—	TopologicalSpace.Opens.ext Set.image_congr TopologicalSpace.Opens.coe_iSup Set.image_iUnion isOpen_iUnion TopologicalSpace.Opens.is_open'
image_iSup₂ 📖	mathematical	—	CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice	—	TopologicalSpace.Opens.ext isOpen_iUnion TopologicalSpace.Opens.is_open' TopologicalSpace.Opens.coe_iSup Set.image_congr Set.image_iUnion₂
image_injective 📖	mathematical	—	AlgebraicGeometry.Scheme.Opens CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor	—	preimage_image_eq
image_le_image_iff 📖	mathematical	—	AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory opensFunctor	—	preimage_image_eq preimage_mono image_mono
image_le_image_of_le 📖	mathematical	AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory opensFunctor	—	image_mono
image_le_opensRange 📖	mathematical	—	AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory opensFunctor opensRange	—	image_top_eq_opensRange image_mono le_top
image_mono 📖	mathematical	AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory opensFunctor	—	Set.image_mono
image_preimage_eq_opensRange_inf 📖	mathematical	—	CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice opensRange	—	TopologicalSpace.Opens.ext Set.image_congr Set.image_preimage_eq_range_inter
image_preimage_eq_opensRange_inter 📖	mathematical	—	CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice opensRange	—	image_preimage_eq_opensRange_inf
image_preimage_le 📖	mathematical	—	AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory opensFunctor TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom'	—	Eq.trans_le image_preimage_eq_opensRange_inf inf_le_right
image_top_eq_opensRange 📖	mathematical	—	CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder opensRange	—	TopologicalSpace.Opens.ext Set.image_congr Set.image_univ
instIsContinuousOpensOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat 📖	mathematical	—	CategoryTheory.Functor.IsContinuous AlgebraicGeometry.Scheme.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor Opens.grothendieckTopology	—	Topology.IsOpenEmbedding.functor_isContinuous isOpenEmbedding
instIsIsoCommRingCatAppObjOpensOpensFunctor 📖	mathematical	—	CategoryTheory.IsIso CommRingCat CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' app	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso AlgebraicGeometry.instIsOpenImmersionCommRingCatOfIsOpenImmersion
inv_image 📖	mathematical	—	CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor CategoryTheory.Iso.inv AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.of_isIso toLRSHom isIso_toLRSHom CategoryTheory.Iso.isIso_inv TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' CategoryTheory.Iso.hom	—	TopologicalSpace.Opens.ext AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.of_isIso isIso_toLRSHom CategoryTheory.Iso.isIso_inv Equiv.image_eq_preimage_symm
isIso_app 📖	mathematical	AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensRange	CategoryTheory.IsIso CommRingCat CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' app	—	TopologicalSpace.Opens.ext Set.image_preimage_eq_of_subset instIsIsoCommRingCatAppObjOpensOpensFunctor
isOpenEmbedding 📖	mathematical	—	Topology.IsOpenEmbedding TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom'	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open
map_mem_image_iff 📖	mathematical	—	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Scheme.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder opensFunctor DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom'	—	apply_mem_image_iff
mem_opensRange 📖	mathematical	—	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Scheme.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensRange DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom'	—	—
opensFunctor_map_homOfLE 📖	mathematical	AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	CategoryTheory.Functor.map AlgebraicGeometry.Scheme.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor CategoryTheory.homOfLE CategoryTheory.Functor.obj image_mono	—	—
opensRange_comp 📖	mathematical	—	opensRange CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.IsOpenImmersion.comp CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor	—	TopologicalSpace.Opens.ext AlgebraicGeometry.IsOpenImmersion.comp Set.range_comp
opensRange_comp_of_isIso 📖	mathematical	—	opensRange CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.IsOpenImmersion.comp AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.of_isIso AlgebraicGeometry.Scheme.toLocallyRingedSpace toLRSHom isIso_toLRSHom	—	AlgebraicGeometry.IsOpenImmersion.comp AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.of_isIso isIso_toLRSHom opensRange_comp opensRange_of_isIso image_top_eq_opensRange
opensRange_of_isIso 📖	mathematical	—	opensRange AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.of_isIso AlgebraicGeometry.Scheme.toLocallyRingedSpace toLRSHom isIso_toLRSHom Top.top AlgebraicGeometry.Scheme.Opens OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	TopologicalSpace.Opens.ext AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.of_isIso isIso_toLRSHom Set.range_eq_univ Homeomorph.surjective
opensRange_pullbackFst 📖	mathematical	—	opensRange CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right CategoryTheory.Limits.pullback.fst AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom'	—	TopologicalSpace.Opens.ext AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.IsOpenImmersion.instFstScheme AlgebraicGeometry.IsOpenImmersion.range_pullbackFst
opensRange_pullbackSnd 📖	mathematical	—	opensRange CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.IsOpenImmersion.hasPullback_of_left CategoryTheory.Limits.pullback.snd AlgebraicGeometry.IsOpenImmersion.instSndScheme CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom'	—	TopologicalSpace.Opens.ext AlgebraicGeometry.IsOpenImmersion.hasPullback_of_left AlgebraicGeometry.IsOpenImmersion.instSndScheme AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd
preimage_image_eq 📖	mathematical	—	CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor	—	TopologicalSpace.Opens.ext Set.image_congr Set.preimage_image_eq Topology.IsEmbedding.injective Topology.IsOpenEmbedding.toIsEmbedding isOpenEmbedding
preimage_opensRange 📖	mathematical	—	CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' opensRange Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	Set.preimage_range IsOpen.preimage ContinuousMap.continuous

---

← Back to Index