Covers of schemes over a base #
In this file we define the typeclass Cover.Over. For a cover 𝒰 of an S-scheme X,
the datum 𝒰.Over S contains S-scheme structures on the components of 𝒰 and asserts
that the component maps are morphisms of S-schemes.
We provide instances of 𝒰.Over S for standard constructions on covers.
Bundle an S-scheme with P into an object of P.Over ⊤ S.
Equations
- X.asOverProp S h = { toComma := X.asOver S, prop := h }
Instances For
Bundle an S-morphism of S-scheme with P into a morphism in P.Over ⊤ S.
Equations
Instances For
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.
- isOver_map (j : 𝒰.I₀) : Hom.IsOver (𝒰.f j) S
Instances
Equations
- S.instOverCoverOfIsIsoOfIsOver f = { over := fun (x : (AlgebraicGeometry.Scheme.coverOfIsIso f).I₀) => inferInstanceAs (X.Over S), isOver_map := ⋯ }
The pullback of a cover of S-schemes along a morphism of S-schemes. This is not
definitionally equal to AlgebraicGeometry.Scheme.Cover.pullback₁, as here we take
the pullback in Over S, whose underlying scheme is only isomorphic but not equal to the
pullback in Scheme.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- S.instOverXPullbackCoverOver 𝒰 f j = { hom := (CategoryTheory.Limits.pullback (AlgebraicGeometry.Scheme.Hom.asOver f S) (AlgebraicGeometry.Scheme.Hom.asOver (𝒰.f j) S)).hom }
Equations
- S.instOverPullbackCoverOver 𝒰 f = { over := inferInstance, isOver_map := ⋯ }
A variant of AlgebraicGeometry.Scheme.Cover.pullbackCoverOver with the arguments in the
fiber products flipped.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- S.instOverXPullbackCoverOver' 𝒰 f j = { hom := (CategoryTheory.Limits.pullback (AlgebraicGeometry.Scheme.Hom.asOver (𝒰.f j) S) (AlgebraicGeometry.Scheme.Hom.asOver f S)).hom }
Equations
- S.instOverPullbackCoverOver' 𝒰 f = { over := inferInstance, isOver_map := ⋯ }
The pullback of a cover of S-schemes with Q along a morphism of S-schemes. This is not
definitionally equal to AlgebraicGeometry.Scheme.Cover.pullbackCover, as here we take
the pullback in Q.Over ⊤ S, whose underlying scheme is only isomorphic but not equal to the
pullback in Scheme.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- S.instOverPullbackCoverOverProp 𝒰 f hX hW hQ = { over := inferInstance, isOver_map := ⋯ }
A variant of AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp with the arguments in the
fiber products flipped.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- S.instOverPullbackCoverOverProp' 𝒰 f hX hW hQ = { over := inferInstance, isOver_map := ⋯ }
Equations
- S.instOverXBind 𝒰 𝒱 j = inferInstanceAs (((𝒱 j.fst).X j.snd).Over S)
Equations
- One or more equations did not get rendered due to their size.