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 AlgebraicGeometry.Scheme} (X S : AlgebraicGeometry.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 AlgebraicGeometry.Scheme} {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) (S : AlgebraicGeometry.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 : AlgebraicGeometry.Scheme) {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} [X.Over S] (𝒰 : AlgebraicGeometry.Scheme.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) : AlgebraicGeometry.Scheme.Hom.IsOver (𝒰.map j) S

instance AlgebraicGeometry.Scheme.instOverCoverOfIsIsoOfIsOver {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [P.ContainsIdentities] [P.RespectsIso] {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [X.Over S] [Y.Over S] [AlgebraicGeometry.Scheme.Hom.IsOver f S] [CategoryTheory.IsIso f] : AlgebraicGeometry.Scheme.Cover.Over S (AlgebraicGeometry.Scheme.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 AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [W.Over S] [X.Over S] [AlgebraicGeometry.Scheme.Cover.Over S 𝒰] [AlgebraicGeometry.Scheme.Hom.IsOver f S] : AlgebraicGeometry.Scheme.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 AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [W.Over S] [X.Over S] [AlgebraicGeometry.Scheme.Cover.Over S 𝒰] [AlgebraicGeometry.Scheme.Hom.IsOver f S] : (AlgebraicGeometry.Scheme.Cover.pullbackCoverOver S 𝒰 f).J = 𝒰.J

@[simp]

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

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_f {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [W.Over S] [X.Over S] [AlgebraicGeometry.Scheme.Cover.Over S 𝒰] [AlgebraicGeometry.Scheme.Hom.IsOver f S] (x : ↑↑W.toPresheafedSpace) : (AlgebraicGeometry.Scheme.Cover.pullbackCoverOver S 𝒰 f).f x = 𝒰.f (f.base x)

@[simp]

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

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

Equations

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

def AlgebraicGeometry.Scheme.Cover.pullbackCoverOver' {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [W.Over S] [X.Over S] [AlgebraicGeometry.Scheme.Cover.Over S 𝒰] [AlgebraicGeometry.Scheme.Hom.IsOver f S] : AlgebraicGeometry.Scheme.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 AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [W.Over S] [X.Over S] [AlgebraicGeometry.Scheme.Cover.Over S 𝒰] [AlgebraicGeometry.Scheme.Hom.IsOver f S] (x : 𝒰.J) : (AlgebraicGeometry.Scheme.Cover.pullbackCoverOver' S 𝒰 f).map x = (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Hom.asOver (𝒰.map x) S) (AlgebraicGeometry.Scheme.Hom.asOver f S)).left

@[simp]

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

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_f {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [W.Over S] [X.Over S] [AlgebraicGeometry.Scheme.Cover.Over S 𝒰] [AlgebraicGeometry.Scheme.Hom.IsOver f S] (x : ↑↑W.toPresheafedSpace) : (AlgebraicGeometry.Scheme.Cover.pullbackCoverOver' S 𝒰 f).f x = 𝒰.f (f.base x)

@[simp]

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

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

Equations

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

def AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [W.Over S] [X.Over S] [AlgebraicGeometry.Scheme.Cover.Over S 𝒰] [AlgebraicGeometry.Scheme.Hom.IsOver f S] {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [Q.HasOfPostcompProperty Q] [Q.IsStableUnderBaseChange] [Q.IsStableUnderComposition] (hX : Q (X ↘ S)) (hW : Q (W ↘ S)) (hQ : ∀ (j : 𝒰.J), Q (𝒰.obj j ↘ S)) : AlgebraicGeometry.Scheme.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 AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [W.Over S] [X.Over S] [AlgebraicGeometry.Scheme.Cover.Over S 𝒰] [AlgebraicGeometry.Scheme.Hom.IsOver f S] {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.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) : (AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp S 𝒰 f hX hW hQ).map x = (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Hom.asOverProp f S) (AlgebraicGeometry.Scheme.Hom.asOverProp (𝒰.map x) S)).left

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_J {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [W.Over S] [X.Over S] [AlgebraicGeometry.Scheme.Cover.Over S 𝒰] [AlgebraicGeometry.Scheme.Hom.IsOver f S] {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [Q.HasOfPostcompProperty Q] [Q.IsStableUnderBaseChange] [Q.IsStableUnderComposition] (hX : Q (X ↘ S)) (hW : Q (W ↘ S)) (hQ : ∀ (j : 𝒰.J), Q (𝒰.obj j ↘ S)) : (AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp S 𝒰 f hX hW hQ).J = 𝒰.J

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_obj {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [W.Over S] [X.Over S] [AlgebraicGeometry.Scheme.Cover.Over S 𝒰] [AlgebraicGeometry.Scheme.Hom.IsOver f S] {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.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) : (AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp S 𝒰 f hX hW hQ).obj x = (CategoryTheory.Limits.pullback (AlgebraicGeometry.Scheme.Hom.asOverProp f S) (AlgebraicGeometry.Scheme.Hom.asOverProp (𝒰.map x) S)).left

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_f {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [W.Over S] [X.Over S] [AlgebraicGeometry.Scheme.Cover.Over S 𝒰] [AlgebraicGeometry.Scheme.Hom.IsOver f S] {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.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.toPresheafedSpace) : (AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp S 𝒰 f hX hW hQ).f x = 𝒰.f (f.base x)

instance AlgebraicGeometry.Scheme.instOverObjPullbackCoverOverProp {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [W.Over S] [X.Over S] [AlgebraicGeometry.Scheme.Cover.Over S 𝒰] [AlgebraicGeometry.Scheme.Hom.IsOver f S] {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.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) : ((AlgebraicGeometry.Scheme.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 AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [W.Over S] [X.Over S] [AlgebraicGeometry.Scheme.Cover.Over S 𝒰] [AlgebraicGeometry.Scheme.Hom.IsOver f S] {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [Q.HasOfPostcompProperty Q] [Q.IsStableUnderBaseChange] [Q.IsStableUnderComposition] (hX : Q (X ↘ S)) (hW : Q (W ↘ S)) (hQ : ∀ (j : 𝒰.J), Q (𝒰.obj j ↘ S)) : AlgebraicGeometry.Scheme.Cover.Over S (AlgebraicGeometry.Scheme.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 AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [W.Over S] [X.Over S] [AlgebraicGeometry.Scheme.Cover.Over S 𝒰] [AlgebraicGeometry.Scheme.Hom.IsOver f S] {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [Q.HasOfPostcompProperty Q] [Q.IsStableUnderBaseChange] [Q.IsStableUnderComposition] (hX : Q (X ↘ S)) (hW : Q (W ↘ S)) (hQ : ∀ (j : 𝒰.J), Q (𝒰.obj j ↘ S)) : AlgebraicGeometry.Scheme.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 AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [W.Over S] [X.Over S] [AlgebraicGeometry.Scheme.Cover.Over S 𝒰] [AlgebraicGeometry.Scheme.Hom.IsOver f S] {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.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) : (AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp' S 𝒰 f hX hW hQ).obj x = (CategoryTheory.Limits.pullback (AlgebraicGeometry.Scheme.Hom.asOverProp (𝒰.map x) S) (AlgebraicGeometry.Scheme.Hom.asOverProp f S)).left

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_J {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [W.Over S] [X.Over S] [AlgebraicGeometry.Scheme.Cover.Over S 𝒰] [AlgebraicGeometry.Scheme.Hom.IsOver f S] {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [Q.HasOfPostcompProperty Q] [Q.IsStableUnderBaseChange] [Q.IsStableUnderComposition] (hX : Q (X ↘ S)) (hW : Q (W ↘ S)) (hQ : ∀ (j : 𝒰.J), Q (𝒰.obj j ↘ S)) : (AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp' S 𝒰 f hX hW hQ).J = 𝒰.J

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_f {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [W.Over S] [X.Over S] [AlgebraicGeometry.Scheme.Cover.Over S 𝒰] [AlgebraicGeometry.Scheme.Hom.IsOver f S] {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.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.toPresheafedSpace) : (AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp' S 𝒰 f hX hW hQ).f x = 𝒰.f (f.base x)

theorem AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_map {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [W.Over S] [X.Over S] [AlgebraicGeometry.Scheme.Cover.Over S 𝒰] [AlgebraicGeometry.Scheme.Hom.IsOver f S] {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.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) : (AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp' S 𝒰 f hX hW hQ).map x = (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Hom.asOverProp (𝒰.map x) S) (AlgebraicGeometry.Scheme.Hom.asOverProp f S)).left

instance AlgebraicGeometry.Scheme.instOverObjPullbackCoverOverProp' {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [W.Over S] [X.Over S] [AlgebraicGeometry.Scheme.Cover.Over S 𝒰] [AlgebraicGeometry.Scheme.Hom.IsOver f S] {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.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) : ((AlgebraicGeometry.Scheme.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 AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [W.Over S] [X.Over S] [AlgebraicGeometry.Scheme.Cover.Over S 𝒰] [AlgebraicGeometry.Scheme.Hom.IsOver f S] {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [Q.HasOfPostcompProperty Q] [Q.IsStableUnderBaseChange] [Q.IsStableUnderComposition] (hX : Q (X ↘ S)) (hW : Q (W ↘ S)) (hQ : ∀ (j : 𝒰.J), Q (𝒰.obj j ↘ S)) : AlgebraicGeometry.Scheme.Cover.Over S (AlgebraicGeometry.Scheme.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 AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [P.IsStableUnderComposition] {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (𝒱 : (x : 𝒰.J) → AlgebraicGeometry.Scheme.Cover P (𝒰.obj x)) [X.Over S] [AlgebraicGeometry.Scheme.Cover.Over S 𝒰] [(x : 𝒰.J) → AlgebraicGeometry.Scheme.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 AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [P.IsStableUnderComposition] {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (𝒱 : (x : 𝒰.J) → AlgebraicGeometry.Scheme.Cover P (𝒰.obj x)) [X.Over S] [AlgebraicGeometry.Scheme.Cover.Over S 𝒰] [(x : 𝒰.J) → AlgebraicGeometry.Scheme.Cover.Over S (𝒱 x)] : AlgebraicGeometry.Scheme.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 := ⋯ }