mathlib3 documentation

algebraic_geometry.open_immersion.Scheme

Open immersions of schemes #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[reducible]

A morphism of Schemes is an open immersion if it is an open immersion as a morphism of LocallyRingedSpaces

@[protected]

To show that a locally ringed space is a scheme, it suffices to show that it has a jointly surjective family of open immersions from affine schemes.

Equations

An open cover of X consists of a family of open immersions into X, and for each x : X an open immersion (indexed by f x) that covers x.

This is merely a coverage in the Zariski pretopology, 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.

Instances for algebraic_geometry.Scheme.open_cover
@[simp]
theorem algebraic_geometry.Scheme.open_cover.bind_obj {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : Π (x : 𝒰.J), (𝒰.obj x).open_cover) (x : Σ (i : 𝒰.J), (f i).J) :
(𝒰.bind f).obj x = (f x.fst).obj x.snd
@[simp]
theorem algebraic_geometry.Scheme.open_cover.bind_J {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : Π (x : 𝒰.J), (𝒰.obj x).open_cover) :
(𝒰.bind f).J = Σ (i : 𝒰.J), (f i).J
noncomputable def algebraic_geometry.Scheme.open_cover.bind {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : Π (x : 𝒰.J), (𝒰.obj x).open_cover) :

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

Equations
@[simp]
theorem algebraic_geometry.Scheme.open_cover.bind_map {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (f : Π (x : 𝒰.J), (𝒰.obj x).open_cover) (x : Σ (i : 𝒰.J), (f i).J) :
(𝒰.bind f).map x = (f x.fst).map x.snd 𝒰.map x.fst

An isomorphism X ⟶ Y is an open cover of Y.

Equations
@[simp]
theorem algebraic_geometry.Scheme.open_cover.copy_map {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (J : Type u_3) (obj : J algebraic_geometry.Scheme) (map : Π (i : J), obj i X) (e₁ : J 𝒰.J) (e₂ : Π (i : J), obj i 𝒰.obj (e₁ i)) (e₂_1 : (i : J), map i = (e₂ i).hom 𝒰.map (e₁ i)) (i : J) :
(𝒰.copy J obj map e₁ e₂ e₂_1).map i = map i
def algebraic_geometry.Scheme.open_cover.copy {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (J : Type u_3) (obj : J algebraic_geometry.Scheme) (map : Π (i : J), obj i X) (e₁ : J 𝒰.J) (e₂ : Π (i : J), obj i 𝒰.obj (e₁ i)) (e₂_1 : (i : J), map i = (e₂ i).hom 𝒰.map (e₁ i)) :

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

Equations
@[simp]
theorem algebraic_geometry.Scheme.open_cover.copy_J {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (J : Type u_3) (obj : J algebraic_geometry.Scheme) (map : Π (i : J), obj i X) (e₁ : J 𝒰.J) (e₂ : Π (i : J), obj i 𝒰.obj (e₁ i)) (e₂_1 : (i : J), map i = (e₂ i).hom 𝒰.map (e₁ i)) :
(𝒰.copy J obj map e₁ e₂ e₂_1).J = J
@[simp]
theorem algebraic_geometry.Scheme.open_cover.copy_obj {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (J : Type u_3) (obj : J algebraic_geometry.Scheme) (map : Π (i : J), obj i X) (e₁ : J 𝒰.J) (e₂ : Π (i : J), obj i 𝒰.obj (e₁ i)) (e₂_1 : (i : J), map i = (e₂ i).hom 𝒰.map (e₁ i)) (ᾰ : J) :
(𝒰.copy J obj map e₁ e₂ e₂_1).obj = obj ᾰ
@[simp]

Adding an open immersion into an open cover gives another open cover.

Equations
@[simp]
@[simp]

We may bind the basic open sets of an open affine cover to form a affine cover that is also a basis.

Equations

The coordinate ring of a component in the affine_basis_cover.

Equations

Every open cover of a quasi-compact scheme can be refined into a finite subcover.

Equations

The universal property of open immersions: For an open immersion f : X ⟶ Z, given any morphism of schemes g : Y ⟶ Z whose topological image is contained in the image of f, we can lift this morphism to a unique Y ⟶ X that commutes with these maps.

Equations
@[reducible]

The restriction of an isomorphism onto an open set.

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

Equations

Given open covers { Uᵢ } and { Uⱼ }, we may form the open cover { Uᵢ ∩ Uⱼ }.

Equations

If U is a family of open sets that covers X, then X.restrict U forms an X.open_cover.

Equations

The restrictions onto two equal open sets are isomorphic. This currently has bad defeqs when unfolded, but it should not matter for now. Replace this definition if better defeqs are needed.

Equations

Restricting a morphism twice is isomorpic to one restriction.

Equations