RelativeGluing

📁 Source: Mathlib/AlgebraicGeometry/RelativeGluing.lean

Statistics

Metric	Count
Definitions RelativeGluingData, cover, functor, glued, instCategoryI₀Cover, instLocallyDirectedIsOpenImmersionCover, natTrans, toBase	8
Theorems cover_I₀, cover_X, cover_f, equifibered, instIsLocallyDirectedI₀CompFunctorForgetOfIsThin, instIsOpenImmersionMapI₀Functor, isPullback_natTrans_ι_toBase, preimage_toBase_eq_range_ι, toBase_preimage_eq_opensRange_ι, ι_toBase, ι_toBase_assoc, isLocallyDirected_of_equifibered_of_injective	12
Total	20

AlgebraicGeometry.Scheme

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocallyDirected_of_equifibered_of_injective 📖	mathematical	Quiver.IsThin CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.Equifibered AlgebraicGeometry.Scheme instCategory TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace CategoryTheory.Functor.obj DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' CategoryTheory.Functor.map	CategoryTheory.Functor.IsLocallyDirected CategoryTheory.Functor.comp CategoryTheory.types forget	—	CategoryTheory.Functor.exists_map_eq_of_isLocallyDirected Hom.comp_apply CategoryTheory.NatTrans.naturality Pullback.instHasPullback Pullback.exists_preimage_pullback CategoryTheory.IsPullback.isoPullback_inv_fst CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp CategoryTheory.IsPullback.isoPullback_inv_fst_assoc

AlgebraicGeometry.Scheme.Cover

Definitions

Name	Category	Theorems
RelativeGluingData 📖	CompData	—

AlgebraicGeometry.Scheme.Cover.RelativeGluingData

Definitions

Name	Category	Theorems
cover 📖	CompOp	4 math math: cover_X, cover_I₀, cover_f, AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.colimitDesc_preimage
functor 📖	CompOp	18 math math: cover_X, toBase_preimage_eq_opensRange_ι, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst_assoc, ι_toBase, ι_toBase_assoc, equifibered, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι_assoc, cover_f, AlgebraicGeometry.Scheme.AffineZariskiSite.opensRange_relativeGluingData_map, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.relativeGluingData_functor, instIsLocallyDirectedI₀CompFunctorForgetOfIsThin, AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.opensRange_map, preimage_toBase_eq_range_ι, AlgebraicGeometry.Scheme.Hom.instIsLocallyDirectedI₀DirectedCoverCompFunctorNormalizationGlueDataForget, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst, instIsOpenImmersionMapI₀Functor, isPullback_natTrans_ι_toBase
glued 📖	CompOp	6 math math: cover_X, toBase_preimage_eq_opensRange_ι, cover_I₀, cover_f, preimage_toBase_eq_range_ι, AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.colimitDesc_preimage
instCategoryI₀Cover 📖	CompOp	—
instLocallyDirectedIsOpenImmersionCover 📖	CompOp	—
natTrans 📖	CompOp	5 math math: ι_toBase, ι_toBase_assoc, equifibered, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.relativeGluingData_natTrans_app, isPullback_natTrans_ι_toBase
toBase 📖	CompOp	6 math math: toBase_preimage_eq_opensRange_ι, ι_toBase, ι_toBase_assoc, preimage_toBase_eq_range_ι, AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.colimitDesc_preimage, isPullback_natTrans_ι_toBase

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cover_I₀ 📖	mathematical	Quiver.IsThin CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	glued cover	—	—
cover_X 📖	mathematical	Quiver.IsThin CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	CategoryTheory.PreZeroHypercover.X glued cover CategoryTheory.Functor.obj functor	—	—
cover_f 📖	mathematical	Quiver.IsThin CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	CategoryTheory.PreZeroHypercover.f glued cover CategoryTheory.Limits.colimit.ι functor AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit instIsOpenImmersionMapI₀Functor instIsLocallyDirectedI₀CompFunctorForgetOfIsThin	—	AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit instIsOpenImmersionMapI₀Functor instIsLocallyDirectedI₀CompFunctorForgetOfIsThin
equifibered 📖	mathematical	—	CategoryTheory.NatTrans.Equifibered CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion functor AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected natTrans	—	—
instIsLocallyDirectedI₀CompFunctorForgetOfIsThin 📖	mathematical	Quiver.IsThin CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	CategoryTheory.Functor.IsLocallyDirected CategoryTheory.Functor.comp CategoryTheory.types functor AlgebraicGeometry.Scheme.forget	—	AlgebraicGeometry.Scheme.isLocallyDirected_of_equifibered_of_injective equifibered AlgebraicGeometry.Scheme.Hom.injective AlgebraicGeometry.instUniversallyInjectiveOfMonoScheme AlgebraicGeometry.IsOpenImmersion.mono instIsOpenImmersionMapI₀Functor AlgebraicGeometry.Scheme.Cover.instIsLocallyDirectedI₀CompFunctorOfLocallyDirectedForget
instIsOpenImmersionMapI₀Functor 📖	mathematical	—	AlgebraicGeometry.IsOpenImmersion CategoryTheory.Functor.obj CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage functor CategoryTheory.Functor.map	—	CategoryTheory.MorphismProperty.of_isPullback AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange CategoryTheory.IsPullback.flip equifibered AlgebraicGeometry.Scheme.OpenCover.instIsOpenImmersionMapI₀FunctorOfLocallyDirected
isPullback_natTrans_ι_toBase 📖	mathematical	Quiver.IsThin CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	CategoryTheory.IsPullback CategoryTheory.Functor.obj functor AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected CategoryTheory.Limits.colimit AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit instIsOpenImmersionMapI₀Functor instIsLocallyDirectedI₀CompFunctorForgetOfIsThin CategoryTheory.NatTrans.app natTrans CategoryTheory.Limits.colimit.ι CategoryTheory.PreZeroHypercover.f toBase	—	AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit instIsOpenImmersionMapI₀Functor instIsLocallyDirectedI₀CompFunctorForgetOfIsThin ι_toBase CategoryTheory.CommSq.w AlgebraicGeometry.Scheme.IsLocallyDirected.instIsOpenImmersionι preimage_toBase_eq_range_ι AlgebraicGeometry.Scheme.Hom.comp_apply CategoryTheory.Limits.PullbackCone.condition CategoryTheory.cancel_mono AlgebraicGeometry.IsOpenImmersion.mono AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.Category.assoc AlgebraicGeometry.IsOpenImmersion.lift_fac_assoc AlgebraicGeometry.IsOpenImmersion.lift_fac
preimage_toBase_eq_range_ι 📖	mathematical	Quiver.IsThin CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	Set.preimage TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace glued 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' toBase Set.range CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.f CategoryTheory.Limits.colimit functor AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit instIsOpenImmersionMapI₀Functor instIsLocallyDirectedI₀CompFunctorForgetOfIsThin CategoryTheory.Functor.obj CategoryTheory.Limits.colimit.ι	—	Set.ext AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit instIsOpenImmersionMapI₀Functor instIsLocallyDirectedI₀CompFunctorForgetOfIsThin AlgebraicGeometry.Scheme.IsLocallyDirected.ι_jointly_surjective AlgebraicGeometry.Scheme.Cover.exists_of_f_eq_f ι_toBase AlgebraicGeometry.Scheme.exists_preimage_of_isPullback equifibered AlgebraicGeometry.Scheme.Hom.injective AlgebraicGeometry.instUniversallyInjectiveOfMonoScheme AlgebraicGeometry.IsOpenImmersion.mono AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.Scheme.Hom.comp_apply AlgebraicGeometry.Scheme.Cover.trans_map CategoryTheory.Limits.colimit.w
toBase_preimage_eq_opensRange_ι 📖	mathematical	Quiver.IsThin CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder glued TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' toBase AlgebraicGeometry.Scheme.Hom.opensRange CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme.instIsOpenImmersionF functor CategoryTheory.Limits.colimit AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit instIsOpenImmersionMapI₀Functor instIsLocallyDirectedI₀CompFunctorForgetOfIsThin CategoryTheory.Limits.colimit.ι AlgebraicGeometry.Scheme.IsLocallyDirected.instIsOpenImmersionι	—	AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit instIsOpenImmersionMapI₀Functor instIsLocallyDirectedI₀CompFunctorForgetOfIsThin AlgebraicGeometry.Scheme.IsLocallyDirected.instIsOpenImmersionι preimage_toBase_eq_range_ι
ι_toBase 📖	mathematical	Quiver.IsThin CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.obj functor CategoryTheory.Limits.colimit AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit instIsOpenImmersionMapI₀Functor instIsLocallyDirectedI₀CompFunctorForgetOfIsThin CategoryTheory.Limits.colimit.ι toBase AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected CategoryTheory.NatTrans.app natTrans CategoryTheory.PreZeroHypercover.f	—	AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit instIsOpenImmersionMapI₀Functor instIsLocallyDirectedI₀CompFunctorForgetOfIsThin CategoryTheory.Limits.colimit.ι_desc
ι_toBase_assoc 📖	mathematical	Quiver.IsThin CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.obj functor CategoryTheory.Limits.colimit AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit instIsOpenImmersionMapI₀Functor instIsLocallyDirectedI₀CompFunctorForgetOfIsThin CategoryTheory.Limits.colimit.ι toBase AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected CategoryTheory.NatTrans.app natTrans CategoryTheory.PreZeroHypercover.f	—	AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit instIsOpenImmersionMapI₀Functor instIsLocallyDirectedI₀CompFunctorForgetOfIsThin CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_toBase

---

← Back to Index