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.

Equations

• X.asOverProp S h = { toComma := X.asOver S, prop := h }

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

• f.asOverProp S = { toCommaMorphism := f.asOver S, prop_hom_left := trivial, prop_hom_right := trivial }

class AlgebraicGeometry.Scheme.Cover.Over (S : Scheme) {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X : Scheme} [X.Over S] (𝒰 : Cover (precoverage 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 : 𝒰.I₀) : (𝒰.X j).Over S
• isOver_map (j : 𝒰.I₀) : Hom.IsOver (𝒰.f j) S

instance AlgebraicGeometry.Scheme.instOverCoverOfIsIsoOfIsOver {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] [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)

Equations

• S.instOverCoverOfIsIsoOfIsOver f = { over := fun (x : (AlgebraicGeometry.Scheme.coverOfIsIso f).I₀) => inferInstanceAs (X.Over S), isOver_map := ⋯ }

def AlgebraicGeometry.Scheme.Cover.pullbackCoverOver {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover (precoverage P) X) (f : W ⟶ X) [W.Over S] [X.Over S] [Cover.Over S 𝒰] [Hom.IsOver f S] : Cover (precoverage 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.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.

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_I₀ {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover (precoverage P) X) (f : W ⟶ X) [W.Over S] [X.Over S] [Cover.Over S 𝒰] [Hom.IsOver f S] : (pullbackCoverOver S 𝒰 f).I₀ = 𝒰.I₀

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_X {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover (precoverage P) X) (f : W ⟶ X) [W.Over S] [X.Over S] [Cover.Over S 𝒰] [Hom.IsOver f S] (x : 𝒰.I₀) : (pullbackCoverOver S 𝒰 f).X x = (CategoryTheory.Limits.pullback (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_f {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover (precoverage P) X) (f : W ⟶ X) [W.Over S] [X.Over S] [Cover.Over S 𝒰] [Hom.IsOver f S] (x : 𝒰.I₀) : (pullbackCoverOver S 𝒰 f).f x = (CategoryTheory.Limits.pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left

instance AlgebraicGeometry.Scheme.instOverXPullbackCoverOver {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover (precoverage P) X) (f : W ⟶ X) [W.Over S] [X.Over S] [Cover.Over S 𝒰] [Hom.IsOver f S] (j : 𝒰.I₀) : ((Cover.pullbackCoverOver S 𝒰 f).X j).Over S

Equations

• S.instOverXPullbackCoverOver 𝒰 f j = { hom := (CategoryTheory.Limits.pullback (AlgebraicGeometry.Scheme.Hom.asOver f S) (AlgebraicGeometry.Scheme.Hom.asOver (𝒰.f j) S)).hom }

instance AlgebraicGeometry.Scheme.instOverPullbackCoverOver {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover (precoverage 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)

Equations

• S.instOverPullbackCoverOver 𝒰 f = { over := inferInstance, isOver_map := ⋯ }

def AlgebraicGeometry.Scheme.Cover.pullbackCoverOver' {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover (precoverage P) X) (f : W ⟶ X) [W.Over S] [X.Over S] [Cover.Over S 𝒰] [Hom.IsOver f S] : Cover (precoverage P) W

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.

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_f {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover (precoverage P) X) (f : W ⟶ X) [W.Over S] [X.Over S] [Cover.Over S 𝒰] [Hom.IsOver f S] (x : 𝒰.I₀) : (pullbackCoverOver' S 𝒰 f).f x = (CategoryTheory.Limits.pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_X {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover (precoverage P) X) (f : W ⟶ X) [W.Over S] [X.Over S] [Cover.Over S 𝒰] [Hom.IsOver f S] (x : 𝒰.I₀) : (pullbackCoverOver' S 𝒰 f).X x = (CategoryTheory.Limits.pullback (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_I₀ {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover (precoverage P) X) (f : W ⟶ X) [W.Over S] [X.Over S] [Cover.Over S 𝒰] [Hom.IsOver f S] : (pullbackCoverOver' S 𝒰 f).I₀ = 𝒰.I₀

instance AlgebraicGeometry.Scheme.instOverXPullbackCoverOver' {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover (precoverage P) X) (f : W ⟶ X) [W.Over S] [X.Over S] [Cover.Over S 𝒰] [Hom.IsOver f S] (j : 𝒰.I₀) : ((Cover.pullbackCoverOver' S 𝒰 f).X j).Over S

Equations

• S.instOverXPullbackCoverOver' 𝒰 f j = { hom := (CategoryTheory.Limits.pullback (AlgebraicGeometry.Scheme.Hom.asOver (𝒰.f j) S) (AlgebraicGeometry.Scheme.Hom.asOver f S)).hom }

instance AlgebraicGeometry.Scheme.instOverPullbackCoverOver' {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover (precoverage 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)

Equations

• S.instOverPullbackCoverOver' 𝒰 f = { over := inferInstance, isOver_map := ⋯ }

def AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover (precoverage 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 : 𝒰.I₀), Q (𝒰.X j ↘ S)) : Cover (precoverage 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.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_f {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover (precoverage 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 : 𝒰.I₀), Q (𝒰.X j ↘ S)) (x : 𝒰.I₀) : (pullbackCoverOverProp S 𝒰 f hX hW hQ).f x = (CategoryTheory.Limits.pullback.fst (Hom.asOverProp f S) (Hom.asOverProp (𝒰.f x) S)).left

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_X {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover (precoverage 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 : 𝒰.I₀), Q (𝒰.X j ↘ S)) (x : 𝒰.I₀) : (pullbackCoverOverProp S 𝒰 f hX hW hQ).X x = (CategoryTheory.Limits.pullback (Hom.asOverProp f S) (Hom.asOverProp (𝒰.f x) S)).left

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_I₀ {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover (precoverage 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 : 𝒰.I₀), Q (𝒰.X j ↘ S)) : (pullbackCoverOverProp S 𝒰 f hX hW hQ).I₀ = 𝒰.I₀

instance AlgebraicGeometry.Scheme.instOverXPullbackCoverOverProp {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover (precoverage 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 : 𝒰.I₀), Q (𝒰.X j ↘ S)) (j : 𝒰.I₀) : ((Cover.pullbackCoverOverProp S 𝒰 f hX hW hQ).X j).Over S

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.Scheme.instOverPullbackCoverOverProp {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover (precoverage 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 : 𝒰.I₀), Q (𝒰.X j ↘ S)) : Cover.Over S (Cover.pullbackCoverOverProp S 𝒰 f hX hW hQ)

Equations

• S.instOverPullbackCoverOverProp 𝒰 f hX hW hQ = { over := inferInstance, isOver_map := ⋯ }

def AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp' {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover (precoverage 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 : 𝒰.I₀), Q (𝒰.X j ↘ S)) : Cover (precoverage P) W

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.

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_f {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover (precoverage 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 : 𝒰.I₀), Q (𝒰.X j ↘ S)) (x : 𝒰.I₀) : (pullbackCoverOverProp' S 𝒰 f hX hW hQ).f x = (CategoryTheory.Limits.pullback.snd (Hom.asOverProp (𝒰.f x) S) (Hom.asOverProp f S)).left

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_I₀ {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover (precoverage 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 : 𝒰.I₀), Q (𝒰.X j ↘ S)) : (pullbackCoverOverProp' S 𝒰 f hX hW hQ).I₀ = 𝒰.I₀

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_X {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover (precoverage 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 : 𝒰.I₀), Q (𝒰.X j ↘ S)) (x : 𝒰.I₀) : (pullbackCoverOverProp' S 𝒰 f hX hW hQ).X x = (CategoryTheory.Limits.pullback (Hom.asOverProp (𝒰.f x) S) (Hom.asOverProp f S)).left

instance AlgebraicGeometry.Scheme.instOverXPullbackCoverOverProp' {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover (precoverage 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 : 𝒰.I₀), Q (𝒰.X j ↘ S)) (j : 𝒰.I₀) : ((Cover.pullbackCoverOverProp' S 𝒰 f hX hW hQ).X j).Over S

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.Scheme.instOverPullbackCoverOverProp' {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover (precoverage 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 : 𝒰.I₀), Q (𝒰.X j ↘ S)) : Cover.Over S (Cover.pullbackCoverOverProp' S 𝒰 f hX hW hQ)

Equations

• S.instOverPullbackCoverOverProp' 𝒰 f hX hW hQ = { over := inferInstance, isOver_map := ⋯ }

instance AlgebraicGeometry.Scheme.instOverXBind {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] [P.IsStableUnderComposition] {X : Scheme} (𝒰 : Cover (precoverage P) X) (𝒱 : (x : 𝒰.I₀) → Cover (precoverage P) (𝒰.X x)) [X.Over S] [Cover.Over S 𝒰] [(x : 𝒰.I₀) → Cover.Over S (𝒱 x)] (j : (CategoryTheory.Precoverage.ZeroHypercover.bind 𝒰 𝒱).I₀) : ((CategoryTheory.Precoverage.ZeroHypercover.bind 𝒰 𝒱).X j).Over S

Equations

• S.instOverXBind 𝒰 𝒱 j = inferInstanceAs (((𝒱 j.fst).X j.snd).Over S)

instance AlgebraicGeometry.Scheme.instOverBind {P : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] [P.IsStableUnderComposition] {X : Scheme} (𝒰 : Cover (precoverage P) X) (𝒱 : (x : 𝒰.I₀) → Cover (precoverage P) (𝒰.X x)) [X.Over S] [Cover.Over S 𝒰] [(x : 𝒰.I₀) → Cover.Over S (𝒱 x)] : Cover.Over S (CategoryTheory.Precoverage.ZeroHypercover.bind 𝒰 𝒱)

Equations

• One or more equations did not get rendered due to their size.