Over

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

Statistics

Metric	Count
Definitions Over, over, pullbackCoverOver, pullbackCoverOver', pullbackCoverOverProp, pullbackCoverOverProp', asOverProp, asOverProp, instOverBind, instOverCoverOfIsIsoOfIsOver, instOverPullbackCoverOver, instOverPullbackCoverOver', instOverPullbackCoverOverProp, instOverPullbackCoverOverProp', instOverXBind, instOverXPullbackCoverOver, instOverXPullbackCoverOver', instOverXPullbackCoverOverProp, instOverXPullbackCoverOverProp'	19
Theorems isOver_map, pullbackCoverOver'_I₀, pullbackCoverOver'_X, pullbackCoverOver'_f, pullbackCoverOverProp'_I₀, pullbackCoverOverProp'_X, pullbackCoverOverProp'_f, pullbackCoverOverProp_I₀, pullbackCoverOverProp_X, pullbackCoverOverProp_f, pullbackCoverOver_I₀, pullbackCoverOver_X, pullbackCoverOver_f	13
Total	32

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
asOverProp 📖	CompOp	4 math math: Cover.pullbackCoverOverProp_f, Cover.pullbackCoverOverProp'_X, Cover.pullbackCoverOverProp'_f, Cover.pullbackCoverOverProp_X
instOverBind 📖	CompOp	—
instOverCoverOfIsIsoOfIsOver 📖	CompOp	—
instOverPullbackCoverOver 📖	CompOp	—
instOverPullbackCoverOver' 📖	CompOp	—
instOverPullbackCoverOverProp 📖	CompOp	—
instOverPullbackCoverOverProp' 📖	CompOp	—
instOverXBind 📖	CompOp	—
instOverXPullbackCoverOver 📖	CompOp	—
instOverXPullbackCoverOver' 📖	CompOp	—
instOverXPullbackCoverOverProp 📖	CompOp	—
instOverXPullbackCoverOverProp' 📖	CompOp	—

AlgebraicGeometry.Scheme.Cover

Definitions

Name	Category	Theorems
Over 📖	CompData	—
pullbackCoverOver 📖	CompOp	3 math math: pullbackCoverOver_X, pullbackCoverOver_I₀, pullbackCoverOver_f
pullbackCoverOver' 📖	CompOp	3 math math: pullbackCoverOver'_X, pullbackCoverOver'_I₀, pullbackCoverOver'_f
pullbackCoverOverProp 📖	CompOp	3 math math: pullbackCoverOverProp_I₀, pullbackCoverOverProp_f, pullbackCoverOverProp_X
pullbackCoverOverProp' 📖	CompOp	3 math math: pullbackCoverOverProp'_X, pullbackCoverOverProp'_f, pullbackCoverOverProp'_I₀

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pullbackCoverOver'_I₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage pullbackCoverOver'	—	—
pullbackCoverOver'_X 📖	mathematical	—	CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage pullbackCoverOver' CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Limits.pullback CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.OverClass.asOver Over.over AlgebraicGeometry.Scheme.Hom.asOver CategoryTheory.PreZeroHypercover.f Over.isOver_map	—	—
pullbackCoverOver'_f 📖	mathematical	—	CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage pullbackCoverOver' CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Limits.pullback CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.OverClass.asOver CategoryTheory.PreZeroHypercover.X Over.over AlgebraicGeometry.Scheme.Hom.asOver Over.isOver_map CategoryTheory.Limits.pullback.snd	—	Over.isOver_map
pullbackCoverOverProp'_I₀ 📖	mathematical	CategoryTheory.over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.OverClass CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage Over.over	CategoryTheory.PreZeroHypercover.I₀ pullbackCoverOverProp'	—	—
pullbackCoverOverProp'_X 📖	mathematical	CategoryTheory.over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.OverClass CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage Over.over	pullbackCoverOverProp' CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Limits.pullback CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.MorphismProperty.IsMultiplicative.instTop AlgebraicGeometry.Scheme.asOverProp AlgebraicGeometry.Scheme.Hom.asOverProp CategoryTheory.PreZeroHypercover.f Over.isOver_map	—	—
pullbackCoverOverProp'_f 📖	mathematical	CategoryTheory.over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.OverClass CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage Over.over	CategoryTheory.PreZeroHypercover.f pullbackCoverOverProp' CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Limits.pullback CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.MorphismProperty.IsMultiplicative.instTop AlgebraicGeometry.Scheme.asOverProp AlgebraicGeometry.Scheme.Hom.asOverProp Over.isOver_map CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism CategoryTheory.Limits.pullback.snd	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop Over.isOver_map
pullbackCoverOverProp_I₀ 📖	mathematical	CategoryTheory.over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.OverClass CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage Over.over	CategoryTheory.PreZeroHypercover.I₀ pullbackCoverOverProp	—	—
pullbackCoverOverProp_X 📖	mathematical	CategoryTheory.over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.OverClass CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage Over.over	pullbackCoverOverProp CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Limits.pullback CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.MorphismProperty.IsMultiplicative.instTop AlgebraicGeometry.Scheme.asOverProp AlgebraicGeometry.Scheme.Hom.asOverProp CategoryTheory.PreZeroHypercover.f Over.isOver_map	—	—
pullbackCoverOverProp_f 📖	mathematical	CategoryTheory.over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.OverClass CategoryTheory.PreZeroHypercover.X CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage Over.over	CategoryTheory.PreZeroHypercover.f pullbackCoverOverProp CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Limits.pullback CategoryTheory.MorphismProperty.Over CategoryTheory.MorphismProperty.Comma.instCategory CategoryTheory.MorphismProperty.IsMultiplicative.instTop AlgebraicGeometry.Scheme.asOverProp AlgebraicGeometry.Scheme.Hom.asOverProp Over.isOver_map CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism CategoryTheory.Limits.pullback.fst	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop Over.isOver_map
pullbackCoverOver_I₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage pullbackCoverOver	—	—
pullbackCoverOver_X 📖	mathematical	—	CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage pullbackCoverOver CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Limits.pullback CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.OverClass.asOver Over.over AlgebraicGeometry.Scheme.Hom.asOver CategoryTheory.PreZeroHypercover.f Over.isOver_map	—	—
pullbackCoverOver_f 📖	mathematical	—	CategoryTheory.PreZeroHypercover.f AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage pullbackCoverOver CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Limits.pullback CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.OverClass.asOver CategoryTheory.PreZeroHypercover.X Over.over AlgebraicGeometry.Scheme.Hom.asOver Over.isOver_map CategoryTheory.Limits.pullback.fst	—	Over.isOver_map

AlgebraicGeometry.Scheme.Cover.Over

Definitions

Name	Category	Theorems
over 📖	CompOp	5 math math: AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_X, AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_X, AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_f, AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_f, isOver_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOver_map 📖	mathematical	—	AlgebraicGeometry.Scheme.Hom.IsOver CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage CategoryTheory.PreZeroHypercover.f over	—	—

AlgebraicGeometry.Scheme.Hom

Definitions

Name	Category	Theorems
asOverProp 📖	CompOp	4 math math: AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_f, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_X, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_f, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_X

---

← Back to Index