mathlib documentation

algebraic_geometry.open_immersion

Open immersions of structured spaces #

We say that a morphism of presheafed spaces f : X ⟶ Y is an open immersions if the underlying map of spaces is an open embedding f : X ⟶ U ⊆ Y, and the sheaf map Y(V) ⟶ f _* X(V) is an iso for each V ⊆ U.

Abbreviations are also provided for SheafedSpace, LocallyRingedSpace and Scheme.

Main definitions #

Main results #

@[class]

An open immersion of PresheafedSpaces is an open embedding f : X ⟶ U ⊆ Y of the underlying spaces, such that the sheaf map Y(V) ⟶ f _* X(V) is an iso for each V ⊆ U.

Instances of this typeclass
@[reducible]

A morphism of SheafedSpaces is an open immersion if it is an open immersion as a morphism of PresheafedSpaces

@[reducible]

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

@[reducible]

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

For an open immersion f : X ⟶ Y and an open set U ⊆ X, we have the map X(U) ⟶ Y(U).

Equations
Instances for algebraic_geometry.PresheafedSpace.is_open_immersion.inv_app
@[protected, instance]
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

Suppose X Y : SheafedSpace C, where C is a concrete category, whose forgetful functor reflects isomorphisms, preserves limits and filtered colimits. Then a morphism X ⟶ Y that is a topological open embedding is an open immersion iff every stalk map is an iso.

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
@[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
structure algebraic_geometry.Scheme.open_cover (X : algebraic_geometry.Scheme) :
Type (max (u+1) (v+1))

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