Sigma

📁 Source: Mathlib/AlgebraicGeometry/Cover/Sigma.lean

Statistics

Metric	Count
Definitions sigma, instUniqueI₀Sigma, sigma, sigmaFunctor, toSigma	5
Theorems sigma_h₀, sigma_s₀, presieve₀_sigma, sigmaFunctor_map, sigmaFunctor_obj, sigma_I₀, sigma_X, sigma_f, toSigma_h₀, toSigma_s₀	10
Total	15

AlgebraicGeometry.Scheme.Cover

Definitions

Name	Category	Theorems
instUniqueI₀Sigma 📖	CompOp	3 math math: toSigma_s₀, Hom.sigma_h₀, Hom.sigma_s₀
sigma 📖	CompOp	10 math math: isSheafFor_sigma_iff, sigmaFunctor_obj, toSigma_s₀, sigma_X, Hom.sigma_h₀, toSigma_h₀, Hom.sigma_s₀, sigma_I₀, presieve₀_sigma, sigma_f
sigmaFunctor 📖	CompOp	2 math math: sigmaFunctor_obj, sigmaFunctor_map
toSigma 📖	CompOp	2 math math: toSigma_s₀, toSigma_h₀

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
presieve₀_sigma 📖	mathematical	—	CategoryTheory.PreZeroHypercover.presieve₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage sigma CategoryTheory.Presieve.singleton CategoryTheory.Limits.sigmaObj CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Functor.comp CategoryTheory.types AlgebraicGeometry.Scheme.forget CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small CategoryTheory.Limits.Sigma.desc CategoryTheory.PreZeroHypercover.f	—	le_antisymm AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small CategoryTheory.Presieve.ofArrows_le_iff CategoryTheory.Presieve.singleton_self
sigmaFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map AlgebraicGeometry.Scheme.Cover AlgebraicGeometry.Scheme.precoverage CategoryTheory.Precoverage.ZeroHypercover.instCategory AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory sigmaFunctor Hom.sigma	—	—
sigmaFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Cover AlgebraicGeometry.Scheme.precoverage CategoryTheory.Precoverage.ZeroHypercover.instCategory AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory sigmaFunctor sigma	—	—
sigma_I₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage sigma	—	—
sigma_X 📖	mathematical	—	CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage sigma CategoryTheory.Limits.sigmaObj CategoryTheory.PreZeroHypercover.I₀	—	—
sigma_f 📖	mathematical	—	CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage sigma CategoryTheory.Limits.Sigma.desc CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.PreZeroHypercover.X	—	—
toSigma_h₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.h₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage sigma toSigma CategoryTheory.Limits.Sigma.ι CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.PreZeroHypercover.X	—	—
toSigma_s₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.s₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage sigma toSigma CategoryTheory.PreZeroHypercover.I₀ Unique.instInhabited instUniqueI₀Sigma	—	—

AlgebraicGeometry.Scheme.Cover.Hom

Definitions

Name	Category	Theorems
sigma 📖	CompOp	3 math math: AlgebraicGeometry.Scheme.Cover.sigmaFunctor_map, sigma_h₀, sigma_s₀

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sigma_h₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.h₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.Scheme.Cover.sigma sigma CategoryTheory.Limits.Sigma.desc CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.PreZeroHypercover.X Unique.instInhabited AlgebraicGeometry.Scheme.Cover.instUniqueI₀Sigma CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.Limits.Sigma.ι	—	—
sigma_s₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.s₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.Scheme.Cover.sigma sigma CategoryTheory.PreZeroHypercover.I₀ Unique.instInhabited AlgebraicGeometry.Scheme.Cover.instUniqueI₀Sigma	—	—

---

← Back to Index