OpenImmersion

📁 Source: Mathlib/Geometry/RingedSpace/OpenImmersion.lean

Statistics

Metric	Count
Definitions IsOpenImmersion, invApp, isoRestrict, opensFunctor, pullbackConeOfLeft, pullbackConeOfLeftIsLimit, IsOpenImmersion, invApp, isoOfRangeEq, isoRestrict, opensFunctor, pullbackConeOfLeft, pullbackConeOfLeftFst, pullbackConeOfLeftIsLimit, pullbackConeOfLeftLift, toLocallyRingedSpace, toLocallyRingedSpaceHom, toSheafedSpace, toSheafedSpaceHom, IsOpenImmersion, forgetCreatesPullbackOfLeft, forgetCreatesPullbackOfRight, invApp, isoRestrict, opensFunctor	25
Theorems app_invApp, app_invApp_assoc, app_inv_app', app_inv_app'_assoc, comp, forgetToPresheafedSpacePreservesOpenImmersion, forgetToPresheafedSpace_preservesPullback_of_left, forgetToPresheafedSpace_preservesPullback_of_right, forgetToPresheafedSpace_reflectsPullback_of_left, forgetToPresheafedSpace_reflectsPullback_of_right, forgetToTop_preservesPullback_of_left, forget_preservesPullbackOfLeft, forget_preservesPullback_of_right, forget_reflectsPullback_of_left, forget_reflectsPullback_of_right, hasPullback_of_left, hasPullback_of_right, instIsIsoCommRingCatInvApp, instIsOpenImmersionCommRingCatMapSheafedSpaceForgetToSheafedSpace, instOfRestrict, instSndPullbackConeOfLeft, invApp_app, invApp_app_apply, invApp_app_assoc, inv_invApp, inv_naturality, inv_naturality_assoc, isoRestrict_hom_ofRestrict, isoRestrict_hom_ofRestrict_assoc, isoRestrict_inv_ofRestrict, isoRestrict_inv_ofRestrict_assoc, lift_fac, lift_fac_assoc, lift_range, lift_uniq, mono, ofRestrict, ofRestrict_invApp, ofRestrict_invApp_apply, of_isIso, of_stalk_iso, pullback_fst_of_right, pullback_snd_isIso_of_range_subset, pullback_snd_of_left, pullback_to_base_isOpenImmersion, stalk_iso, to_iso, app_invApp, app_invApp_assoc, app_inv_app', app_inv_app'_assoc, base_open, c_iso, c_iso', comp, forget_preservesLimitsOfLeft, forget_preservesLimitsOfRight, hasPullback_of_left, hasPullback_of_right, instIsIsoInvApp, invApp_app, invApp_app_apply, invApp_app_assoc, inv_invApp, inv_naturality, inv_naturality_assoc, isIso_of_subset, isoOfRangeEq_hom, isoOfRangeEq_inv, isoRestrict_hom_c_app, isoRestrict_hom_ofRestrict, isoRestrict_hom_ofRestrict_assoc, isoRestrict_inv_ofRestrict, isoRestrict_inv_ofRestrict_assoc, lift_fac, lift_fac_assoc, lift_uniq, locallyRingedSpace_toLocallyRingedSpace, mono, ofIsIso, ofIso, ofRestrict, ofRestrict_invApp, ofRestrict_invApp_apply, pullbackConeOfLeftLift_fst, pullbackConeOfLeftLift_snd, pullbackConeSndIsOpenImmersion, pullbackFstOfRight, pullbackSndOfLeft, pullbackToBaseIsOpenImmersion, pullback_cone_of_left_condition, pullback_snd_isIso_of_range_subset, sheafedSpace_toSheafedSpace, stalk_iso, toLocallyRingedSpaceHom_val, toLocallyRingedSpace_isOpenImmersion, toLocallyRingedSpace_toSheafedSpace, toSheafedSpaceHom_base, toSheafedSpaceHom_c, toSheafedSpaceHom_hom_base, toSheafedSpaceHom_hom_c, toSheafedSpace_isOpenImmersion, toSheafedSpace_toPresheafedSpace, to_iso, app_invApp, app_invApp_assoc, app_inv_app', app_inv_app'_assoc, comp, forgetMapIsOpenImmersion, hasLimit_cospan_forget_of_left, hasLimit_cospan_forget_of_left', hasLimit_cospan_forget_of_right, hasLimit_cospan_forget_of_right', image_preimage_is_empty, instIsIsoInvApp, instMono, invApp_app, invApp_app_apply, invApp_app_assoc, inv_invApp, inv_naturality, inv_naturality_assoc, isoRestrict_hom_hom_c_app, isoRestrict_hom_ofRestrict, isoRestrict_hom_ofRestrict_assoc, isoRestrict_inv_ofRestrict, isoRestrict_inv_ofRestrict_assoc, ofRestrict, ofRestrict_invApp, ofRestrict_invApp_apply, of_isIso, of_stalk_iso, sheafedSpace_forgetPreserves_of_left, sheafedSpace_forgetPreserves_of_right, sheafedSpace_hasPullback_of_left, sheafedSpace_hasPullback_of_right, sheafedSpace_pullback_fst_of_right, sheafedSpace_pullback_snd_of_left, sheafedSpace_pullback_to_base_isOpenImmersion, sigma_ι_isOpenEmbedding, sigma_ι_isOpenImmersion, sigma_ι_isOpenImmersion_aux, stalk_iso, to_iso, isOpenImmersion_iff_hom, instIsOpenImmersionCommRingCatOfIsOpenImmersion	147
Total	172

AlgebraicGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsOpenImmersionCommRingCatOfIsOpenImmersion 📖	mathematical	—	PresheafedSpace.IsOpenImmersion CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace LocallyRingedSpace.Hom.toHom	—	—

AlgebraicGeometry.LocallyRingedSpace

Definitions

Name	Category	Theorems
IsOpenImmersion 📖	MathDef	15 math math: GlueData.ι_isOpenImmersion, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionιLocallyRingedSpaceToLocallyRingedSpaceGlueData, IsOpenImmersion.comp, IsOpenImmersion.ofRestrict, IsOpenImmersion.pullback_snd_of_left, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace_isOpenImmersion, IsOpenImmersion.of_stalk_iso, IsOpenImmersion.pullback_to_base_isOpenImmersion, IsOpenImmersion.of_isIso, AlgebraicGeometry.IsOpenImmersion.instIsOpenImmersionMapSchemeLocallyRingedSpaceForgetToLocallyRingedSpace, GlueData.f_open, IsOpenImmersion.pullback_fst_of_right, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionFLocallyRingedSpaceToLocallyRingedSpaceGlueData, IsOpenImmersion.instOfRestrict, IsOpenImmersion.instSndPullbackConeOfLeft

AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion

Definitions

Name	Category	Theorems
invApp 📖	CompOp	13 math math: inv_naturality, invApp_app_apply, inv_naturality_assoc, inv_invApp, invApp_app, app_invApp_assoc, app_invApp, instIsIsoCommRingCatInvApp, invApp_app_assoc, ofRestrict_invApp, app_inv_app', app_inv_app'_assoc, ofRestrict_invApp_apply
isoRestrict 📖	CompOp	4 math math: isoRestrict_inv_ofRestrict_assoc, isoRestrict_hom_ofRestrict, isoRestrict_hom_ofRestrict_assoc, isoRestrict_inv_ofRestrict
opensFunctor 📖	CompOp	12 math math: inv_naturality, invApp_app_apply, inv_naturality_assoc, inv_invApp, invApp_app, app_invApp_assoc, app_invApp, instIsIsoCommRingCatInvApp, invApp_app_assoc, app_inv_app', app_inv_app'_assoc, ofRestrict_invApp_apply
pullbackConeOfLeft 📖	CompOp	1 math math: instSndPullbackConeOfLeft
pullbackConeOfLeftIsLimit 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
app_invApp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.LocallyRingedSpace.toTopCat opensFunctor TopologicalSpace.Opens.map CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c invApp CategoryTheory.Functor.map Quiver.Hom.op Set CategoryTheory.CategoryStruct.toQuiver OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.image DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier Set.preimage TopologicalSpace.Opens.carrier CategoryTheory.homOfLE Set.image_preimage_subset	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp AlgebraicGeometry.instIsOpenImmersionCommRingCatOfIsOpenImmersion
app_invApp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c AlgebraicGeometry.LocallyRingedSpace.toTopCat opensFunctor TopologicalSpace.Opens.map invApp CategoryTheory.Functor.map Quiver.Hom.op Set CategoryTheory.CategoryStruct.toQuiver OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.image DFunLike.coe ContinuousMap ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory TopCat.instConcreteCategoryContinuousMapCarrier Set.preimage TopologicalSpace.Opens.carrier CategoryTheory.homOfLE Set.image_preimage_subset	—	Set.image_preimage_subset CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' app_invApp
app_inv_app' 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.LocallyRingedSpace.toTopCat Set.instHasSubset SetLike.coe TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.instSetLike Set.range AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward opensFunctor TopologicalSpace.Opens.map CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c invApp CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.image Set.preimage TopologicalSpace.Opens.carrier CategoryTheory.eqToHom le_antisymm Set.image_preimage_subset Set.instInter Preorder.toLE Set.subset_inter_iff Set.image_preimage_eq_inter_range	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp AlgebraicGeometry.instIsOpenImmersionCommRingCatOfIsOpenImmersion
app_inv_app'_assoc 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.LocallyRingedSpace.toTopCat Set.instHasSubset SetLike.coe TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.instSetLike Set.range AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c opensFunctor TopologicalSpace.Opens.map invApp CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.image Set.preimage TopologicalSpace.Opens.carrier CategoryTheory.eqToHom le_antisymm Set.image_preimage_subset Set.instInter Preorder.toLE Set.subset_inter_iff Set.image_preimage_eq_inter_range	—	le_antisymm Set.image_preimage_subset Set.subset_inter_iff Set.image_preimage_eq_inter_range CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' app_inv_app'
comp 📖	mathematical	—	AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion CategoryTheory.CategoryStruct.comp AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.LocallyRingedSpace.instCategory	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.comp AlgebraicGeometry.instIsOpenImmersionCommRingCatOfIsOpenImmersion
forgetToPresheafedSpacePreservesOpenImmersion 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CommRingCat CommRingCat.instCategory CategoryTheory.Functor.obj AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Functor.comp AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace CategoryTheory.Functor.map	—	—
forgetToPresheafedSpace_preservesPullback_of_left 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.PresheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Functor.comp AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace	—	CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone AlgebraicGeometry.instIsOpenImmersionCommRingCatOfIsOpenImmersion
forgetToPresheafedSpace_preservesPullback_of_right 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.PresheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Functor.comp AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace	—	CategoryTheory.Limits.preservesPullback_symmetry forgetToPresheafedSpace_preservesPullback_of_left
forgetToPresheafedSpace_reflectsPullback_of_left 📖	mathematical	—	CategoryTheory.Limits.ReflectsLimit AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.PresheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Functor.comp AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace	—	CategoryTheory.Limits.reflectsLimit_of_reflectsIsomorphisms CategoryTheory.reflectsIsomorphisms_comp AlgebraicGeometry.LocallyRingedSpace.instReflectsIsomorphismsSheafedSpaceCommRingCatForgetToSheafedSpace CategoryTheory.reflectsIsomorphisms_of_full_and_faithful AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_full AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_faithful hasPullback_of_left forgetToPresheafedSpace_preservesPullback_of_left
forgetToPresheafedSpace_reflectsPullback_of_right 📖	mathematical	—	CategoryTheory.Limits.ReflectsLimit AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.PresheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Functor.comp AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace	—	CategoryTheory.Limits.reflectsLimit_of_reflectsIsomorphisms CategoryTheory.reflectsIsomorphisms_comp AlgebraicGeometry.LocallyRingedSpace.instReflectsIsomorphismsSheafedSpaceCommRingCatForgetToSheafedSpace CategoryTheory.reflectsIsomorphisms_of_full_and_faithful AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_full AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_faithful hasPullback_of_right forgetToPresheafedSpace_preservesPullback_of_right
forgetToTop_preservesPullback_of_left 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory TopCat TopCat.instCategory CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Functor.comp AlgebraicGeometry.SheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace AlgebraicGeometry.SheafedSpace.forget	—	CategoryTheory.Limits.comp_preservesLimit forgetToPresheafedSpace_preservesPullback_of_left CategoryTheory.Limits.preservesLimit_of_iso_diagram AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.forget_preservesLimitsOfLeft AlgebraicGeometry.instIsOpenImmersionCommRingCatOfIsOpenImmersion
forget_preservesPullbackOfLeft 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.SheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.instCategory CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace	—	CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone AlgebraicGeometry.instIsOpenImmersionCommRingCatOfIsOpenImmersion CategoryTheory.CreatesLimit.toReflectsLimit instIsOpenImmersionCommRingCatMapSheafedSpaceForgetToSheafedSpace
forget_preservesPullback_of_right 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.SheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.instCategory CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace	—	CategoryTheory.Limits.preservesPullback_symmetry forget_preservesPullbackOfLeft
forget_reflectsPullback_of_left 📖	mathematical	—	CategoryTheory.Limits.ReflectsLimit AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.SheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.instCategory CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace	—	CategoryTheory.Limits.reflectsLimit_of_reflectsIsomorphisms AlgebraicGeometry.LocallyRingedSpace.instReflectsIsomorphismsSheafedSpaceCommRingCatForgetToSheafedSpace hasPullback_of_left forget_preservesPullbackOfLeft
forget_reflectsPullback_of_right 📖	mathematical	—	CategoryTheory.Limits.ReflectsLimit AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.SheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.instCategory CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace	—	CategoryTheory.Limits.reflectsLimit_of_reflectsIsomorphisms AlgebraicGeometry.LocallyRingedSpace.instReflectsIsomorphismsSheafedSpaceCommRingCatForgetToSheafedSpace hasPullback_of_right forget_preservesPullback_of_right
hasPullback_of_left 📖	mathematical	—	CategoryTheory.Limits.HasPullback AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory	—	—
hasPullback_of_right 📖	mathematical	—	CategoryTheory.Limits.HasPullback AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory	—	CategoryTheory.Limits.hasPullback_symmetry hasPullback_of_left
instIsIsoCommRingCatInvApp 📖	mathematical	—	CategoryTheory.IsIso CommRingCat CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.LocallyRingedSpace.toTopCat opensFunctor invApp	—	AlgebraicGeometry.instIsOpenImmersionCommRingCatOfIsOpenImmersion AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.instIsIsoInvApp
instIsOpenImmersionCommRingCatMapSheafedSpaceForgetToSheafedSpace 📖	mathematical	—	AlgebraicGeometry.SheafedSpace.IsOpenImmersion CommRingCat CommRingCat.instCategory CategoryTheory.Functor.obj AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace CategoryTheory.Functor.map	—	—
instOfRestrict 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier AlgebraicGeometry.LocallyRingedSpace.toTopCat TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion AlgebraicGeometry.LocallyRingedSpace.restrict AlgebraicGeometry.LocallyRingedSpace.ofRestrict	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict
instSndPullbackConeOfLeft 📖	mathematical	—	AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory CategoryTheory.Limits.cospan pullbackConeOfLeft CategoryTheory.Limits.PullbackCone.snd	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict
invApp_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.LocallyRingedSpace.toTopCat opensFunctor TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom invApp CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c CategoryTheory.Functor.map CategoryTheory.Functor.op TopologicalSpace.Opens.map CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app AlgebraicGeometry.instIsOpenImmersionCommRingCatOfIsOpenImmersion
invApp_app_apply 📖	mathematical	—	DFunLike.coe RingHom CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.LocallyRingedSpace.toTopCat opensFunctor TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CategoryTheory.ConcreteCategory.hom CommRingCat.instConcreteCategoryRingHomCarrier CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c invApp CategoryTheory.Functor.map CategoryTheory.Functor.op TopologicalSpace.Opens.map CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise invApp_app
invApp_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.LocallyRingedSpace.toTopCat opensFunctor invApp TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c CategoryTheory.Functor.map CategoryTheory.Functor.op TopologicalSpace.Opens.map CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' invApp_app
inv_invApp 📖	mathematical	—	CategoryTheory.inv CommRingCat CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.LocallyRingedSpace.toTopCat opensFunctor invApp instIsIsoCommRingCatInvApp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c CategoryTheory.Functor.map CategoryTheory.Functor.op TopologicalSpace.Opens.map CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_invApp AlgebraicGeometry.instIsOpenImmersionCommRingCatOfIsOpenImmersion
inv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.LocallyRingedSpace.toTopCat opensFunctor Opposite.unop CategoryTheory.Functor.map invApp CategoryTheory.Functor.op	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_naturality AlgebraicGeometry.instIsOpenImmersionCommRingCatOfIsOpenImmersion
inv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Functor.map Opposite.op AlgebraicGeometry.LocallyRingedSpace.toTopCat opensFunctor Opposite.unop invApp CategoryTheory.Functor.op	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inv_naturality
isoRestrict_hom_ofRestrict 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.LocallyRingedSpace.restrict AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open CategoryTheory.Iso.hom isoRestrict AlgebraicGeometry.LocallyRingedSpace.ofRestrict	—	CategoryTheory.Functor.map_injective AlgebraicGeometry.LocallyRingedSpace.instFaithfulSheafedSpaceCommRingCatForgetToSheafedSpace AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict
isoRestrict_hom_ofRestrict_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.LocallyRingedSpace.restrict AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open CategoryTheory.Iso.hom isoRestrict AlgebraicGeometry.LocallyRingedSpace.ofRestrict	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoRestrict_hom_ofRestrict
isoRestrict_inv_ofRestrict 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.LocallyRingedSpace.restrict AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open CategoryTheory.Iso.inv isoRestrict AlgebraicGeometry.LocallyRingedSpace.ofRestrict	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open isoRestrict_hom_ofRestrict CategoryTheory.Iso.inv_hom_id_assoc
isoRestrict_inv_ofRestrict_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.LocallyRingedSpace.restrict AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open CategoryTheory.Iso.inv isoRestrict AlgebraicGeometry.LocallyRingedSpace.ofRestrict	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoRestrict_inv_ofRestrict
lift_fac 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace Set.instHasSubset Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.LocallyRingedSpace.instCategory lift	—	hasPullback_of_left pullback_snd_isIso_of_range_subset CategoryTheory.Category.assoc CategoryTheory.Limits.pullback.condition CategoryTheory.IsIso.inv_hom_id_assoc
lift_fac_assoc 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace Set.instHasSubset Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.LocallyRingedSpace.instCategory lift	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_fac
lift_range 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace Set.instHasSubset Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom	lift Set.preimage	—	hasPullback_of_left pullback_snd_isIso_of_range_subset CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits TopCat.topCat_hasLimits forgetToTop_preservesPullback_of_left CategoryTheory.Limits.PreservesPullback.iso_hom_fst AlgebraicGeometry.LocallyRingedSpace.comp_base CategoryTheory.Category.assoc TopCat.coe_comp Set.range_comp Set.range_eq_univ TopCat.epi_iff_surjective CategoryTheory.Functor.map_isIso CategoryTheory.Functor.map_inv CategoryTheory.epi_comp CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.IsIso.inv_isIso CategoryTheory.Iso.isIso_hom Set.image_univ TopCat.pullback_fst_range Set.ext
lift_uniq 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace Set.instHasSubset Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom CategoryTheory.CategoryStruct.comp AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.LocallyRingedSpace.instCategory	lift	—	CategoryTheory.cancel_mono mono lift_fac
mono 📖	mathematical	—	CategoryTheory.Mono AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory	—	CategoryTheory.Functor.mono_of_mono_map CategoryTheory.Functor.reflectsMonomorphisms_of_faithful AlgebraicGeometry.LocallyRingedSpace.instFaithfulSheafedSpaceCommRingCatForgetToSheafedSpace AlgebraicGeometry.SheafedSpace.IsOpenImmersion.instMono
ofRestrict 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace TopCat.str AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion AlgebraicGeometry.LocallyRingedSpace.restrict AlgebraicGeometry.LocallyRingedSpace.ofRestrict	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict
ofRestrict_invApp 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier TopCat.of AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	invApp AlgebraicGeometry.LocallyRingedSpace.restrict AlgebraicGeometry.LocallyRingedSpace.ofRestrict ofRestrict CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict_invApp
ofRestrict_invApp_apply 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier TopCat.of AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	RingHom CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op IsOpenMap.functor AlgebraicGeometry.LocallyRingedSpace.toTopCat AlgebraicGeometry.LocallyRingedSpace.restrict opensFunctor AlgebraicGeometry.LocallyRingedSpace.ofRestrict ofRestrict Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier invApp	—	ofRestrict Mathlib.Tactic.Elementwise.hom_elementwise ofRestrict_invApp
of_isIso 📖	mathematical	—	AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion	—	AlgebraicGeometry.SheafedSpace.IsOpenImmersion.of_isIso AlgebraicGeometry.LocallyRingedSpace.is_sheafedSpace_iso
of_stalk_iso 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom CategoryTheory.IsIso TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap	AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion	—	CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.SheafedSpace.IsOpenImmersion.of_stalk_iso CommRingCat.hasLimits CommRingCat.forgetReflectIsos CommRingCat.forget_preservesLimits CommRingCat.FilteredColimits.forget_preservesFilteredColimits
pullback_fst_of_right 📖	mathematical	—	AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion CategoryTheory.Limits.pullback AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory hasPullback_of_right CategoryTheory.Limits.pullback.fst	—	hasPullback_of_right CategoryTheory.Limits.hasPullback_symmetry CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd comp of_isIso CategoryTheory.Iso.isIso_hom pullback_snd_of_left
pullback_snd_isIso_of_range_subset 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace Set.instHasSubset Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom	CategoryTheory.IsIso AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory CategoryTheory.Limits.pullback hasPullback_of_left CategoryTheory.Limits.pullback.snd	—	CategoryTheory.Functor.ReflectsIsomorphisms.reflects AlgebraicGeometry.LocallyRingedSpace.instReflectsIsomorphismsSheafedSpaceCommRingCatForgetToSheafedSpace hasPullback_of_left CategoryTheory.reflectsIsomorphisms_of_full_and_faithful AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_full AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_faithful AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_left forgetToPresheafedSpacePreservesOpenImmersion forgetToPresheafedSpace_preservesPullback_of_left CategoryTheory.Limits.PreservesPullback.iso_hom_snd CategoryTheory.IsIso.comp_isIso' CategoryTheory.Iso.isIso_hom AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullback_snd_isIso_of_range_subset
pullback_snd_of_left 📖	mathematical	—	AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion CategoryTheory.Limits.pullback AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory hasPullback_of_left CategoryTheory.Limits.pullback.snd	—	hasPullback_of_left CategoryTheory.Limits.limit.isoLimitCone_hom_π comp of_isIso CategoryTheory.Iso.isIso_hom instSndPullbackConeOfLeft
pullback_to_base_isOpenImmersion 📖	mathematical	—	AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion CategoryTheory.Limits.limit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory CategoryTheory.Limits.cospan hasPullback_of_right CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingCospan.one CategoryTheory.Limits.limit.π	—	hasPullback_of_right CategoryTheory.Limits.limit.w CategoryTheory.Limits.cospan_map_inl comp pullback_fst_of_right
stalk_iso 📖	mathematical	—	CategoryTheory.IsIso CommRingCat CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.stalk_iso AlgebraicGeometry.instIsOpenImmersionCommRingCatOfIsOpenImmersion CommRingCat.Colimits.hasColimits_commRingCat
to_iso 📖	mathematical	—	CategoryTheory.IsIso AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory	—	CategoryTheory.isIso_iff_of_reflects_iso AlgebraicGeometry.LocallyRingedSpace.instReflectsIsomorphismsSheafedSpaceCommRingCatForgetToSheafedSpace AlgebraicGeometry.SheafedSpace.IsOpenImmersion.to_iso instIsOpenImmersionCommRingCatMapSheafedSpaceForgetToSheafedSpace

AlgebraicGeometry.PresheafedSpace

Definitions

Name	Category	Theorems
IsOpenImmersion 📖	CompData	15 math math: IsOpenImmersion.ofIso, GlueData.ιIsOpenImmersion, IsOpenImmersion.ofIsIso, IsOpenImmersion.pullbackSndOfLeft, IsOpenImmersion.pullbackFstOfRight, IsOpenImmersion.pullbackToBaseIsOpenImmersion, IsOpenImmersion.ofRestrict, GlueData.f_open, IsOpenImmersion.pullbackConeSndIsOpenImmersion, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpacePreservesOpenImmersion, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionCommRingCatFPresheafedSpaceToPresheafedSpaceGlueDataToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData, IsOpenImmersion.comp, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.forgetMapIsOpenImmersion, AlgebraicGeometry.SheafedSpace.isOpenImmersion_iff_hom, AlgebraicGeometry.instIsOpenImmersionCommRingCatOfIsOpenImmersion

AlgebraicGeometry.PresheafedSpace.IsOpenImmersion

Definitions

Name	Category	Theorems
invApp 📖	CompOp	21 math math: invApp_app_assoc, app_inv_app', ofRestrict_invApp, invApp_app, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app_assoc, inv_naturality_assoc, ofRestrict_invApp_apply, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app, app_inv_app'_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app', AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app_assoc, app_invApp, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app, invApp_app_apply, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app, inv_naturality, app_invApp_assoc, inv_invApp, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app', instIsIsoInvApp
isoOfRangeEq 📖	CompOp	2 math math: isoOfRangeEq_hom, isoOfRangeEq_inv
isoRestrict 📖	CompOp	5 math math: isoRestrict_inv_ofRestrict, isoRestrict_inv_ofRestrict_assoc, isoRestrict_hom_c_app, isoRestrict_hom_ofRestrict, isoRestrict_hom_ofRestrict_assoc
opensFunctor 📖	CompOp	23 math math: invApp_app_assoc, app_inv_app', isoRestrict_hom_c_app, invApp_app, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app_assoc, inv_naturality_assoc, ofRestrict_invApp_apply, AlgebraicGeometry.PresheafedSpace.GlueData.ι_image_preimage_eq, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app, app_inv_app'_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app', AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app_assoc, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_hom_c_app, app_invApp, AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app, invApp_app_apply, AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app, inv_naturality, app_invApp_assoc, inv_invApp, AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app', instIsIsoInvApp
pullbackConeOfLeft 📖	CompOp	3 math math: pullbackConeOfLeftLift_snd, pullbackConeOfLeftLift_fst, pullbackConeSndIsOpenImmersion
pullbackConeOfLeftFst 📖	CompOp	1 math math: pullback_cone_of_left_condition
pullbackConeOfLeftIsLimit 📖	CompOp	—
pullbackConeOfLeftLift 📖	CompOp	2 math math: pullbackConeOfLeftLift_snd, pullbackConeOfLeftLift_fst
toLocallyRingedSpace 📖	CompOp	5 math math: toLocallyRingedSpace_toSheafedSpace, toScheme_toLocallyRingedSpace, locallyRingedSpace_toLocallyRingedSpace, toLocallyRingedSpace_isOpenImmersion, toLocallyRingedSpaceHom_val
toLocallyRingedSpaceHom 📖	CompOp	2 math math: toLocallyRingedSpace_isOpenImmersion, toLocallyRingedSpaceHom_val
toSheafedSpace 📖	CompOp	8 math math: toSheafedSpace_toPresheafedSpace, toSheafedSpaceHom_hom_c, toLocallyRingedSpace_toSheafedSpace, sheafedSpace_toSheafedSpace, toSheafedSpace_isOpenImmersion, toSheafedSpaceHom_base, toSheafedSpaceHom_hom_base, toSheafedSpaceHom_c
toSheafedSpaceHom 📖	CompOp	5 math math: toSheafedSpaceHom_hom_c, toSheafedSpace_isOpenImmersion, toSheafedSpaceHom_base, toSheafedSpaceHom_hom_base, toSheafedSpaceHom_c

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
app_invApp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base opensFunctor TopologicalSpace.Opens.map CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c invApp CategoryTheory.Functor.map Quiver.Hom.op Set CategoryTheory.CategoryStruct.toQuiver OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.image DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier Set.preimage TopologicalSpace.Opens.carrier AlgebraicGeometry.PresheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.homOfLE Set.image_preimage_subset	—	Set.image_preimage_subset c_iso CategoryTheory.Category.assoc CategoryTheory.IsIso.comp_inv_eq CategoryTheory.NatTrans.naturality
app_invApp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c opensFunctor TopologicalSpace.Opens.map invApp CategoryTheory.Functor.map Quiver.Hom.op Set CategoryTheory.CategoryStruct.toQuiver OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.image DFunLike.coe ContinuousMap ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory TopCat.instConcreteCategoryContinuousMapCarrier Set.preimage TopologicalSpace.Opens.carrier AlgebraicGeometry.PresheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.homOfLE Set.image_preimage_subset	—	Set.image_preimage_subset CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' app_invApp
app_inv_app' 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier Set.instHasSubset SetLike.coe TopologicalSpace.Opens AlgebraicGeometry.PresheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.instSetLike Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward opensFunctor TopologicalSpace.Opens.map CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c invApp CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.image Set.preimage TopologicalSpace.Opens.carrier CategoryTheory.eqToHom le_antisymm Set.image_preimage_subset Set.instInter Preorder.toLE Set.subset_inter_iff Set.image_preimage_eq_inter_range	—	le_antisymm Set.image_preimage_subset Set.subset_inter_iff Set.image_preimage_eq_inter_range app_invApp CategoryTheory.eqToHom_op
app_inv_app'_assoc 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier Set.instHasSubset SetLike.coe TopologicalSpace.Opens AlgebraicGeometry.PresheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.instSetLike Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c opensFunctor TopologicalSpace.Opens.map invApp CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.image Set.preimage TopologicalSpace.Opens.carrier CategoryTheory.eqToHom le_antisymm Set.image_preimage_subset Set.instInter Preorder.toLE Set.subset_inter_iff Set.image_preimage_eq_inter_range	—	le_antisymm Set.image_preimage_subset Set.subset_inter_iff Set.image_preimage_eq_inter_range CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' app_inv_app'
base_open 📖	mathematical	—	Topology.IsOpenEmbedding TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.PresheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base	—	—
c_iso 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op IsOpenMap.functor AlgebraicGeometry.PresheafedSpace.Hom.base Topology.IsOpenEmbedding.isOpenMap DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.instTopologicalSpaceCarrierCarrier base_open TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c	—	—
c_iso' 📖	mathematical	CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder opensFunctor	CategoryTheory.IsIso Opposite CategoryTheory.Category.opposite AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c	—	c_iso
comp 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.CategoryStruct.comp AlgebraicGeometry.PresheafedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces	—	Topology.IsOpenEmbedding.comp base_open CategoryTheory.IsIso.comp_isIso' c_iso' TopologicalSpace.Opens.ext Set.ext Set.image_congr Set.image_comp Set.preimage_image_eq Topology.IsEmbedding.injective Topology.IsOpenEmbedding.toIsEmbedding Topology.IsOpenEmbedding.isOpenMap
forget_preservesLimitsOfLeft 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces TopCat TopCat.instCategory CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan AlgebraicGeometry.PresheafedSpace.forget	—	CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits TopCat.topCat_hasLimits CategoryTheory.Category.id_comp CategoryTheory.Limits.PullbackCone.condition_one CategoryTheory.Category.comp_id
forget_preservesLimitsOfRight 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces TopCat TopCat.instCategory CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan AlgebraicGeometry.PresheafedSpace.forget	—	CategoryTheory.Limits.preservesPullback_symmetry forget_preservesLimitsOfLeft
hasPullback_of_left 📖	mathematical	—	CategoryTheory.Limits.HasPullback AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces	—	—
hasPullback_of_right 📖	mathematical	—	CategoryTheory.Limits.HasPullback AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces	—	CategoryTheory.Limits.hasPullback_symmetry hasPullback_of_left
instIsIsoInvApp 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op opensFunctor invApp	—	c_iso CategoryTheory.IsIso.comp_isIso CategoryTheory.Functor.map_isIso CategoryTheory.instIsIsoEqToHom CategoryTheory.IsIso.inv_isIso
invApp_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op opensFunctor TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base invApp CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c CategoryTheory.Functor.map CategoryTheory.Functor.op TopologicalSpace.Opens.map CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite	—	c_iso invApp.eq_1 CategoryTheory.Category.assoc CategoryTheory.IsIso.inv_hom_id CategoryTheory.Category.comp_id
invApp_app_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op opensFunctor TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.c invApp CategoryTheory.Functor.map CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise invApp_app
invApp_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op opensFunctor invApp TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c CategoryTheory.Functor.map CategoryTheory.Functor.op TopologicalSpace.Opens.map CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' invApp_app
inv_invApp 📖	mathematical	—	CategoryTheory.inv CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op opensFunctor invApp instIsIsoInvApp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c CategoryTheory.Functor.map CategoryTheory.Functor.op TopologicalSpace.Opens.map CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite	—	instIsIsoInvApp CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.IsIso.hom_inv_id c_iso CategoryTheory.Category.assoc CategoryTheory.IsIso.inv_hom_id_assoc CategoryTheory.eqToHom_trans CategoryTheory.Functor.map_id
inv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op opensFunctor Opposite.unop AlgebraicGeometry.PresheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.map invApp CategoryTheory.Functor.op	—	c_iso CategoryTheory.IsIso.comp_inv_eq CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.NatTrans.naturality CategoryTheory.IsIso.inv_hom_id_assoc
inv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Functor.map Opposite.op opensFunctor Opposite.unop AlgebraicGeometry.PresheafedSpace.instTopologicalSpaceCarrierCarrier invApp CategoryTheory.Functor.op	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inv_naturality
isIso_of_subset 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier Set.instHasSubset SetLike.coe TopologicalSpace.Opens AlgebraicGeometry.PresheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.instSetLike Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base	CategoryTheory.IsIso CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c	—	Topology.IsOpenEmbedding.isOpenMap base_open TopologicalSpace.Opens.ext Set.inter_eq_left Set.image_preimage_eq_inter_range c_iso
isoOfRangeEq_hom 📖	mathematical	Set.range TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base	CategoryTheory.Iso.hom AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces isoOfRangeEq lift	—	—
isoOfRangeEq_inv 📖	mathematical	Set.range TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base	CategoryTheory.Iso.inv AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces isoOfRangeEq lift	—	—
isoRestrict_hom_c_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.PresheafedSpace.restrict AlgebraicGeometry.PresheafedSpace.Hom.base base_open TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.Iso.hom TopCat TopCat.instCategory CategoryTheory.Iso.refl AlgebraicGeometry.PresheafedSpace.Hom.c AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces isoRestrict CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.op IsOpenMap.functor Opposite.unop TopologicalSpace.Opens.map opensFunctor CategoryTheory.CategoryStruct.id CategoryTheory.Functor.map CategoryTheory.eqToHom	—	base_open
isoRestrict_hom_ofRestrict 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.PresheafedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.PresheafedSpace.restrict AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.PresheafedSpace.Hom.base base_open CategoryTheory.Iso.hom isoRestrict AlgebraicGeometry.PresheafedSpace.ofRestrict	—	AlgebraicGeometry.PresheafedSpace.Hom.ext base_open CategoryTheory.NatTrans.ext CategoryTheory.Functor.whiskerRight_id' CategoryTheory.Category.comp_id AlgebraicGeometry.PresheafedSpace.comp_c_app CategoryTheory.NatTrans.naturality_assoc CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_id
isoRestrict_hom_ofRestrict_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.PresheafedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.PresheafedSpace.restrict AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.PresheafedSpace.Hom.base base_open CategoryTheory.Iso.hom isoRestrict AlgebraicGeometry.PresheafedSpace.ofRestrict	—	base_open CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoRestrict_hom_ofRestrict
isoRestrict_inv_ofRestrict 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.PresheafedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.PresheafedSpace.restrict AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.PresheafedSpace.Hom.base base_open CategoryTheory.Iso.inv isoRestrict AlgebraicGeometry.PresheafedSpace.ofRestrict	—	base_open CategoryTheory.Iso.inv_comp_eq isoRestrict_hom_ofRestrict
isoRestrict_inv_ofRestrict_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.PresheafedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.PresheafedSpace.restrict AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.PresheafedSpace.Hom.base base_open CategoryTheory.Iso.inv isoRestrict AlgebraicGeometry.PresheafedSpace.ofRestrict	—	base_open CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoRestrict_inv_ofRestrict
lift_fac 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier Set.instHasSubset Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.PresheafedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces lift	—	hasPullback_of_left pullback_snd_isIso_of_range_subset CategoryTheory.Category.assoc CategoryTheory.Limits.pullback.condition CategoryTheory.IsIso.inv_hom_id_assoc
lift_fac_assoc 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier Set.instHasSubset Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.PresheafedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces lift	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_fac
lift_uniq 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier Set.instHasSubset Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.CategoryStruct.comp AlgebraicGeometry.PresheafedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces	lift	—	CategoryTheory.cancel_mono mono lift_fac
locallyRingedSpace_toLocallyRingedSpace 📖	mathematical	—	toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.toPresheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.instIsOpenImmersionCommRingCatOfIsOpenImmersion	—	AlgebraicGeometry.instIsOpenImmersionCommRingCatOfIsOpenImmersion
mono 📖	mathematical	—	CategoryTheory.Mono AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces	—	base_open isoRestrict_hom_ofRestrict CategoryTheory.mono_comp CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom AlgebraicGeometry.PresheafedSpace.ofRestrict_mono
ofIsIso 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion	—	ofIso
ofIso 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Iso.hom AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces	—	Homeomorph.isOpenEmbedding Topology.IsOpenEmbedding.isOpenMap CategoryTheory.NatIso.isIso_app_of_isIso AlgebraicGeometry.PresheafedSpace.c_isIso_of_iso CategoryTheory.Iso.isIso_hom
ofRestrict 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier TopCat.str AlgebraicGeometry.PresheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion AlgebraicGeometry.PresheafedSpace.restrict AlgebraicGeometry.PresheafedSpace.ofRestrict	—	Topology.IsOpenEmbedding.isOpenMap TopologicalSpace.Opens.ext Set.preimage_image_eq Topology.IsEmbedding.injective Topology.IsOpenEmbedding.toIsEmbedding Preorder.subsingleton_hom CategoryTheory.Functor.map_isIso CategoryTheory.IsIso.id
ofRestrict_invApp 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier TopCat.of AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.PresheafedSpace.instTopologicalSpaceCarrierCarrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	invApp AlgebraicGeometry.PresheafedSpace.restrict AlgebraicGeometry.PresheafedSpace.ofRestrict ofRestrict CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op	—	ofRestrict c_iso CategoryTheory.IsIso.comp_inv_eq CategoryTheory.Category.id_comp
ofRestrict_invApp_apply 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier TopCat.of AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.PresheafedSpace.instTopologicalSpaceCarrierCarrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op IsOpenMap.functor opensFunctor AlgebraicGeometry.PresheafedSpace.restrict AlgebraicGeometry.PresheafedSpace.ofRestrict ofRestrict invApp	—	ofRestrict Mathlib.Tactic.Elementwise.hom_elementwise ofRestrict_invApp CategoryTheory.id_apply
pullbackConeOfLeftLift_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.PresheafedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan pullbackConeOfLeft pullbackConeOfLeftLift CategoryTheory.Limits.PullbackCone.fst	—	AlgebraicGeometry.PresheafedSpace.Hom.ext CategoryTheory.Limits.limit.lift_π CategoryTheory.NatTrans.ext CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp CategoryTheory.NatTrans.naturality_assoc CategoryTheory.Limits.PullbackCone.condition AlgebraicGeometry.PresheafedSpace.congr_app CategoryTheory.Functor.map_isIso CategoryTheory.instIsIsoEqToHom Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.IsIso.comp_inv_eq invApp_app_assoc CategoryTheory.Functor.congr_obj CategoryTheory.eqToHom_unop CategoryTheory.eqToHom_map CategoryTheory.eqToHom_op CategoryTheory.inv.congr_simp CategoryTheory.inv_eqToHom CategoryTheory.eqToHom_app CategoryTheory.eqToHom_trans CategoryTheory.Category.comp_id
pullbackConeOfLeftLift_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.PresheafedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan pullbackConeOfLeft pullbackConeOfLeftLift CategoryTheory.Limits.PullbackCone.snd	—	AlgebraicGeometry.PresheafedSpace.Hom.ext CategoryTheory.Limits.limit.lift_π CategoryTheory.NatTrans.ext CategoryTheory.Category.assoc CategoryTheory.NatTrans.naturality_assoc CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
pullbackConeSndIsOpenImmersion 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Limits.cospan pullbackConeOfLeft CategoryTheory.Limits.PullbackCone.snd	—	pullback_cone_of_left_condition CategoryTheory.Limits.PullbackCone.mk_snd ofRestrict
pullbackFstOfRight 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Limits.pullback AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces hasPullback_of_right CategoryTheory.Limits.pullback.fst	—	hasPullback_of_right CategoryTheory.Limits.hasPullback_symmetry CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd comp ofIso pullbackSndOfLeft
pullbackSndOfLeft 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Limits.pullback AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces hasPullback_of_left CategoryTheory.Limits.pullback.snd	—	hasPullback_of_left CategoryTheory.Limits.limit.isoLimitCone_hom_π comp ofIso pullbackConeSndIsOpenImmersion
pullbackToBaseIsOpenImmersion 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Limits.limit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Limits.cospan hasPullback_of_right CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingCospan.one CategoryTheory.Limits.limit.π	—	hasPullback_of_right CategoryTheory.Limits.limit.w CategoryTheory.Limits.cospan_map_inl comp pullbackFstOfRight
pullback_cone_of_left_condition 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.PresheafedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.PresheafedSpace.restrict CategoryTheory.Limits.pullback TopCat TopCat.instCategory AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits TopCat.topCat_hasLimits CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.snd TopCat.snd_isOpenEmbedding_of_left base_open pullbackConeOfLeftFst AlgebraicGeometry.PresheafedSpace.ofRestrict	—	AlgebraicGeometry.PresheafedSpace.Hom.ext CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits TopCat.topCat_hasLimits TopCat.snd_isOpenEmbedding_of_left base_open CategoryTheory.Limits.pullback.condition CategoryTheory.NatTrans.ext Set.image_preimage_subset CategoryTheory.Functor.congr_obj CategoryTheory.NatTrans.comp_app app_invApp_assoc CategoryTheory.NatTrans.naturality_assoc CategoryTheory.eqToHom_app CategoryTheory.eqToHom_unop CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp
pullback_snd_isIso_of_range_subset 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier Set.instHasSubset Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base	CategoryTheory.IsIso AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Limits.pullback hasPullback_of_left CategoryTheory.Limits.pullback.snd	—	hasPullback_of_left CategoryTheory.Limits.limit.isoLimitCone_hom_π CategoryTheory.IsIso.comp_isIso AlgebraicGeometry.PresheafedSpace.base_isIso_of_iso CategoryTheory.Iso.isIso_hom TopCat.snd_iso_of_left_embedding_range_subset Topology.IsOpenEmbedding.isEmbedding base_open to_iso pullbackSndOfLeft CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso
sheafedSpace_toSheafedSpace 📖	mathematical	—	toSheafedSpace AlgebraicGeometry.SheafedSpace.toPresheafedSpace CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces	—	—
stalk_iso 📖	mathematical	—	CategoryTheory.IsIso TopCat.Presheaf.stalk AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.PresheafedSpace.Hom.stalkMap	—	base_open isoRestrict_hom_ofRestrict AlgebraicGeometry.PresheafedSpace.stalkMap.comp CategoryTheory.IsIso.comp_isIso AlgebraicGeometry.PresheafedSpace.ofRestrict_stalkMap_isIso AlgebraicGeometry.PresheafedSpace.stalkMap.isIso CategoryTheory.Iso.isIso_hom
toLocallyRingedSpaceHom_val 📖	mathematical	—	AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom toLocallyRingedSpace toLocallyRingedSpaceHom CategoryTheory.InducedCategory.homMk AlgebraicGeometry.SheafedSpace CommRingCat CommRingCat.instCategory AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace	—	—
toLocallyRingedSpace_isOpenImmersion 📖	mathematical	—	AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion toLocallyRingedSpace toLocallyRingedSpaceHom	—	—
toLocallyRingedSpace_toSheafedSpace 📖	mathematical	—	AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace toSheafedSpace CommRingCat CommRingCat.instCategory	—	—
toSheafedSpaceHom_base 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toSheafedSpaceHom	—	toSheafedSpaceHom_hom_base
toSheafedSpaceHom_c 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.Hom.c AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toSheafedSpaceHom	—	toSheafedSpaceHom_hom_c
toSheafedSpaceHom_hom_base 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toSheafedSpaceHom	—	—
toSheafedSpaceHom_hom_c 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.Hom.c AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toSheafedSpaceHom	—	—
toSheafedSpace_isOpenImmersion 📖	mathematical	—	AlgebraicGeometry.SheafedSpace.IsOpenImmersion toSheafedSpace toSheafedSpaceHom	—	—
toSheafedSpace_toPresheafedSpace 📖	mathematical	—	AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace	—	—
to_iso 📖	mathematical	—	CategoryTheory.IsIso AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces	—	Set.image_preimage_eq TopCat.epi_iff_surjective Topology.IsOpenEmbedding.isOpenMap base_open c_iso CategoryTheory.NatIso.isIso_of_isIso_app AlgebraicGeometry.PresheafedSpace.isIso_of_components Topology.IsOpenEmbedding.isEmbedding Set.range_eq_univ continuous_subtype_val continuous_id' CategoryTheory.Iso.isIso_hom

AlgebraicGeometry.SheafedSpace

Definitions

Name	Category	Theorems
IsOpenImmersion 📖	MathDef	15 math math: AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.instIsOpenImmersionCommRingCatMapSheafedSpaceForgetToSheafedSpace, IsOpenImmersion.comp, IsOpenImmersion.sheafedSpace_pullback_snd_of_left, IsOpenImmersion.ofRestrict, IsOpenImmersion.sheafedSpace_pullback_to_base_isOpenImmersion, GlueData.f_open, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionCommRingCatFSheafedSpaceToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData, IsOpenImmersion.sigma_ι_isOpenImmersion, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpace_isOpenImmersion, IsOpenImmersion.of_isIso, IsOpenImmersion.sigma_ι_isOpenImmersion_aux, GlueData.ιIsOpenImmersion, isOpenImmersion_iff_hom, IsOpenImmersion.sheafedSpace_pullback_fst_of_right, IsOpenImmersion.of_stalk_iso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOpenImmersion_iff_hom 📖	mathematical	—	IsOpenImmersion AlgebraicGeometry.PresheafedSpace.IsOpenImmersion toPresheafedSpace CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces	—	—

AlgebraicGeometry.SheafedSpace.IsOpenImmersion

Definitions

Name	Category	Theorems
forgetCreatesPullbackOfLeft 📖	CompOp	—
forgetCreatesPullbackOfRight 📖	CompOp	—
invApp 📖	CompOp	13 math math: app_invApp, instIsIsoInvApp, invApp_app_apply, ofRestrict_invApp, app_inv_app', inv_naturality, ofRestrict_invApp_apply, inv_naturality_assoc, app_inv_app'_assoc, app_invApp_assoc, invApp_app, invApp_app_assoc, inv_invApp
isoRestrict 📖	CompOp	5 math math: isoRestrict_inv_ofRestrict_assoc, isoRestrict_hom_ofRestrict, isoRestrict_hom_hom_c_app, isoRestrict_inv_ofRestrict, isoRestrict_hom_ofRestrict_assoc
opensFunctor 📖	CompOp	12 math math: app_invApp, instIsIsoInvApp, invApp_app_apply, app_inv_app', inv_naturality, ofRestrict_invApp_apply, inv_naturality_assoc, app_inv_app'_assoc, app_invApp_assoc, invApp_app, invApp_app_assoc, inv_invApp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
app_invApp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor TopologicalSpace.Opens.map CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c invApp CategoryTheory.Functor.map Quiver.Hom.op Set CategoryTheory.CategoryStruct.toQuiver OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.image DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier Set.preimage TopologicalSpace.Opens.carrier CategoryTheory.homOfLE Set.image_preimage_subset	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp
app_invApp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor TopologicalSpace.Opens.map invApp CategoryTheory.Functor.map Quiver.Hom.op Set CategoryTheory.CategoryStruct.toQuiver OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.image DFunLike.coe ContinuousMap ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory TopCat.instConcreteCategoryContinuousMapCarrier Set.preimage TopologicalSpace.Opens.carrier CategoryTheory.homOfLE Set.image_preimage_subset	—	Set.image_preimage_subset CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' app_invApp
app_inv_app' 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace Set.instHasSubset SetLike.coe TopologicalSpace.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.instSetLike Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward opensFunctor TopologicalSpace.Opens.map CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c invApp CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.image Set.preimage TopologicalSpace.Opens.carrier CategoryTheory.eqToHom le_antisymm Set.image_preimage_subset Set.instInter Preorder.toLE Set.subset_inter_iff Set.image_preimage_eq_inter_range	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp
app_inv_app'_assoc 📖	mathematical	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace Set.instHasSubset SetLike.coe TopologicalSpace.Opens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.instSetLike Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c opensFunctor TopologicalSpace.Opens.map invApp CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.image Set.preimage TopologicalSpace.Opens.carrier CategoryTheory.eqToHom le_antisymm Set.image_preimage_subset Set.instInter Preorder.toLE Set.subset_inter_iff Set.image_preimage_eq_inter_range	—	le_antisymm Set.image_preimage_subset Set.subset_inter_iff Set.image_preimage_eq_inter_range CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' app_inv_app'
comp 📖	mathematical	—	AlgebraicGeometry.SheafedSpace.IsOpenImmersion CategoryTheory.CategoryStruct.comp AlgebraicGeometry.SheafedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.SheafedSpace.instCategory	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.comp
forgetMapIsOpenImmersion 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.Functor.obj AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace CategoryTheory.Functor.map	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso
hasLimit_cospan_forget_of_left 📖	mathematical	—	CategoryTheory.Limits.HasLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Functor.comp AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory CategoryTheory.Limits.cospan AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_left forgetMapIsOpenImmersion CategoryTheory.Limits.hasLimit_of_iso
hasLimit_cospan_forget_of_left' 📖	mathematical	—	CategoryTheory.Limits.HasLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Limits.cospan CategoryTheory.Functor.obj CategoryTheory.Functor.comp AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace CategoryTheory.Limits.WalkingCospan.left CategoryTheory.Limits.WalkingCospan.right CategoryTheory.Limits.WalkingCospan.one CategoryTheory.Functor.map CategoryTheory.Limits.WalkingCospan.Hom.inl CategoryTheory.Limits.WalkingCospan.Hom.inr	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_left forgetMapIsOpenImmersion
hasLimit_cospan_forget_of_right 📖	mathematical	—	CategoryTheory.Limits.HasLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Functor.comp AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory CategoryTheory.Limits.cospan AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_right forgetMapIsOpenImmersion CategoryTheory.Limits.hasLimit_of_iso
hasLimit_cospan_forget_of_right' 📖	mathematical	—	CategoryTheory.Limits.HasLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Limits.cospan CategoryTheory.Functor.obj CategoryTheory.Functor.comp AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace CategoryTheory.Limits.WalkingCospan.left CategoryTheory.Limits.WalkingCospan.right CategoryTheory.Limits.WalkingCospan.one CategoryTheory.Functor.map CategoryTheory.Limits.WalkingCospan.Hom.inl CategoryTheory.Limits.WalkingCospan.Hom.inr	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_right forgetMapIsOpenImmersion
image_preimage_is_empty 📖	mathematical	—	CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CategoryTheory.Limits.colimit CategoryTheory.Discrete CategoryTheory.discreteCategory AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Functor.comp AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace CategoryTheory.Limits.instHasColimitCompOfPreservesColimit CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.preservesColimitOfShape_of_createsColimitsOfShape_and_hasColimitsOfShape AlgebraicGeometry.SheafedSpace.instCreatesColimitsOfShapePresheafedSpaceForgetToPresheafedSpaceOfSmallOfHasLimitsOfShapeOpposite CategoryTheory.instSmallDiscrete UnivLE.small UnivLE.self CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits Opposite CategoryTheory.Category.opposite AlgebraicGeometry.PresheafedSpace.instHasColimitsOfShape TopCat.topCat_hasColimitsOfShape TopCat.instHasLimitsOfShapePresheaf TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.Limits.colimit.ι CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit CategoryTheory.CreatesColimitsOfShape.CreatesColimit CategoryTheory.Iso.inv CategoryTheory.preservesColimitIso AlgebraicGeometry.SheafedSpace.toPresheafedSpace IsOpenMap.functor CategoryTheory.InducedCategory.Hom.hom Topology.IsOpenEmbedding.isOpenMap DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier sigma_ι_isOpenEmbedding Bot.bot OrderBot.toBot Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Order.Frame.toHeytingAlgebra TopologicalSpace.Opens.instFrame HeytingAlgebra.toOrderBot	—	TopologicalSpace.Opens.ext CategoryTheory.Limits.instHasColimitCompOfPreservesColimit CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.preservesColimitOfShape_of_createsColimitsOfShape_and_hasColimitsOfShape CategoryTheory.instSmallDiscrete UnivLE.small UnivLE.self CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits AlgebraicGeometry.PresheafedSpace.instHasColimitsOfShape TopCat.topCat_hasColimitsOfShape TopCat.instHasLimitsOfShapePresheaf CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit Topology.IsOpenEmbedding.isOpenMap sigma_ι_isOpenEmbedding Set.ext AlgebraicGeometry.SheafedSpace.instPreservesColimitsOfShapeTopCatForgetOfSmallOfHasLimitsOfShapeOpposite CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.ConcreteCategory.congr_arg univLE_of_max TopCat.sigmaIsoSigma_hom_ι CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_hom_assoc CategoryTheory.ι_preservesColimitIso_hom_assoc CategoryTheory.ι_preservesColimitIso_inv
instIsIsoInvApp 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor invApp	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.instIsIsoInvApp
instMono 📖	mathematical	—	CategoryTheory.Mono AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory	—	CategoryTheory.Functor.mono_of_mono_map CategoryTheory.reflectsMonomorphisms_of_reflectsLimitsOfShape CategoryTheory.Limits.ReflectsFiniteLimits.reflects CategoryTheory.Limits.instReflectsFiniteLimitsOfReflectsLimits CategoryTheory.Limits.fullyFaithful_reflectsLimits AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_full AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_faithful AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.mono
invApp_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces invApp CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c CategoryTheory.Functor.map CategoryTheory.Functor.op TopologicalSpace.Opens.map CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app
invApp_app_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.c invApp CategoryTheory.Functor.map CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise invApp_app
invApp_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor invApp TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c CategoryTheory.Functor.map CategoryTheory.Functor.op TopologicalSpace.Opens.map CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' invApp_app
inv_invApp 📖	mathematical	—	CategoryTheory.inv CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor invApp instIsIsoInvApp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c CategoryTheory.Functor.map CategoryTheory.Functor.op TopologicalSpace.Opens.map CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_invApp
inv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor Opposite.unop CategoryTheory.Functor.map invApp CategoryTheory.Functor.op	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_naturality
inv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Functor.map Opposite.op AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor Opposite.unop invApp CategoryTheory.Functor.op	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inv_naturality
isoRestrict_hom_hom_c_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.PresheafedSpace.restrict AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.Functor.obj TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.Iso.hom TopCat TopCat.instCategory CategoryTheory.Iso.refl AlgebraicGeometry.PresheafedSpace.Hom.c AlgebraicGeometry.SheafedSpace.restrict AlgebraicGeometry.SheafedSpace.instCategory isoRestrict CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.op IsOpenMap.functor Opposite.unop TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor CategoryTheory.CategoryStruct.id CategoryTheory.Functor.map CategoryTheory.eqToHom	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open
isoRestrict_hom_ofRestrict 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.SheafedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.SheafedSpace.restrict AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open CategoryTheory.Iso.hom isoRestrict AlgebraicGeometry.SheafedSpace.ofRestrict	—	CategoryTheory.InducedCategory.hom_ext AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict
isoRestrict_hom_ofRestrict_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.SheafedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.SheafedSpace.restrict AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open CategoryTheory.Iso.hom isoRestrict AlgebraicGeometry.SheafedSpace.ofRestrict	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoRestrict_hom_ofRestrict
isoRestrict_inv_ofRestrict 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.SheafedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.SheafedSpace.restrict AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open CategoryTheory.Iso.inv isoRestrict AlgebraicGeometry.SheafedSpace.ofRestrict	—	CategoryTheory.InducedCategory.hom_ext AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict
isoRestrict_inv_ofRestrict_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.SheafedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.SheafedSpace.restrict AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open CategoryTheory.Iso.inv isoRestrict AlgebraicGeometry.SheafedSpace.ofRestrict	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoRestrict_inv_ofRestrict
ofRestrict 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace TopCat.str AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	AlgebraicGeometry.SheafedSpace.IsOpenImmersion AlgebraicGeometry.SheafedSpace.restrict AlgebraicGeometry.SheafedSpace.ofRestrict	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict
ofRestrict_invApp 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier TopCat.of AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	invApp AlgebraicGeometry.SheafedSpace.restrict AlgebraicGeometry.SheafedSpace.ofRestrict ofRestrict CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict_invApp
ofRestrict_invApp_apply 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier TopCat.of AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens AlgebraicGeometry.SheafedSpace.restrict CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op opensFunctor AlgebraicGeometry.SheafedSpace.ofRestrict ofRestrict invApp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	ofRestrict Mathlib.Tactic.Elementwise.hom_elementwise ofRestrict_invApp
of_isIso 📖	mathematical	—	AlgebraicGeometry.SheafedSpace.IsOpenImmersion	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofIsIso CategoryTheory.Functor.map_isIso
of_stalk_iso 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.IsIso TopCat.Presheaf.stalk AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.PresheafedSpace.Hom.stalkMap	AlgebraicGeometry.SheafedSpace.IsOpenImmersion	—	TopCat.Presheaf.app_isIso_of_stalkFunctor_map_iso Topology.IsOpenEmbedding.isOpenMap TopCat.Presheaf.stalkPushforward.stalkPushforward_iso_of_isInducing Topology.IsEmbedding.toIsInducing Topology.IsOpenEmbedding.toIsEmbedding CategoryTheory.IsIso.comp_isIso' CategoryTheory.IsIso.inv_isIso CategoryTheory.Category.comp_id CategoryTheory.IsIso.hom_inv_id CategoryTheory.Category.assoc
sheafedSpace_forgetPreserves_of_left 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory TopCat TopCat.instCategory CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan AlgebraicGeometry.SheafedSpace.forget	—	CategoryTheory.Limits.comp_preservesLimit CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit hasLimit_cospan_forget_of_left AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.forget_preservesLimitsOfLeft CategoryTheory.Limits.preservesLimit_of_iso_diagram
sheafedSpace_forgetPreserves_of_right 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory TopCat TopCat.instCategory CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan AlgebraicGeometry.SheafedSpace.forget	—	CategoryTheory.Limits.preservesPullback_symmetry sheafedSpace_forgetPreserves_of_left
sheafedSpace_hasPullback_of_left 📖	mathematical	—	CategoryTheory.Limits.HasPullback AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory	—	CategoryTheory.hasLimit_of_created hasLimit_cospan_forget_of_left
sheafedSpace_hasPullback_of_right 📖	mathematical	—	CategoryTheory.Limits.HasPullback AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory	—	CategoryTheory.hasLimit_of_created hasLimit_cospan_forget_of_right
sheafedSpace_pullback_fst_of_right 📖	mathematical	—	AlgebraicGeometry.SheafedSpace.IsOpenImmersion CategoryTheory.Limits.pullback AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory sheafedSpace_hasPullback_of_right CategoryTheory.Limits.pullback.fst	—	sheafedSpace_hasPullback_of_right AlgebraicGeometry.SheafedSpace.isOpenImmersion_iff_hom CategoryTheory.Limits.instHasLimitCompOfPreservesLimit CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit hasLimit_cospan_forget_of_right CategoryTheory.preservesLimitIso_hom_π hasLimit_cospan_forget_of_right' CategoryTheory.Limits.HasLimit.isoOfNatIso_hom_π CategoryTheory.Category.comp_id AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.comp AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofIso AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackFstOfRight
sheafedSpace_pullback_snd_of_left 📖	mathematical	—	AlgebraicGeometry.SheafedSpace.IsOpenImmersion CategoryTheory.Limits.pullback AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory sheafedSpace_hasPullback_of_left CategoryTheory.Limits.pullback.snd	—	sheafedSpace_hasPullback_of_left AlgebraicGeometry.SheafedSpace.isOpenImmersion_iff_hom CategoryTheory.Limits.instHasLimitCompOfPreservesLimit CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit hasLimit_cospan_forget_of_left CategoryTheory.preservesLimitIso_hom_π hasLimit_cospan_forget_of_left' CategoryTheory.Limits.HasLimit.isoOfNatIso_hom_π CategoryTheory.Category.comp_id AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.comp AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofIso AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackSndOfLeft
sheafedSpace_pullback_to_base_isOpenImmersion 📖	mathematical	—	AlgebraicGeometry.SheafedSpace.IsOpenImmersion CategoryTheory.Limits.limit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory CategoryTheory.Limits.cospan sheafedSpace_hasPullback_of_right CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingCospan.one CategoryTheory.Limits.limit.π	—	sheafedSpace_hasPullback_of_right CategoryTheory.Limits.limit.w CategoryTheory.Limits.cospan_map_inl comp sheafedSpace_pullback_fst_of_right
sigma_ι_isOpenEmbedding 📖	mathematical	—	Topology.IsOpenEmbedding TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory CategoryTheory.Limits.colimit AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Limits.colimit.ι	—	CategoryTheory.Limits.instHasColimitCompOfPreservesColimit CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit AlgebraicGeometry.SheafedSpace.instPreservesColimitsOfShapeTopCatForgetOfSmallOfHasLimitsOfShapeOpposite CategoryTheory.instSmallDiscrete UnivLE.small UnivLE.self CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.ι_preservesColimitIso_inv CategoryTheory.Limits.hasColimitOfHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_hom CategoryTheory.Iso.eq_comp_inv univLE_of_max TopCat.sigmaIsoSigma_hom_ι CategoryTheory.Category.assoc CategoryTheory.Iso.isIso_inv TopCat.isOpenEmbedding_iff_isIso_comp CategoryTheory.NatIso.hom_app_isIso Topology.IsOpenEmbedding.sigmaMk
sigma_ι_isOpenImmersion 📖	mathematical	—	AlgebraicGeometry.SheafedSpace.IsOpenImmersion CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory CategoryTheory.Limits.colimit CategoryTheory.Limits.colimit.ι	—	Small.equiv_small CategoryTheory.Limits.hasColimit_equivalence_comp CategoryTheory.Limits.HasColimit.isoOfEquivalence_inv_π CategoryTheory.Category.id_comp CategoryTheory.Category.assoc CategoryTheory.Limits.HasColimit.isoOfEquivalence_hom_π CategoryTheory.Limits.colimit.w comp of_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.NatIso.hom_app_isIso sigma_ι_isOpenImmersion_aux CategoryTheory.Iso.isIso_hom
sigma_ι_isOpenImmersion_aux 📖	mathematical	—	AlgebraicGeometry.SheafedSpace.IsOpenImmersion CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory CategoryTheory.Limits.colimit CategoryTheory.Limits.colimit.ι	—	sigma_ι_isOpenEmbedding CategoryTheory.Limits.instHasColimitCompOfPreservesColimit CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit CategoryTheory.instSmallDiscrete UnivLE.small UnivLE.self CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.preservesColimitOfShape_of_createsColimitsOfShape_and_hasColimitsOfShape AlgebraicGeometry.PresheafedSpace.instHasColimitsOfShape TopCat.topCat_hasColimitsOfShape TopCat.instHasLimitsOfShapePresheaf CategoryTheory.ι_preservesColimitIso_inv CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.InducedCategory.hom_ext Topology.IsOpenEmbedding.isOpenMap AlgebraicGeometry.PresheafedSpace.comp_c_app CategoryTheory.Limits.hasLimitOfHasLimitsOfShape AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_hom_π AlgebraicGeometry.PresheafedSpace.c_isIso_of_iso CategoryTheory.Iso.isIso_inv CategoryTheory.Limits.limit_π_isIso_of_is_strict_terminal image_preimage_is_empty CategoryTheory.subsingleton_of_unop CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.IsIso.comp_isIso CategoryTheory.NatIso.isIso_app_of_isIso CategoryTheory.Iso.isIso_hom
stalk_iso 📖	mathematical	—	CategoryTheory.IsIso TopCat.Presheaf.stalk AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.SheafedSpace AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.PresheafedSpace.Hom.stalkMap	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.stalk_iso
to_iso 📖	mathematical	—	CategoryTheory.IsIso AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory	—	CategoryTheory.isIso_of_reflects_iso AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.to_iso CategoryTheory.reflectsIsomorphisms_of_full_and_faithful AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_full AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_faithful

---

← Back to Index