Documentation

Mathlib.AlgebraicGeometry.OpenImmersion

Open immersions of schemes #

@[reducible, inline]

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

Equations

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

The image of an open immersion as an open set.

Equations
@[reducible, inline]

The functor opens X ⥤ opens Y associated with an open immersion f : X ⟶ Y.

Equations

f ''ᵁ U is notation for the image (as an open set) of U under an open immersion f.

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

Pretty printer defined by notation3 command.

Equations
  • One or more equations did not get rendered due to their size.
theorem AlgebraicGeometry.Scheme.Hom.image_iSup {X Y : Scheme} (f : X.Hom Y) [H : IsOpenImmersion f] {ι : Sort u_1} (s : ιX.Opens) :
f.opensFunctor.obj (⨆ (i : ι), s i) = ⨆ (i : ι), f.opensFunctor.obj (s i)
theorem AlgebraicGeometry.Scheme.Hom.image_iSup₂ {X Y : Scheme} (f : X.Hom Y) [H : IsOpenImmersion f] {ι : Sort u_1} {κ : ιSort u_2} (s : (i : ι) → κ iX.Opens) :
f.opensFunctor.obj (⨆ (i : ι), ⨆ (j : κ i), s i j) = ⨆ (i : ι), ⨆ (j : κ i), f.opensFunctor.obj (s i j)

The isomorphism Γ(Y, f(U)) ≅ Γ(X, U) induced by an open immersion f : X ⟶ Y.

Equations
theorem AlgebraicGeometry.Scheme.Hom.appIso_hom' {X Y : Scheme} (f : X.Hom Y) [H : IsOpenImmersion f] (U : X.Opens) :
(f.appIso U).hom = f.appLE (f.opensFunctor.obj U) U

A variant of app_invApp that gives an eqToHom instead of homOfLE.

The open sets of an open subscheme corresponds to the open sets containing in the image.

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

If X ⟶ Y is an open immersion, and Y is a scheme, then so is X.

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

The restriction of a Scheme along an open embedding.

Equations
  • X.restrict h = { toPresheafedSpace := X.restrict h, IsSheaf := , isLocalRing := , local_affine := }

The canonical map from the restriction to the subspace.

Equations

An open immersion induces an isomorphism from the domain onto the image

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

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
  • One or more equations did not get rendered due to their size.

Two open immersions with equal range are isomorphic.

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

If f is an open immersion X ⟶ Y, the global sections of X are naturally isomorphic to the sections of Y over the image of f.

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

Given an open immersion f : U ⟶ X, the isomorphism between global sections of U and the sections of X at the image of f.

Equations