Covers of schemes

This file provides the basic API for covers of schemes. A cover of a scheme X with respect to a morphism property P is a jointly surjective indexed family of scheme morphisms with target X all satisfying P.

Implementation details

The definition on the pullback of a cover along a morphism depends on results that are developed later in the import tree. Hence in this file, they have additional assumptions that will be automatically satisfied in later files. The motivation here is that we already know that these assumptions are satisfied for open immersions and hence the cover API for open immersions can be used to deduce these assumptions in the general case.

structure AlgebraicGeometry.Scheme.Cover (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) (X : AlgebraicGeometry.Scheme) : Type (max (u + 1) (v + 1))

A cover of X consists of jointly surjective indexed family of scheme morphisms with target X all satisfying P.

This is merely a coverage in the pretopology defined by P, and it would be optimal if we could reuse the existing API about pretopologies, However, the definitions of sieves and grothendieck topologies uses Props, so that the actual open sets and immersions are hard to obtain. Also, since such a coverage in the pretopology usually contains a proper class of immersions, it is quite hard to glue them, reason about finite covers, etc.

Note: The map_prop field is equipped with a default argument by infer_instance. In general this causes worse error messages, but in practice P is mostly defined via class.

• J : Type v

  index set of a cover of a scheme X

• obj (j : self.J) : AlgebraicGeometry.Scheme

  the components of a cover

• map (j : self.J) : self.obj j ⟶ X

  the components map to X

• f (x : ↑↑X.toPresheafedSpace) : self.J

  given a point of x : X, f x is the index of the component which contains x

• covers (x : ↑↑X.toPresheafedSpace) : x ∈ Set.range ⇑(self.map (self.f x)).base

  the components cover X

• map_prop (j : self.J) : P (self.map j)

  the component maps satisfy P

theorem AlgebraicGeometry.Scheme.Cover.iUnion_range {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) : ⋃ (i : 𝒰.J), Set.range ⇑(𝒰.map i).base = Set.univ

theorem AlgebraicGeometry.Scheme.Cover.exists_eq {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (x : ↑↑X.toPresheafedSpace) : ∃ (i : 𝒰.J) (y : ↑↑(𝒰.obj i).toPresheafedSpace), (𝒰.map i).base y = x

def AlgebraicGeometry.Scheme.Cover.mkOfCovers {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} (J : Type u_1) (obj : J → AlgebraicGeometry.Scheme) (map : (j : J) → obj j ⟶ X) (covers : ∀ (x : ↑↑X.toPresheafedSpace), ∃ (j : J) (y : ↑↑(obj j).toPresheafedSpace), (map j).base y = x) (map_prop : ∀ (j : J), P (map j) := by infer_instance) : AlgebraicGeometry.Scheme.Cover P X

Given a family of schemes with morphisms to X satisfying P that jointly cover X, this an associated P-cover of X.

Equations

• AlgebraicGeometry.Scheme.Cover.mkOfCovers J obj map covers map_prop = { J := J, obj := obj, map := map, f := fun (x : ↑↑X.toPresheafedSpace) => ⋯.choose, covers := ⋯, map_prop := map_prop }

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.mkOfCovers_f {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} (J : Type u_1) (obj : J → AlgebraicGeometry.Scheme) (map : (j : J) → obj j ⟶ X) (covers : ∀ (x : ↑↑X.toPresheafedSpace), ∃ (j : J) (y : ↑↑(obj j).toPresheafedSpace), (map j).base y = x) (map_prop : ∀ (j : J), P (map j) := by infer_instance) (x : ↑↑X.toPresheafedSpace) : (AlgebraicGeometry.Scheme.Cover.mkOfCovers J obj map covers map_prop).f x = ⋯.choose

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.mkOfCovers_J {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} (J : Type u_1) (obj : J → AlgebraicGeometry.Scheme) (map : (j : J) → obj j ⟶ X) (covers : ∀ (x : ↑↑X.toPresheafedSpace), ∃ (j : J) (y : ↑↑(obj j).toPresheafedSpace), (map j).base y = x) (map_prop : ∀ (j : J), P (map j) := by infer_instance) : (AlgebraicGeometry.Scheme.Cover.mkOfCovers J obj map covers map_prop).J = J

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.mkOfCovers_obj {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} (J : Type u_1) (obj : J → AlgebraicGeometry.Scheme) (map : (j : J) → obj j ⟶ X) (covers : ∀ (x : ↑↑X.toPresheafedSpace), ∃ (j : J) (y : ↑↑(obj j).toPresheafedSpace), (map j).base y = x) (map_prop : ∀ (j : J), P (map j) := by infer_instance) (a✝ : J) : (AlgebraicGeometry.Scheme.Cover.mkOfCovers J obj map covers map_prop).obj a✝ = obj a✝

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.mkOfCovers_map {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} (J : Type u_1) (obj : J → AlgebraicGeometry.Scheme) (map : (j : J) → obj j ⟶ X) (covers : ∀ (x : ↑↑X.toPresheafedSpace), ∃ (j : J) (y : ↑↑(obj j).toPresheafedSpace), (map j).base y = x) (map_prop : ∀ (j : J), P (map j) := by infer_instance) (j : J) : (AlgebraicGeometry.Scheme.Cover.mkOfCovers J obj map covers map_prop).map j = map j

def AlgebraicGeometry.Scheme.Cover.changeProp {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} (Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (h : ∀ (j : 𝒰.J), Q (𝒰.map j)) : AlgebraicGeometry.Scheme.Cover Q X

Turn a P-cover into a Q-cover by showing that the components satisfiy Q.

Equations

• AlgebraicGeometry.Scheme.Cover.changeProp Q 𝒰 h = { J := 𝒰.J, obj := 𝒰.obj, map := 𝒰.map, f := 𝒰.f, covers := ⋯, map_prop := h }

def AlgebraicGeometry.Scheme.Cover.bind {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) [P.IsStableUnderComposition] (f : (x : 𝒰.J) → AlgebraicGeometry.Scheme.Cover P (𝒰.obj x)) : AlgebraicGeometry.Scheme.Cover P X

Given a P-cover { Uᵢ } of X, and for each Uᵢ a P-cover, we may combine these covers to form a P-cover of X.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.bind_map {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) [P.IsStableUnderComposition] (f : (x : 𝒰.J) → AlgebraicGeometry.Scheme.Cover P (𝒰.obj x)) (x : (i : 𝒰.J) × (f i).J) : (𝒰.bind f).map x = CategoryTheory.CategoryStruct.comp ((f x.fst).map x.snd) (𝒰.map x.fst)

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.bind_J {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) [P.IsStableUnderComposition] (f : (x : 𝒰.J) → AlgebraicGeometry.Scheme.Cover P (𝒰.obj x)) : (𝒰.bind f).J = ((i : 𝒰.J) × (f i).J)

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.bind_obj {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) [P.IsStableUnderComposition] (f : (x : 𝒰.J) → AlgebraicGeometry.Scheme.Cover P (𝒰.obj x)) (x : (i : 𝒰.J) × (f i).J) : (𝒰.bind f).obj x = (f x.fst).obj x.snd

def AlgebraicGeometry.Scheme.coverOfIsIso {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.ContainsIdentities] [P.RespectsIso] {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] : AlgebraicGeometry.Scheme.Cover P Y

An isomorphism X ⟶ Y is a P-cover of Y.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.coverOfIsIso_J {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.ContainsIdentities] [P.RespectsIso] {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] : (AlgebraicGeometry.Scheme.coverOfIsIso f).J = PUnit.{v + 1}

@[simp]

theorem AlgebraicGeometry.Scheme.coverOfIsIso_obj {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.ContainsIdentities] [P.RespectsIso] {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] (x✝ : PUnit.{v + 1}) : (AlgebraicGeometry.Scheme.coverOfIsIso f).obj x✝ = X

@[simp]

theorem AlgebraicGeometry.Scheme.coverOfIsIso_map {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.ContainsIdentities] [P.RespectsIso] {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] (x✝ : PUnit.{v + 1}) : (AlgebraicGeometry.Scheme.coverOfIsIso f).map x✝ = f

def AlgebraicGeometry.Scheme.Cover.copy {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.RespectsIso] {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (J : Type u_1) (obj : J → AlgebraicGeometry.Scheme) (map : (i : J) → obj i ⟶ X) (e₁ : J ≃ 𝒰.J) (e₂ : (i : J) → obj i ≅ 𝒰.obj (e₁ i)) (h : ∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂ i).hom (𝒰.map (e₁ i))) : AlgebraicGeometry.Scheme.Cover P X

We construct a cover from another, by providing the needed fields and showing that the provided fields are isomorphic with the original cover.

Equations

• 𝒰.copy J obj map e₁ e₂ h = { J := J, obj := obj, map := map, f := fun (x : ↑↑X.toPresheafedSpace) => e₁.symm (𝒰.f x), covers := ⋯, map_prop := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.copy_J {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.RespectsIso] {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (J : Type u_1) (obj : J → AlgebraicGeometry.Scheme) (map : (i : J) → obj i ⟶ X) (e₁ : J ≃ 𝒰.J) (e₂ : (i : J) → obj i ≅ 𝒰.obj (e₁ i)) (h : ∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂ i).hom (𝒰.map (e₁ i))) : (𝒰.copy J obj map e₁ e₂ h).J = J

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.copy_obj {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.RespectsIso] {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (J : Type u_1) (obj : J → AlgebraicGeometry.Scheme) (map : (i : J) → obj i ⟶ X) (e₁ : J ≃ 𝒰.J) (e₂ : (i : J) → obj i ≅ 𝒰.obj (e₁ i)) (h : ∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂ i).hom (𝒰.map (e₁ i))) (a✝ : J) : (𝒰.copy J obj map e₁ e₂ h).obj a✝ = obj a✝

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.copy_map {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.RespectsIso] {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (J : Type u_1) (obj : J → AlgebraicGeometry.Scheme) (map : (i : J) → obj i ⟶ X) (e₁ : J ≃ 𝒰.J) (e₂ : (i : J) → obj i ≅ 𝒰.obj (e₁ i)) (h : ∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂ i).hom (𝒰.map (e₁ i))) (i : J) : (𝒰.copy J obj map e₁ e₂ h).map i = map i

def AlgebraicGeometry.Scheme.Cover.pushforwardIso {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.RespectsIso] [P.ContainsIdentities] [P.IsStableUnderComposition] {X Y : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : X ⟶ Y) [CategoryTheory.IsIso f] : AlgebraicGeometry.Scheme.Cover P Y

The pushforward of a cover along an isomorphism.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pushforwardIso_map {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.RespectsIso] [P.ContainsIdentities] [P.IsStableUnderComposition] {X Y : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : X ⟶ Y) [CategoryTheory.IsIso f] (x✝ : 𝒰.J) : (𝒰.pushforwardIso f).map x✝ = CategoryTheory.CategoryStruct.comp (𝒰.map x✝) f

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pushforwardIso_J {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.RespectsIso] [P.ContainsIdentities] [P.IsStableUnderComposition] {X Y : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : X ⟶ Y) [CategoryTheory.IsIso f] : (𝒰.pushforwardIso f).J = 𝒰.J

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pushforwardIso_obj {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.RespectsIso] [P.ContainsIdentities] [P.IsStableUnderComposition] {X Y : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : X ⟶ Y) [CategoryTheory.IsIso f] (x✝ : 𝒰.J) : (𝒰.pushforwardIso f).obj x✝ = 𝒰.obj x✝

def AlgebraicGeometry.Scheme.Cover.add {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X Y : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : Y ⟶ X) (hf : P f := by infer_instance) : AlgebraicGeometry.Scheme.Cover P X

Adding map satisfying P into a cover gives another cover.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.add_J {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X Y : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : Y ⟶ X) (hf : P f := by infer_instance) : (𝒰.add f hf).J = Option 𝒰.J

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.add_map {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X Y : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : Y ⟶ X) (hf : P f := by infer_instance) (i : Option 𝒰.J) : (𝒰.add f hf).map i = Option.rec f 𝒰.map i

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.add_obj {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X Y : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : Y ⟶ X) (hf : P f := by infer_instance) (i : Option 𝒰.J) : (𝒰.add f hf).obj i = Option.rec Y 𝒰.obj i

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.add_f {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X Y : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : Y ⟶ X) (hf : P f := by infer_instance) (x : ↑↑X.toPresheafedSpace) : (𝒰.add f hf).f x = some (𝒰.f x)

class AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) : Prop

A morphism property of schemes is said to preserve joint surjectivity, if for any pair of morphisms f : X ⟶ S and g : Y ⟶ S where g satisfies P, any pair of points x : X and y : Y with f x = g y can be lifted to a point of X ×[S] Y.

In later files, this will be automatic, since this holds for any morphism g (see AlgebraicGeometry.Scheme.isJointlySurjectivePreserving). But at this early stage in the import tree, we only know it for open immersions.

• exists_preimage_fst_triplet_of_prop {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} [CategoryTheory.Limits.HasPullback f g] (hg : P g) (x : ↑↑X.toPresheafedSpace) (y : ↑↑Y.toPresheafedSpace) (h : f.base x = g.base y) : ∃ (a : ↑↑(CategoryTheory.Limits.pullback f g).toPresheafedSpace), (CategoryTheory.Limits.pullback.fst f g).base a = x

theorem AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving.exists_preimage_snd_triplet_of_prop {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} [CategoryTheory.Limits.HasPullback f g] (hf : P f) (x : ↑↑X.toPresheafedSpace) (y : ↑↑Y.toPresheafedSpace) (h : f.base x = g.base y) : ∃ (a : ↑↑(CategoryTheory.Limits.pullback f g).toPresheafedSpace), (CategoryTheory.Limits.pullback.snd f g).base a = y

instance AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving @AlgebraicGeometry.IsOpenImmersion

def AlgebraicGeometry.Scheme.Cover.pullbackCover {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [∀ (x : 𝒰.J), CategoryTheory.Limits.HasPullback f (𝒰.map x)] : AlgebraicGeometry.Scheme.Cover P W

Given a cover on X, we may pull them back along a morphism W ⟶ X to obtain a cover of W.

Note that this requires the (unnecessary) assumptions that the pullback exists and that P preserves joint surjectivity. This is needed, because we don't know these in general at this stage of the import tree, but this API is used in the case of P = IsOpenImmersion to obtain these results in the general case.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackCover_f {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [∀ (x : 𝒰.J), CategoryTheory.Limits.HasPullback f (𝒰.map x)] (x : ↑↑W.toPresheafedSpace) : (𝒰.pullbackCover f).f x = 𝒰.f (f.base x)

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackCover_J {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [∀ (x : 𝒰.J), CategoryTheory.Limits.HasPullback f (𝒰.map x)] : (𝒰.pullbackCover f).J = 𝒰.J

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackCover_map {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [∀ (x : 𝒰.J), CategoryTheory.Limits.HasPullback f (𝒰.map x)] (x✝ : 𝒰.J) : (𝒰.pullbackCover f).map x✝ = CategoryTheory.Limits.pullback.fst f (𝒰.map x✝)

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackCover_obj {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [∀ (x : 𝒰.J), CategoryTheory.Limits.HasPullback f (𝒰.map x)] (x : 𝒰.J) : (𝒰.pullbackCover f).obj x = CategoryTheory.Limits.pullback f (𝒰.map x)

def AlgebraicGeometry.Scheme.Cover.pullbackHom {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) (i : 𝒰.1) [∀ (x : 𝒰.J), CategoryTheory.Limits.HasPullback f (𝒰.map x)] : (𝒰.pullbackCover f).obj i ⟶ 𝒰.obj i

The family of morphisms from the pullback cover to the original cover.

Equations

• 𝒰.pullbackHom f i = CategoryTheory.Limits.pullback.snd f (𝒰.map i)

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackHom_map {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [∀ (x : 𝒰.J), CategoryTheory.Limits.HasPullback f (𝒰.map x)] (i : 𝒰.1) : CategoryTheory.CategoryStruct.comp (𝒰.pullbackHom f i) (𝒰.map i) = CategoryTheory.CategoryStruct.comp ((𝒰.pullbackCover f).map i) f

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackHom_map_assoc {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [∀ (x : 𝒰.J), CategoryTheory.Limits.HasPullback f (𝒰.map x)] (i : 𝒰.1) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (𝒰.pullbackHom f i) (CategoryTheory.CategoryStruct.comp (𝒰.map i) h) = CategoryTheory.CategoryStruct.comp ((𝒰.pullbackCover f).map i) (CategoryTheory.CategoryStruct.comp f h)

def AlgebraicGeometry.Scheme.Cover.pullbackCover' {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [∀ (x : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map x) f] : AlgebraicGeometry.Scheme.Cover P W

Given a cover on X, we may pull them back along a morphism f : W ⟶ X to obtain a cover of W. This is similar to Scheme.Cover.pullbackCover, but here we take pullback (𝒰.map x) f instead of pullback f (𝒰.map x).

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackCover'_obj {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [∀ (x : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map x) f] (x : 𝒰.J) : (𝒰.pullbackCover' f).obj x = CategoryTheory.Limits.pullback (𝒰.map x) f

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackCover'_map {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [∀ (x : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map x) f] (x✝ : 𝒰.J) : (𝒰.pullbackCover' f).map x✝ = CategoryTheory.Limits.pullback.snd (𝒰.map x✝) f

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackCover'_J {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [∀ (x : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map x) f] : (𝒰.pullbackCover' f).J = 𝒰.J

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackCover'_f {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderBaseChange] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (f : W ⟶ X) [∀ (x : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map x) f] (x : ↑↑W.toPresheafedSpace) : (𝒰.pullbackCover' f).f x = 𝒰.f (f.base x)

def AlgebraicGeometry.Scheme.Cover.inter {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderBaseChange] [P.IsStableUnderComposition] [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X : AlgebraicGeometry.Scheme} (𝒰₁ : AlgebraicGeometry.Scheme.Cover P X) (𝒰₂ : AlgebraicGeometry.Scheme.Cover P X) [∀ (i : 𝒰₁.J) (j : 𝒰₂.J), CategoryTheory.Limits.HasPullback (𝒰₁.map i) (𝒰₂.map j)] : AlgebraicGeometry.Scheme.Cover P X

Given covers { Uᵢ } and { Uⱼ }, we may form the cover { Uᵢ ×[X] Uⱼ }.

Equations

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

structure AlgebraicGeometry.Scheme.AffineCover (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) (X : AlgebraicGeometry.Scheme) : Type (max (u + 1) (v + 1))

An affine cover of X consists of a jointly surjective family of maps into X from spectra of rings.

Note: The map_prop field is equipped with a default argument by infer_instance. In general this causes worse error messages, but in practice P is mostly defined via class.

• J : Type v

  index set of an affine cover of a scheme X

• obj (j : self.J) : CommRingCat

  the ring associated to a component of an affine cover

• map (j : self.J) : AlgebraicGeometry.Spec (self.obj j) ⟶ X

  the components map to X

• f (x : ↑↑X.toPresheafedSpace) : self.J

  given a point of x : X, f x is the index of the component which contains x

• covers (x : ↑↑X.toPresheafedSpace) : x ∈ Set.range ⇑(self.map (self.f x)).base

  the components cover X

• map_prop (j : self.J) : P (self.map j)

  the component maps satisfy P

def AlgebraicGeometry.Scheme.AffineCover.cover {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.AffineCover P X) : AlgebraicGeometry.Scheme.Cover P X

The cover associated to an affine cover.

Equations

• 𝒰.cover = { J := 𝒰.J, obj := fun (j : 𝒰.J) => AlgebraicGeometry.Spec (𝒰.obj j), map := 𝒰.map, f := 𝒰.f, covers := ⋯, map_prop := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.AffineCover.cover_map {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.AffineCover P X) (j : 𝒰.J) : 𝒰.cover.map j = 𝒰.map j

@[simp]

theorem AlgebraicGeometry.Scheme.AffineCover.cover_J {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.AffineCover P X) : 𝒰.cover.J = 𝒰.J

@[simp]

theorem AlgebraicGeometry.Scheme.AffineCover.cover_obj {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.AffineCover P X) (j : 𝒰.J) : 𝒰.cover.obj j = AlgebraicGeometry.Spec (𝒰.obj j)

@[simp]

theorem AlgebraicGeometry.Scheme.AffineCover.cover_f {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.AffineCover P X) (x : ↑↑X.toPresheafedSpace) : 𝒰.cover.f x = 𝒰.f x

structure AlgebraicGeometry.Scheme.Cover.Hom {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} (𝒰 𝒱 : AlgebraicGeometry.Scheme.Cover P X) : Type (max u v)

A morphism between covers 𝒰 ⟶ 𝒱 indicates that 𝒰 is a refinement of 𝒱. Since covers of schemes are indexed, the definition also involves a map on the indexing types.

• idx : 𝒰.J → 𝒱.J

  The map on indexing types associated to a morphism of covers.

• app (j : 𝒰.J) : 𝒰.obj j ⟶ 𝒱.obj (self.idx j)

  The morphism between open subsets associated to a morphism of covers.

• app_prop (j : 𝒰.J) : P (self.app j)
• w (j : 𝒰.J) : CategoryTheory.CategoryStruct.comp (self.app j) (𝒱.map (self.idx j)) = 𝒰.map j

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.Hom.w_assoc {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} {𝒰 𝒱 : AlgebraicGeometry.Scheme.Cover P X} (self : 𝒰.Hom 𝒱) (j : 𝒰.J) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.app j) (CategoryTheory.CategoryStruct.comp (𝒱.map (self.idx j)) h) = CategoryTheory.CategoryStruct.comp (𝒰.map j) h

def AlgebraicGeometry.Scheme.Cover.Hom.id {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.ContainsIdentities] {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) : 𝒰.Hom 𝒰

The identity morphism in the category of covers of a scheme.

Equations

• AlgebraicGeometry.Scheme.Cover.Hom.id 𝒰 = { idx := fun (j : 𝒰.J) => j, app := fun (x : 𝒰.J) => CategoryTheory.CategoryStruct.id (𝒰.obj x), app_prop := ⋯, w := ⋯ }

def AlgebraicGeometry.Scheme.Cover.Hom.comp {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderComposition] {X : AlgebraicGeometry.Scheme} {𝒰 𝒱 𝒲 : AlgebraicGeometry.Scheme.Cover P X} (f : 𝒰.Hom 𝒱) (g : 𝒱.Hom 𝒲) : 𝒰.Hom 𝒲

The composition of two morphisms in the category of covers of a scheme.

Equations

• f.comp g = { idx := fun (j : 𝒰.J) => g.idx (f.idx j), app := fun (x : 𝒰.J) => CategoryTheory.CategoryStruct.comp (f.app x) (g.app (f.idx x)), app_prop := ⋯, w := ⋯ }

instance AlgebraicGeometry.Scheme.Cover.category {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsMultiplicative] {X : AlgebraicGeometry.Scheme} : CategoryTheory.Category.{max u v, max (v + 1) (u + 1)} (AlgebraicGeometry.Scheme.Cover P X)

Equations

• AlgebraicGeometry.Scheme.Cover.category = CategoryTheory.Category.mk ⋯ ⋯ ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.id_idx_apply {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsMultiplicative] {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (j : 𝒰.J) : (CategoryTheory.CategoryStruct.id 𝒰).idx j = j

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.id_app {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsMultiplicative] {X : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover P X) (j : 𝒰.J) : (CategoryTheory.CategoryStruct.id 𝒰).app j = CategoryTheory.CategoryStruct.id (𝒰.obj j)

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.comp_idx_apply {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsMultiplicative] {X : AlgebraicGeometry.Scheme} {𝒰 𝒱 𝒲 : AlgebraicGeometry.Scheme.Cover P X} (f : 𝒰 ⟶ 𝒱) (g : 𝒱 ⟶ 𝒲) (j : 𝒰.J) : (CategoryTheory.CategoryStruct.comp f g).idx j = g.idx (f.idx j)

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.comp_app {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsMultiplicative] {X : AlgebraicGeometry.Scheme} {𝒰 𝒱 𝒲 : AlgebraicGeometry.Scheme.Cover P X} (f : 𝒰 ⟶ 𝒱) (g : 𝒱 ⟶ 𝒲) (j : 𝒰.J) : (CategoryTheory.CategoryStruct.comp f g).app j = CategoryTheory.CategoryStruct.comp (f.app j) (g.app (f.idx j))