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.Sheaf.val 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	glued ι sheafValGluedMk	—	CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv_apply_val

---

← Back to Index