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} {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)

Equations

• S.instOverCoverOfIsIsoOfIsOver f = { over := fun (x : (AlgebraicGeometry.Scheme.coverOfIsIso f).J) => 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 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.

Equations

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

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

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

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

Equations

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

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)

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

Equations

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

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

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

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

Equations

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

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)

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

Equations

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

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

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_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_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

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

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

Equations

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

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'_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'_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'_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

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.

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)

Equations

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

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

• S.instOverObjBind 𝒰 𝒱 j = inferInstanceAs (((𝒱 j.fst).obj j.snd).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 𝒱)

Equations

• S.instOverBind 𝒰 𝒱 = { over := fun (x : (𝒰.bind 𝒱).J) => match x with | ⟨i, j⟩ => inferInstanceAs (((𝒱 i).obj j).Over S), isOver_map := ⋯ }