Restrict

📁 Source: Mathlib/AlgebraicGeometry/Restrict.lean

Statistics

Metric	Count
Definitions isoImage, isoOpensRange, preimageIso, resLE, resLEStalkMap, restrict, iSupOpenCover, instCanonicallyOverToScheme, instCoeOut, isoOfLE, stalkIso, toScheme, topIso, ι, homOfLE, isoOfEq, openCoverOfISupEqTop, openCoverOfIsOpenCover, restrictFunctor, restrictFunctorΓ, restrictRestrictComm, topIso, arrowResLEAppIso, basicOpenIsoSpecAway, morphismRestrict, morphismRestrictEq, morphismRestrictOpensRange, morphismRestrictRestrict, morphismRestrictRestrictBasicOpen, morphismRestrictStalkMap, opensRestrict, pullbackRestrictIsoRestrict, «term_∣__», ΓRestrictAlgebra	34
Theorems coe_resLE_apply, coe_resLE_base, isPullback_resLE, isoImage_hom_ι, isoImage_hom_ι_assoc, isoImage_inv_ι, isoImage_inv_ι_assoc, isoOpensRange_hom_ι, isoOpensRange_hom_ι_assoc, isoOpensRange_inv_comp, isoOpensRange_inv_comp_assoc, le_preimage_resLE_iff, le_resLE_preimage_iff, map_resLE, map_resLE_assoc, preimageIso_hom_ι, preimageIso_hom_ι_assoc, preimageIso_inv_ι, preimageIso_inv_ι_assoc, resLE_appLE, resLE_comp_resLE, resLE_comp_resLE_assoc, resLE_comp_ι, resLE_comp_ι_assoc, resLE_congr, resLE_eq_morphismRestrict, resLE_id, resLE_map, resLE_map_assoc, resLE_preimage, restrict_I₀, restrict_X, restrict_f, eq_presheaf_map_eqToHom, exists_toScheme, forall_toScheme, germ_stalkIso_hom, germ_stalkIso_hom_assoc, germ_stalkIso_inv, germ_stalkIso_inv_assoc, instIsIsoCommRingCatAppLEιTopToScheme, instIsOpenImmersionι, instIsOverι, isoOfLE_hom_ι, isoOfLE_hom_ι_assoc, isoOfLE_inv_ι, isoOfLE_inv_ι_assoc, mem_basicOpen_toScheme, mem_ι_image_iff, nonempty_iff, opensRange_ι, over_def, range_ι, stalkIso_inv, toScheme_carrier, toScheme_presheaf_map, toScheme_presheaf_obj, topIso_hom, topIso_inv, ι_app, ι_appIso, ι_appLE, ι_appTop, ι_app_self, ι_apply, ι_base_apply, ι_image_basicOpen, ι_image_basicOpen', ι_image_basicOpen_topIso_inv, ι_image_le, ι_image_top, ι_preimage_self, homOfLE_app, homOfLE_appLE, homOfLE_appTop, homOfLE_apply, homOfLE_base, homOfLE_homOfLE, homOfLE_homOfLE_assoc, homOfLE_rfl, homOfLE_ι, homOfLE_ι_assoc, isoOfEq_hom, isoOfEq_hom_ι, isoOfEq_hom_ι_assoc, isoOfEq_inv, isoOfEq_inv_ι, isoOfEq_inv_ι_assoc, isoOfEq_rfl, map_basicOpen, map_basicOpen_map, openCoverOfIsOpenCover_I₀, openCoverOfIsOpenCover_X, openCoverOfIsOpenCover_f, opensRange_homOfLE, restrictFunctor_map_left, restrictFunctor_obj_hom, restrictFunctor_obj_left, restrictFunctorΓ_hom_app, restrictFunctorΓ_inv_app, toIso_inv_ι, toIso_inv_ι_assoc, topIso_hom, ι_image_homOfLE_le_ι_image, ι_toIso_inv, ι_toIso_inv_assoc, basicOpenIsoSpecAway_inv_homOfLE, basicOpenIsoSpecAway_inv_homOfLE_assoc, coe_opensRestrict_apply_coe, coe_opensRestrict_symm_apply, image_morphismRestrict_preimage, instIsIsoSchemeMorphismRestrict, instIsOpenImmersionHomOfLE, instIsOpenImmersionMorphismRestrict, instIsOverHomOfLE, isPullback_morphismRestrict, isPullback_opens_inf, isPullback_opens_inf_le, morphismRestrict_app, morphismRestrict_app', morphismRestrict_appLE, morphismRestrict_appTop, morphismRestrict_base, morphismRestrict_base_coe, morphismRestrict_comp, morphismRestrict_id, morphismRestrict_ι, morphismRestrict_ι_assoc, pullbackRestrictIsoRestrict_hom_morphismRestrict, pullbackRestrictIsoRestrict_hom_morphismRestrict_assoc, pullbackRestrictIsoRestrict_hom_ι, pullbackRestrictIsoRestrict_hom_ι_assoc, pullbackRestrictIsoRestrict_inv_fst, pullbackRestrictIsoRestrict_inv_fst_assoc, Γ_map_morphismRestrict	135
Total	169

AlgebraicGeometry

Definitions

Name	Category	Theorems
arrowResLEAppIso 📖	CompOp	—
basicOpenIsoSpecAway 📖	CompOp	2 math math: basicOpenIsoSpecAway_inv_homOfLE_assoc, basicOpenIsoSpecAway_inv_homOfLE
morphismRestrict 📖	CompOp	55 math math: Γ_map_morphismRestrict, morphismRestrict_base_coe, Scheme.Opens.toSpecΓ_naturality, instGeometricallyIrreducibleMorphismRestrict, Scheme.Hom.exists_isIso_morphismRestrict_toNormalization, morphismRestrict_ι_assoc, pullbackRestrictIsoRestrict_hom_morphismRestrict_assoc, Scheme.Hom.resLE_eq_morphismRestrict, image_morphismRestrict_preimage, IsZariskiLocalAtTarget.restrict, IsFinite.instMorphismRestrict, Flat.instMorphismRestrict, instQuasiCompactMorphismRestrict, IsImmersion.instMorphismRestrict, Scheme.Opens.toSpecΓ_naturality_assoc, isIso_morphismRestrict_iff_isIso_app, morphismRestrict_base, morphismRestrict_ι, Scheme.OpenCover.restrict_f, HasAffineProperty.restrict, instIsIsoSchemeMorphismRestrict, instLocallyQuasiFiniteMorphismRestrict, instGeometricallyReducedMorphismRestrict, morphismRestrict_comp, IsProper.instMorphismRestrict, IsZariskiLocalAtTarget.iff_of_iSup_eq_top, morphismRestrict_app', instLocallyOfFiniteTypeMorphismRestrict, IsIntegralHom.instMorphismRestrict, instIsOpenImmersionMorphismRestrict, instQuasiSeparatedMorphismRestrict, HasAffineProperty.iff_of_iSup_eq_top, morphismRestrict_appTop, Scheme.Hom.exists_mem_and_isIso_morphismRestrict_toNormalization, IsLocalAtTarget.restrict, Proj.fromOfGlobalSections_morphismRestrict, Scheme.ker_morphismRestrict_ideal, IsLocalAtTarget.iff_of_iSup_eq_top, instIsClosedImmersionMorphismRestrict, isPullback_morphismRestrict, instSmoothMorphismRestrict, exists_isFinite_morphismRestrict_of_finite_preimage_singleton, AffineTargetMorphismProperty.IsLocal.to_basicOpen, instGeometricallyIntegralMorphismRestrict, pullbackRestrictIsoRestrict_hom_morphismRestrict, instUniversallyClosedMorphismRestrict, IsPreimmersion.instMorphismRestrict, exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimage, IsSeparated.instMorphismRestrict, instLocallyOfFinitePresentationMorphismRestrict, morphismRestrict_app, sourceAffineLocally_morphismRestrict, Etale.instMorphismRestrict, isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange, morphismRestrict_id
morphismRestrictEq 📖	CompOp	—
morphismRestrictOpensRange 📖	CompOp	—
morphismRestrictRestrict 📖	CompOp	—
morphismRestrictRestrictBasicOpen 📖	CompOp	—
morphismRestrictStalkMap 📖	CompOp	—
opensRestrict 📖	CompOp	2 math math: coe_opensRestrict_symm_apply, coe_opensRestrict_apply_coe
pullbackRestrictIsoRestrict 📖	CompOp	6 math math: pullbackRestrictIsoRestrict_hom_morphismRestrict_assoc, pullbackRestrictIsoRestrict_inv_fst, pullbackRestrictIsoRestrict_hom_ι_assoc, pullbackRestrictIsoRestrict_hom_ι, pullbackRestrictIsoRestrict_inv_fst_assoc, pullbackRestrictIsoRestrict_hom_morphismRestrict
«term_∣__» 📖	CompOp	—
ΓRestrictAlgebra 📖	CompOp	1 math math: Γ_restrict_isLocalization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basicOpenIsoSpecAway_inv_homOfLE 📖	mathematical	CommRingCat.carrier Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing CommRingCat.commRing	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory Spec CommRingCat.of Localization.Away CommRing.toCommMonoid OreLocalization.instCommRing Submonoid.powers CommMonoid.toMonoid OreLocalization.oreSetComm Scheme.Opens.toScheme PrimeSpectrum.basicOpen CommRing.toCommSemiring CategoryTheory.Iso.inv basicOpenIsoSpecAway Scheme.homOfLE Spec.map CommRingCat.ofHom IsLocalization.Away.awayToAwayRight OreLocalization.instAlgebra Ring.toSemiring CommRing.toRing Algebra.id Localization.isLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring	—	Localization.isLocalization CategoryTheory.cancel_mono IsOpenImmersion.mono Scheme.Opens.instIsOpenImmersionι Scheme.isOpenImmersion_SpecMap_localizationAway CategoryTheory.Category.assoc Scheme.homOfLE_ι IsOpenImmersion.isoOfRangeEq_inv_fac RingHom.ext IsLocalization.Away.awayToAwayRight_eq
basicOpenIsoSpecAway_inv_homOfLE_assoc 📖	mathematical	CommRingCat.carrier Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing CommRingCat.commRing	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory Spec CommRingCat.of Localization.Away CommRing.toCommMonoid OreLocalization.instCommRing Submonoid.powers CommMonoid.toMonoid OreLocalization.oreSetComm Scheme.Opens.toScheme PrimeSpectrum.basicOpen CommRing.toCommSemiring CategoryTheory.Iso.inv basicOpenIsoSpecAway Scheme.homOfLE Spec.map CommRingCat.ofHom IsLocalization.Away.awayToAwayRight OreLocalization.instAlgebra Ring.toSemiring CommRing.toRing Algebra.id Localization.isLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring	—	Localization.isLocalization CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' basicOpenIsoSpecAway_inv_homOfLE
coe_opensRestrict_apply_coe 📖	mathematical	—	SetLike.coe TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.instSetLike Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder DFunLike.coe Equiv Scheme.Opens.toScheme EquivLike.toFunLike Equiv.instEquivLike opensRestrict Set.image SetLike.instMembership TopCat.str	—	Set.image_congr
coe_opensRestrict_symm_apply 📖	mathematical	—	SetLike.coe TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace Scheme.Opens.toScheme SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.instSetLike DFunLike.coe Equiv Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder EquivLike.toFunLike Equiv.instEquivLike Equiv.symm opensRestrict Set.preimage ContinuousMap TopCat.str ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory TopCat.instConcreteCategoryContinuousMapCarrier PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' Scheme.Opens.ι Scheme.Hom.opensRange Scheme.Opens.instIsOpenImmersionι Equiv.subtypeEquivProp	—	—
image_morphismRestrict_preimage 📖	mathematical	—	CategoryTheory.Functor.obj Scheme.Opens Scheme.Opens.toScheme Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' SheafedSpace.instTopologicalSpaceCarrierCarrier Scheme.Hom.opensFunctor Scheme.Opens.ι Scheme.Opens.instIsOpenImmersionι morphismRestrict	—	IsOpenImmersion.image_preimage_eq_preimage_image_of_isPullback Scheme.Opens.instIsOpenImmersionι isPullback_morphismRestrict
instIsIsoSchemeMorphismRestrict 📖	mathematical	—	CategoryTheory.IsIso Scheme Scheme.instCategory Scheme.Opens.toScheme CategoryTheory.Functor.obj Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' morphismRestrict	—	CategoryTheory.IsIso.comp_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.Limits.pullback_snd_iso_of_left_iso
instIsOpenImmersionHomOfLE 📖	mathematical	Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier	IsOpenImmersion Scheme.Opens.toScheme Scheme.homOfLE	—	Scheme.Opens.instIsOpenImmersionι IsOpenImmersion.instLift
instIsOpenImmersionMorphismRestrict 📖	mathematical	—	IsOpenImmersion Scheme.Opens.toScheme CategoryTheory.Functor.obj Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' morphismRestrict	—	PresheafedSpace.IsOpenImmersion.comp instIsOpenImmersionCommRingCatOfIsOpenImmersion IsOpenImmersion.of_isIso CategoryTheory.Iso.isIso_inv IsOpenImmersion.instSndScheme
instIsOverHomOfLE 📖	mathematical	Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier	Scheme.Hom.IsOver Scheme.Opens.toScheme Scheme.homOfLE CategoryTheory.CanonicallyOverClass.toOverClass Scheme Scheme.instCategory Scheme.Opens.instCanonicallyOverToScheme	—	Scheme.homOfLE_ι
isPullback_morphismRestrict 📖	mathematical	—	CategoryTheory.IsPullback Scheme Scheme.instCategory Scheme.Opens.toScheme CategoryTheory.Functor.obj Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' morphismRestrict Scheme.Opens.ι	—	CategoryTheory.Category.id_comp CategoryTheory.IsPullback.paste_horiz TopologicalSpace.Opens.isOpenEmbedding IsOpenImmersion.hasPullback_of_right IsOpenImmersion.ofRestrict CategoryTheory.IsPullback.of_horiz_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.IsIso.id Scheme.Opens.instIsOpenImmersionι pullbackRestrictIsoRestrict_inv_fst CategoryTheory.Category.comp_id CategoryTheory.IsPullback.flip CategoryTheory.IsPullback.of_hasPullback
isPullback_opens_inf 📖	mathematical	—	CategoryTheory.IsPullback Scheme Scheme.instCategory Scheme.Opens.toScheme Scheme.Opens SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier Scheme.homOfLE inf_le_left inf_le_right Scheme.Opens.ι	—	CategoryTheory.IsPullback.of_iso isPullback_morphismRestrict inf_le_left inf_le_right Scheme.Opens.instIsOpenImmersionι TopologicalSpace.Opens.functor_map_eq_inf CategoryTheory.Category.comp_id CategoryTheory.Category.assoc CategoryTheory.cancel_mono IsOpenImmersion.mono morphismRestrict_ι Scheme.homOfLE_ι Scheme.isoOfEq_hom_ι Scheme.Hom.isoImage_hom_ι CategoryTheory.Category.id_comp
isPullback_opens_inf_le 📖	mathematical	Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier	CategoryTheory.IsPullback Scheme Scheme.instCategory Scheme.Opens.toScheme SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice Scheme.homOfLE inf_le_left inf_le_right	—	CategoryTheory.IsPullback.of_iso isPullback_morphismRestrict inf_le_left inf_le_right Scheme.Opens.instIsOpenImmersionι TopologicalSpace.Opens.map_comp_obj Scheme.Hom.comp_base Scheme.homOfLE_ι TopologicalSpace.Opens.functor_map_eq_inf Topology.IsOpenEmbedding.isOpenMap TopologicalSpace.Opens.isOpenEmbedding CategoryTheory.Category.assoc CategoryTheory.cancel_mono IsOpenImmersion.mono Scheme.isoOfEq_hom_ι Scheme.Hom.isoImage_hom_ι morphismRestrict_ι_assoc CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
morphismRestrict_app 📖	mathematical	—	Scheme.Hom.app Scheme.Opens.toScheme CategoryTheory.Functor.obj Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' morphismRestrict CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite CategoryTheory.Category.opposite PresheafedSpace.presheaf Opposite.op SheafedSpace.instTopologicalSpaceCarrierCarrier Scheme.Hom.opensFunctor Scheme.Opens.ι Scheme.Opens.instIsOpenImmersionι CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.eqToHom image_morphismRestrict_preimage	—	Scheme.Opens.instIsOpenImmersionι image_morphismRestrict_preimage Scheme.Hom.preimage_image_eq CategoryTheory.eqToHom_op morphismRestrict_ι Set.image_preimage_subset CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp CategoryTheory.eqToHom_unop CategoryTheory.Category.assoc CategoryTheory.NatTrans.naturality_assoc Scheme.Hom.congr_app
morphismRestrict_app' 📖	mathematical	—	Scheme.Hom.app Scheme.Opens.toScheme CategoryTheory.Functor.obj Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' morphismRestrict Scheme.Hom.appLE SheafedSpace.instTopologicalSpaceCarrierCarrier Scheme.Hom.opensFunctor Scheme.Opens.ι Scheme.Opens.instIsOpenImmersionι Eq.le image_morphismRestrict_preimage	—	morphismRestrict_app
morphismRestrict_appLE 📖	mathematical	Scheme.Opens Scheme.Opens.toScheme CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' Preorder.toLE SheafedSpace.instTopologicalSpaceCarrierCarrier morphismRestrict	Scheme.Hom.appLE Scheme.Hom.opensFunctor Scheme.Opens.ι Scheme.Opens.instIsOpenImmersionι HasSubset.Subset.trans Set Set.instHasSubset Set.instIsTransSubset Set.image DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier CategoryTheory.InducedCategory.Hom.hom SheafedSpace PresheafedSpace PresheafedSpace.categoryOfPresheafedSpaces LocallyRingedSpace.Hom.toShHom Scheme.Hom.toLRSHom SetLike.coe TopologicalSpace.Opens.instSetLike Set.image_mono Eq.le image_morphismRestrict_preimage	—	Scheme.Opens.instIsOpenImmersionι HasSubset.Subset.trans Set.instIsTransSubset Set.image_mono Eq.le image_morphismRestrict_preimage Scheme.Hom.appLE.eq_1 morphismRestrict_app' Scheme.Opens.toScheme_presheaf_map LE.le.trans Scheme.Hom.appLE_map
morphismRestrict_appTop 📖	mathematical	—	Scheme.Hom.appTop Scheme.Opens.toScheme CategoryTheory.Functor.obj Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' morphismRestrict CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite CategoryTheory.Category.opposite PresheafedSpace.presheaf Opposite.op SheafedSpace.instTopologicalSpaceCarrierCarrier Scheme.Hom.opensFunctor Scheme.Opens.ι Scheme.Opens.instIsOpenImmersionι Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Scheme.Hom.app CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.eqToHom image_morphismRestrict_preimage	—	morphismRestrict_app
morphismRestrict_base 📖	mathematical	—	DFunLike.coe PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace Scheme.Opens.toScheme CategoryTheory.Functor.obj Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier morphismRestrict Set.restrictPreimage TopologicalSpace.Opens.carrier SheafedSpace.instTopologicalSpaceCarrierCarrier	—	morphismRestrict_base_coe
morphismRestrict_base_coe 📖	mathematical	—	TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike DFunLike.coe Scheme.Opens.toScheme CategoryTheory.Functor.obj Scheme.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier morphismRestrict	—	morphismRestrict_ι
morphismRestrict_comp 📖	mathematical	—	morphismRestrict CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory Scheme.Opens.toScheme CategoryTheory.Functor.obj Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' SheafedSpace.instTopologicalSpaceCarrierCarrier	—	CategoryTheory.Limits.hasPullbackHorizPaste IsOpenImmersion.hasPullback_of_right Scheme.Opens.instIsOpenImmersionι IsOpenImmersion.instFstScheme CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_snd CategoryTheory.cancel_mono IsOpenImmersion.mono CategoryTheory.Category.assoc pullbackRestrictIsoRestrict_inv_fst CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_fst CategoryTheory.Limits.pullback.condition pullbackRestrictIsoRestrict_inv_fst_assoc
morphismRestrict_id 📖	mathematical	—	morphismRestrict CategoryTheory.CategoryStruct.id Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory Scheme.Opens.toScheme CategoryTheory.Functor.obj Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom'	—	CategoryTheory.cancel_mono IsOpenImmersion.mono Scheme.Opens.instIsOpenImmersionι morphismRestrict_ι CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
morphismRestrict_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory Scheme.Opens.toScheme CategoryTheory.Functor.obj Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' morphismRestrict Scheme.Opens.ι	—	CategoryTheory.Category.assoc CategoryTheory.Limits.pullback.condition IsOpenImmersion.hasPullback_of_right Scheme.Opens.instIsOpenImmersionι pullbackRestrictIsoRestrict_inv_fst_assoc
morphismRestrict_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory Scheme.Opens.toScheme CategoryTheory.Functor.obj Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' morphismRestrict Scheme.Opens.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' morphismRestrict_ι
pullbackRestrictIsoRestrict_hom_morphismRestrict 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory CategoryTheory.Limits.pullback Scheme.Opens.toScheme Scheme.Opens.ι IsOpenImmersion.hasPullback_of_right Scheme.Opens.instIsOpenImmersionι CategoryTheory.Functor.obj Scheme.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' CategoryTheory.Iso.hom pullbackRestrictIsoRestrict morphismRestrict CategoryTheory.Limits.pullback.snd	—	CategoryTheory.Iso.hom_inv_id_assoc IsOpenImmersion.hasPullback_of_right Scheme.Opens.instIsOpenImmersionι
pullbackRestrictIsoRestrict_hom_morphismRestrict_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory CategoryTheory.Limits.pullback Scheme.Opens.toScheme Scheme.Opens.ι IsOpenImmersion.hasPullback_of_right Scheme.Opens.instIsOpenImmersionι CategoryTheory.Functor.obj Scheme.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' CategoryTheory.Iso.hom pullbackRestrictIsoRestrict morphismRestrict CategoryTheory.Limits.pullback.snd	—	IsOpenImmersion.hasPullback_of_right Scheme.Opens.instIsOpenImmersionι CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackRestrictIsoRestrict_hom_morphismRestrict
pullbackRestrictIsoRestrict_hom_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory CategoryTheory.Limits.pullback Scheme.Opens.toScheme Scheme.Opens.ι IsOpenImmersion.hasPullback_of_right Scheme.Opens.instIsOpenImmersionι CategoryTheory.Functor.obj Scheme.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' CategoryTheory.Iso.hom pullbackRestrictIsoRestrict TopologicalSpace.Opens TopCat.str CategoryTheory.Limits.pullback.fst	—	IsOpenImmersion.hasPullback_of_right Scheme.Opens.instIsOpenImmersionι IsOpenImmersion.isoOfRangeEq_hom_fac
pullbackRestrictIsoRestrict_hom_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory CategoryTheory.Limits.pullback Scheme.Opens.toScheme Scheme.Opens.ι IsOpenImmersion.hasPullback_of_right Scheme.Opens.instIsOpenImmersionι CategoryTheory.Functor.obj Scheme.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' CategoryTheory.Iso.hom pullbackRestrictIsoRestrict TopologicalSpace.Opens TopCat.str CategoryTheory.Limits.pullback.fst	—	IsOpenImmersion.hasPullback_of_right Scheme.Opens.instIsOpenImmersionι CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackRestrictIsoRestrict_hom_ι
pullbackRestrictIsoRestrict_inv_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory Scheme.Opens.toScheme CategoryTheory.Functor.obj Scheme.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' CategoryTheory.Limits.pullback Scheme.Opens.ι IsOpenImmersion.hasPullback_of_right Scheme.Opens.instIsOpenImmersionι CategoryTheory.Iso.inv pullbackRestrictIsoRestrict CategoryTheory.Limits.pullback.fst TopologicalSpace.Opens TopCat.str	—	IsOpenImmersion.hasPullback_of_right Scheme.Opens.instIsOpenImmersionι IsOpenImmersion.isoOfRangeEq_inv_fac
pullbackRestrictIsoRestrict_inv_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory Scheme.Opens.toScheme CategoryTheory.Functor.obj Scheme.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' CategoryTheory.Limits.pullback Scheme.Opens.ι IsOpenImmersion.hasPullback_of_right Scheme.Opens.instIsOpenImmersionι CategoryTheory.Iso.inv pullbackRestrictIsoRestrict CategoryTheory.Limits.pullback.fst TopologicalSpace.Opens TopCat.str	—	IsOpenImmersion.hasPullback_of_right Scheme.Opens.instIsOpenImmersionι CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackRestrictIsoRestrict_inv_fst
Γ_map_morphismRestrict 📖	mathematical	—	Scheme.Hom.appTop Scheme.Opens.toScheme CategoryTheory.Functor.obj Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' morphismRestrict CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite CategoryTheory.Category.opposite PresheafedSpace.presheaf Opposite.op SheafedSpace.instTopologicalSpaceCarrierCarrier Scheme.Hom.opensFunctor Scheme.Opens.ι Scheme.Opens.instIsOpenImmersionι Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Scheme.Hom.app CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.eqToHom image_morphismRestrict_preimage	—	morphismRestrict_appTop

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
homOfLE 📖	CompOp	42 math math: Hom.resLE_map_assoc, isoOfEq_inv, Opens.toSpecΓ_SpecMap_map, AlgebraicGeometry.isPullback_opens_inf, homOfLE_ι, Hom.resLE_map, PartialMap.Opens.isDominant_homOfLE, Opens.toSpecΓ_SpecMap_presheaf_map_assoc, opensRange_homOfLE, ι_image_homOfLE_le_ι_image, AlgebraicGeometry.Proj.basicOpenToSpec_SpecMap_awayMap, IsLocallyDirected.homOfLE_tAux, Opens.toSpecΓ_SpecMap_map_assoc, IsLocallyDirected.fst_inv_eq_snd_inv, Opens.toSpecΓ_SpecMap_presheaf_map, homOfLE_appTop, homOfLE_homOfLE_assoc, IdealSheafData.glueDataObjMap_glueDataObjι_assoc, homOfLE_homOfLE, Hom.resLE_id, IdealSheafData.glueDataObjMap_glueDataObjι, AlgebraicGeometry.Proj.homOfLE_toBasicOpenOfGlobalSections_ι_assoc, homOfLE_app, directedAffineCover_trans, AlgebraicGeometry.Proj.basicOpenToSpec_SpecMap_awayMap_assoc, PartialMap.restrict_hom, AlgebraicGeometry.instIsOpenImmersionHomOfLE, Hom.map_resLE, AlgebraicGeometry.basicOpenIsoSpecAway_inv_homOfLE_assoc, AlgebraicGeometry.basicOpenIsoSpecAway_inv_homOfLE, Hom.map_resLE_assoc, homOfLE_base, IsLocallyDirected.exists_of_pullback_V_V, homOfLE_ι_assoc, AlgebraicGeometry.Proj.homOfLE_toBasicOpenOfGlobalSections_ι, AlgebraicGeometry.instIsOverHomOfLE, restrictFunctor_map_left, AlgebraicGeometry.isPullback_opens_inf_le, IsLocallyDirected.homOfLE_tAux_assoc, isoOfEq_hom, homOfLE_apply, homOfLE_rfl
isoOfEq 📖	CompOp	9 math math: isoOfEq_inv, PartialMap.ext_iff, isoOfEq_inv_ι, isoOfEq_hom_ι, isoOfEq_hom_ι_assoc, isoOfEq_inv_ι_assoc, isoOfEq_rfl, AlgebraicGeometry.Proj.fromOfGlobalSections_morphismRestrict, isoOfEq_hom
openCoverOfISupEqTop 📖	CompOp	—
openCoverOfIsOpenCover 📖	CompOp	3 math math: openCoverOfIsOpenCover_I₀, openCoverOfIsOpenCover_f, openCoverOfIsOpenCover_X
restrictFunctor 📖	CompOp	7 math math: restrictFunctorΓ_inv_app, AffineZariskiSite.restrictIsoSpec_hom_app, restrictFunctorΓ_hom_app, restrictFunctor_obj_left, restrictFunctor_map_left, restrictFunctor_obj_hom, AffineZariskiSite.restrictIsoSpec_inv_app
restrictFunctorΓ 📖	CompOp	2 math math: restrictFunctorΓ_inv_app, restrictFunctorΓ_hom_app
restrictRestrictComm 📖	CompOp	—
topIso 📖	CompOp	6 math math: Hom.toPartialMap_hom, ι_toIso_inv, ι_toIso_inv_assoc, toIso_inv_ι_assoc, topIso_hom, toIso_inv_ι

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homOfLE_app 📖	mathematical	Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	Hom.app Opens.toScheme homOfLE CategoryTheory.Functor.map Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op CategoryTheory.Functor.obj Hom.opensFunctor Opens.ι Opens.instIsOpenImmersionι TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.homOfLE ι_image_homOfLE_le_ι_image	—	Opens.instIsOpenImmersionι homOfLE_ι Hom.congr_app TopologicalSpace.Opens.map_functor_eq Hom.naturality ι_image_homOfLE_le_ι_image Set.image_preimage_subset CategoryTheory.isIso_op CategoryTheory.Functor.map_isIso CategoryTheory.instIsIsoEqToHom CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_inv CategoryTheory.IsIso.eq_comp_inv
homOfLE_appLE 📖	mathematical	Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier Opens.toScheme CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' homOfLE	Hom.appLE CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op Hom.opensFunctor Opens.ι Opens.instIsOpenImmersionι Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.homOfLE LE.le.trans Hom.image_mono ι_image_homOfLE_le_ι_image	—	Opens.instIsOpenImmersionι LE.le.trans Hom.image_mono ι_image_homOfLE_le_ι_image homOfLE_app
homOfLE_appTop 📖	mathematical	Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	Hom.appTop Opens.toScheme homOfLE CategoryTheory.Functor.map Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op CategoryTheory.Functor.obj Hom.opensFunctor Opens.ι Opens.instIsOpenImmersionι Top.top OrderTop.toTop SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.homOfLE ι_image_homOfLE_le_ι_image	—	homOfLE_app
homOfLE_apply 📖	mathematical	Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike DFunLike.coe Opens.toScheme CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' homOfLE	—	homOfLE_base
homOfLE_base 📖	mathematical	Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	AlgebraicGeometry.PresheafedSpace.Hom.base Opens.toScheme AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' homOfLE CategoryTheory.Functor.map TopologicalSpace.Opens TopCat.str Preorder.smallCategory TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat CategoryTheory.homOfLE	—	TopCat.ext homOfLE_ι
homOfLE_homOfLE 📖	mathematical	Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory Opens.toScheme homOfLE LE.le.trans	—	LE.le.trans CategoryTheory.cancel_mono AlgebraicGeometry.IsOpenImmersion.mono Opens.instIsOpenImmersionι CategoryTheory.Category.assoc homOfLE_ι
homOfLE_homOfLE_assoc 📖	mathematical	Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory Opens.toScheme homOfLE LE.le.trans	—	LE.le.trans CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homOfLE_homOfLE
homOfLE_rfl 📖	mathematical	—	homOfLE refl Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier instReflLe CategoryTheory.CategoryStruct.id AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory Opens.toScheme	—	refl instReflLe CategoryTheory.cancel_mono AlgebraicGeometry.IsOpenImmersion.mono Opens.instIsOpenImmersionι homOfLE_ι CategoryTheory.Category.id_comp
homOfLE_ι 📖	mathematical	Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory Opens.toScheme homOfLE Opens.ι	—	AlgebraicGeometry.IsOpenImmersion.lift_fac Opens.instIsOpenImmersionι
homOfLE_ι_assoc 📖	mathematical	Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory Opens.toScheme homOfLE Opens.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homOfLE_ι
isoOfEq_hom 📖	mathematical	—	CategoryTheory.Iso.hom AlgebraicGeometry.Scheme instCategory Opens.toScheme isoOfEq homOfLE Eq.le Opens PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	—	—
isoOfEq_hom_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory Opens.toScheme CategoryTheory.Iso.hom isoOfEq Opens.ι	—	AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac Opens.instIsOpenImmersionι
isoOfEq_hom_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory Opens.toScheme CategoryTheory.Iso.hom isoOfEq Opens.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoOfEq_hom_ι
isoOfEq_inv 📖	mathematical	—	CategoryTheory.Iso.inv AlgebraicGeometry.Scheme instCategory Opens.toScheme isoOfEq homOfLE Eq.ge Opens PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	—	—
isoOfEq_inv_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory Opens.toScheme CategoryTheory.Iso.inv isoOfEq Opens.ι	—	AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac Opens.instIsOpenImmersionι
isoOfEq_inv_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory Opens.toScheme CategoryTheory.Iso.inv isoOfEq Opens.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoOfEq_inv_ι
isoOfEq_rfl 📖	mathematical	—	isoOfEq refl Opens IsPreorder.toRefl IsEquiv.toIsPreorder eq_isEquiv CategoryTheory.Iso.refl AlgebraicGeometry.Scheme instCategory Opens.toScheme	—	CategoryTheory.Iso.ext refl IsPreorder.toRefl IsEquiv.toIsPreorder eq_isEquiv CategoryTheory.cancel_mono AlgebraicGeometry.IsOpenImmersion.mono Opens.instIsOpenImmersionι isoOfEq_hom_ι CategoryTheory.Iso.refl_hom CategoryTheory.Category.id_comp
map_basicOpen 📖	mathematical	—	CategoryTheory.Functor.obj Opens Opens.toScheme 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 Opens.ι Opens.instIsOpenImmersionι basicOpen Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder 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.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom Opens.ι_image_top	—	Opens.ι_image_basicOpen'
map_basicOpen_map 📖	mathematical	—	CategoryTheory.Functor.obj Opens Opens.toScheme 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 Opens.ι Opens.instIsOpenImmersionι basicOpen Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder 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 Opens.topIso	—	Opens.ι_image_basicOpen_topIso_inv
openCoverOfIsOpenCover_I₀ 📖	mathematical	TopologicalSpace.IsOpenCover TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover precoverage AlgebraicGeometry.IsOpenImmersion openCoverOfIsOpenCover	—	—
openCoverOfIsOpenCover_X 📖	mathematical	TopologicalSpace.IsOpenCover TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover precoverage AlgebraicGeometry.IsOpenImmersion openCoverOfIsOpenCover Opens.toScheme	—	—
openCoverOfIsOpenCover_f 📖	mathematical	TopologicalSpace.IsOpenCover TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover precoverage AlgebraicGeometry.IsOpenImmersion openCoverOfIsOpenCover Opens.ι	—	—
opensRange_homOfLE 📖	mathematical	Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	Hom.opensRange Opens.toScheme homOfLE AlgebraicGeometry.instIsOpenImmersionHomOfLE CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' Opens.ι	—	Hom.image_injective Opens.instIsOpenImmersionι AlgebraicGeometry.instIsOpenImmersionHomOfLE AlgebraicGeometry.IsOpenImmersion.comp homOfLE_ι Hom.opensRange.congr_simp Opens.opensRange_ι Hom.image_preimage_eq_opensRange_inf inf_of_le_right
restrictFunctor_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left AlgebraicGeometry.Scheme instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit Opens.toScheme Opens.ι CategoryTheory.Functor.map 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 CategoryTheory.Over CategoryTheory.instCategoryOver restrictFunctor homOfLE	—	—
restrictFunctor_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom AlgebraicGeometry.Scheme instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit 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 CategoryTheory.Over CategoryTheory.instCategoryOver restrictFunctor Opens.ι	—	—
restrictFunctor_obj_left 📖	mathematical	—	CategoryTheory.Comma.left AlgebraicGeometry.Scheme instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit 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 CategoryTheory.Over CategoryTheory.instCategoryOver restrictFunctor Opens.toScheme	—	—
restrictFunctorΓ_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite Opens CategoryTheory.Category.opposite 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 CategoryTheory.Functor.comp CategoryTheory.Over AlgebraicGeometry.Scheme instCategory CategoryTheory.instCategoryOver CategoryTheory.Functor.op restrictFunctor CategoryTheory.Over.forget Γ AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category restrictFunctorΓ CategoryTheory.Functor.map TopologicalSpace.Opens TopCat.str Opposite.op CategoryTheory.Functor.obj TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat Opposite.unop IsOpenMap.functor TopologicalSpace.Opens.inclusion' Top.top Opens.toScheme OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.eqToHom_op
restrictFunctorΓ_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite Opens CategoryTheory.Category.opposite 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 AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Functor.comp CategoryTheory.Over AlgebraicGeometry.Scheme instCategory CategoryTheory.instCategoryOver CategoryTheory.Functor.op restrictFunctor CategoryTheory.Over.forget Γ CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category restrictFunctorΓ CategoryTheory.Functor.map TopologicalSpace.Opens TopCat.str Opposite.op CategoryTheory.Functor.obj TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat Opposite.unop IsOpenMap.functor TopologicalSpace.Opens.inclusion' Top.top Opens.toScheme OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.eqToHom_op
toIso_inv_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory Opens.toScheme Top.top 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 toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.Iso.inv topIso Opens.ι CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.inv_hom_id
toIso_inv_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory Opens.toScheme Top.top 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 toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.Iso.inv topIso Opens.ι	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' toIso_inv_ι
topIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom AlgebraicGeometry.Scheme instCategory Opens.toScheme Top.top 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 toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder topIso Opens.ι	—	—
ι_image_homOfLE_le_ι_image 📖	mathematical	Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	CategoryTheory.Functor.obj Opens.toScheme Preorder.smallCategory Hom.opensFunctor Opens.ι Opens.instIsOpenImmersionι TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' homOfLE	—	Opens.instIsOpenImmersionι homOfLE_base instIsConcreteLE Set.image_congr
ι_toIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory Opens.toScheme Top.top 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 toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Opens.ι CategoryTheory.Iso.inv topIso CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.hom_inv_id
ι_toIso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory Opens.toScheme Top.top 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 toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Opens.ι CategoryTheory.Iso.inv topIso	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' ι_toIso_inv

AlgebraicGeometry.Scheme.Hom

Definitions

Name	Category	Theorems
isoImage 📖	CompOp	4 math math: isoImage_inv_ι, isoImage_inv_ι_assoc, isoImage_hom_ι, isoImage_hom_ι_assoc
isoOpensRange 📖	CompOp	8 math math: isoOpensRange_hom_ι_assoc, isoOpensRange_hom_ι, AlgebraicGeometry.Scheme.IsLocallyDirected.homOfLE_tAux, AlgebraicGeometry.Scheme.IsLocallyDirected.fst_inv_eq_snd_inv, isoOpensRange_inv_comp_assoc, AlgebraicGeometry.Scheme.IsLocallyDirected.exists_of_pullback_V_V, AlgebraicGeometry.Scheme.IsLocallyDirected.homOfLE_tAux_assoc, isoOpensRange_inv_comp
preimageIso 📖	CompOp	4 math math: preimageIso_hom_ι_assoc, preimageIso_inv_ι, preimageIso_hom_ι, preimageIso_inv_ι_assoc
resLE 📖	CompOp	35 math math: resLE_map_assoc, AlgebraicGeometry.Proj.fromOfGlobalSections_resLE, resLE_eq_morphismRestrict, AlgebraicGeometry.instQuasiSeparatedResLE, coe_resLE_base, resLE_map, coe_resLE_apply, isPullback_resLE, AlgebraicGeometry.IsImmersion.instResLE, AlgebraicGeometry.IsLocalAtSource.iff_exists_resLE, AlgebraicGeometry.opensDiagram_map, AlgebraicGeometry.instSmoothResLE, resLE_congr, AlgebraicGeometry.opensCone_π_app, resLE_id, AlgebraicGeometry.IsSeparated.instResLE, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_appLE_assoc, AlgebraicGeometry.Etale.instResLE, resLE_comp_resLE_assoc, AlgebraicGeometry.Flat.instResLE, AlgebraicGeometry.instLocallyQuasiFiniteResLE, AlgebraicGeometry.IsLocalAtSource.resLE, AlgebraicGeometry.IsZariskiLocalAtSource.resLE, map_resLE, resLE_preimage, le_preimage_resLE_iff, resLE_comp_ι_assoc, map_resLE_assoc, resLE_comp_ι, AlgebraicGeometry.IsZariskiLocalAtSource.iff_exists_resLE, resLE_comp_resLE, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_appLE, AlgebraicGeometry.instLocallyOfFiniteTypeResLE, le_resLE_preimage_iff, AlgebraicGeometry.instLocallyOfFinitePresentationResLE
resLEStalkMap 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_resLE_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'	SetLike.instMembership TopologicalSpace.Opens.instSetLike DFunLike.coe AlgebraicGeometry.Scheme.Opens.toScheme CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier resLE	—	AlgebraicGeometry.morphismRestrict_base AlgebraicGeometry.Scheme.homOfLE_apply
coe_resLE_base 📖	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'	SetLike.instMembership TopologicalSpace.Opens.instSetLike DFunLike.coe AlgebraicGeometry.Scheme.Opens.toScheme CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier resLE	—	coe_resLE_apply
isPullback_resLE 📖	mathematical	CategoryTheory.IsPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory 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' SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice	AlgebraicGeometry.Scheme.Opens.toScheme resLE	—	CategoryTheory.IsPullback.paste_horiz LE.le.trans_eq CategoryTheory.CommSq.w CategoryTheory.IsPullback.toCommSq preimage_mono CategoryTheory.IsPullback.flip AlgebraicGeometry.IsOpenImmersion.isPullback AlgebraicGeometry.instIsOpenImmersionHomOfLE LE.le.trans map_resLE resLE_map AlgebraicGeometry.Scheme.opensRange_homOfLE resLE_comp_ι comp_preimage AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι image_injective image_preimage_eq_opensRange_inf AlgebraicGeometry.Scheme.Opens.opensRange_ι inf_of_le_right CategoryTheory.IsPullback.of_bot CategoryTheory.IsPullback.paste_vert AlgebraicGeometry.isPullback_morphismRestrict CategoryTheory.cancel_mono AlgebraicGeometry.IsOpenImmersion.mono CategoryTheory.Category.assoc AlgebraicGeometry.morphismRestrict_ι_assoc AlgebraicGeometry.morphismRestrict_ι resLE_comp_ι_assoc
isoImage_hom_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme 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.hom isoImage AlgebraicGeometry.Scheme.Opens.ι	—	AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac
isoImage_hom_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme 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.hom isoImage AlgebraicGeometry.Scheme.Opens.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoImage_hom_ι
isoImage_inv_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme 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 isoImage AlgebraicGeometry.Scheme.Opens.ι	—	AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac
isoImage_inv_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme 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 isoImage AlgebraicGeometry.Scheme.Opens.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoImage_inv_ι
isoOpensRange_hom_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme opensRange CategoryTheory.Iso.hom isoOpensRange AlgebraicGeometry.Scheme.Opens.ι	—	AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac
isoOpensRange_hom_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme opensRange CategoryTheory.Iso.hom isoOpensRange AlgebraicGeometry.Scheme.Opens.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoOpensRange_hom_ι
isoOpensRange_inv_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme opensRange CategoryTheory.Iso.inv isoOpensRange AlgebraicGeometry.Scheme.Opens.ι	—	AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac
isoOpensRange_inv_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme opensRange CategoryTheory.Iso.inv isoOpensRange AlgebraicGeometry.Scheme.Opens.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoOpensRange_inv_comp
le_preimage_resLE_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 TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom'	AlgebraicGeometry.Scheme.Opens.toScheme resLE opensFunctor AlgebraicGeometry.Scheme.Opens.ι AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι	—	le_resLE_preimage_iff
le_resLE_preimage_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 TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom'	AlgebraicGeometry.Scheme.Opens.toScheme resLE opensFunctor AlgebraicGeometry.Scheme.Opens.ι AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι	—	AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι resLE_preimage image_le_image_iff image_preimage_eq_opensRange_inf AlgebraicGeometry.Scheme.Opens.opensRange_ι AlgebraicGeometry.Scheme.Opens.ι_image_le
map_resLE 📖	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 AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Scheme.homOfLE resLE LE.le.trans	—	LE.le.trans resLE_comp_resLE CategoryTheory.Category.id_comp resLE.congr_simp
map_resLE_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 AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Scheme.homOfLE resLE LE.le.trans	—	LE.le.trans CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_resLE
preimageIso_hom_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme 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' CategoryTheory.Iso.hom preimageIso AlgebraicGeometry.Scheme.Opens.ι	—	AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι
preimageIso_hom_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme 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' CategoryTheory.Iso.hom preimageIso AlgebraicGeometry.Scheme.Opens.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' preimageIso_hom_ι
preimageIso_inv_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme 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' CategoryTheory.Iso.inv preimageIso AlgebraicGeometry.Scheme.Opens.ι	—	AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι
preimageIso_inv_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme 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' CategoryTheory.Iso.inv preimageIso AlgebraicGeometry.Scheme.Opens.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' preimageIso_inv_ι
resLE_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' AlgebraicGeometry.Scheme.Opens.toScheme resLE	appLE opensFunctor AlgebraicGeometry.Scheme.Opens.ι AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι le_resLE_preimage_iff	—	AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι le_resLE_preimage_iff image_mono Eq.le AlgebraicGeometry.image_morphismRestrict_preimage AlgebraicGeometry.Scheme.ι_image_homOfLE_le_ι_image AlgebraicGeometry.morphismRestrict_app' AlgebraicGeometry.Scheme.homOfLE_app CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp
resLE_comp_resLE 📖	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 AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme resLE LE.le.trans Quiver.Hom.le CategoryTheory.Functor.map CategoryTheory.homOfLE	—	LE.le.trans CategoryTheory.cancel_mono AlgebraicGeometry.IsOpenImmersion.mono AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι CategoryTheory.Category.assoc resLE_comp_ι resLE_comp_ι_assoc
resLE_comp_resLE_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 AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme resLE LE.le.trans Quiver.Hom.le CategoryTheory.Functor.map CategoryTheory.homOfLE	—	LE.le.trans CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' resLE_comp_resLE
resLE_comp_ι 📖	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 AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme resLE AlgebraicGeometry.Scheme.Opens.ι	—	CategoryTheory.Category.assoc AlgebraicGeometry.morphismRestrict_ι AlgebraicGeometry.Scheme.homOfLE_ι_assoc
resLE_comp_ι_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 AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme resLE AlgebraicGeometry.Scheme.Opens.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' resLE_comp_ι
resLE_congr 📖	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'	AlgebraicGeometry.Scheme.Opens.toScheme resLE	—	—
resLE_eq_morphismRestrict 📖	mathematical	—	resLE 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 TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' le_rfl AlgebraicGeometry.morphismRestrict	—	le_rfl AlgebraicGeometry.Scheme.homOfLE_rfl CategoryTheory.Category.id_comp
resLE_id 📖	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	resLE CategoryTheory.CategoryStruct.id AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.homOfLE	—	AlgebraicGeometry.morphismRestrict_id
resLE_map 📖	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 AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme resLE AlgebraicGeometry.Scheme.homOfLE LE.le.trans Quiver.Hom.le CategoryTheory.Functor.map LE.le.hom	—	LE.le.trans resLE_comp_resLE CategoryTheory.Category.comp_id resLE.congr_simp
resLE_map_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 AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme resLE AlgebraicGeometry.Scheme.homOfLE LE.le.trans Quiver.Hom.le CategoryTheory.Functor.map LE.le.hom	—	LE.le.trans CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' resLE_map
resLE_preimage 📖	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'	AlgebraicGeometry.Scheme.Opens.toScheme resLE AlgebraicGeometry.Scheme.Opens.ι opensFunctor AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι	—	AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι comp_preimage resLE_comp_ι preimage_image_eq

AlgebraicGeometry.Scheme.OpenCover

Definitions

Name	Category	Theorems
restrict 📖	CompOp	3 math math: restrict_f, restrict_I₀, restrict_X

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrict_I₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion restrict	—	—
restrict_X 📖	mathematical	—	CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion restrict 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' CategoryTheory.PreZeroHypercover.f	—	—
restrict_f 📖	mathematical	—	CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion restrict AlgebraicGeometry.morphismRestrict CategoryTheory.PreZeroHypercover.X	—	—

AlgebraicGeometry.Scheme.Opens

Definitions

Name	Category	Theorems
iSupOpenCover 📖	CompOp	—
instCanonicallyOverToScheme 📖	CompOp	4 math math: AlgebraicGeometry.Scheme.instIsOverFromSpecStalkOfMem, over_def, instIsOverι, AlgebraicGeometry.instIsOverHomOfLE
instCoeOut 📖	CompOp	—
isoOfLE 📖	CompOp	4 math math: isoOfLE_hom_ι_assoc, isoOfLE_hom_ι, isoOfLE_inv_ι, isoOfLE_inv_ι_assoc
stalkIso 📖	CompOp	5 math math: stalkIso_inv, germ_stalkIso_inv, germ_stalkIso_inv_assoc, germ_stalkIso_hom, germ_stalkIso_hom_assoc
toScheme 📖	CompOp	281 math math: AlgebraicGeometry.Scheme.Hom.resLE_map_assoc, ι_image_basicOpen, AlgebraicGeometry.Γ_map_morphismRestrict, AlgebraicGeometry.Scheme.Hom.toPartialMap_hom, AlgebraicGeometry.Scheme.isoOfEq_inv, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop, AlgebraicGeometry.Scheme.PartialMap.ext_iff, AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom_ι_assoc, AlgebraicGeometry.opensCone_pt, AlgebraicGeometry.Proj.basicOpenIsoSpec_inv_ι_assoc, AlgebraicGeometry.morphismRestrict_base_coe, AlgebraicGeometry.instLocallyQuasiFiniteCompSchemeιQuasiFiniteLocus, toSpecΓ_naturality, toSpecΓ_SpecMap_presheaf_map_top, AlgebraicGeometry.Scheme.restrictFunctorΓ_inv_app, AlgebraicGeometry.instGeometricallyIrreducibleMorphismRestrict, mem_ι_image_iff, AlgebraicGeometry.Scheme.Hom.exists_isIso_morphismRestrict_toNormalization, AlgebraicGeometry.morphismRestrict_ι_assoc, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict_assoc, topIso_inv, AlgebraicGeometry.instIsDominantιCoborderRange, AlgebraicGeometry.image_morphismRestrict_preimage, AlgebraicGeometry.instQuasiSeparatedResLE, AlgebraicGeometry.Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp, toSpecΓ_SpecMap_map, AlgebraicGeometry.Scheme.ι_toIso_inv, AlgebraicGeometry.Scheme.instIsOverFromSpecStalkOfMem, AlgebraicGeometry.Scheme.Hom.coe_resLE_base, AlgebraicGeometry.isPullback_opens_inf, AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι_assoc, AlgebraicGeometry.Scheme.isoOfEq_inv_ι, AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom_ι, AlgebraicGeometry.IsZariskiLocalAtTarget.restrict, stalkIso_inv, AlgebraicGeometry.sourceLocalClosure.iff_forall_exists, AlgebraicGeometry.IsFinite.instMorphismRestrict, AlgebraicGeometry.Scheme.ι_toIso_inv_assoc, AlgebraicGeometry.Flat.instMorphismRestrict, AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_ker_glueDataObjι, AlgebraicGeometry.instQuasiCompactMorphismRestrict, AlgebraicGeometry.Proj.basicOpenToSpec_app_top, isoOfLE_hom_ι_assoc, AlgebraicGeometry.Scheme.isoOfEq_hom_ι, AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_iSup_eq_top, AlgebraicGeometry.Scheme.homOfLE_ι, AlgebraicGeometry.IsImmersion.instMorphismRestrict, AlgebraicGeometry.Scheme.Hom.resLE_map, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι_eq_support_inter, AlgebraicGeometry.Scheme.Hom.coe_resLE_apply, AlgebraicGeometry.Scheme.Hom.ι_toNormalization, AlgebraicGeometry.Scheme.PartialMap.Opens.isDominant_homOfLE, opensRange_ι, toSpecΓ_naturality_assoc, AlgebraicGeometry.IsAffineOpen.isoSpec_inv, fromSpecStalkOfMem_ι_assoc, AlgebraicGeometry.Scheme.Hom.isPullback_resLE, AlgebraicGeometry.IsImmersion.instResLE, AlgebraicGeometry.IsImmersion.isPullback_toImage_liftCoborder, toSpecΓ_SpecMap_presheaf_map_assoc, AlgebraicGeometry.Scheme.opensRange_homOfLE, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι, AlgebraicGeometry.isIso_morphismRestrict_iff_isIso_app, AlgebraicGeometry.morphismRestrict_base, ι_image_basicOpen_topIso_inv, nonempty_iff, AlgebraicGeometry.Scheme.ι_image_homOfLE_le_ι_image, AlgebraicGeometry.Proj.basicOpenToSpec_SpecMap_awayMap, AlgebraicGeometry.coe_opensRestrict_symm_apply, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst, toScheme_presheaf_obj, AlgebraicGeometry.IsLocalAtSource.iff_exists_resLE, toSpecΓ_appTop_assoc, AlgebraicGeometry.instIsClosedImmersionLiftCoborder, AlgebraicGeometry.Scheme.PartialMap.equiv_toPartialMap_iff_of_isSeparated, AlgebraicGeometry.Scheme.IdealSheafData.subschemeCover_map_subschemeι, toSpecΓ_SpecMap_presheaf_map_top_assoc, AlgebraicGeometry.liftCoborder_app, toSpecΓ_preimage_basicOpen, AlgebraicGeometry.Proj.basicOpenIsoSpec_inv_ι, toSpecΓ_appTop, AlgebraicGeometry.Scheme.Hom.isoOpensRange_hom_ι_assoc, AlgebraicGeometry.Γ_restrict_isLocalization, AlgebraicGeometry.instSmoothResLE, toScheme_carrier, AlgebraicGeometry.Scheme.Hom.isoOpensRange_hom_ι, AlgebraicGeometry.morphismRestrict_ι, AlgebraicGeometry.Scheme.Hom.preimageIso_inv_ι, AlgebraicGeometry.ΓSpecIso_obj_hom, AlgebraicGeometry.instIsIntegralToSchemeOfNonemptyCarrierCarrierCommRingCat, AlgebraicGeometry.Scheme.IsLocallyDirected.homOfLE_tAux, toSpecΓ_SpecMap_map_assoc, AlgebraicGeometry.Scheme.OpenCover.restrict_f, AlgebraicGeometry.HasAffineProperty.restrict, AlgebraicGeometry.instIsLocallyNoetherianToScheme, AlgebraicGeometry.instIsOpenImmersionCompSchemeιQuasiFiniteLocusToNormalization, toSpecΓ_top, AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec_hom_app, AlgebraicGeometry.instIsIsoSchemeMorphismRestrict, AlgebraicGeometry.Scheme.Hom.liftCoborder_preimage, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι_assoc, AlgebraicGeometry.affineOpensRestrict_apply_coe_coe, ι_appIso, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ, AlgebraicGeometry.instLocallyQuasiFiniteMorphismRestrict, instIsOpenImmersionι, AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv, AlgebraicGeometry.Scheme.IsLocallyDirected.fst_inv_eq_snd_inv, toSpecΓ_SpecMap_presheaf_map, AlgebraicGeometry.instGeometricallyReducedMorphismRestrict, AlgebraicGeometry.Scheme.openCoverOfIsOpenCover_X, AlgebraicGeometry.Scheme.homOfLE_appTop, AlgebraicGeometry.Scheme.homOfLE_homOfLE_assoc, AlgebraicGeometry.isLocalIso_iff, AlgebraicGeometry.Scheme.Hom.resLE_congr, AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjMap_glueDataObjι_assoc, AlgebraicGeometry.Scheme.PartialMap.instIsReducedToScheme, AlgebraicGeometry.morphismRestrict_comp, AlgebraicGeometry.IsProper.instMorphismRestrict, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top, AlgebraicGeometry.Scheme.restrictFunctorΓ_hom_app, AlgebraicGeometry.Scheme.directedAffineCover_X, isoOfLE_hom_ι, over_def, fromSpecStalkOfMem_ι, AlgebraicGeometry.instIsReducedToScheme, AlgebraicGeometry.Scheme.homOfLE_homOfLE, AlgebraicGeometry.IsAffineOpen.instIsAffineToSchemeBasicOpen, AlgebraicGeometry.opensDiagram_obj, AlgebraicGeometry.Scheme.toIso_inv_ι_assoc, AlgebraicGeometry.morphismRestrict_app', AlgebraicGeometry.opensCone_π_app, AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover_X, AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjMap_glueDataObjι, AlgebraicGeometry.Proj.homOfLE_toBasicOpenOfGlobalSections_ι_assoc, AlgebraicGeometry.IsSeparated.instResLE, toSpecΓ_SpecMap_appLE_assoc, AlgebraicGeometry.Etale.instResLE, ι_appTop, AlgebraicGeometry.Scheme.map_basicOpen, AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι, AlgebraicGeometry.Scheme.isoOfEq_hom_ι_assoc, AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec_assoc, AlgebraicGeometry.Scheme.isoOfEq_inv_ι_assoc, AlgebraicGeometry.Scheme.Hom.preimageIso_inv_ι_assoc, AlgebraicGeometry.Scheme.Hom.resLE_comp_resLE_assoc, AlgebraicGeometry.instLocallyOfFiniteTypeMorphismRestrict, AlgebraicGeometry.IsIntegralHom.instMorphismRestrict, AlgebraicGeometry.instIsOpenImmersionMorphismRestrict, ι_preimage_self, AlgebraicGeometry.instQuasiSeparatedMorphismRestrict, AlgebraicGeometry.HasAffineProperty.iff_of_iSup_eq_top, AlgebraicGeometry.Scheme.homOfLE_app, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_glueDataObjMap, AlgebraicGeometry.Scheme.isoOfEq_rfl, AlgebraicGeometry.IsAffineOpen.ι_basicOpen_preimage, AlgebraicGeometry.Flat.instResLE, AlgebraicGeometry.morphismRestrict_appTop, AlgebraicGeometry.Scheme.Hom.exists_mem_and_isIso_morphismRestrict_toNormalization, AlgebraicGeometry.instIsReducedToScheme_1, AlgebraicGeometry.Scheme.PartialMap.ofFromSpecStalk_comp, isoOfLE_inv_ι, AlgebraicGeometry.Scheme.Hom.ι_toNormalization_assoc, AlgebraicGeometry.IsLocalAtTarget.restrict, AlgebraicGeometry.Proj.fromOfGlobalSections_morphismRestrict, AlgebraicGeometry.Scheme.Hom.isoImage_inv_ι, AlgebraicGeometry.instLocallyQuasiFiniteResLE, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι, AlgebraicGeometry.Scheme.Hom.isoImage_inv_ι_assoc, AlgebraicGeometry.Scheme.ker_morphismRestrict_ideal, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι, AlgebraicGeometry.IsLocalAtTarget.iff_of_iSup_eq_top, AlgebraicGeometry.Proj.basicOpenToSpec_SpecMap_awayMap_assoc, AlgebraicGeometry.Scheme.IdealSheafData.instIsPreimmersionGlueDataObjι, AlgebraicGeometry.Scheme.PartialMap.restrict_hom, AlgebraicGeometry.IsLocalAtSource.resLE, AlgebraicGeometry.IsZariskiLocalAtSource.resLE, AlgebraicGeometry.instIsOpenImmersionHomOfLE, fromSpecStalkOfMem_toSpecΓ, toScheme_presheaf_map, AlgebraicGeometry.Scheme.topIso_hom, AlgebraicGeometry.Scheme.Hom.map_resLE, AlgebraicGeometry.basicOpenIsoSpecAway_inv_homOfLE_assoc, AlgebraicGeometry.Scheme.Hom.resLE_preimage, AlgebraicGeometry.Scheme.Hom.le_preimage_resLE_iff, AlgebraicGeometry.instIsClosedImmersionMorphismRestrict, AlgebraicGeometry.isPullback_morphismRestrict, AlgebraicGeometry.Scheme.Hom.resLE_comp_ι_assoc, AlgebraicGeometry.basicOpenIsoSpecAway_inv_homOfLE, AlgebraicGeometry.Scheme.Hom.map_resLE_assoc, AlgebraicGeometry.IsLocalIso.exists_isOpenImmersion, mem_basicOpen_toScheme, AlgebraicGeometry.noetherianSpace_of_isAffineOpen, AlgebraicGeometry.instSmoothMorphismRestrict, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_apply, ι_app_self, AlgebraicGeometry.Scheme.Hom.resLE_comp_ι, AlgebraicGeometry.Scheme.Hom.liftCoborder_ι_assoc, AlgebraicGeometry.exists_isFinite_morphismRestrict_of_finite_preimage_singleton, AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.to_basicOpen, range_ι, ι_image_basicOpen', AlgebraicGeometry.Scheme.Hom.isoOpensRange_inv_comp_assoc, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ_assoc, instIsOverι, ι_apply, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst_assoc, fromSpecStalkOfMem_toSpecΓ_assoc, AlgebraicGeometry.Scheme.PartialMap.isOver_iff, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_base_apply, AlgebraicGeometry.Scheme.OpenCover.restrict_I₀, AlgebraicGeometry.Proj.basicOpenIsoSpec_hom, AlgebraicGeometry.Scheme.homOfLE_base, AlgebraicGeometry.instGeometricallyIntegralMorphismRestrict, AlgebraicGeometry.Scheme.PartialMap.Opens.isDominant_ι, AlgebraicGeometry.Scheme.map_basicOpen_map, AlgebraicGeometry.affineOpensRestrict_symm_apply_coe, AlgebraicGeometry.IsAffineOpen.isLocalization_stalk', AlgebraicGeometry.Scheme.Hom.liftCoborder_ι, AlgebraicGeometry.Scheme.IsLocallyDirected.exists_of_pullback_V_V, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict, AlgebraicGeometry.spread_out_unique_of_isGermInjective, ι_image_le, AlgebraicGeometry.instIsLocallyArtinianToScheme, AlgebraicGeometry.IsZariskiLocalAtSource.iff_exists_resLE, AlgebraicGeometry.Scheme.Hom.resLE_comp_resLE, AlgebraicGeometry.IsLocalAtSource.iff_of_iSup_eq_top, ι_app, AlgebraicGeometry.Scheme.Hom.isoImage_hom_ι, AlgebraicGeometry.spread_out_unique_of_isGermInjective', AlgebraicGeometry.instUniversallyClosedMorphismRestrict, AlgebraicGeometry.Scheme.toIso_inv_ι, AlgebraicGeometry.instIsAffineToSchemeValOpensMemSetAffineOpens, AlgebraicGeometry.Scheme.homOfLE_ι_assoc, AlgebraicGeometry.IsPreimmersion.instMorphismRestrict, AlgebraicGeometry.exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimage, AlgebraicGeometry.IsSeparated.instMorphismRestrict, AlgebraicGeometry.Scheme.IdealSheafData.ker_glueDataObjι_appTop, AlgebraicGeometry.Proj.homOfLE_toBasicOpenOfGlobalSections_ι, AlgebraicGeometry.Scheme.restrictFunctor_obj_left, AlgebraicGeometry.instLocallyOfFinitePresentationMorphismRestrict, AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι_ι, instIsIsoCommRingCatAppLEιTopToScheme, AlgebraicGeometry.instIsOverHomOfLE, AlgebraicGeometry.Scheme.restrictFunctor_map_left, AlgebraicGeometry.morphismRestrict_app, ι_image_top, AlgebraicGeometry.IsAffineOpen.isoSpec_hom, AlgebraicGeometry.isPullback_opens_inf_le, AlgebraicGeometry.Scheme.IsLocallyDirected.t_id, AlgebraicGeometry.Scheme.Hom.isoImage_hom_ι_assoc, topIso_hom, AlgebraicGeometry.Scheme.PartialMap.compHom_hom, AlgebraicGeometry.spread_out_of_isGermInjective, AlgebraicGeometry.Scheme.IsLocallyDirected.homOfLE_tAux_assoc, AlgebraicGeometry.Scheme.OpenCover.restrict_X, toSpecΓ_SpecMap_appLE, AlgebraicGeometry.sourceAffineLocally_morphismRestrict, AlgebraicGeometry.Etale.instMorphismRestrict, AlgebraicGeometry.instLocallyOfFiniteTypeResLE, AlgebraicGeometry.Scheme.Hom.le_resLE_preimage_iff, AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv_assoc, AlgebraicGeometry.coe_opensRestrict_apply_coe, AlgebraicGeometry.Scheme.Hom.isoOpensRange_inv_comp, toSpecΓ_preimage_zeroLocus, AlgebraicGeometry.Scheme.isoOfEq_hom, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_appTop, AlgebraicGeometry.spread_out_of_isGermInjective', ι_base_apply, AlgebraicGeometry.instIsAffineHomιBasicOpen, AlgebraicGeometry.Scheme.homOfLE_apply, AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec, AlgebraicGeometry.Scheme.homOfLE_rfl, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι_assoc, AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec_inv_app, AlgebraicGeometry.isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange, AlgebraicGeometry.instLocallyOfFinitePresentationResLE, isoOfLE_inv_ι_assoc, AlgebraicGeometry.exists_etale_isCompl_of_quasiFiniteAt, AlgebraicGeometry.morphismRestrict_id
topIso 📖	CompOp	11 math math: AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop, topIso_inv, AlgebraicGeometry.Proj.basicOpenToSpec_app_top, ι_image_basicOpen_topIso_inv, toSpecΓ_appTop_assoc, toSpecΓ_appTop, AlgebraicGeometry.ΓSpecIso_obj_hom, AlgebraicGeometry.Scheme.map_basicOpen_map, AlgebraicGeometry.Scheme.IdealSheafData.ker_glueDataObjι_appTop, topIso_hom, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_appTop
ι 📖	CompOp	144 math math: ι_image_basicOpen, AlgebraicGeometry.Γ_map_morphismRestrict, AlgebraicGeometry.Proj.basicOpenIsoSpec_inv_ι_assoc, AlgebraicGeometry.instLocallyQuasiFiniteCompSchemeιQuasiFiniteLocus, toSpecΓ_SpecMap_presheaf_map_top, mem_ι_image_iff, AlgebraicGeometry.morphismRestrict_ι_assoc, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict_assoc, topIso_inv, AlgebraicGeometry.instIsDominantιCoborderRange, AlgebraicGeometry.image_morphismRestrict_preimage, AlgebraicGeometry.Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp, AlgebraicGeometry.Scheme.ι_toIso_inv, AlgebraicGeometry.isPullback_opens_inf, AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι_assoc, AlgebraicGeometry.Scheme.isoOfEq_inv_ι, stalkIso_inv, AlgebraicGeometry.sourceLocalClosure.iff_forall_exists, AlgebraicGeometry.Scheme.ι_toIso_inv_assoc, AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_ker_glueDataObjι, isoOfLE_hom_ι_assoc, AlgebraicGeometry.Scheme.isoOfEq_hom_ι, AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_iSup_eq_top, AlgebraicGeometry.Scheme.homOfLE_ι, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι_eq_support_inter, AlgebraicGeometry.Scheme.Hom.ι_toNormalization, germ_stalkIso_inv, opensRange_ι, AlgebraicGeometry.IsAffineOpen.isoSpec_inv, fromSpecStalkOfMem_ι_assoc, AlgebraicGeometry.Scheme.directedAffineCover_f, AlgebraicGeometry.IsImmersion.isPullback_toImage_liftCoborder, AlgebraicGeometry.Scheme.opensRange_homOfLE, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι, ι_image_basicOpen_topIso_inv, AlgebraicGeometry.Scheme.ι_image_homOfLE_le_ι_image, AlgebraicGeometry.coe_opensRestrict_symm_apply, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst, toScheme_presheaf_obj, AlgebraicGeometry.Scheme.openCoverOfIsOpenCover_f, AlgebraicGeometry.Scheme.PartialMap.equiv_toPartialMap_iff_of_isSeparated, AlgebraicGeometry.Scheme.IdealSheafData.subschemeCover_map_subschemeι, toSpecΓ_SpecMap_presheaf_map_top_assoc, AlgebraicGeometry.liftCoborder_app, toSpecΓ_preimage_basicOpen, AlgebraicGeometry.Proj.basicOpenIsoSpec_inv_ι, AlgebraicGeometry.Scheme.Hom.isoOpensRange_hom_ι_assoc, AlgebraicGeometry.morphismRestrict_appLE, AlgebraicGeometry.Scheme.Hom.isoOpensRange_hom_ι, AlgebraicGeometry.morphismRestrict_ι, AlgebraicGeometry.Scheme.Hom.preimageIso_inv_ι, germ_stalkIso_inv_assoc, AlgebraicGeometry.opensDiagramι_app, AlgebraicGeometry.instIsOpenImmersionCompSchemeιQuasiFiniteLocusToNormalization, toSpecΓ_top, AlgebraicGeometry.Scheme.Hom.liftCoborder_preimage, germ_stalkIso_hom, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι_assoc, AlgebraicGeometry.affineOpensRestrict_apply_coe_coe, ι_appIso, instIsOpenImmersionι, AlgebraicGeometry.Scheme.homOfLE_appTop, AlgebraicGeometry.isLocalIso_iff, isoOfLE_hom_ι, over_def, fromSpecStalkOfMem_ι, AlgebraicGeometry.Scheme.toIso_inv_ι_assoc, AlgebraicGeometry.morphismRestrict_app', AlgebraicGeometry.Proj.homOfLE_toBasicOpenOfGlobalSections_ι_assoc, ι_appTop, AlgebraicGeometry.Scheme.map_basicOpen, AlgebraicGeometry.Scheme.Hom.preimageIso_hom_ι, AlgebraicGeometry.Scheme.isoOfEq_hom_ι_assoc, AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec_assoc, AlgebraicGeometry.Scheme.isoOfEq_inv_ι_assoc, AlgebraicGeometry.Scheme.Hom.preimageIso_inv_ι_assoc, AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover_f, ι_preimage_self, AlgebraicGeometry.Scheme.homOfLE_app, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_glueDataObjMap, AlgebraicGeometry.Scheme.homOfLE_appLE, AlgebraicGeometry.IsAffineOpen.ι_basicOpen_preimage, AlgebraicGeometry.morphismRestrict_appTop, AlgebraicGeometry.Scheme.PartialMap.ofFromSpecStalk_comp, isoOfLE_inv_ι, AlgebraicGeometry.Scheme.Hom.ι_toNormalization_assoc, AlgebraicGeometry.Scheme.Hom.isoImage_inv_ι, AlgebraicGeometry.Scheme.Hom.isoImage_inv_ι_assoc, AlgebraicGeometry.Scheme.ker_morphismRestrict_ideal, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι, germ_stalkIso_hom_assoc, toScheme_presheaf_map, AlgebraicGeometry.Scheme.topIso_hom, AlgebraicGeometry.Scheme.Hom.resLE_preimage, AlgebraicGeometry.Scheme.Hom.le_preimage_resLE_iff, AlgebraicGeometry.isPullback_morphismRestrict, AlgebraicGeometry.Scheme.Hom.resLE_comp_ι_assoc, AlgebraicGeometry.IsLocalIso.exists_isOpenImmersion, ι_app_self, AlgebraicGeometry.Scheme.Hom.resLE_comp_ι, AlgebraicGeometry.Scheme.Hom.liftCoborder_ι_assoc, range_ι, ι_image_basicOpen', AlgebraicGeometry.Scheme.Hom.isoOpensRange_inv_comp_assoc, instIsOverι, ι_apply, AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst_assoc, AlgebraicGeometry.Scheme.PartialMap.isOver_iff, AlgebraicGeometry.Scheme.PartialMap.Opens.isDominant_ι, AlgebraicGeometry.Scheme.map_basicOpen_map, AlgebraicGeometry.affineOpensRestrict_symm_apply_coe, AlgebraicGeometry.Scheme.Hom.liftCoborder_ι, AlgebraicGeometry.Scheme.IsLocallyDirected.exists_of_pullback_V_V, AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict, AlgebraicGeometry.spread_out_unique_of_isGermInjective, ι_image_le, AlgebraicGeometry.Scheme.Hom.resLE_appLE, AlgebraicGeometry.IsLocalAtSource.iff_of_iSup_eq_top, ι_app, AlgebraicGeometry.Scheme.Hom.isoImage_hom_ι, AlgebraicGeometry.spread_out_unique_of_isGermInjective', AlgebraicGeometry.Scheme.toIso_inv_ι, AlgebraicGeometry.Scheme.homOfLE_ι_assoc, AlgebraicGeometry.Proj.homOfLE_toBasicOpenOfGlobalSections_ι, AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι_ι, instIsIsoCommRingCatAppLEιTopToScheme, AlgebraicGeometry.Scheme.restrictFunctor_map_left, AlgebraicGeometry.morphismRestrict_app, ι_image_top, AlgebraicGeometry.Scheme.Hom.isoImage_hom_ι_assoc, topIso_hom, AlgebraicGeometry.spread_out_of_isGermInjective, AlgebraicGeometry.Scheme.openCoverBasicOpenTop_f, AlgebraicGeometry.Scheme.Hom.le_resLE_preimage_iff, AlgebraicGeometry.Scheme.Hom.isoOpensRange_inv_comp, AlgebraicGeometry.Scheme.restrictFunctor_obj_hom, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι, AlgebraicGeometry.spread_out_of_isGermInjective', ι_base_apply, AlgebraicGeometry.instIsAffineHomιBasicOpen, AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι_assoc, isoOfLE_inv_ι_assoc, AlgebraicGeometry.exists_etale_isCompl_of_quasiFiniteAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_presheaf_map_eqToHom 📖	mathematical	CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens toScheme 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 ι instIsOpenImmersionι	CategoryTheory.Functor.map Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat Topology.IsOpenEmbedding.functor_obj_injective TopologicalSpace.Opens.inclusion' TopologicalSpace.Opens.isOpenEmbedding	—	instIsOpenImmersionι
exists_toScheme 📖	mathematical	—	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike	—	—
forall_toScheme 📖	mathematical	—	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike	—	—
germ_stalkIso_hom 📖	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 toScheme	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat TopCat.Presheaf.germ CategoryTheory.Iso.hom stalkIso AlgebraicGeometry.Scheme.Hom.opensFunctor ι instIsOpenImmersionι Set Set.instMembership SetLike.coe DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom AlgebraicGeometry.Scheme.Hom.toLRSHom	—	AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ CommRingCat.Colimits.hasColimits_commRingCat TopologicalSpace.Opens.isOpenEmbedding
germ_stalkIso_hom_assoc 📖	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 toScheme	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat TopCat.Presheaf.germ CategoryTheory.Iso.hom stalkIso AlgebraicGeometry.Scheme.Hom.opensFunctor ι instIsOpenImmersionι Set Set.instMembership SetLike.coe DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom AlgebraicGeometry.Scheme.Hom.toLRSHom	—	CommRingCat.Colimits.hasColimits_commRingCat instIsOpenImmersionι CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' germ_stalkIso_hom
germ_stalkIso_inv 📖	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 toScheme	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Hom.opensFunctor ι instIsOpenImmersionι TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat TopCat.Presheaf.germ Set Set.instMembership SetLike.coe DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom AlgebraicGeometry.Scheme.Hom.toLRSHom CategoryTheory.Iso.inv stalkIso	—	AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ CommRingCat.Colimits.hasColimits_commRingCat TopologicalSpace.Opens.isOpenEmbedding
germ_stalkIso_inv_assoc 📖	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 toScheme	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Hom.opensFunctor ι instIsOpenImmersionι TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat TopCat.Presheaf.germ Set Set.instMembership SetLike.coe DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom AlgebraicGeometry.Scheme.Hom.toLRSHom CategoryTheory.Iso.inv stalkIso	—	CommRingCat.Colimits.hasColimits_commRingCat instIsOpenImmersionι CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' germ_stalkIso_inv
instIsIsoCommRingCatAppLEιTopToScheme 📖	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 toScheme Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder AlgebraicGeometry.Scheme.Hom.appLE ι Eq.ge TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' ι_preimage_self	—	Eq.ge ι_preimage_self AlgebraicGeometry.IsOpenImmersion.ofRestrict AlgebraicGeometry.Scheme.ofRestrict_appLE instIsOpenImmersionι ι_image_top CategoryTheory.Functor.map_isIso CategoryTheory.isIso_op CategoryTheory.Iso.isIso_hom
instIsOpenImmersionι 📖	mathematical	—	AlgebraicGeometry.IsOpenImmersion toScheme ι	—	AlgebraicGeometry.IsOpenImmersion.ofRestrict
instIsOverι 📖	mathematical	—	AlgebraicGeometry.Scheme.Hom.IsOver toScheme ι CategoryTheory.CanonicallyOverClass.toOverClass AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory instCanonicallyOverToScheme CategoryTheory.instOverClass	—	CategoryTheory.Category.comp_id
isoOfLE_hom_ι 📖	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.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory toScheme CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' ι CategoryTheory.Iso.hom isoOfLE	—	AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac instIsOpenImmersionι
isoOfLE_hom_ι_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.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory toScheme CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' ι CategoryTheory.Iso.hom isoOfLE	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoOfLE_hom_ι
isoOfLE_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.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory toScheme CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' ι CategoryTheory.Iso.inv isoOfLE	—	AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac instIsOpenImmersionι
isoOfLE_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.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory toScheme CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' ι CategoryTheory.Iso.inv isoOfLE	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoOfLE_inv_ι
mem_basicOpen_toScheme 📖	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 toScheme AlgebraicGeometry.Scheme.basicOpen CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat IsOpenMap.functor TopologicalSpace.Opens.inclusion' Opposite.unop Opposite.op	—	instIsOpenImmersionι AlgebraicGeometry.Scheme.Hom.preimage_image_eq AlgebraicGeometry.Scheme.basicOpen_res_eq CategoryTheory.isIso_op CategoryTheory.instIsIsoEqToHom AlgebraicGeometry.Scheme.Hom.preimage_basicOpen
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 toScheme Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.Scheme.Hom.opensFunctor ι instIsOpenImmersionι	—	AlgebraicGeometry.Scheme.Hom.apply_mem_image_iff instIsOpenImmersionι
nonempty_iff 📖	mathematical	—	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace toScheme Set.Nonempty SetLike.coe AlgebraicGeometry.Scheme.Opens TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	—	—
opensRange_ι 📖	mathematical	—	AlgebraicGeometry.Scheme.Hom.opensRange toScheme ι instIsOpenImmersionι	—	TopologicalSpace.Opens.ext instIsOpenImmersionι Subtype.range_val
over_def 📖	mathematical	—	CategoryTheory.over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory toScheme CategoryTheory.OverClass CategoryTheory.CanonicallyOverClass.toOverClass instCanonicallyOverToScheme ι	—	—
range_ι 📖	mathematical	—	Set.range TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace toScheme 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' ι SetLike.coe AlgebraicGeometry.Scheme.Opens TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	—	Subtype.range_val
stalkIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CommRingCat CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace toScheme AlgebraicGeometry.PresheafedSpace.presheaf TopCat.carrier AlgebraicGeometry.Scheme.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier stalkIso AlgebraicGeometry.Scheme.Hom.stalkMap ι	—	CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Category.comp_id CategoryTheory.Iso.inv_comp_eq TopCat.Presheaf.stalk_hom_ext instIsOpenImmersionι germ_stalkIso_hom_assoc Eq.le Set.preimage_image_eq Subtype.val_injective TopCat.Presheaf.germ_res AlgebraicGeometry.Scheme.Hom.germ_stalkMap
toScheme_carrier 📖	mathematical	—	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace toScheme Set.Elem SetLike.coe AlgebraicGeometry.Scheme.Opens TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	—	—
toScheme_presheaf_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace toScheme TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens CategoryTheory.Functor.obj AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.Scheme.Hom.opensFunctor ι instIsOpenImmersionι Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom.unop	—	—
toScheme_presheaf_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace toScheme 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 ι instIsOpenImmersionι	—	—
topIso_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 toScheme TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder topIso CategoryTheory.Functor.map TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat IsOpenMap.functor TopologicalSpace.Opens.inclusion' Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.Hom.opensFunctor ι instIsOpenImmersionι CategoryTheory.eqToHom	—	—
topIso_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 toScheme TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder topIso CategoryTheory.Functor.map TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat IsOpenMap.functor TopologicalSpace.Opens.inclusion' Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.Hom.opensFunctor ι instIsOpenImmersionι CategoryTheory.eqToHom	—	—
ι_app 📖	mathematical	—	AlgebraicGeometry.Scheme.Hom.app toScheme ι CategoryTheory.Functor.map 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 CategoryTheory.Functor.obj AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.Scheme.Hom.opensFunctor instIsOpenImmersionι TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.homOfLE Set.image_preimage_subset DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	—	—
ι_appIso 📖	mathematical	—	AlgebraicGeometry.Scheme.Hom.appIso toScheme ι instIsOpenImmersionι CategoryTheory.Iso.refl 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 AlgebraicGeometry.Scheme.Hom.opensFunctor	—	AlgebraicGeometry.Scheme.ofRestrict_appIso
ι_appLE 📖	mathematical	AlgebraicGeometry.Scheme.Opens toScheme 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 AlgebraicGeometry.Scheme.Hom.toLRSHom' ι	AlgebraicGeometry.Scheme.Hom.appLE CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Hom.opensFunctor instIsOpenImmersionι Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.homOfLE Set Set.instHasSubset Set.image DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom AlgebraicGeometry.Scheme.Hom.toLRSHom SetLike.coe TopologicalSpace.Opens.instSetLike Set.preimage Set.image_subset_iff	—	instIsOpenImmersionι Set.image_subset_iff Set.image_preimage_subset AlgebraicGeometry.Scheme.Hom.image_mono
ι_appTop 📖	mathematical	—	AlgebraicGeometry.Scheme.Hom.appTop toScheme ι CategoryTheory.Functor.map 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 Top.top OrderTop.toTop Preorder.toLE AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder TopologicalSpace.Opens.instCompleteLattice CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Hom.opensFunctor instIsOpenImmersionι SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.homOfLE le_top	—	—
ι_app_self 📖	mathematical	—	AlgebraicGeometry.Scheme.Hom.app toScheme ι CategoryTheory.Functor.map 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 CategoryTheory.Functor.obj AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.Scheme.Hom.opensFunctor instIsOpenImmersionι Opposite.unop TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom	—	—
ι_apply 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace toScheme 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.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	—	—
ι_base_apply 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace toScheme 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.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	—	ι_apply
ι_image_basicOpen 📖	mathematical	—	CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens toScheme 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 ι instIsOpenImmersionι AlgebraicGeometry.Scheme.basicOpen Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder TopologicalSpace.Opens TopCat.str TopCat TopCat.instCategory TopologicalSpace.Opens.toTopCat IsOpenMap.functor TopologicalSpace.Opens.inclusion' Opposite.unop Opposite.op	—	instIsOpenImmersionι ι_image_top ι_image_basicOpen' AlgebraicGeometry.Scheme.basicOpen_res_eq CategoryTheory.isIso_op CategoryTheory.instIsIsoEqToHom
ι_image_basicOpen' 📖	mathematical	—	CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens toScheme 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 ι instIsOpenImmersionι AlgebraicGeometry.Scheme.basicOpen Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder 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.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom ι_image_top	—	TopologicalSpace.Opens.isOpenEmbedding AlgebraicGeometry.IsOpenImmersion.ofRestrict instIsOpenImmersionι ι_image_top AlgebraicGeometry.Scheme.image_basicOpen Topology.IsOpenEmbedding.isOpenMap TopologicalSpace.Opens.isOpenEmbedding_obj_top AlgebraicGeometry.Scheme.basicOpen_res_eq CategoryTheory.isIso_op CategoryTheory.instIsIsoEqToHom CommRingCat.comp_apply CategoryTheory.Functor.map_comp CategoryTheory.op_comp CategoryTheory.eqToHom_trans CategoryTheory.eqToHom_refl CategoryTheory.op_id AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict_invApp CategoryTheory.Functor.map_id
ι_image_basicOpen_topIso_inv 📖	mathematical	—	CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens toScheme 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 ι instIsOpenImmersionι AlgebraicGeometry.Scheme.basicOpen Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder 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 topIso	—	instIsOpenImmersionι ι_image_top ι_image_basicOpen' AlgebraicGeometry.Scheme.basicOpen_res_eq CategoryTheory.isIso_op CategoryTheory.instIsIsoEqToHom topIso_inv
ι_image_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 toScheme Preorder.smallCategory AlgebraicGeometry.Scheme.Hom.opensFunctor ι instIsOpenImmersionι	—	instIsOpenImmersionι ι_image_top AlgebraicGeometry.Scheme.Hom.image_mono le_top
ι_image_top 📖	mathematical	—	CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens toScheme 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 ι instIsOpenImmersionι Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	TopologicalSpace.Opens.isOpenEmbedding_obj_top
ι_preimage_self 📖	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 toScheme TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' ι Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	TopologicalSpace.Opens.inclusion'_map_eq_top

---

← Back to Index