Gluing

📁 Source: Mathlib/AlgebraicGeometry/Gluing.lean

Statistics

Metric	Count
Definitions fromGlued, glueMorphisms, gluedCover, gluedCoverT', glued, gluedScheme, instCreatesColimitLocallyRingedSpaceWalkingMultispanProdJMultispanDiagramForgetToLocallyRingedSpace, isoCarrier, isoLocallyRingedSpace, openCover, toGlueData, toLocallyRingedSpaceGlueData, vPullbackCone, vPullbackConeIsLimit, ι, V, cocone, glueData, instCreatesColimitLocallyRingedSpaceForgetToLocallyRingedSpace, isColimit, isColimitForgetToLocallyRingedSpace, openCover, t, tAux	24
Theorems fromGlued_injective, fromGlued_isOpenEmbedding, fromGlued_open_map, gluedCoverT'_fst_fst, gluedCoverT'_fst_fst_assoc, gluedCoverT'_fst_snd, gluedCoverT'_fst_snd_assoc, gluedCoverT'_snd_fst, gluedCoverT'_snd_fst_assoc, gluedCoverT'_snd_snd, gluedCoverT'_snd_snd_assoc, gluedCover_J, gluedCover_U, gluedCover_V, gluedCover_f, gluedCover_t, gluedCover_t', glued_cover_cocycle, glued_cover_cocycle_fst, glued_cover_cocycle_snd, hom_ext, instEpiTopCatBaseCommRingCatFromGlued, instIsIsoCommRingCatStalkMapFromGlued, instIsIsoFromGlued, instIsOpenImmersionFromGlued, isOpenEmbedding_fromGlued, isOpenMap_fromGlued, ι_fromGlued, ι_fromGlued_assoc, ι_glueMorphisms, ι_glueMorphisms_assoc, f_open, glue_condition, glue_condition_assoc, instHasMulticoequalizerDiagram, instIsOpenImmersionCommRingCatFPresheafedSpaceToPresheafedSpaceGlueDataToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData, instIsOpenImmersionCommRingCatFSheafedSpaceToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData, instIsOpenImmersionFLocallyRingedSpaceToLocallyRingedSpaceGlueData, instIsOpenImmersionιLocallyRingedSpaceToLocallyRingedSpaceGlueData, instPreservesColimitTopCatWalkingMultispanProdJMultispanDiagramForgetToTop, instPreservesColimitWalkingMultispanProdJMultispanDiagramForget, isOpen_iff, openCover_I₀, openCover_X, openCover_f, ι_eq_iff, ι_isOpenImmersion, ι_isoCarrier_inv, ι_isoLocallyRingedSpace_inv, ι_jointly_surjective, V_self, exists_of_pullback_V_V, fst_inv_eq_snd_inv, glueDataι_naturality, homOfLE_tAux, homOfLE_tAux_assoc, instHasColimit, instIsLocallyDirectedWidePushoutShapeCompForgetOfIsOpenImmersionMap, instIsOpenImmersionι, instPreservesColimitLocallyRingedSpaceForgetToLocallyRingedSpace, openCover_I₀, openCover_X, openCover_f, t_id, ι_eq_ι_iff, ι_jointly_surjective, hom_ext_of_forall, instIsLocalAtTargetIsomorphismsZariskiPrecoverage	68
Total	92

AlgebraicGeometry.Scheme

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_ext_of_forall 📖	—	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory Opens.toScheme Opens.ι	—	—	presieve₀_mem_precoverage_iff Opens.range_ι Opens.instIsOpenImmersionι Cover.hom_ext
instIsLocalAtTargetIsomorphismsZariskiPrecoverage 📖	mathematical	—	CategoryTheory.MorphismProperty.IsLocalAtTarget AlgebraicGeometry.Scheme instCategory CategoryTheory.MorphismProperty.isomorphisms zariskiPrecoverage instHasPullbacksPrecoverageOfHasPullbacks AlgebraicGeometry.IsOpenImmersion instHasPullbacksIsOpenImmersion	—	CategoryTheory.MorphismProperty.IsLocalAtTarget.mk_of_isStableUnderBaseChange instHasPullbacksPrecoverageOfHasPullbacks instHasPullbacksIsOpenImmersion CategoryTheory.MorphismProperty.IsStableUnderBaseChange.isomorphisms CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1 CategoryTheory.Precoverage.ZeroHypercover.instHasPullbacksPresieve₀OfHasPullbacks AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right instIsOpenImmersionF AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.pullback.condition CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.cancel_epi CategoryTheory.epi_comp CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom CategoryTheory.Limits.pullback.map_isIso CategoryTheory.IsIso.id CategoryTheory.Category.assoc CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.IsIso.hom_inv_id_assoc CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst_assoc CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_snd_assoc Cover.hom_ext instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange CategoryTheory.Limits.pullback.condition_assoc Cover.ι_glueMorphisms Cover.ι_glueMorphisms_assoc CategoryTheory.IsIso.inv_hom_id_assoc

AlgebraicGeometry.Scheme.Cover

Definitions

Name	Category	Theorems
fromGlued 📖	CompOp	11 math math: isOpenMap_fromGlued, instIsIsoFromGlued, instIsIsoCommRingCatStalkMapFromGlued, isOpenEmbedding_fromGlued, ι_fromGlued_assoc, fromGlued_isOpenEmbedding, instEpiTopCatBaseCommRingCatFromGlued, instIsOpenImmersionFromGlued, fromGlued_open_map, ι_fromGlued, fromGlued_injective
glueMorphisms 📖	CompOp	2 math math: ι_glueMorphisms, ι_glueMorphisms_assoc
gluedCover 📖	CompOp	17 math math: isOpenMap_fromGlued, instIsIsoFromGlued, gluedCover_t, gluedCover_U, instIsIsoCommRingCatStalkMapFromGlued, gluedCover_V, isOpenEmbedding_fromGlued, ι_fromGlued_assoc, gluedCover_J, gluedCover_f, fromGlued_isOpenEmbedding, instEpiTopCatBaseCommRingCatFromGlued, instIsOpenImmersionFromGlued, fromGlued_open_map, gluedCover_t', ι_fromGlued, fromGlued_injective
gluedCoverT' 📖	CompOp	12 math math: gluedCoverT'_snd_snd_assoc, glued_cover_cocycle_fst, glued_cover_cocycle, gluedCoverT'_fst_fst, gluedCoverT'_snd_fst, glued_cover_cocycle_snd, gluedCoverT'_snd_fst_assoc, gluedCoverT'_fst_snd_assoc, gluedCoverT'_snd_snd, gluedCoverT'_fst_snd, gluedCoverT'_fst_fst_assoc, gluedCover_t'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fromGlued_injective 📖	mathematical	—	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Scheme.GlueData.glued gluedCover DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' fromGlued	—	AlgebraicGeometry.Scheme.GlueData.ι_jointly_surjective AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeTopCatWalkingCospanCospanForgetToTop_1 AlgebraicGeometry.Scheme.GlueData.instHasMulticoequalizerDiagram AlgebraicGeometry.Scheme.GlueData.ι_eq_iff ι_fromGlued CategoryTheory.ConcreteCategory.comp_apply CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp CategoryTheory.Limits.hasPullback_symmetry CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst
fromGlued_isOpenEmbedding 📖	mathematical	—	Topology.IsOpenEmbedding TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Scheme.GlueData.glued gluedCover AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' fromGlued	—	isOpenEmbedding_fromGlued
fromGlued_open_map 📖	mathematical	—	IsOpenMap TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Scheme.GlueData.glued gluedCover AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' fromGlued	—	isOpenMap_fromGlued
gluedCoverT'_fst_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Limits.pullback.fst AlgebraicGeometry.IsOpenImmersion.instFstScheme gluedCoverT' CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Category.assoc CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst_assoc CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_fst CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst_assoc
gluedCoverT'_fst_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Limits.pullback.fst AlgebraicGeometry.IsOpenImmersion.instFstScheme gluedCoverT' CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' gluedCoverT'_fst_fst
gluedCoverT'_fst_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Limits.pullback.fst AlgebraicGeometry.IsOpenImmersion.instFstScheme gluedCoverT' CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Category.assoc CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst_assoc CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_snd CategoryTheory.Limits.limit.lift_π CategoryTheory.Category.comp_id CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_snd
gluedCoverT'_fst_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Limits.pullback.fst AlgebraicGeometry.IsOpenImmersion.instFstScheme gluedCoverT' CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' gluedCoverT'_fst_snd
gluedCoverT'_snd_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Limits.pullback.fst AlgebraicGeometry.IsOpenImmersion.instFstScheme gluedCoverT' CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Category.assoc CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd_assoc CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_fst_assoc CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst_assoc
gluedCoverT'_snd_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Limits.pullback.fst AlgebraicGeometry.IsOpenImmersion.instFstScheme gluedCoverT' CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' gluedCoverT'_snd_fst
gluedCoverT'_snd_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Limits.pullback.fst AlgebraicGeometry.IsOpenImmersion.instFstScheme gluedCoverT' CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Category.assoc CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd_assoc CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_fst_assoc CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst_assoc
gluedCoverT'_snd_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Limits.pullback.fst AlgebraicGeometry.IsOpenImmersion.instFstScheme gluedCoverT' CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' gluedCoverT'_snd_snd
gluedCover_J 📖	mathematical	—	CategoryTheory.GlueData.J AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.GlueData.toGlueData gluedCover CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion	—	—
gluedCover_U 📖	mathematical	—	CategoryTheory.GlueData.U AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.GlueData.toGlueData gluedCover CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion	—	—
gluedCover_V 📖	mathematical	—	CategoryTheory.GlueData.V AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.GlueData.toGlueData gluedCover CategoryTheory.Limits.pullback CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.PreZeroHypercover.f	—	—
gluedCover_f 📖	mathematical	—	CategoryTheory.GlueData.f AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.GlueData.toGlueData gluedCover CategoryTheory.Limits.pullback.fst CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.PreZeroHypercover.f	—	—
gluedCover_t 📖	mathematical	—	CategoryTheory.GlueData.t AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.GlueData.toGlueData gluedCover CategoryTheory.Iso.hom CategoryTheory.Limits.pullback CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.PreZeroHypercover.f CategoryTheory.Limits.pullbackSymmetry	—	—
gluedCover_t' 📖	mathematical	—	CategoryTheory.GlueData.t' AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.GlueData.toGlueData gluedCover gluedCoverT'	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.IsOpenImmersion.instFstScheme
glued_cover_cocycle 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Limits.pullback.fst AlgebraicGeometry.IsOpenImmersion.instFstScheme gluedCoverT' CategoryTheory.CategoryStruct.id	—	CategoryTheory.Limits.pullback.hom_ext AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Category.id_comp CategoryTheory.Category.assoc glued_cover_cocycle_fst glued_cover_cocycle_snd
glued_cover_cocycle_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Limits.pullback.fst AlgebraicGeometry.IsOpenImmersion.instFstScheme gluedCoverT'	—	CategoryTheory.Limits.pullback.hom_ext AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Category.assoc gluedCoverT'_fst_fst gluedCoverT'_fst_snd gluedCoverT'_snd_snd
glued_cover_cocycle_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Limits.pullback.fst AlgebraicGeometry.IsOpenImmersion.instFstScheme gluedCoverT' CategoryTheory.Limits.pullback.snd	—	CategoryTheory.Limits.pullback.hom_ext AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Category.assoc gluedCoverT'_snd_fst gluedCoverT'_fst_snd gluedCoverT'_snd_snd CategoryTheory.Limits.pullback.condition
hom_ext 📖	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.PreZeroHypercover.f	—	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso instIsIsoFromGlued CategoryTheory.Limits.Multicoequalizer.hom_ext AlgebraicGeometry.Scheme.GlueData.instHasMulticoequalizerDiagram fromGlued.eq_1 CategoryTheory.Limits.Multicoequalizer.π_desc_assoc AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage
instEpiTopCatBaseCommRingCatFromGlued 📖	mathematical	—	CategoryTheory.Epi TopCat TopCat.instCategory AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Scheme.GlueData.glued gluedCover AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' fromGlued	—	TopCat.epi_iff_surjective AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage covers CategoryTheory.ConcreteCategory.comp_apply ι_fromGlued
instIsIsoCommRingCatStalkMapFromGlued 📖	mathematical	—	CategoryTheory.IsIso CommRingCat CommRingCat.instCategory TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf DFunLike.coe AlgebraicGeometry.Scheme.GlueData.glued gluedCover TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' fromGlued AlgebraicGeometry.Scheme.Hom.stalkMap	—	CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.Scheme.GlueData.ι_jointly_surjective Inseparable.of_eq ι_fromGlued AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom AlgebraicGeometry.IsOpenImmersion.instIsIsoCommRingCatStalkMap AlgebraicGeometry.Scheme.GlueData.ι_isOpenImmersion CategoryTheory.IsIso.eq_comp_inv AlgebraicGeometry.Scheme.Hom.stalkMap_comp CategoryTheory.IsIso.comp_isIso CategoryTheory.Iso.isIso_hom AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.IsIso.inv_isIso
instIsIsoFromGlued 📖	mathematical	—	CategoryTheory.IsIso AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.GlueData.glued gluedCover fromGlued	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.to_iso AlgebraicGeometry.instIsOpenImmersionCommRingCatOfIsOpenImmersion instIsOpenImmersionFromGlued instEpiTopCatBaseCommRingCatFromGlued CategoryTheory.isIso_of_reflects_iso CategoryTheory.reflectsIsomorphisms_comp CategoryTheory.reflectsIsomorphisms_of_full_and_faithful AlgebraicGeometry.Scheme.instFullLocallyRingedSpaceForgetToLocallyRingedSpace AlgebraicGeometry.Scheme.instFaithfulLocallyRingedSpaceForgetToLocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instReflectsIsomorphismsSheafedSpaceCommRingCatForgetToSheafedSpace AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_full AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_faithful
instIsOpenImmersionFromGlued 📖	mathematical	—	AlgebraicGeometry.IsOpenImmersion AlgebraicGeometry.Scheme.GlueData.glued gluedCover fromGlued	—	AlgebraicGeometry.IsOpenImmersion.of_isIso_stalkMap isOpenEmbedding_fromGlued instIsIsoCommRingCatStalkMapFromGlued
isOpenEmbedding_fromGlued 📖	mathematical	—	Topology.IsOpenEmbedding TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Scheme.GlueData.glued gluedCover AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' fromGlued	—	Topology.IsOpenEmbedding.of_continuous_injective_isOpenMap AlgebraicGeometry.Scheme.Hom.continuous fromGlued_injective isOpenMap_fromGlued
isOpenMap_fromGlued 📖	mathematical	—	IsOpenMap TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Scheme.GlueData.glued gluedCover AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' fromGlued	—	isOpen_iff_forall_mem_open AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage Set.inter_subset_left Set.image_preimage_eq_inter_range Topology.IsOpenEmbedding.isOpenMap AlgebraicGeometry.Scheme.Hom.isOpenEmbedding AlgebraicGeometry.Scheme.instIsOpenImmersionF Set.image_congr Set.preimage_image_eq fromGlued_injective AlgebraicGeometry.Scheme.GlueData.isOpen_iff covers
ι_fromGlued 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.GlueData.U AlgebraicGeometry.Scheme.GlueData.toGlueData gluedCover AlgebraicGeometry.Scheme.GlueData.glued AlgebraicGeometry.Scheme.GlueData.ι fromGlued CategoryTheory.PreZeroHypercover.f CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion	—	CategoryTheory.Limits.Multicoequalizer.π_desc AlgebraicGeometry.Scheme.GlueData.instHasMulticoequalizerDiagram
ι_fromGlued_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.GlueData.U AlgebraicGeometry.Scheme.GlueData.toGlueData gluedCover AlgebraicGeometry.Scheme.GlueData.glued AlgebraicGeometry.Scheme.GlueData.ι fromGlued CategoryTheory.PreZeroHypercover.f CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_fromGlued
ι_glueMorphisms 📖	mathematical	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd	glueMorphisms	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF hom_ext AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage CategoryTheory.Limits.pullback.condition_assoc CategoryTheory.Category.assoc CategoryTheory.IsIso.hom_inv_id_assoc CategoryTheory.Limits.colimit.ι_desc AlgebraicGeometry.Scheme.GlueData.instHasMulticoequalizerDiagram
ι_glueMorphisms_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd	glueMorphisms	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_glueMorphisms

AlgebraicGeometry.Scheme.GlueData

Definitions

Name	Category	Theorems
glued 📖	CompOp	57 math math: oneHypercover_I₁, AlgebraicGeometry.Scheme.Cover.isOpenMap_fromGlued, AlgebraicGeometry.Scheme.Cover.instIsIsoFromGlued, AlgebraicGeometry.Scheme.LocalRepresentability.instIsLocallySurjectiveHomYonedaGluedToSheafOfIsLocallySurjectiveZariskiTopologyDescFunctorOppositeType, AlgebraicGeometry.Scheme.Cover.instIsIsoCommRingCatStalkMapFromGlued, AlgebraicGeometry.Scheme.Pullback.gluedLift_p1, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_snd, openCover_f, AlgebraicGeometry.Scheme.Cover.isOpenEmbedding_fromGlued, AlgebraicGeometry.Scheme.Cover.ι_fromGlued_assoc, glue_condition, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_fst_assoc, AlgebraicGeometry.Scheme.Pullback.gluedLift_p2, isOpen_iff, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_fst_assoc, AlgebraicGeometry.Scheme.LocalRepresentability.comp_toGlued_eq, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_ι_assoc, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_fst, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_snd_assoc, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_openCover_map, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_fst, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_fst_assoc, openCover_X, AlgebraicGeometry.Scheme.LocalRepresentability.yoneda_toGlued_yonedaGluedToSheaf_assoc, oneHypercover_p₂, sheafValGluedMk_val, AlgebraicGeometry.Scheme.LocalRepresentability.instIsIsoSheafZariskiTopologyTypeYonedaGluedToSheaf, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_snd_assoc, AlgebraicGeometry.Scheme.LocalRepresentability.yoneda_toGlued_yonedaGluedToSheaf, ι_isoCarrier_inv, AlgebraicGeometry.Scheme.IsLocallyDirected.glueDataι_naturality, AlgebraicGeometry.Scheme.LocalRepresentability.instIsLocallyInjectiveHomYonedaGluedToSheaf, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_snd, AlgebraicGeometry.Scheme.Cover.fromGlued_isOpenEmbedding, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_ι, oneHypercover_X, ι_isoLocallyRingedSpace_inv, AlgebraicGeometry.Scheme.LocalRepresentability.instIsOpenImmersionToGlued, AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf_app_comp, glue_condition_assoc, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_snd_assoc, oneHypercover_I₀, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_snd, AlgebraicGeometry.Scheme.Cover.instEpiTopCatBaseCommRingCatFromGlued, openCover_I₀, oneHypercover_f, AlgebraicGeometry.Scheme.Pullback.p_comm, AlgebraicGeometry.Scheme.Cover.instIsOpenImmersionFromGlued, oneHypercover_Y, oneHypercover_p₁, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_fst, ι_jointly_surjective, AlgebraicGeometry.Scheme.Pullback.lift_comp_ι, AlgebraicGeometry.Scheme.Cover.fromGlued_open_map, AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf_app_toGlued, AlgebraicGeometry.Scheme.Cover.ι_fromGlued, AlgebraicGeometry.Scheme.Cover.fromGlued_injective
gluedScheme 📖	CompOp	—
instCreatesColimitLocallyRingedSpaceWalkingMultispanProdJMultispanDiagramForgetToLocallyRingedSpace 📖	CompOp	—
isoCarrier 📖	CompOp	1 math math: ι_isoCarrier_inv
isoLocallyRingedSpace 📖	CompOp	1 math math: ι_isoLocallyRingedSpace_inv
openCover 📖	CompOp	4 math math: openCover_f, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_openCover_map, openCover_X, openCover_I₀
toGlueData 📖	CompOp	50 math math: AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd_assoc, AlgebraicGeometry.Scheme.Cover.gluedCover_t, AlgebraicGeometry.Scheme.Cover.gluedCover_U, AlgebraicGeometry.Scheme.Pullback.gluing_t, instHasMulticoequalizerDiagram, AlgebraicGeometry.Scheme.Cover.gluedCover_V, AlgebraicGeometry.Scheme.Cover.ι_fromGlued_assoc, glue_condition, f_open, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_fst_assoc, isOpen_iff, instPreservesColimitTopCatWalkingMultispanProdJMultispanDiagramForgetToTop, AlgebraicGeometry.Scheme.Pullback.gluing_J, AlgebraicGeometry.Scheme.Pullback.gluing_f, instPreservesColimitWalkingMultispanProdJMultispanDiagramForget, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_ι_assoc, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_fst, ι_isOpenImmersion, AlgebraicGeometry.Scheme.Cover.gluedCover_J, ι_eq_iff, openCover_X, AlgebraicGeometry.Scheme.Pullback.gluing_U, oneHypercover_p₂, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_V, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_f, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_t', AlgebraicGeometry.Scheme.Cover.gluedCover_f, ι_isoCarrier_inv, AlgebraicGeometry.Scheme.Pullback.gluing_ι, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst_assoc, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_ι, oneHypercover_X, ι_isoLocallyRingedSpace_inv, glue_condition_assoc, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_snd_assoc, oneHypercover_I₀, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_snd, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_J, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_t, openCover_I₀, oneHypercover_Y, AlgebraicGeometry.Scheme.Pullback.gluing_t', oneHypercover_p₁, ι_jointly_surjective, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_U, AlgebraicGeometry.Scheme.Pullback.gluing_V, AlgebraicGeometry.Scheme.Cover.gluedCover_t', AlgebraicGeometry.Scheme.Cover.ι_fromGlued, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst
toLocallyRingedSpaceGlueData 📖	CompOp	6 math math: instIsOpenImmersionCommRingCatFSheafedSpaceToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData, instIsOpenImmersionιLocallyRingedSpaceToLocallyRingedSpaceGlueData, ι_isoCarrier_inv, instIsOpenImmersionCommRingCatFPresheafedSpaceToPresheafedSpaceGlueDataToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData, ι_isoLocallyRingedSpace_inv, instIsOpenImmersionFLocallyRingedSpaceToLocallyRingedSpaceGlueData
vPullbackCone 📖	CompOp	—
vPullbackConeIsLimit 📖	CompOp	—
ι 📖	CompOp	19 math math: openCover_f, AlgebraicGeometry.Scheme.Cover.ι_fromGlued_assoc, glue_condition, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_fst_assoc, isOpen_iff, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_fst, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_fst, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_fst_assoc, sheafValGluedMk_val, ι_isoCarrier_inv, AlgebraicGeometry.Scheme.IsLocallyDirected.glueDataι_naturality, AlgebraicGeometry.Scheme.Pullback.gluing_ι, glue_condition_assoc, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_snd_assoc, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_snd, oneHypercover_f, ι_jointly_surjective, AlgebraicGeometry.Scheme.Pullback.lift_comp_ι, AlgebraicGeometry.Scheme.Cover.ι_fromGlued

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
f_open 📖	mathematical	—	AlgebraicGeometry.IsOpenImmersion CategoryTheory.GlueData.V AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory toGlueData CategoryTheory.GlueData.J CategoryTheory.GlueData.U CategoryTheory.GlueData.f	—	—
glue_condition 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.GlueData.V toGlueData CategoryTheory.GlueData.J glued CategoryTheory.GlueData.t CategoryTheory.GlueData.U CategoryTheory.GlueData.f ι	—	CategoryTheory.GlueData.glue_condition instHasMulticoequalizerDiagram
glue_condition_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.GlueData.V toGlueData CategoryTheory.GlueData.J CategoryTheory.GlueData.t CategoryTheory.GlueData.U CategoryTheory.GlueData.f glued ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' glue_condition
instHasMulticoequalizerDiagram 📖	mathematical	—	CategoryTheory.Limits.HasMulticoequalizer AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J toGlueData CategoryTheory.GlueData.diagram	—	CategoryTheory.hasColimit_of_created CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize AlgebraicGeometry.LocallyRingedSpace.instHasColimits
instIsOpenImmersionCommRingCatFPresheafedSpaceToPresheafedSpaceGlueDataToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.IsOpenImmersion CommRingCat CommRingCat.instCategory CategoryTheory.GlueData.V AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces AlgebraicGeometry.PresheafedSpace.GlueData.toGlueData AlgebraicGeometry.SheafedSpace.GlueData.toPresheafedSpaceGlueData AlgebraicGeometry.LocallyRingedSpace.GlueData.toSheafedSpaceGlueData toLocallyRingedSpaceGlueData CategoryTheory.GlueData.J CategoryTheory.GlueData.U CategoryTheory.GlueData.f	—	f_open
instIsOpenImmersionCommRingCatFSheafedSpaceToSheafedSpaceGlueDataToLocallyRingedSpaceGlueData 📖	mathematical	—	AlgebraicGeometry.SheafedSpace.IsOpenImmersion CommRingCat CommRingCat.instCategory CategoryTheory.GlueData.V AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.SheafedSpace.GlueData.toGlueData AlgebraicGeometry.LocallyRingedSpace.GlueData.toSheafedSpaceGlueData toLocallyRingedSpaceGlueData CategoryTheory.GlueData.J CategoryTheory.GlueData.U CategoryTheory.GlueData.f	—	f_open
instIsOpenImmersionFLocallyRingedSpaceToLocallyRingedSpaceGlueData 📖	mathematical	—	AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion CategoryTheory.GlueData.V AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.LocallyRingedSpace.GlueData.toGlueData toLocallyRingedSpaceGlueData CategoryTheory.GlueData.J CategoryTheory.GlueData.U CategoryTheory.GlueData.f	—	f_open
instIsOpenImmersionιLocallyRingedSpaceToLocallyRingedSpaceGlueData 📖	mathematical	—	AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion CategoryTheory.GlueData.U AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.LocallyRingedSpace.GlueData.toGlueData toLocallyRingedSpaceGlueData 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.ι	—	AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isOpenImmersion
instPreservesColimitTopCatWalkingMultispanProdJMultispanDiagramForgetToTop 📖	mathematical	—	CategoryTheory.Limits.PreservesColimit AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory TopCat TopCat.instCategory CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J toGlueData CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram AlgebraicGeometry.Scheme.forgetToTop	—	CategoryTheory.Limits.comp_preservesColimit CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize AlgebraicGeometry.LocallyRingedSpace.instHasColimits 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
instPreservesColimitWalkingMultispanProdJMultispanDiagramForget 📖	mathematical	—	CategoryTheory.Limits.PreservesColimit AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.types CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J toGlueData CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram AlgebraicGeometry.Scheme.forget	—	CategoryTheory.Limits.comp_preservesColimit instPreservesColimitTopCatWalkingMultispanProdJMultispanDiagramForgetToTop CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint TopCat.instIsLeftAdjointForgetContinuousMapCarrier
isOpen_iff 📖	mathematical	—	IsOpen TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace glued AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.GlueData.U AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory toGlueData Set.preimage DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' ι	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self Homeomorph.isOpen_preimage TopCat.GlueData.isOpen_iff Set.preimage_comp ι_isoCarrier_inv
openCover_I₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory glued CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion openCover CategoryTheory.GlueData.J toGlueData	—	—
openCover_X 📖	mathematical	—	CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory glued CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion openCover CategoryTheory.GlueData.U toGlueData	—	—
openCover_f 📖	mathematical	—	CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory glued CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion openCover ι	—	—
ι_eq_iff 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.GlueData.U AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory toGlueData CategoryTheory.GlueData.glued instHasMulticoequalizerDiagram TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.GlueData.ι Rel CategoryTheory.GlueData.J	—	instHasMulticoequalizerDiagram CategoryTheory.Limits.hasColimitOfHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self TopCat.mono_iff_injective CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_inv CategoryTheory.ConcreteCategory.comp_apply ι_isoCarrier_inv TopCat.GlueData.ι_eq_iff_rel
ι_isOpenImmersion 📖	mathematical	—	AlgebraicGeometry.IsOpenImmersion CategoryTheory.GlueData.U AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory toGlueData CategoryTheory.GlueData.glued instHasMulticoequalizerDiagram CategoryTheory.GlueData.ι	—	instHasMulticoequalizerDiagram AlgebraicGeometry.IsOpenImmersion.eq_1 CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize AlgebraicGeometry.LocallyRingedSpace.instHasColimits ι_isoLocallyRingedSpace_inv AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.comp instIsOpenImmersionιLocallyRingedSpaceToLocallyRingedSpaceGlueData AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.of_isIso CategoryTheory.Iso.isIso_inv
ι_isoCarrier_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory CategoryTheory.GlueData.U TopCat.GlueData.toGlueData AlgebraicGeometry.PresheafedSpace.GlueData.toTopGlueData CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.GlueData.toPresheafedSpaceGlueData AlgebraicGeometry.LocallyRingedSpace.GlueData.toSheafedSpaceGlueData toLocallyRingedSpaceGlueData CategoryTheory.GlueData.glued CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.MultispanShape.prod CategoryTheory.GlueData.J CategoryTheory.Limits.WalkingMultispan.instSmallCategory TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CategoryTheory.Limits.MultispanShape.L CategoryTheory.Limits.MultispanShape.R CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.GlueData.diagram AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace glued CategoryTheory.GlueData.ι CategoryTheory.Iso.inv isoCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory toGlueData AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' ι	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape TopCat.topCat_hasColimitsOfShape CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR UnivLE.small UnivLE.self CommRingCat.hasLimits CategoryTheory.Iso.trans_inv CategoryTheory.GlueData.hasColimit_mapGlueData_diagram CategoryTheory.GlueData.ι_gluedIso_inv_assoc CategoryTheory.Functor.mapIso_inv AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_map AlgebraicGeometry.PresheafedSpace.forget_map AlgebraicGeometry.PresheafedSpace.comp_base CategoryTheory.Category.assoc AlgebraicGeometry.SheafedSpace.instHasColimitsOfShapeOfSmallOfHasLimitsOfShapeOpposite CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits AlgebraicGeometry.PresheafedSpace.instHasColimitsOfShape TopCat.instHasLimitsOfShapePresheaf AlgebraicGeometry.SheafedSpace.GlueData.ι_isoPresheafedSpace_inv CategoryTheory.InducedCategory.comp_hom CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize AlgebraicGeometry.LocallyRingedSpace.instHasColimits CommRingCat.hasLimitsOfShape Opposite.small AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv instHasMulticoequalizerDiagram ι_isoLocallyRingedSpace_inv
ι_isoLocallyRingedSpace_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.LocallyRingedSpace.instCategory CategoryTheory.GlueData.U AlgebraicGeometry.LocallyRingedSpace.GlueData.toGlueData toLocallyRingedSpaceGlueData 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 AlgebraicGeometry.Scheme.toLocallyRingedSpace glued CategoryTheory.GlueData.ι CategoryTheory.Iso.inv isoLocallyRingedSpace AlgebraicGeometry.Scheme.Hom.toLRSHom AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory toGlueData instHasMulticoequalizerDiagram	—	CategoryTheory.GlueData.ι_gluedIso_inv instHasMulticoequalizerDiagram CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize AlgebraicGeometry.LocallyRingedSpace.instHasColimits AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace_1 f_open
ι_jointly_surjective 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.GlueData.U AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory toGlueData glued TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' ι	—	instHasMulticoequalizerDiagram CategoryTheory.GlueData.ι_jointly_surjective instPreservesColimitWalkingMultispanProdJMultispanDiagramForget AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeWalkingCospanCospanForget_1 f_open

AlgebraicGeometry.Scheme.IsLocallyDirected

Definitions

Name	Category	Theorems
V 📖	CompOp	3 math math: exists_of_pullback_V_V, V_self, t_id
cocone 📖	CompOp	—
glueData 📖	CompOp	1 math math: glueDataι_naturality
instCreatesColimitLocallyRingedSpaceForgetToLocallyRingedSpace 📖	CompOp	—
isColimit 📖	CompOp	—
isColimitForgetToLocallyRingedSpace 📖	CompOp	—
openCover 📖	CompOp	3 math math: openCover_f, openCover_I₀, openCover_X
t 📖	CompOp	1 math math: t_id
tAux 📖	CompOp	2 math math: homOfLE_tAux, homOfLE_tAux_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
V_self 📖	mathematical	AlgebraicGeometry.IsOpenImmersion CategoryTheory.Functor.obj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.map	V Top.top AlgebraicGeometry.Scheme.Opens OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	top_le_iff le_iSup_of_le CategoryTheory.Functor.map_id AlgebraicGeometry.Scheme.Hom.opensRange.congr_simp AlgebraicGeometry.Scheme.Hom.opensRange_of_isIso CategoryTheory.IsIso.id
exists_of_pullback_V_V 📖	mathematical	AlgebraicGeometry.IsOpenImmersion CategoryTheory.Functor.obj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.map	CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme.Opens.toScheme V AlgebraicGeometry.Scheme.Opens.ι AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Scheme.Hom.opensRange iSup AlgebraicGeometry.Scheme.Opens Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup TopologicalSpace.Opens.instCompleteLattice TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Iso.hom AlgebraicGeometry.Scheme.Hom.isoOpensRange AlgebraicGeometry.Scheme.homOfLE le_iSup_of_le le_rfl PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Limits.pullback.snd DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	—	AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι le_iSup_of_le le_rfl TopologicalSpace.Opens.mem_iSup CategoryTheory.Functor.exists_map_eq_of_isLocallyDirected CategoryTheory.Limits.pullback.condition CategoryTheory.Category.assoc AlgebraicGeometry.Scheme.homOfLE_ι AlgebraicGeometry.Scheme.Hom.isoOpensRange_hom_ι CategoryTheory.Functor.map_comp AlgebraicGeometry.IsOpenImmersion.of_comp AlgebraicGeometry.IsOpenImmersion.instFstScheme CategoryTheory.Limits.limit.lift_π AlgebraicGeometry.IsOpenImmersion.comp AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Iso.isIso_hom AlgebraicGeometry.instIsOpenImmersionHomOfLE Topology.IsEmbedding.injective Topology.IsOpenEmbedding.toIsEmbedding AlgebraicGeometry.Scheme.Hom.isOpenEmbedding AlgebraicGeometry.Scheme.Hom.comp_apply CategoryTheory.Limits.pullback.lift_fst_assoc
fst_inv_eq_snd_inv 📖	mathematical	AlgebraicGeometry.IsOpenImmersion CategoryTheory.Functor.obj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.map Quiver.IsThin CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.Scheme.Hom.opensRange Quiver.Hom	CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Scheme.homOfLE AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.instIsOpenImmersionHomOfLE CategoryTheory.Limits.pullback.fst CategoryTheory.Iso.inv AlgebraicGeometry.Scheme.Hom.isoOpensRange CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.Scheme.hom_ext_of_forall AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right AlgebraicGeometry.instIsOpenImmersionHomOfLE CategoryTheory.Functor.exists_map_eq_of_isLocallyDirected CategoryTheory.Category.assoc AlgebraicGeometry.Scheme.Hom.isoOpensRange_inv_comp AlgebraicGeometry.Scheme.homOfLE_ι CategoryTheory.Limits.pullback.condition CategoryTheory.cancel_mono AlgebraicGeometry.IsOpenImmersion.mono AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι AlgebraicGeometry.Scheme.Hom.isoOpensRange_hom_ι CategoryTheory.Limits.pullback.lift_fst AlgebraicGeometry.IsOpenImmersion.comp AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Iso.isIso_hom AlgebraicGeometry.IsOpenImmersion.of_comp AlgebraicGeometry.IsOpenImmersion.instFstScheme Topology.IsEmbedding.injective Topology.IsOpenEmbedding.toIsEmbedding AlgebraicGeometry.Scheme.Hom.isOpenEmbedding AlgebraicGeometry.Scheme.inv_hom_apply CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso AlgebraicGeometry.Scheme.Hom.isoOpensRange_hom_ι_assoc CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Iso.hom_inv_id_assoc
glueDataι_naturality 📖	mathematical	AlgebraicGeometry.IsOpenImmersion CategoryTheory.Functor.obj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.map Quiver.IsThin CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp DFunLike.coe Equiv Shrink EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivShrink AlgebraicGeometry.Scheme.GlueData.glued glueData AlgebraicGeometry.Scheme.GlueData.ι	—	top_le_iff le_iSup_of_le CategoryTheory.Functor.map_id AlgebraicGeometry.Scheme.Hom.opensRange.congr_simp AlgebraicGeometry.Scheme.Hom.opensRange_of_isIso CategoryTheory.IsIso.id CategoryTheory.Iso.isIso_hom AlgebraicGeometry.Scheme.GlueData.glue_condition CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso AlgebraicGeometry.IsOpenImmersion.lift_fac_assoc CategoryTheory.Category.assoc le_rfl CategoryTheory.Iso.eq_inv_comp homOfLE_tAux CategoryTheory.cancel_mono AlgebraicGeometry.IsOpenImmersion.mono AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι AlgebraicGeometry.Scheme.homOfLE_ι AlgebraicGeometry.Scheme.Hom.isoOpensRange_hom_ι CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
homOfLE_tAux 📖	mathematical	AlgebraicGeometry.IsOpenImmersion CategoryTheory.Functor.obj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.map Quiver.IsThin CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Scheme.Hom.opensRange Quiver.Hom iSup AlgebraicGeometry.Scheme.Opens CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup TopologicalSpace.Opens.instCompleteLattice TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.Scheme.homOfLE le_iSup_of_le le_rfl PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder tAux CategoryTheory.Iso.inv AlgebraicGeometry.Scheme.Hom.isoOpensRange	—	AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms
homOfLE_tAux_assoc 📖	mathematical	AlgebraicGeometry.IsOpenImmersion CategoryTheory.Functor.obj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.map Quiver.IsThin CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Scheme.Hom.opensRange Quiver.Hom iSup AlgebraicGeometry.Scheme.Opens CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup TopologicalSpace.Opens.instCompleteLattice TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.Scheme.homOfLE le_iSup_of_le le_rfl PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder tAux CategoryTheory.Iso.inv AlgebraicGeometry.Scheme.Hom.isoOpensRange	—	le_iSup_of_le le_rfl CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homOfLE_tAux
instHasColimit 📖	mathematical	AlgebraicGeometry.IsOpenImmersion CategoryTheory.Functor.obj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.map Quiver.IsThin CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.HasColimit	—	—
instIsLocallyDirectedWidePushoutShapeCompForgetOfIsOpenImmersionMap 📖	mathematical	AlgebraicGeometry.IsOpenImmersion CategoryTheory.Functor.obj CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WidePushoutShape.category AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.map	CategoryTheory.Functor.IsLocallyDirected CategoryTheory.Functor.comp CategoryTheory.types AlgebraicGeometry.Scheme.forget	—	CategoryTheory.mono_iff_injective Topology.IsEmbedding.injective Topology.IsOpenEmbedding.toIsEmbedding AlgebraicGeometry.Scheme.Hom.isOpenEmbedding CategoryTheory.instIsLocallyDirectedWidePushoutShapeOfMonoObjNoneSomeMapInit
instIsOpenImmersionι 📖	mathematical	AlgebraicGeometry.IsOpenImmersion CategoryTheory.Functor.obj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.map Quiver.IsThin CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.colimit instHasColimit CategoryTheory.Limits.colimit.ι	—	instHasColimit AlgebraicGeometry.Scheme.instIsOpenImmersionF
instPreservesColimitLocallyRingedSpaceForgetToLocallyRingedSpace 📖	mathematical	AlgebraicGeometry.IsOpenImmersion CategoryTheory.Functor.obj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.map Quiver.IsThin CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.PreservesColimit AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace	—	CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone
openCover_I₀ 📖	mathematical	AlgebraicGeometry.IsOpenImmersion CategoryTheory.Functor.obj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.map Quiver.IsThin CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.Limits.colimit instHasColimit CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage openCover	—	instHasColimit
openCover_X 📖	mathematical	AlgebraicGeometry.IsOpenImmersion CategoryTheory.Functor.obj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.map Quiver.IsThin CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	CategoryTheory.PreZeroHypercover.X CategoryTheory.Limits.colimit instHasColimit CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage openCover	—	instHasColimit
openCover_f 📖	mathematical	AlgebraicGeometry.IsOpenImmersion CategoryTheory.Functor.obj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.map Quiver.IsThin CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	CategoryTheory.PreZeroHypercover.f CategoryTheory.Limits.colimit instHasColimit CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage openCover CategoryTheory.Limits.colimit.ι	—	instHasColimit
t_id 📖	mathematical	AlgebraicGeometry.IsOpenImmersion CategoryTheory.Functor.obj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.map Quiver.IsThin CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	t CategoryTheory.CategoryStruct.id AlgebraicGeometry.Scheme.Opens.toScheme V	—	AlgebraicGeometry.Scheme.Cover.hom_ext CategoryTheory.Category.comp_id CategoryTheory.cancel_mono AlgebraicGeometry.IsOpenImmersion.mono AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι CategoryTheory.Category.assoc AlgebraicGeometry.IsOpenImmersion.lift_fac AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms AlgebraicGeometry.Scheme.homOfLE_ι AlgebraicGeometry.Scheme.Hom.isoOpensRange_hom_ι
ι_eq_ι_iff 📖	mathematical	AlgebraicGeometry.IsOpenImmersion CategoryTheory.Functor.obj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.map Quiver.IsThin CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.Limits.colimit instHasColimit TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.Limits.colimit.ι	—	instHasColimit Equiv.surjective Topology.IsEmbedding.injective Topology.IsOpenEmbedding.toIsEmbedding AlgebraicGeometry.Scheme.Hom.isOpenEmbedding AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv glueDataι_naturality TopologicalSpace.Opens.mem_iSup AlgebraicGeometry.Scheme.GlueData.ι_isOpenImmersion CategoryTheory.Category.assoc AlgebraicGeometry.Scheme.GlueData.glue_condition AlgebraicGeometry.Scheme.GlueData.instHasMulticoequalizerDiagram AlgebraicGeometry.Scheme.GlueData.ι_eq_iff CategoryTheory.Limits.colimit.w
ι_jointly_surjective 📖	mathematical	AlgebraicGeometry.IsOpenImmersion CategoryTheory.Functor.obj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.map Quiver.IsThin CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.Limits.colimit instHasColimit TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.Limits.colimit.ι	—	instHasColimit AlgebraicGeometry.Scheme.GlueData.ι_jointly_surjective Topology.IsEmbedding.injective Topology.IsOpenEmbedding.toIsEmbedding AlgebraicGeometry.Scheme.Hom.isOpenEmbedding AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Iso.isIso_inv Equiv.apply_symm_apply CategoryTheory.eqToHom_naturality CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv CategoryTheory.eqToHom_map CategoryTheory.Category.comp_id

---

← Back to Index