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]

abbrev AlgebraicGeometry.Scheme.asOverProp {P : CategoryTheory.MorphismProperty Scheme} (X S : Scheme) [X.Over S] (h : P (X ↘ S)) : P.Over ⊤ S

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

@[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.

class AlgebraicGeometry.Scheme.Cover.Over (S : Scheme) {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} [X.Over S] (𝒰 : Cover P X) : Type (max u u_1)

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.

• over (j : 𝒰.J) : (𝒰.obj j).Over S
• isOver_map (j : 𝒰.J) : Hom.IsOver (𝒰.map j) S

instance AlgebraicGeometry.Scheme.instOverCoverOfIsIsoOfIsOver {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.ContainsIdentities] [P.RespectsIso] {X Y : Scheme} (f : X ⟶ Y) [X.Over S] [Y.Over S] [Hom.IsOver f S] [CategoryTheory.IsIso f] : Cover.Over S (coverOfIsIso f)

def AlgebraicGeometry.Scheme.Cover.pullbackCoverOver {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] : Cover P W

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.

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_J {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] : (pullbackCoverOver S 𝒰 f).J = 𝒰.J

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_f {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] (x : ↥W) : (pullbackCoverOver S 𝒰 f).f x = 𝒰.f ((CategoryTheory.ConcreteCategory.hom f.base) x)

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_map {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] (x : 𝒰.J) : (pullbackCoverOver S 𝒰 f).map x = (CategoryTheory.Limits.pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.map x) S)).left

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_obj {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] (x : 𝒰.J) : (pullbackCoverOver S 𝒰 f).obj x = (CategoryTheory.Limits.pullback (Hom.asOver f S) (Hom.asOver (𝒰.map x) S)).left

instance AlgebraicGeometry.Scheme.instOverObjPullbackCoverOver {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] (j : 𝒰.J) : ((Cover.pullbackCoverOver S 𝒰 f).obj j).Over S

instance AlgebraicGeometry.Scheme.instOverPullbackCoverOver {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] : Cover.Over S (Cover.pullbackCoverOver S 𝒰 f)

def AlgebraicGeometry.Scheme.Cover.pullbackCoverOver' {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] : Cover P W

A variant of AlgebraicGeometry.Scheme.Cover.pullbackCoverOver with the arguments in the fiber products flipped.

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_map {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] (x : 𝒰.J) : (pullbackCoverOver' S 𝒰 f).map x = (CategoryTheory.Limits.pullback.snd (Hom.asOver (𝒰.map x) S) (Hom.asOver f S)).left

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_J {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] : (pullbackCoverOver' S 𝒰 f).J = 𝒰.J

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_f {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] (x : ↥W) : (pullbackCoverOver' S 𝒰 f).f x = 𝒰.f ((CategoryTheory.ConcreteCategory.hom f.base) x)

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_obj {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] (x : 𝒰.J) : (pullbackCoverOver' S 𝒰 f).obj x = (CategoryTheory.Limits.pullback (Hom.asOver (𝒰.map x) S) (Hom.asOver f S)).left

instance AlgebraicGeometry.Scheme.instOverObjPullbackCoverOver' {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] (j : 𝒰.J) : ((Cover.pullbackCoverOver' S 𝒰 f).obj j).Over S

instance AlgebraicGeometry.Scheme.instOverPullbackCoverOver' {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] : Cover.Over S (Cover.pullbackCoverOver' S 𝒰 f)

def AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp {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)) : Cover P W

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.

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_f {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)) (x : ↥W) : (pullbackCoverOverProp S 𝒰 f hX hW hQ).f x = 𝒰.f ((CategoryTheory.ConcreteCategory.hom f.base) x)

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_obj {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)) (x : 𝒰.J) : (pullbackCoverOverProp S 𝒰 f hX hW hQ).obj x = (CategoryTheory.Limits.pullback (Hom.asOverProp f S) (Hom.asOverProp (𝒰.map x) S)).left

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_J {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)) : (pullbackCoverOverProp S 𝒰 f hX hW hQ).J = 𝒰.J

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_map {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)) (x : 𝒰.J) : (pullbackCoverOverProp S 𝒰 f hX hW hQ).map x = (CategoryTheory.Limits.pullback.fst (Hom.asOverProp f S) (Hom.asOverProp (𝒰.map x) S)).left

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

instance AlgebraicGeometry.Scheme.instOverPullbackCoverOverProp {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)) : Cover.Over S (Cover.pullbackCoverOverProp S 𝒰 f hX hW hQ)

def AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp' {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)) : Cover P W

A variant of AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp with the arguments in the fiber products flipped.

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_J {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)) : (pullbackCoverOverProp' S 𝒰 f hX hW hQ).J = 𝒰.J

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_map {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)) (x : 𝒰.J) : (pullbackCoverOverProp' S 𝒰 f hX hW hQ).map x = (CategoryTheory.Limits.pullback.snd (Hom.asOverProp (𝒰.map x) S) (Hom.asOverProp f S)).left

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_obj {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)) (x : 𝒰.J) : (pullbackCoverOverProp' S 𝒰 f hX hW hQ).obj x = (CategoryTheory.Limits.pullback (Hom.asOverProp (𝒰.map x) S) (Hom.asOverProp f S)).left

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_f {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)) (x : ↥W) : (pullbackCoverOverProp' S 𝒰 f hX hW hQ).f x = 𝒰.f ((CategoryTheory.ConcreteCategory.hom f.base) x)

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

instance AlgebraicGeometry.Scheme.instOverPullbackCoverOverProp' {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)) : Cover.Over S (Cover.pullbackCoverOverProp' S 𝒰 f hX hW hQ)

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

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 𝒱)