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 Scheme) (X : 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) : Scheme

  the components of a cover

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

  the components map to X

• f (x : ↥X) : self.J

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

• covers (x : ↥X) : x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (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 Scheme} {X : Scheme} (𝒰 : Cover P X) : ⋃ (i : 𝒰.J), Set.range ⇑(CategoryTheory.ConcreteCategory.hom (𝒰.map i).base) = Set.univ

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

instance AlgebraicGeometry.Scheme.Cover.nonempty_of_nonempty {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} [Nonempty ↥X] (𝒰 : Cover P X) : Nonempty 𝒰.J

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

def AlgebraicGeometry.Scheme.Cover.bind {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover P X) [P.IsStableUnderComposition] (f : (x : 𝒰.J) → Cover P (𝒰.obj x)) : 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.

@[simp]

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

@[simp]

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

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.bind_map {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover P X) [P.IsStableUnderComposition] (f : (x : 𝒰.J) → 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)

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

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

@[simp]

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

@[simp]

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

@[simp]

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

def AlgebraicGeometry.Scheme.Cover.copy {P : CategoryTheory.MorphismProperty Scheme} [P.RespectsIso] {X : Scheme} (𝒰 : Cover P X) (J : Type u_1) (obj : J → 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))) : 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.

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.copy_obj {P : CategoryTheory.MorphismProperty Scheme} [P.RespectsIso] {X : Scheme} (𝒰 : Cover P X) (J : Type u_1) (obj : J → 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_J {P : CategoryTheory.MorphismProperty Scheme} [P.RespectsIso] {X : Scheme} (𝒰 : Cover P X) (J : Type u_1) (obj : J → 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_map {P : CategoryTheory.MorphismProperty Scheme} [P.RespectsIso] {X : Scheme} (𝒰 : Cover P X) (J : Type u_1) (obj : J → 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 Scheme} [P.RespectsIso] [P.ContainsIdentities] [P.IsStableUnderComposition] {X Y : Scheme} (𝒰 : Cover P X) (f : X ⟶ Y) [CategoryTheory.IsIso f] : Cover P Y

The pushforward of a cover along an isomorphism.

@[simp]

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

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pushforwardIso_map {P : CategoryTheory.MorphismProperty Scheme} [P.RespectsIso] [P.ContainsIdentities] [P.IsStableUnderComposition] {X Y : 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 Scheme} [P.RespectsIso] [P.ContainsIdentities] [P.IsStableUnderComposition] {X Y : Scheme} (𝒰 : Cover P X) (f : X ⟶ Y) [CategoryTheory.IsIso f] : (𝒰.pushforwardIso f).J = 𝒰.J

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

Adding map satisfying P into a cover gives another cover.

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.add_J {P : CategoryTheory.MorphismProperty Scheme} {X Y : 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_f {P : CategoryTheory.MorphismProperty Scheme} {X Y : Scheme} (𝒰 : Cover P X) (f : Y ⟶ X) (hf : P f := by infer_instance) (x : ↥X) : (𝒰.add f hf).f x = some (𝒰.f x)

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.add_obj {P : CategoryTheory.MorphismProperty Scheme} {X Y : 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_map {P : CategoryTheory.MorphismProperty Scheme} {X Y : 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

class AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving (P : CategoryTheory.MorphismProperty 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 : Scheme} {f : X ⟶ S} {g : Y ⟶ S} [CategoryTheory.Limits.HasPullback f g] (hg : P g) (x : ↥X) (y : ↥Y) (h : (CategoryTheory.ConcreteCategory.hom f.base) x = (CategoryTheory.ConcreteCategory.hom g.base) y) : ∃ (a : ↥(CategoryTheory.Limits.pullback f g)), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g).base) a = x

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

instance AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion : IsJointlySurjectivePreserving IsOpenImmersion

def AlgebraicGeometry.Scheme.Cover.pullbackCover {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover P X) (f : W ⟶ X) [∀ (x : 𝒰.J), CategoryTheory.Limits.HasPullback f (𝒰.map x)] : 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.

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackCover_obj {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : 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)

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackCover_map {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : 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_J {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : 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_f {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover P X) (f : W ⟶ X) [∀ (x : 𝒰.J), CategoryTheory.Limits.HasPullback f (𝒰.map x)] (x : ↥W) : (𝒰.pullbackCover f).f x = 𝒰.f ((CategoryTheory.ConcreteCategory.hom f.base) x)

def AlgebraicGeometry.Scheme.Cover.pullbackHom {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : 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.

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackHom_map {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : 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 Scheme} [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover P X) (f : W ⟶ X) [∀ (x : 𝒰.J), CategoryTheory.Limits.HasPullback f (𝒰.map x)] (i : 𝒰.1) {Z : 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 Scheme} [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover P X) (f : W ⟶ X) [∀ (x : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map x) f] : 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).

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackCover'_obj {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : 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'_f {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover P X) (f : W ⟶ X) [∀ (x : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map x) f] (x : ↥W) : (𝒰.pullbackCover' f).f x = 𝒰.f ((CategoryTheory.ConcreteCategory.hom f.base) x)

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackCover'_map {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : 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 Scheme} [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover P X) (f : W ⟶ X) [∀ (x : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map x) f] : (𝒰.pullbackCover' f).J = 𝒰.J

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

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

structure AlgebraicGeometry.Scheme.AffineCover (P : CategoryTheory.MorphismProperty Scheme) (X : 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) : Spec (self.obj j) ⟶ X

  the components map to X

• f (x : ↥X) : self.J

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

• covers (x : ↥X) : x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (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 Scheme} {X : Scheme} (𝒰 : AffineCover P X) : Cover P X

The cover associated to an affine cover.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def AlgebraicGeometry.Scheme.Cover.reindex {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover P X) {ι : Type u_1} (e : ι ≃ 𝒰.J) : Cover P X

Replace the index type of a cover by an equivalent one.

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.reindex_f {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover P X) {ι : Type u_1} (e : ι ≃ 𝒰.J) (a✝ : ↥X) : (𝒰.reindex e).f a✝ = (⇑e.symm ∘ 𝒰.f) a✝

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.reindex_J {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover P X) {ι : Type u_1} (e : ι ≃ 𝒰.J) : (𝒰.reindex e).J = ι

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.reindex_obj {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover P X) {ι : Type u_1} (e : ι ≃ 𝒰.J) (a✝ : ι) : (𝒰.reindex e).obj a✝ = (𝒰.obj ∘ ⇑e) a✝

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.reindex_map {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover P X) {ι : Type u_1} (e : ι ≃ 𝒰.J) (i : ι) : (𝒰.reindex e).map i = 𝒰.map (e i)

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

Any v-cover 𝒰 induces a u-cover indexed by the points of X.

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.ulift_map {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover P X) (x : ↥X) : 𝒰.ulift.map x = 𝒰.map (𝒰.f x)

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.ulift_J {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover P X) : 𝒰.ulift.J = ↥X

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.ulift_obj {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover P X) (x : ↥X) : 𝒰.ulift.obj x = 𝒰.obj (𝒰.f x)

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.ulift_f {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover P X) (a : ↥X) : 𝒰.ulift.f a = a

structure AlgebraicGeometry.Scheme.Cover.Hom {P : CategoryTheory.MorphismProperty Scheme} {X : 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

theorem AlgebraicGeometry.Scheme.Cover.Hom.ext_iff {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} {𝒰 𝒱 : Cover P X} {x y : 𝒰.Hom 𝒱} : x = y ↔ x.idx = y.idx ∧ x.app ≍ y.app

theorem AlgebraicGeometry.Scheme.Cover.Hom.ext {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} {𝒰 𝒱 : Cover P X} {x y : 𝒰.Hom 𝒱} (idx : x.idx = y.idx) (app : x.app ≍ y.app) : x = y

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.Hom.w_assoc {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} {𝒰 𝒱 : Cover P X} (self : 𝒰.Hom 𝒱) (j : 𝒰.J) {Z : 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 Scheme} [P.ContainsIdentities] {X : Scheme} (𝒰 : Cover P X) : 𝒰.Hom 𝒰

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

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

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

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

@[simp]

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

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.id_app {P : CategoryTheory.MorphismProperty Scheme} [P.IsMultiplicative] {X : 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 Scheme} [P.IsMultiplicative] {X : 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 Scheme} [P.IsMultiplicative] {X : 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))