Structures · Geometry
AlgebraicGeometry.Scheme.Cover.Over
A P-cover of a scheme X over S is a cover, where the components are over S and the
component maps commute with the structure morphisms.
- Defined in
- Mathlib.AlgebraicGeometry.Cover.Over
- Shape
- 2 explicit arguments · adds over, isOver_map
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by33
- AlgebraicGeometry.Scheme.Cover.toPresieveOver
- AlgebraicGeometry.Scheme.Cover.toPresieveOverProp
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOver
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'
- AlgebraicGeometry.Scheme.Cover.toPresieveOver_le_arrows_iff
- AlgebraicGeometry.Scheme.Cover.overEquiv_generate_toPresieveOver_eq_ofArrows
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_f
- AlgebraicGeometry.Scheme.instOverPullbackCoverOverProp'
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_I₀
- AlgebraicGeometry.Scheme.instOverXPullbackCoverOverProp
- AlgebraicGeometry.Scheme.Cover.toPresieveOverProp.congr_simp
- AlgebraicGeometry.Scheme.instOverXPullbackCoverOver
- AlgebraicGeometry.Scheme.instOverXPullbackCoverOver'
- AlgebraicGeometry.Scheme.instOverPullbackCoverOverProp
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_X
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_X
- AlgebraicGeometry.Scheme.Cover.Over.isOver_map
- AlgebraicGeometry.Scheme.instOverBind
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_f
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_X
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_I₀
- AlgebraicGeometry.Scheme.instOverPullbackCoverOver'
- AlgebraicGeometry.Scheme.Cover.Over.over
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_X
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_f
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_I₀
- AlgebraicGeometry.Scheme.instOverXBind
- AlgebraicGeometry.Scheme.instOverXPullbackCoverOverProp'
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_f
- AlgebraicGeometry.Scheme.instOverPullbackCoverOver
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_I₀
Ancestors0
No ancestors.