Gluing

📁 Source: Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean

Statistics

Metric	Count
Definitions isoSheafedSpace, toGlueData, toSheafedSpaceGlueData, vPullbackConeIsLimit, diagramOverOpen, diagramOverOpenπ, opensImagePreimageMap, toGlueData, toTopGlueData, vPullbackConeIsLimit, ιInvApp, ιInvAppπApp, ιInvAppπEqMap, isoPresheafedSpace, toGlueData, toPresheafedSpaceGlueData, vPullbackConeIsLimit	17
Theorems f_open, instPreservesLimitSheafedSpaceCommRingCatWalkingCospanCospanFForgetToSheafedSpace, ι_isOpenImmersion, ι_isoSheafedSpace_inv, ι_isoSheafedSpace_inv_assoc, ι_jointly_surjective, componentwise_diagram_π_isIso, f_invApp_f_app, f_invApp_f_app_assoc, f_open, opensImagePreimageMap_app, opensImagePreimageMap_app', opensImagePreimageMap_app_assoc, pullback_base, snd_invApp_t_app, snd_invApp_t_app', snd_invApp_t_app_assoc, ιInvApp_π, ιIsOpenImmersion, ι_image_preimage_eq, ι_isOpenEmbedding, ι_jointly_surjective, π_ιInvApp_eq_id, π_ιInvApp_π, f_open, ιIsOpenImmersion, ι_isoPresheafedSpace_inv, ι_jointly_surjective	28
Total	45

AlgebraicGeometry.LocallyRingedSpace.GlueData

Definitions

Name	Category	Theorems
isoSheafedSpace 📖	CompOp	2 math math: ι_isoSheafedSpace_inv, ι_isoSheafedSpace_inv_assoc
toGlueData 📖	CompOp	9 math math: ι_isOpenImmersion, ι_isoSheafedSpace_inv, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionιLocallyRingedSpaceToLocallyRingedSpaceGlueData, ι_jointly_surjective, ι_isoSheafedSpace_inv_assoc, AlgebraicGeometry.Scheme.GlueData.ι_isoLocallyRingedSpace_inv, f_open, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionFLocallyRingedSpaceToLocallyRingedSpaceGlueData, instPreservesLimitSheafedSpaceCommRingCatWalkingCospanCospanFForgetToSheafedSpace
toSheafedSpaceGlueData 📖	CompOp	5 math math: AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionCommRingCatFSheafedSpaceToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData, ι_isoSheafedSpace_inv, AlgebraicGeometry.Scheme.GlueData.ι_isoCarrier_inv, ι_isoSheafedSpace_inv_assoc, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionCommRingCatFPresheafedSpaceToPresheafedSpaceGlueDataToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData
vPullbackConeIsLimit 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
f_open 📖	mathematical	—	AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion CategoryTheory.GlueData.V AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory toGlueData CategoryTheory.GlueData.J CategoryTheory.GlueData.U CategoryTheory.GlueData.f	—	—
instPreservesLimitSheafedSpaceCommRingCatWalkingCospanCospanFForgetToSheafedSpace 📖	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 CategoryTheory.GlueData.V toGlueData CategoryTheory.GlueData.J CategoryTheory.GlueData.U CategoryTheory.GlueData.f AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace	—	AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_preservesPullback_of_right f_open
ι_isOpenImmersion 📖	mathematical	—	AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion CategoryTheory.GlueData.U AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory toGlueData CategoryTheory.GlueData.glued CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize AlgebraicGeometry.LocallyRingedSpace.instHasColimits CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram CategoryTheory.GlueData.ι	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize AlgebraicGeometry.LocallyRingedSpace.instHasColimits AlgebraicGeometry.SheafedSpace.instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CommRingCat.hasLimitsOfShape Opposite.small ι_isoSheafedSpace_inv AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.comp AlgebraicGeometry.SheafedSpace.GlueData.ιIsOpenImmersion CommRingCat.hasLimits AlgebraicGeometry.SheafedSpace.IsOpenImmersion.of_isIso CategoryTheory.Iso.isIso_inv
ι_isoSheafedSpace_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.SheafedSpace CommRingCat CommRingCat.instCategory CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.SheafedSpace.instCategory CategoryTheory.GlueData.U AlgebraicGeometry.SheafedSpace.GlueData.toGlueData toSheafedSpaceGlueData CategoryTheory.GlueData.glued CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory AlgebraicGeometry.SheafedSpace.instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R CommRingCat.hasLimitsOfShape Opposite CategoryTheory.Category.opposite Opposite.small CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory toGlueData CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize AlgebraicGeometry.LocallyRingedSpace.instHasColimits CategoryTheory.GlueData.ι CategoryTheory.Iso.inv isoSheafedSpace AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom	—	CategoryTheory.GlueData.ι_gluedIso_inv CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize AlgebraicGeometry.LocallyRingedSpace.instHasColimits CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape AlgebraicGeometry.LocallyRingedSpace.preservesColimits_forgetToSheafedSpace AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_preservesPullback_of_right f_open
ι_isoSheafedSpace_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.SheafedSpace CommRingCat CommRingCat.instCategory CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.SheafedSpace.instCategory CategoryTheory.GlueData.U CategoryTheory.GlueData.mapGlueData AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory toGlueData AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace CategoryTheory.GlueData.glued CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J AlgebraicGeometry.SheafedSpace.GlueData.toGlueData toSheafedSpaceGlueData CategoryTheory.Limits.WalkingMultispan.instSmallCategory AlgebraicGeometry.SheafedSpace.instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R CommRingCat.hasLimitsOfShape Opposite CategoryTheory.Category.opposite Opposite.small CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram CategoryTheory.GlueData.ι AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize AlgebraicGeometry.LocallyRingedSpace.instHasColimits CategoryTheory.Iso.inv isoSheafedSpace AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize AlgebraicGeometry.LocallyRingedSpace.instHasColimits AlgebraicGeometry.SheafedSpace.instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CommRingCat.hasLimitsOfShape Opposite.small CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_isoSheafedSpace_inv
ι_jointly_surjective 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace CategoryTheory.GlueData.U AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory toGlueData CategoryTheory.GlueData.glued CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize AlgebraicGeometry.LocallyRingedSpace.instHasColimits CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom CategoryTheory.GlueData.ι	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize AlgebraicGeometry.LocallyRingedSpace.instHasColimits CategoryTheory.GlueData.ι_jointly_surjective CategoryTheory.Limits.comp_preservesColimit CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape AlgebraicGeometry.LocallyRingedSpace.preservesColimits_forgetToSheafedSpace AlgebraicGeometry.SheafedSpace.instPreservesColimitsOfShapeTopCatForgetOfSmallOfHasLimitsOfShapeOpposite CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CommRingCat.hasLimitsOfShape Opposite.small CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint TopCat.instIsLeftAdjointForgetContinuousMapCarrier CategoryTheory.Limits.comp_preservesLimit AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToTop_preservesPullback_of_left f_open CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits TopCat.forget_preservesLimits

AlgebraicGeometry.PresheafedSpace.GlueData

Definitions

Name	Category	Theorems
diagramOverOpen 📖	CompOp	4 math math: componentwise_diagram_π_isIso, ιInvApp_π, π_ιInvApp_π, π_ιInvApp_eq_id
diagramOverOpenπ 📖	CompOp	4 math math: componentwise_diagram_π_isIso, ιInvApp_π, π_ιInvApp_π, π_ιInvApp_eq_id
opensImagePreimageMap 📖	CompOp	3 math math: opensImagePreimageMap_app, opensImagePreimageMap_app', opensImagePreimageMap_app_assoc
toGlueData 📖	CompOp	20 math math: ιIsOpenImmersion, snd_invApp_t_app_assoc, pullback_base, ι_image_preimage_eq, opensImagePreimageMap_app, opensImagePreimageMap_app', f_invApp_f_app_assoc, ι_isOpenEmbedding, f_open, componentwise_diagram_π_isIso, AlgebraicGeometry.SheafedSpace.GlueData.ι_isoPresheafedSpace_inv, f_invApp_f_app, opensImagePreimageMap_app_assoc, snd_invApp_t_app, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionCommRingCatFPresheafedSpaceToPresheafedSpaceGlueDataToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData, ι_jointly_surjective, ιInvApp_π, π_ιInvApp_π, π_ιInvApp_eq_id, snd_invApp_t_app'
toTopGlueData 📖	CompOp	1 math math: AlgebraicGeometry.Scheme.GlueData.ι_isoCarrier_inv
vPullbackConeIsLimit 📖	CompOp	—
ιInvApp 📖	CompOp	3 math math: ιInvApp_π, π_ιInvApp_π, π_ιInvApp_eq_id
ιInvAppπApp 📖	CompOp	—
ιInvAppπEqMap 📖	CompOp	2 math math: π_ιInvApp_π, π_ιInvApp_eq_id

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
componentwise_diagram_π_isIso 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Limits.limit Opposite CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toGlueData CategoryTheory.Category.opposite CategoryTheory.Limits.WalkingMultispan.instSmallCategory diagramOverOpen CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Functor.obj Opposite.op CategoryTheory.Limits.WalkingMultispan.right diagramOverOpenπ	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits π_ιInvApp_eq_id CategoryTheory.Category.assoc ιInvApp_π CategoryTheory.Iso.inv_hom_id
f_invApp_f_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CategoryTheory.GlueData.V AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toGlueData CategoryTheory.GlueData.J TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op CategoryTheory.GlueData.U AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor CategoryTheory.GlueData.f f_open TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c CategoryTheory.Limits.pullback AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_right CategoryTheory.Limits.pullback.fst CategoryTheory.Functor.op TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_left CategoryTheory.Limits.pullback.snd AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackSndOfLeft Opposite.unop AlgebraicGeometry.PresheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.map CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_right f_open CategoryTheory.Limits.pullback.condition AlgebraicGeometry.PresheafedSpace.congr_app AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_left AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackSndOfLeft AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.instIsIsoInvApp CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.IsIso.inv_isIso CategoryTheory.IsIso.inv_hom_id_assoc AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_invApp CategoryTheory.Category.assoc CategoryTheory.NatTrans.naturality_assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Functor.map_comp_assoc AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_naturality_assoc Set.image_preimage_subset AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp_assoc CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
f_invApp_f_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CategoryTheory.GlueData.V AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toGlueData CategoryTheory.GlueData.J TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op CategoryTheory.GlueData.U AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor CategoryTheory.GlueData.f f_open AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c CategoryTheory.Limits.pullback AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_right CategoryTheory.Limits.pullback.fst AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_left CategoryTheory.Limits.pullback.snd AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackSndOfLeft CategoryTheory.Functor.map CategoryTheory.Functor.op TopologicalSpace.Opens.map CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite	—	f_open AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_left AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackSndOfLeft CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' f_invApp_f_app
f_open 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.GlueData.V AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toGlueData CategoryTheory.GlueData.J CategoryTheory.GlueData.U CategoryTheory.GlueData.f	—	—
opensImagePreimageMap_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CategoryTheory.GlueData.U AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toGlueData TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op CategoryTheory.GlueData.glued CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory AlgebraicGeometry.PresheafedSpace.instHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R TopCat.instHasLimitsOfShapePresheaf CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.GlueData.ι IsOpenMap.functor Topology.IsOpenEmbedding.isOpenMap DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.instTopologicalSpaceCarrierCarrier ι_isOpenEmbedding TopCat.Presheaf CategoryTheory.GlueData.V TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.GlueData.f opensImagePreimageMap CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c CategoryTheory.Limits.pullback AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_right f_open CategoryTheory.Limits.pullback.fst CategoryTheory.GlueData.t CategoryTheory.Functor.op AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_left AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor CategoryTheory.Limits.pullback.snd AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackSndOfLeft Opposite.unop AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp CategoryTheory.Functor.map CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver opensImagePreimageMap_app'	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_left f_open AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackSndOfLeft AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_right CategoryTheory.Limits.hasColimitOfHasColimitsOfShape AlgebraicGeometry.PresheafedSpace.instHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self TopCat.instHasLimitsOfShapePresheaf CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits Topology.IsOpenEmbedding.isOpenMap ι_isOpenEmbedding opensImagePreimageMap_app'
opensImagePreimageMap_app' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CategoryTheory.GlueData.U AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toGlueData TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op CategoryTheory.GlueData.glued CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory AlgebraicGeometry.PresheafedSpace.instHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R TopCat.instHasLimitsOfShapePresheaf CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.GlueData.ι IsOpenMap.functor Topology.IsOpenEmbedding.isOpenMap DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.instTopologicalSpaceCarrierCarrier ι_isOpenEmbedding TopCat.Presheaf CategoryTheory.GlueData.V TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.GlueData.f opensImagePreimageMap CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c CategoryTheory.Limits.pullback AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_right f_open CategoryTheory.Limits.pullback.fst CategoryTheory.GlueData.t CategoryTheory.Functor.op AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_left AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor CategoryTheory.Limits.pullback.snd AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackSndOfLeft Opposite.unop AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp CategoryTheory.Functor.map CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_left f_open AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackSndOfLeft AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_right CategoryTheory.Limits.hasColimitOfHasColimitsOfShape AlgebraicGeometry.PresheafedSpace.instHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self TopCat.instHasLimitsOfShapePresheaf CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits Topology.IsOpenEmbedding.isOpenMap ι_isOpenEmbedding ι_image_preimage_eq CategoryTheory.Category.assoc CategoryTheory.NatTrans.naturality f_invApp_f_app_assoc CategoryTheory.Functor.map_comp AlgebraicGeometry.PresheafedSpace.comp_c_app CategoryTheory.eqToHom_map CategoryTheory.eqToHom_op CategoryTheory.eqToHom_trans
opensImagePreimageMap_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CategoryTheory.GlueData.U AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toGlueData TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op CategoryTheory.GlueData.glued CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory AlgebraicGeometry.PresheafedSpace.instHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R TopCat.instHasLimitsOfShapePresheaf CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.GlueData.ι IsOpenMap.functor Topology.IsOpenEmbedding.isOpenMap DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.instTopologicalSpaceCarrierCarrier ι_isOpenEmbedding opensImagePreimageMap TopCat.Presheaf CategoryTheory.GlueData.V TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.GlueData.f CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c CategoryTheory.Limits.pullback AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_right f_open CategoryTheory.Limits.pullback.fst CategoryTheory.GlueData.t AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_left AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor CategoryTheory.Limits.pullback.snd AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackSndOfLeft Opposite.unop AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp CategoryTheory.Functor.op CategoryTheory.Functor.map CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver opensImagePreimageMap_app'	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape AlgebraicGeometry.PresheafedSpace.instHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self TopCat.instHasLimitsOfShapePresheaf CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits Topology.IsOpenEmbedding.isOpenMap ι_isOpenEmbedding AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_right f_open AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_left AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackSndOfLeft opensImagePreimageMap_app' CategoryTheory.Category.assoc opensImagePreimageMap_app
pullback_base 📖	mathematical	—	Set.image TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CategoryTheory.Limits.pullback AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.GlueData.V toGlueData CategoryTheory.GlueData.J CategoryTheory.GlueData.U CategoryTheory.GlueData.f AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_right f_open DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.Limits.pullback.snd Set.preimage CategoryTheory.Limits.pullback.fst	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_right f_open CategoryTheory.GlueData.instHasPullbackMapF AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.forget_preservesLimitsOfRight CategoryTheory.Limits.PreservesPullback.iso_hom_fst CategoryTheory.Limits.PreservesPullback.iso_hom_snd TopCat.coe_comp Set.image_comp Set.preimage_comp Set.image_preimage_eq TopCat.epi_iff_surjective CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom Set.image_congr CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits TopCat.topCat_hasLimits TopCat.pullback_snd_image_fst_preimage
snd_invApp_t_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CategoryTheory.Limits.pullback AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.GlueData.V toGlueData CategoryTheory.GlueData.J CategoryTheory.GlueData.U CategoryTheory.GlueData.f AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_left f_open TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor CategoryTheory.Limits.pullback.snd AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackSndOfLeft TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.GlueData.t AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c CategoryTheory.GlueData.f_hasPullback CategoryTheory.GlueData.t' CategoryTheory.Functor.op TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_right CategoryTheory.Limits.pullback.fst AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackFstOfRight Opposite.unop AlgebraicGeometry.PresheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.map CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver snd_invApp_t_app'	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_right f_open AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_left AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackFstOfRight CategoryTheory.GlueData.f_hasPullback AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackSndOfLeft snd_invApp_t_app' CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.eqToHom_map CategoryTheory.eqToHom_trans CategoryTheory.Category.comp_id
snd_invApp_t_app' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CategoryTheory.Limits.pullback AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.GlueData.V toGlueData CategoryTheory.GlueData.J CategoryTheory.GlueData.U CategoryTheory.GlueData.f AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_left f_open TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor CategoryTheory.Limits.pullback.snd AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackSndOfLeft AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_right CategoryTheory.Limits.pullback.fst AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackFstOfRight Opposite.unop AlgebraicGeometry.PresheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.GlueData.f_hasPullback AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.GlueData.t CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c CategoryTheory.Functor.map CategoryTheory.Functor.op TopologicalSpace.Opens.map CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite CategoryTheory.GlueData.t'	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_right f_open AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_left AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackSndOfLeft AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackFstOfRight CategoryTheory.GlueData.f_hasPullback CategoryTheory.GlueData.t_fac CategoryTheory.GlueData.t'_isIso CategoryTheory.IsIso.inv_comp_eq Set.image_comp Set.preimage_image_eq CategoryTheory.ConcreteCategory.comp_apply AlgebraicGeometry.PresheafedSpace.comp_base CategoryTheory.GlueData.t_inv AlgebraicGeometry.PresheafedSpace.id_base CategoryTheory.ConcreteCategory.id_apply Set.image_eq_preimage_of_inverse CategoryTheory.IsIso.inv_hom_id CategoryTheory.IsIso.hom_inv_id AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.instIsIsoInvApp CategoryTheory.IsIso.eq_inv_comp AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_invApp CategoryTheory.Category.assoc CategoryTheory.NatTrans.naturality_assoc AlgebraicGeometry.PresheafedSpace.comp_c_app AlgebraicGeometry.PresheafedSpace.congr_app AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_naturality AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_naturality_assoc le_antisymm Set.image_preimage_subset Set.subset_inter_iff CategoryTheory.ConcreteCategory.congr_arg CategoryTheory.GlueData.t_fac_assoc CategoryTheory.Category.comp_id TopCat.id_app Set.image_preimage_eq_inter_range AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app'_assoc CategoryTheory.Functor.map_comp
snd_invApp_t_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CategoryTheory.Limits.pullback AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.GlueData.V toGlueData CategoryTheory.GlueData.J CategoryTheory.GlueData.U CategoryTheory.GlueData.f AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_left f_open TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor CategoryTheory.Limits.pullback.snd AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackSndOfLeft AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.GlueData.t CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c CategoryTheory.GlueData.f_hasPullback CategoryTheory.GlueData.t' AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_right CategoryTheory.Limits.pullback.fst AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackFstOfRight CategoryTheory.Functor.map CategoryTheory.Functor.op TopologicalSpace.Opens.map CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite Opposite.unop AlgebraicGeometry.PresheafedSpace.instTopologicalSpaceCarrierCarrier Quiver.Hom CategoryTheory.CategoryStruct.toQuiver snd_invApp_t_app'	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_right f_open AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_left AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackSndOfLeft CategoryTheory.GlueData.f_hasPullback AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackFstOfRight snd_invApp_t_app' CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' snd_invApp_t_app
ιInvApp_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CategoryTheory.GlueData.U AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toGlueData TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op CategoryTheory.Limits.limit CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory diagramOverOpen CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Limits.WalkingMultispan.right ιInvApp diagramOverOpenπ CategoryTheory.Functor.map CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram Opposite.unop CategoryTheory.Limits.colimit TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.Limits.colimit.ι CategoryTheory.GlueData.glued IsOpenMap.functor CategoryTheory.GlueData.ι CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits TopologicalSpace.Opens.ext Set.ext Set.image_congr CategoryTheory.Limits.hasColimitOfHasColimitsOfShape AlgebraicGeometry.PresheafedSpace.instHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self TopCat.instHasLimitsOfShapePresheaf AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.forget_preservesLimitsOfRight f_open CategoryTheory.GlueData.hasColimit_mapGlueData_diagram CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit AlgebraicGeometry.PresheafedSpace.instPreservesColimitsOfShapeTopCatForget CategoryTheory.GlueData.ι_gluedIso_inv TopCat.coe_comp TopCat.mono_iff_injective CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_inv TopCat.GlueData.ι_injective CategoryTheory.Limits.limit.lift_π Topology.IsOpenEmbedding.isOpenMap ι_isOpenEmbedding ι_image_preimage_eq CategoryTheory.GlueData.t_id AlgebraicGeometry.PresheafedSpace.congr_app AlgebraicGeometry.PresheafedSpace.id_c_app CategoryTheory.Functor.map_comp AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_naturality_assoc le_antisymm Set.image_preimage_subset Set.subset_inter_iff Set.range_eq_univ TopCat.epi_iff_surjective CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso AlgebraicGeometry.PresheafedSpace.base_isIso_of_iso CategoryTheory.GlueData.f_id Set.image_preimage_eq_inter_range AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app'_assoc CategoryTheory.eqToHom_op
ιIsOpenImmersion 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CategoryTheory.GlueData.U AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toGlueData CategoryTheory.GlueData.glued CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory AlgebraicGeometry.PresheafedSpace.instHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R TopCat.instHasLimitsOfShapePresheaf Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram CategoryTheory.GlueData.ι	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape AlgebraicGeometry.PresheafedSpace.instHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self TopCat.instHasLimitsOfShapePresheaf CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits ι_isOpenEmbedding Topology.IsOpenEmbedding.isOpenMap CategoryTheory.Limits.hasLimitOfHasLimitsOfShape AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_hom_π CategoryTheory.IsIso.comp_isIso CategoryTheory.Iso.isIso_hom componentwise_diagram_π_isIso
ι_image_preimage_eq 📖	mathematical	—	CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CategoryTheory.GlueData.glued AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toGlueData CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory AlgebraicGeometry.PresheafedSpace.instHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R TopCat.instHasLimitsOfShapePresheaf Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.GlueData.U TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.GlueData.ι IsOpenMap.functor Topology.IsOpenEmbedding.isOpenMap DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.instTopologicalSpaceCarrierCarrier ι_isOpenEmbedding CategoryTheory.GlueData.V AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor CategoryTheory.GlueData.f f_open CategoryTheory.GlueData.t	—	TopologicalSpace.Opens.ext CategoryTheory.Limits.hasColimitOfHasColimitsOfShape AlgebraicGeometry.PresheafedSpace.instHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self TopCat.instHasLimitsOfShapePresheaf CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits Topology.IsOpenEmbedding.isOpenMap ι_isOpenEmbedding f_open AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.forget_preservesLimitsOfRight CategoryTheory.GlueData.hasColimit_mapGlueData_diagram CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit AlgebraicGeometry.PresheafedSpace.instPreservesColimitsOfShapeTopCatForget CategoryTheory.GlueData.ι_gluedIso_inv TopCat.coe_comp Set.image_comp Set.preimage_comp Set.preimage_image_eq TopCat.mono_iff_injective CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_inv TopCat.GlueData.preimage_image_eq_image' Set.eq_preimage_iff_image_eq CategoryTheory.ConcreteCategory.bijective_of_isIso AlgebraicGeometry.PresheafedSpace.base_isIso_of_iso CategoryTheory.GlueData.t_isIso CategoryTheory.GlueData.t_inv Set.image_congr Set.image_id'
ι_isOpenEmbedding 📖	mathematical	—	Topology.IsOpenEmbedding TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CategoryTheory.GlueData.U AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toGlueData CategoryTheory.GlueData.glued CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory AlgebraicGeometry.PresheafedSpace.instHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R TopCat.instHasLimitsOfShapePresheaf Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram AlgebraicGeometry.PresheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.GlueData.ι	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape AlgebraicGeometry.PresheafedSpace.instHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self TopCat.instHasLimitsOfShapePresheaf CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.forget_preservesLimitsOfRight f_open CategoryTheory.GlueData.hasColimit_mapGlueData_diagram CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit AlgebraicGeometry.PresheafedSpace.instPreservesColimitsOfShapeTopCatForget CategoryTheory.GlueData.ι_gluedIso_inv TopCat.coe_comp Topology.IsOpenEmbedding.comp Homeomorph.isOpenEmbedding TopCat.GlueData.ι_isOpenEmbedding
ι_jointly_surjective 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CategoryTheory.GlueData.U AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toGlueData CategoryTheory.GlueData.glued CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory AlgebraicGeometry.PresheafedSpace.instHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R TopCat.instHasLimitsOfShapePresheaf Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.GlueData.ι	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape AlgebraicGeometry.PresheafedSpace.instHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self TopCat.instHasLimitsOfShapePresheaf CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.GlueData.ι_jointly_surjective CategoryTheory.Limits.comp_preservesColimit CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit AlgebraicGeometry.PresheafedSpace.instPreservesColimitsOfShapeTopCatForget CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint TopCat.instIsLeftAdjointForgetContinuousMapCarrier CategoryTheory.Limits.comp_preservesLimit AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.forget_preservesLimitsOfRight f_open CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits TopCat.forget_preservesLimits
π_ιInvApp_eq_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.limit Opposite CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toGlueData CategoryTheory.Category.opposite CategoryTheory.Limits.WalkingMultispan.instSmallCategory diagramOverOpen CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Functor.obj Opposite.op CategoryTheory.Limits.WalkingMultispan.right diagramOverOpenπ TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CategoryTheory.GlueData.U TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf ιInvAppπEqMap ιInvApp CategoryTheory.CategoryStruct.id	—	CategoryTheory.Limits.limit.hom_ext CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Limits.hasColimitOfHasColimitsOfShape AlgebraicGeometry.PresheafedSpace.instHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self TopCat.instHasLimitsOfShapePresheaf CategoryTheory.Limits.limit.w CategoryTheory.Category.assoc CategoryTheory.Category.id_comp π_ιInvApp_π
π_ιInvApp_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.limit Opposite CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toGlueData CategoryTheory.Category.opposite CategoryTheory.Limits.WalkingMultispan.instSmallCategory diagramOverOpen CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Functor.obj Opposite.op CategoryTheory.Limits.WalkingMultispan.right diagramOverOpenπ TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CategoryTheory.GlueData.U TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf ιInvAppπEqMap ιInvApp	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Limits.hasColimitOfHasColimitsOfShape AlgebraicGeometry.PresheafedSpace.instHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self TopCat.instHasLimitsOfShapePresheaf CategoryTheory.cancel_mono CategoryTheory.Category.comp_id CategoryTheory.mono_comp AlgebraicGeometry.PresheafedSpace.comp_c_app f_open Topology.IsOpenEmbedding.isOpenMap ι_isOpenEmbedding ι_image_preimage_eq CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso AlgebraicGeometry.PresheafedSpace.c_isIso_of_iso CategoryTheory.GlueData.t_isIso CategoryTheory.instMonoAppOfFunctor CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits CategoryTheory.instIsSplitMonoMap CategoryTheory.instIsIsoEqToHom CategoryTheory.Category.assoc CategoryTheory.Limits.limit.w_assoc CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.GlueData.t_id AlgebraicGeometry.PresheafedSpace.congr_app AlgebraicGeometry.PresheafedSpace.id_c_app CategoryTheory.Functor.map_comp_assoc AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_naturality_assoc Set.image_preimage_subset AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp_assoc CategoryTheory.NatTrans.naturality_assoc CategoryTheory.Functor.map_comp CategoryTheory.Limits.limit.w

AlgebraicGeometry.SheafedSpace.GlueData

Definitions

Name	Category	Theorems
isoPresheafedSpace 📖	CompOp	1 math math: ι_isoPresheafedSpace_inv
toGlueData 📖	CompOp	7 math math: f_open, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionCommRingCatFSheafedSpaceToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv, ι_isoPresheafedSpace_inv, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv_assoc, ιIsOpenImmersion, ι_jointly_surjective
toPresheafedSpaceGlueData 📖	CompOp	3 math math: ι_isoPresheafedSpace_inv, AlgebraicGeometry.Scheme.GlueData.ι_isoCarrier_inv, AlgebraicGeometry.Scheme.GlueData.instIsOpenImmersionCommRingCatFPresheafedSpaceToPresheafedSpaceGlueDataToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData
vPullbackConeIsLimit 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
f_open 📖	mathematical	—	AlgebraicGeometry.SheafedSpace.IsOpenImmersion CategoryTheory.GlueData.V AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory toGlueData CategoryTheory.GlueData.J CategoryTheory.GlueData.U CategoryTheory.GlueData.f	—	—
ιIsOpenImmersion 📖	mathematical	—	AlgebraicGeometry.SheafedSpace.IsOpenImmersion CategoryTheory.GlueData.U AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory toGlueData CategoryTheory.GlueData.glued CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory AlgebraicGeometry.SheafedSpace.instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram CategoryTheory.GlueData.ι	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape AlgebraicGeometry.SheafedSpace.instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits AlgebraicGeometry.PresheafedSpace.instHasColimitsOfShape TopCat.topCat_hasColimitsOfShape TopCat.instHasLimitsOfShapePresheaf ι_isoPresheafedSpace_inv AlgebraicGeometry.PresheafedSpace.GlueData.ιIsOpenImmersion AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.comp AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofIsIso CategoryTheory.Iso.isIso_inv
ι_isoPresheafedSpace_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.PresheafedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.GlueData.U AlgebraicGeometry.PresheafedSpace.GlueData.toGlueData toPresheafedSpaceGlueData CategoryTheory.GlueData.glued CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory AlgebraicGeometry.PresheafedSpace.instHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R TopCat.instHasLimitsOfShapePresheaf Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory toGlueData AlgebraicGeometry.SheafedSpace.instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite CategoryTheory.GlueData.ι CategoryTheory.Iso.inv isoPresheafedSpace CategoryTheory.InducedCategory.Hom.hom	—	CategoryTheory.GlueData.ι_gluedIso_inv CategoryTheory.Limits.hasColimitOfHasColimitsOfShape AlgebraicGeometry.SheafedSpace.instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit f_open AlgebraicGeometry.SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_right
ι_jointly_surjective 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace CategoryTheory.GlueData.U AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory toGlueData CategoryTheory.GlueData.glued CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory AlgebraicGeometry.SheafedSpace.instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram TopCat.carrier 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.GlueData.ι	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape AlgebraicGeometry.SheafedSpace.instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.GlueData.ι_jointly_surjective CategoryTheory.Limits.comp_preservesColimit CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit AlgebraicGeometry.SheafedSpace.instPreservesColimitsOfShapeTopCatForgetOfSmallOfHasLimitsOfShapeOpposite CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint TopCat.instIsLeftAdjointForgetContinuousMapCarrier CategoryTheory.Limits.comp_preservesLimit AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_forgetPreserves_of_right f_open CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits TopCat.forget_preservesLimits

---

← Back to Index