GluingOneHypercover

📁 Source: Mathlib/AlgebraicGeometry/GluingOneHypercover.lean

Statistics

Metric	Count
Definitions oneHypercover, sheafValGluedMk	2
Theorems oneHypercover_I₀, oneHypercover_I₁, oneHypercover_X, oneHypercover_Y, oneHypercover_f, oneHypercover_p₁, oneHypercover_p₂, sheafValGluedMk_val	8
Total	10

AlgebraicGeometry.Scheme.GlueData

Definitions

Name	Category	Theorems
oneHypercover 📖	CompOp	7 math math: oneHypercover_I₁, oneHypercover_p₂, oneHypercover_X, oneHypercover_I₀, oneHypercover_f, oneHypercover_Y, oneHypercover_p₁
sheafValGluedMk 📖	CompOp	1 math math: sheafValGluedMk_val

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
oneHypercover_I₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory glued CategoryTheory.PreOneHypercover.toPreZeroHypercover CategoryTheory.GrothendieckTopology.OneHypercover.toPreOneHypercover AlgebraicGeometry.Scheme.zariskiTopology oneHypercover CategoryTheory.GlueData.J toGlueData	—	—
oneHypercover_I₁ 📖	mathematical	—	CategoryTheory.PreOneHypercover.I₁ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory glued CategoryTheory.GrothendieckTopology.OneHypercover.toPreOneHypercover AlgebraicGeometry.Scheme.zariskiTopology oneHypercover	—	—
oneHypercover_X 📖	mathematical	—	CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory glued CategoryTheory.PreOneHypercover.toPreZeroHypercover CategoryTheory.GrothendieckTopology.OneHypercover.toPreOneHypercover AlgebraicGeometry.Scheme.zariskiTopology oneHypercover CategoryTheory.GlueData.U toGlueData	—	—
oneHypercover_Y 📖	mathematical	—	CategoryTheory.PreOneHypercover.Y AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory glued CategoryTheory.GrothendieckTopology.OneHypercover.toPreOneHypercover AlgebraicGeometry.Scheme.zariskiTopology oneHypercover CategoryTheory.GlueData.V toGlueData CategoryTheory.GlueData.J	—	—
oneHypercover_f 📖	mathematical	—	CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory glued CategoryTheory.PreOneHypercover.toPreZeroHypercover CategoryTheory.GrothendieckTopology.OneHypercover.toPreOneHypercover AlgebraicGeometry.Scheme.zariskiTopology oneHypercover ι	—	—
oneHypercover_p₁ 📖	mathematical	—	CategoryTheory.PreOneHypercover.p₁ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory glued CategoryTheory.GrothendieckTopology.OneHypercover.toPreOneHypercover AlgebraicGeometry.Scheme.zariskiTopology oneHypercover CategoryTheory.GlueData.f toGlueData	—	—
oneHypercover_p₂ 📖	mathematical	—	CategoryTheory.PreOneHypercover.p₂ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory glued CategoryTheory.GrothendieckTopology.OneHypercover.toPreOneHypercover AlgebraicGeometry.Scheme.zariskiTopology oneHypercover CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.GlueData.V toGlueData CategoryTheory.GlueData.J CategoryTheory.GlueData.U CategoryTheory.GlueData.t CategoryTheory.GlueData.f	—	—
sheafValGluedMk_val 📖	mathematical	CategoryTheory.Functor.map Opposite AlgebraicGeometry.Scheme CategoryTheory.Category.opposite AlgebraicGeometry.Scheme.instCategory CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf AlgebraicGeometry.Scheme.zariskiTopology Opposite.op CategoryTheory.GlueData.U toGlueData CategoryTheory.GlueData.V CategoryTheory.GlueData.J Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.GlueData.f CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.GlueData.t	CategoryTheory.Functor.map Opposite AlgebraicGeometry.Scheme CategoryTheory.Category.opposite AlgebraicGeometry.Scheme.instCategory CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf AlgebraicGeometry.Scheme.zariskiTopology Opposite.op glued CategoryTheory.GlueData.U toGlueData Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct ι sheafValGluedMk	—	CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv_apply_val

---

← Back to Index