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.

class AlgebraicGeometry.Scheme.JointlySurjective (K : CategoryTheory.Precoverage Scheme) : Prop

A coverage K on Scheme is called jointly surjective if every covering family in K is jointly surjective.

• exists_eq {X : Scheme} (S : CategoryTheory.Presieve X) (hS : S ∈ K.coverings X) (x : ↥X) : ∃ (Y : Scheme) (g : Y ⟶ X), S g ∧ x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base)

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.Cover (K : CategoryTheory.Precoverage Scheme) (S : Scheme) : Type (max (u + 1) (v + 1))

A cover of X in the coverage K is a 0-hypercover for K.

Equations

• AlgebraicGeometry.Scheme.Cover K = K.ZeroHypercover

theorem AlgebraicGeometry.Scheme.Cover.exists_eq {K : CategoryTheory.Precoverage Scheme} {X : Scheme} [JointlySurjective K] (𝒰 : Cover K X) (x : ↥X) : ∃ (i : 𝒰.I₀) (y : ↥(𝒰.X i)), (CategoryTheory.ConcreteCategory.hom (𝒰.f i).base) y = x

def AlgebraicGeometry.Scheme.Cover.idx {K : CategoryTheory.Precoverage Scheme} {X : Scheme} [JointlySurjective K] (𝒰 : Cover K X) (x : ↥X) : 𝒰.I₀

A choice of an index i such that x is in the range of 𝒰.f i.

Equations

• 𝒰.idx x = ⋯.choose

theorem AlgebraicGeometry.Scheme.Cover.covers {K : CategoryTheory.Precoverage Scheme} {X : Scheme} [JointlySurjective K] (𝒰 : Cover K X) (x : ↥X) : x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (𝒰.f (𝒰.idx x)).base)

theorem AlgebraicGeometry.Scheme.Cover.iUnion_range {K : CategoryTheory.Precoverage Scheme} [JointlySurjective K] {X : Scheme} (𝒰 : Cover K X) : ⋃ (i : 𝒰.I₀), Set.range ⇑(CategoryTheory.ConcreteCategory.hom (𝒰.f i).base) = Set.univ

instance AlgebraicGeometry.Scheme.Cover.nonempty_of_nonempty {K : CategoryTheory.Precoverage Scheme} {X : Scheme} [JointlySurjective K] [Nonempty ↥X] (𝒰 : Cover K X) : Nonempty 𝒰.I₀

theorem AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff {X : Scheme} {P : CategoryTheory.MorphismProperty Scheme} (E : CategoryTheory.PreZeroHypercover X) : E.presieve₀ ∈ (precoverage P).coverings X ↔ (∀ (x : ↥X), ∃ (i : E.I₀), x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (E.f i).base)) ∧ ∀ (i : E.I₀), P (E.f i)

theorem AlgebraicGeometry.Scheme.Cover.map_prop {X : Scheme} {P : CategoryTheory.MorphismProperty Scheme} (𝒰 : Cover (precoverage P) X) (i : 𝒰.I₀) : P (𝒰.f i)

def AlgebraicGeometry.Scheme.Cover.mkOfCovers {X : Scheme} {P : CategoryTheory.MorphismProperty 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 (precoverage 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.

Equations

• AlgebraicGeometry.Scheme.Cover.mkOfCovers J obj map covers map_prop = { I₀ := J, X := obj, f := map, mem₀ := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.mkOfCovers_X {X : Scheme} {P : CategoryTheory.MorphismProperty 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).X a✝ = obj a✝

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.mkOfCovers_f {X : Scheme} {P : CategoryTheory.MorphismProperty 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).f j = map j

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.mkOfCovers_I₀ {X : Scheme} {P : CategoryTheory.MorphismProperty 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).I₀ = J

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

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

Equations

• AlgebraicGeometry.Scheme.coverOfIsIso f = AlgebraicGeometry.Scheme.Cover.mkOfCovers PUnit.{?u.50 + 1} (fun (x : PUnit.{?u.50 + 1}) => X) (fun (x : PUnit.{?u.50 + 1}) => f) ⋯ ⋯

@[simp]

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

@[simp]

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

@[simp]

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

instance AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage {P : CategoryTheory.MorphismProperty Scheme} : JointlySurjective (precoverage P)

def AlgebraicGeometry.Scheme.Cover.changeProp {K : CategoryTheory.Precoverage Scheme} {X : Scheme} {Q : CategoryTheory.MorphismProperty Scheme} [JointlySurjective K] (𝒰 : Cover K X) (h : ∀ (j : 𝒰.I₀), Q (𝒰.f j)) : Cover (precoverage Q) X

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

Equations

• 𝒰.changeProp h = { toPreZeroHypercover := 𝒰.toPreZeroHypercover, mem₀ := ⋯ }

def AlgebraicGeometry.Scheme.Cover.copy {P : CategoryTheory.MorphismProperty Scheme} [P.RespectsIso] {X : Scheme} (𝒰 : Cover (precoverage P) X) (J : Type u_1) (obj : J → Scheme) (map : (i : J) → obj i ⟶ X) (e₁ : J ≃ 𝒰.I₀) (e₂ : (i : J) → obj i ≅ 𝒰.X (e₁ i)) (h : ∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂ i).hom (𝒰.f (e₁ i))) : Cover (precoverage 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 = { I₀ := J, X := obj, f := map, mem₀ := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

def AlgebraicGeometry.Scheme.Cover.pushforwardIso {P : CategoryTheory.MorphismProperty Scheme} [P.RespectsIso] [P.ContainsIdentities] [P.IsStableUnderComposition] {X Y : Scheme} (𝒰 : Cover (precoverage P) X) (f : X ⟶ Y) [CategoryTheory.IsIso f] : Cover (precoverage 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_X {P : CategoryTheory.MorphismProperty Scheme} [P.RespectsIso] [P.ContainsIdentities] [P.IsStableUnderComposition] {X Y : Scheme} (𝒰 : Cover (precoverage P) X) (f : X ⟶ Y) [CategoryTheory.IsIso f] (x✝ : 𝒰.I₀) : (𝒰.pushforwardIso f).X x✝ = 𝒰.X x✝

@[simp]

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

@[simp]

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

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

Adding map satisfying P into a cover gives another cover.

Equations

• 𝒰.add f hf = { toPreZeroHypercover := 𝒰.add f, mem₀ := ⋯ }

@[simp]

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

@[deprecated CategoryTheory.Precoverage.ZeroHypercover.pullback₁ (since := "2025-10-02")]

def AlgebraicGeometry.Scheme.Cover.pullbackCover {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S T : C} [J.IsStableUnderBaseChange] (f : S ⟶ T) (E : J.ZeroHypercover T) [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)] : J.ZeroHypercover S

Alias of CategoryTheory.Precoverage.ZeroHypercover.pullback₁.

---

Pullback of a 0-hypercover along a morphism. The components are pullback f (E.f i).

Equations

• @AlgebraicGeometry.Scheme.Cover.pullbackCover = @CategoryTheory.Precoverage.ZeroHypercover.pullback₁

def AlgebraicGeometry.Scheme.Cover.pullbackHom {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover (precoverage P) X) (f : W ⟶ X) (i : 𝒰.toPreZeroHypercover.1) [∀ (x : 𝒰.I₀), CategoryTheory.Limits.HasPullback f (𝒰.f x)] : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i

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

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackHom_map {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover (precoverage P) X) (f : W ⟶ X) [∀ (x : 𝒰.I₀), CategoryTheory.Limits.HasPullback f (𝒰.f x)] (i : 𝒰.toPreZeroHypercover.1) : CategoryTheory.CategoryStruct.comp (𝒰.pullbackHom f i) (𝒰.f i) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i) f

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.pullbackHom_map_assoc {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme} (𝒰 : Cover (precoverage P) X) (f : W ⟶ X) [∀ (x : 𝒰.I₀), CategoryTheory.Limits.HasPullback f (𝒰.f x)] (i : 𝒰.toPreZeroHypercover.1) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (𝒰.pullbackHom f i) (CategoryTheory.CategoryStruct.comp (𝒰.f i) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i) (CategoryTheory.CategoryStruct.comp f h)

@[deprecated CategoryTheory.Precoverage.ZeroHypercover.pullback₂ (since := "2025-10-02")]

def AlgebraicGeometry.Scheme.Cover.pullbackCover' {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S T : C} [J.IsStableUnderBaseChange] (f : S ⟶ T) (E : J.ZeroHypercover T) [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f] : J.ZeroHypercover S

Alias of CategoryTheory.Precoverage.ZeroHypercover.pullback₂.

---

Pullback of a 0-hypercover along a morphism. The components are pullback (E.f i) f.

Equations

• @AlgebraicGeometry.Scheme.Cover.pullbackCover' = @CategoryTheory.Precoverage.ZeroHypercover.pullback₂

structure AlgebraicGeometry.Scheme.AffineCover (P : CategoryTheory.MorphismProperty Scheme) (S : 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.

• I₀ : Type v

  index set of an affine cover of a scheme S

• X (j : self.I₀) : CommRingCat

  the ring associated to a component of an affine cover

• f (j : self.I₀) : Spec (self.X j) ⟶ S

  the components map to S

• idx (x : ↥S) : self.I₀

  given a point of x : S, idx x is the index of the component which contains x

• covers (x : ↥S) : x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (self.f (self.idx x)).base)

  the components cover S

• map_prop (j : self.I₀) : P (self.f j)

  the component maps satisfy P

@[deprecated AlgebraicGeometry.Scheme.AffineCover.I₀ (since := "2025-09-19")]

def AlgebraicGeometry.Scheme.AffineCover.J {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} (self : AffineCover P S) : Type v

Alias of AlgebraicGeometry.Scheme.AffineCover.I₀.

---

index set of an affine cover of a scheme S

Equations

• @AlgebraicGeometry.Scheme.AffineCover.J = @AlgebraicGeometry.Scheme.AffineCover.I₀

@[deprecated AlgebraicGeometry.Scheme.AffineCover.X (since := "2025-09-19")]

def AlgebraicGeometry.Scheme.AffineCover.obj {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} (self : AffineCover P S) (j : self.I₀) : CommRingCat

Alias of AlgebraicGeometry.Scheme.AffineCover.X.

---

the ring associated to a component of an affine cover

Equations

• @AlgebraicGeometry.Scheme.AffineCover.obj = @AlgebraicGeometry.Scheme.AffineCover.X

@[deprecated AlgebraicGeometry.Scheme.AffineCover.f (since := "2025-09-19")]

def AlgebraicGeometry.Scheme.AffineCover.map {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} (self : AffineCover P S) (j : self.I₀) : Spec (self.X j) ⟶ S

Alias of AlgebraicGeometry.Scheme.AffineCover.f.

---

the components map to S

Equations

• @AlgebraicGeometry.Scheme.AffineCover.map = @AlgebraicGeometry.Scheme.AffineCover.f

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

The cover associated to an affine cover.

Equations

• 𝒰.cover = { I₀ := 𝒰.I₀, X := fun (j : 𝒰.I₀) => AlgebraicGeometry.Spec (𝒰.X j), f := 𝒰.f, mem₀ := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.AffineCover.cover_X {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : AffineCover P X) (j : 𝒰.I₀) : 𝒰.cover.X j = Spec (𝒰.X j)

@[simp]

theorem AlgebraicGeometry.Scheme.AffineCover.cover_f {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : AffineCover P X) (j : 𝒰.I₀) : 𝒰.cover.f j = 𝒰.f j

@[simp]

theorem AlgebraicGeometry.Scheme.AffineCover.cover_I₀ {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : AffineCover P X) : 𝒰.cover.I₀ = 𝒰.I₀

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

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

Equations

• 𝒰.ulift = { I₀ := ↥X, X := fun (x : ↥X) => 𝒰.X ⋯.choose, f := fun (x : ↥X) => 𝒰.f ⋯.choose, mem₀ := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.ulift_I₀ {X : Scheme} {P : CategoryTheory.MorphismProperty Scheme} (𝒰 : Cover (precoverage P) X) : 𝒰.ulift.I₀ = ↥X

@[simp]

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

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.ulift_X {X : Scheme} {P : CategoryTheory.MorphismProperty Scheme} (𝒰 : Cover (precoverage P) X) (x : ↥X) : 𝒰.ulift.X x = 𝒰.X ⋯.choose

structure AlgebraicGeometry.Scheme.Cover.Hom {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 𝒱 : Cover (precoverage 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 : 𝒰.I₀ → 𝒱.I₀

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

• app (j : 𝒰.I₀) : 𝒰.X j ⟶ 𝒱.X (self.idx j)

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

• app_prop (j : 𝒰.I₀) : P (self.app j)
• w (j : 𝒰.I₀) : CategoryTheory.CategoryStruct.comp (self.app j) (𝒱.f (self.idx j)) = 𝒰.f j

theorem AlgebraicGeometry.Scheme.Cover.Hom.ext_iff {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} {𝒰 𝒱 : Cover (precoverage 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 (precoverage 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 (precoverage P) X} (self : 𝒰.Hom 𝒱) (j : 𝒰.I₀) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.app j) (CategoryTheory.CategoryStruct.comp (𝒱.f (self.idx j)) h) = CategoryTheory.CategoryStruct.comp (𝒰.f j) h

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

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

Equations

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

def AlgebraicGeometry.Scheme.Cover.Hom.comp {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderComposition] {X : Scheme} {𝒰 𝒱 𝒲 : Cover (precoverage 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 : 𝒰.I₀) => g.idx (f.idx j), app := fun (x : 𝒰.I₀) => CategoryTheory.CategoryStruct.comp (f.app x) (g.app (f.idx x)), app_prop := ⋯, w := ⋯ }

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.comp_idx_apply {P : CategoryTheory.MorphismProperty Scheme} [P.IsMultiplicative] {X : Scheme} {𝒰 𝒱 𝒲 : Cover (precoverage P) X} (f : 𝒰 ⟶ 𝒱) (g : 𝒱 ⟶ 𝒲) (j : 𝒰.I₀) : (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 (precoverage P) X} (f : 𝒰 ⟶ 𝒱) (g : 𝒱 ⟶ 𝒲) (j : 𝒰.I₀) : (CategoryTheory.CategoryStruct.comp f g).app j = CategoryTheory.CategoryStruct.comp (f.app j) (g.app (f.idx j))