Documentation

Mathlib.AlgebraicGeometry.Cover.Over

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.

@[reducible, inline]

Bundle an S-scheme with P into an object of P.Over ⊤ S.

Equations
Instances For
    @[reducible, inline]
    abbrev AlgebraicGeometry.Scheme.Hom.asOverProp {P : CategoryTheory.MorphismProperty Scheme} {X Y : Scheme} (f : X.Hom Y) (S : Scheme) [X.Over S] [Y.Over S] [f.IsOver S] {hX : P (X S)} {hY : P (Y S)} :
    X.asOverProp S hX Y.asOverProp S hY

    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.

      Instances

        The pullback of a cover of S-schemes along a morphism of S-schemes. This is not definitionally equal to AlgebraicGeometry.Scheme.Cover.pullbackCover, 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
          • One or more equations did not get rendered due to their size.

          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
            • One or more equations did not get rendered due to their size.

            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
              instance AlgebraicGeometry.Scheme.instOverObjPullbackCoverOverProp {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover P X) (f : W X) [W.Over S] [X.Over S] [Cover.Over S 𝒰] [Hom.IsOver f S] {Q : CategoryTheory.MorphismProperty Scheme} [Q.HasOfPostcompProperty Q] [Q.IsStableUnderBaseChange] [Q.IsStableUnderComposition] (hX : Q (X S)) (hW : Q (W S)) (hQ : ∀ (j : 𝒰.J), Q (𝒰.obj j S)) (j : 𝒰.J) :
              ((Cover.pullbackCoverOverProp S 𝒰 f hX hW hQ).obj j).Over S
              Equations
              • One or more equations did not get rendered due to their size.
              Equations

              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
                instance AlgebraicGeometry.Scheme.instOverObjPullbackCoverOverProp' {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover P X) (f : W X) [W.Over S] [X.Over S] [Cover.Over S 𝒰] [Hom.IsOver f S] {Q : CategoryTheory.MorphismProperty Scheme} [Q.HasOfPostcompProperty Q] [Q.IsStableUnderBaseChange] [Q.IsStableUnderComposition] (hX : Q (X S)) (hW : Q (W S)) (hQ : ∀ (j : 𝒰.J), Q (𝒰.obj j S)) (j : 𝒰.J) :
                ((Cover.pullbackCoverOverProp' S 𝒰 f hX hW hQ).obj j).Over S
                Equations
                • One or more equations did not get rendered due to their size.
                Equations
                instance AlgebraicGeometry.Scheme.instOverObjBind {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderComposition] {X : Scheme} (𝒰 : Cover P X) (𝒱 : (x : 𝒰.J) → Cover P (𝒰.obj x)) [X.Over S] [Cover.Over S 𝒰] [(x : 𝒰.J) → Cover.Over S (𝒱 x)] (j : (𝒰.bind 𝒱).J) :
                ((𝒰.bind 𝒱).obj j).Over S
                Equations
                instance AlgebraicGeometry.Scheme.instOverBind {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderComposition] {X : Scheme} (𝒰 : Cover P X) (𝒱 : (x : 𝒰.J) → Cover P (𝒰.obj x)) [X.Over S] [Cover.Over S 𝒰] [(x : 𝒰.J) → Cover.Over S (𝒱 x)] :
                Cover.Over S (𝒰.bind 𝒱)
                Equations