Birationality and Rationality of schemes.

This file defines partial isomorphisms between schemes and uses them to formalize birationality and rationality.

Main definitions

• Scheme.PartialIso X Y: an isomorphism between a dense open subscheme of X and a dense open subscheme of Y.
• Scheme.Birational X Y: X and Y are birational, i.e. there exists a PartialIso X Y.
• Scheme.BirationalOver sX sY: X and Y are birational over S via structure maps sX : X ⟶ S and sY : Y ⟶ S.
• Scheme.IsRationalOver sX: X is rational over S via structure map sX : X ⟶ S, i.e. birational over S to some affine space 𝔸(n; S).

structure AlgebraicGeometry.Scheme.PartialIso (X Y : Scheme) : Type u

A partial isomorphism from X to Y is an isomorphism between dense open subschemes of X and Y.

• source : X.Opens

  The source open subscheme of a partial isomorphism.

• dense_source : Dense ↑self.source
• target : Y.Opens

  The target open subscheme of a partial isomorphism.

• dense_target : Dense ↑self.target
• iso : ↑self.source ≅ ↑self.target

  The underlying isomorphism of a partial isomorphism.

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.PartialIso.IsOver {X Y S : Scheme} (sX : X ⟶ S) (sY : Y ⟶ S) (f : X.PartialIso Y) : Prop

A partial iso is an S-map if the underlying morphism is.

Equations

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

theorem AlgebraicGeometry.Scheme.PartialIso.ext_iff {X Y : Scheme} (f g : X.PartialIso Y) : f = g ↔ ∃ (e : f.source = g.source) (e' : g.target = f.target), f.iso = X.isoOfEq e ≪≫ g.iso ≪≫ Y.isoOfEq e'

theorem AlgebraicGeometry.Scheme.PartialIso.ext {X Y : Scheme} (f g : X.PartialIso Y) (e : f.source = g.source) (e' : g.target = f.target) (H : f.iso = X.isoOfEq e ≪≫ g.iso ≪≫ Y.isoOfEq e') : f = g

def AlgebraicGeometry.Scheme.PartialIso.refl (X : Scheme) : X.PartialIso X

The identity partial isomorphism on X, defined on all of X.

Equations

• AlgebraicGeometry.Scheme.PartialIso.refl X = { source := ⊤, dense_source := ⋯, target := ⊤, dense_target := ⋯, iso := CategoryTheory.Iso.refl ↑⊤ }

@[simp]

theorem AlgebraicGeometry.Scheme.PartialIso.refl_source (X : Scheme) : (refl X).source = ⊤

@[simp]

theorem AlgebraicGeometry.Scheme.PartialIso.refl_target (X : Scheme) : (refl X).target = ⊤

@[simp]

theorem AlgebraicGeometry.Scheme.PartialIso.refl_iso (X : Scheme) : (refl X).iso = CategoryTheory.Iso.refl ↑⊤

def AlgebraicGeometry.Scheme.PartialIso.symm {X Y : Scheme} (f : X.PartialIso Y) : Y.PartialIso X

The inverse of a partial isomorphism.

Equations

• f.symm = { source := f.target, dense_source := ⋯, target := f.source, dense_target := ⋯, iso := f.iso.symm }

@[simp]

theorem AlgebraicGeometry.Scheme.PartialIso.symm_target {X Y : Scheme} (f : X.PartialIso Y) : f.symm.target = f.source

@[simp]

theorem AlgebraicGeometry.Scheme.PartialIso.symm_source {X Y : Scheme} (f : X.PartialIso Y) : f.symm.source = f.target

@[simp]

theorem AlgebraicGeometry.Scheme.PartialIso.symm_iso {X Y : Scheme} (f : X.PartialIso Y) : f.symm.iso = f.iso.symm

theorem AlgebraicGeometry.Scheme.PartialIso.IsOver.symm {X Y S : Scheme} {sX : X ⟶ S} {sY : Y ⟶ S} {f : X.PartialIso Y} (hf : IsOver sX sY f) : IsOver sY sX f.symm

noncomputable def AlgebraicGeometry.Scheme.PartialIso.trans' {X Y Z : Scheme} (f : X.PartialIso Y) (g : Y.PartialIso Z) (e : f.target = g.source) : X.PartialIso Z

Compose two partial isomorphisms along a proof that the target of f equals the source of g. See trans for the version that does not require this.

Equations

• f.trans' g e = { source := f.source, dense_source := ⋯, target := g.target, dense_target := ⋯, iso := f.iso ≪≫ Y.isoOfEq e ≪≫ g.iso }

@[simp]

theorem AlgebraicGeometry.Scheme.PartialIso.trans'_target {X Y Z : Scheme} (f : X.PartialIso Y) (g : Y.PartialIso Z) (e : f.target = g.source) : (f.trans' g e).target = g.target

@[simp]

theorem AlgebraicGeometry.Scheme.PartialIso.trans'_iso {X Y Z : Scheme} (f : X.PartialIso Y) (g : Y.PartialIso Z) (e : f.target = g.source) : (f.trans' g e).iso = f.iso ≪≫ Y.isoOfEq e ≪≫ g.iso

@[simp]

theorem AlgebraicGeometry.Scheme.PartialIso.trans'_source {X Y Z : Scheme} (f : X.PartialIso Y) (g : Y.PartialIso Z) (e : f.target = g.source) : (f.trans' g e).source = f.source

theorem AlgebraicGeometry.Scheme.PartialIso.IsOver.trans' {X Y Z S : Scheme} {sX : X ⟶ S} {sY : Y ⟶ S} {sZ : Z ⟶ S} {f : X.PartialIso Y} {g : Y.PartialIso Z} {e : f.target = g.source} (hf : IsOver sX sY f) (hg : IsOver sY sZ g) : IsOver sX sZ (f.trans' g e)

noncomputable def AlgebraicGeometry.Scheme.PartialIso.restrictSource {X Y : Scheme} (f : X.PartialIso Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.source) : X.PartialIso Y

Restrict the source of a partial isomorphism to a smaller dense open.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.PartialIso.restrictSource_iso {X Y : Scheme} (f : X.PartialIso Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.source) : (f.restrictSource U hU hU').iso = (Opens.isoOfLE hU').symm ≪≫ Hom.isoImage f.iso.hom ((TopologicalSpace.Opens.map f.source.ι.base).obj U) ≪≫ Hom.isoImage f.target.ι ((Hom.opensFunctor f.iso.hom).obj ((TopologicalSpace.Opens.map f.source.ι.base).obj U))

@[simp]

theorem AlgebraicGeometry.Scheme.PartialIso.restrictSource_target {X Y : Scheme} (f : X.PartialIso Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.source) : (f.restrictSource U hU hU').target = (Hom.opensFunctor f.target.ι).obj ((Hom.opensFunctor f.iso.hom).obj ((TopologicalSpace.Opens.map f.source.ι.base).obj U))

@[simp]

theorem AlgebraicGeometry.Scheme.PartialIso.restrictSource_source {X Y : Scheme} (f : X.PartialIso Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.source) : (f.restrictSource U hU hU').source = U

theorem AlgebraicGeometry.Scheme.PartialIso.IsOver.restrictSource {X Y S : Scheme} {sX : X ⟶ S} {sY : Y ⟶ S} {f : X.PartialIso Y} (hf : IsOver sX sY f) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.source) : IsOver sX sY (f.restrictSource U hU hU')

noncomputable def AlgebraicGeometry.Scheme.PartialIso.restrictTarget {X Y : Scheme} (f : X.PartialIso Y) (U : Y.Opens) (hU : Dense ↑U) (hU' : U ≤ f.target) : X.PartialIso Y

Restrict the target of a partial isomorphism to a smaller dense open.

Equations

• f.restrictTarget U hU hU' = (f.symm.restrictSource U hU hU').symm

@[simp]

theorem AlgebraicGeometry.Scheme.PartialIso.restrictTarget_source {X Y : Scheme} (f : X.PartialIso Y) (U : Y.Opens) (hU : Dense ↑U) (hU' : U ≤ f.target) : (f.restrictTarget U hU hU').source = (Hom.opensFunctor f.source.ι).obj ((TopologicalSpace.Opens.map f.iso.hom.base).obj ((TopologicalSpace.Opens.map f.target.ι.base).obj U))

@[simp]

theorem AlgebraicGeometry.Scheme.PartialIso.restrictTarget_iso {X Y : Scheme} (f : X.PartialIso Y) (U : Y.Opens) (hU : Dense ↑U) (hU' : U ≤ f.target) : (f.restrictTarget U hU hU').iso = (Hom.isoImage f.source.ι ((Hom.opensFunctor f.iso.inv).obj ((TopologicalSpace.Opens.map f.target.ι.base).obj U))).symm ≪≫ (Hom.isoImage f.iso.inv ((TopologicalSpace.Opens.map f.target.ι.base).obj U)).symm ≪≫ Opens.isoOfLE hU'

@[simp]

theorem AlgebraicGeometry.Scheme.PartialIso.restrictTarget_target {X Y : Scheme} (f : X.PartialIso Y) (U : Y.Opens) (hU : Dense ↑U) (hU' : U ≤ f.target) : (f.restrictTarget U hU hU').target = U

theorem AlgebraicGeometry.Scheme.PartialIso.IsOver.restrictTarget {X Y S : Scheme} {sX : X ⟶ S} {sY : Y ⟶ S} {f : X.PartialIso Y} (hf : IsOver sX sY f) (U : Y.Opens) (hU : Dense ↑U) (hU' : U ≤ f.target) : IsOver sX sY (f.restrictTarget U hU hU')

noncomputable def AlgebraicGeometry.Scheme.PartialIso.trans {X Y Z : Scheme} (f : X.PartialIso Y) (g : Y.PartialIso Z) : X.PartialIso Z

Compose two partial isomorphisms, restricting to the intersection of the intermediate opens.

Equations

• f.trans g = (f.restrictTarget (f.target ⊓ g.source) ⋯ ⋯).trans' (g.restrictSource (f.target ⊓ g.source) ⋯ ⋯) ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.PartialIso.trans_iso {X Y Z : Scheme} (f : X.PartialIso Y) (g : Y.PartialIso Z) : (f.trans g).iso = ((Hom.isoImage f.source.ι ((Hom.opensFunctor f.iso.inv).obj ((TopologicalSpace.Opens.map f.target.ι.base).obj (f.target ⊓ g.source)))).symm ≪≫ (Hom.isoImage f.iso.inv ((TopologicalSpace.Opens.map f.target.ι.base).obj (f.target ⊓ g.source))).symm ≪≫ Opens.isoOfLE ⋯) ≪≫ (Opens.isoOfLE ⋯).symm ≪≫ Hom.isoImage g.iso.hom ((TopologicalSpace.Opens.map g.source.ι.base).obj (f.target ⊓ g.source)) ≪≫ Hom.isoImage g.target.ι ((Hom.opensFunctor g.iso.hom).obj ((TopologicalSpace.Opens.map g.source.ι.base).obj (f.target ⊓ g.source)))

@[simp]

theorem AlgebraicGeometry.Scheme.PartialIso.trans_target {X Y Z : Scheme} (f : X.PartialIso Y) (g : Y.PartialIso Z) : (f.trans g).target = (Hom.opensFunctor g.target.ι).obj ((Hom.opensFunctor g.iso.hom).obj ((TopologicalSpace.Opens.map g.source.ι.base).obj (f.target ⊓ g.source)))

@[simp]

theorem AlgebraicGeometry.Scheme.PartialIso.trans_source {X Y Z : Scheme} (f : X.PartialIso Y) (g : Y.PartialIso Z) : (f.trans g).source = (Hom.opensFunctor f.source.ι).obj ((TopologicalSpace.Opens.map f.iso.hom.base).obj ((TopologicalSpace.Opens.map f.target.ι.base).obj (f.target ⊓ g.source)))

theorem AlgebraicGeometry.Scheme.PartialIso.IsOver.trans {X Y Z S : Scheme} {sX : X ⟶ S} {sY : Y ⟶ S} {sZ : Z ⟶ S} {f : X.PartialIso Y} {g : Y.PartialIso Z} (hf : IsOver sX sY f) (hg : IsOver sY sZ g) : IsOver sX sZ (f.trans g)

def AlgebraicGeometry.Scheme.PartialIso.toPartialMap {X Y : Scheme} (f : X.PartialIso Y) : X.PartialMap Y

The underlying partial map of a partial isomorphism.

Equations

• f.toPartialMap = { domain := f.source, dense_domain := ⋯, hom := CategoryTheory.CategoryStruct.comp f.iso.hom f.target.ι }

@[simp]

theorem AlgebraicGeometry.Scheme.PartialIso.toPartialMap_domain {X Y : Scheme} (f : X.PartialIso Y) : f.toPartialMap.domain = f.source

@[simp]

theorem AlgebraicGeometry.Scheme.PartialIso.toPartialMap_hom {X Y : Scheme} (f : X.PartialIso Y) : f.toPartialMap.hom = CategoryTheory.CategoryStruct.comp f.iso.hom f.target.ι

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.PartialIso.toRationalMap {X Y : Scheme} (f : X.PartialIso Y) : X.RationalMap Y

The underlying rational map of a partial isomorphism.

Equations

• f.toRationalMap = f.toPartialMap.toRationalMap

noncomputable def AlgebraicGeometry.Scheme.PartialIso.ofIso {X Y : Scheme} (f : X ≅ Y) : X.PartialIso Y

A scheme isomorphism viewed as a partial isomorphism defined on all of X and Y.

Equations

• AlgebraicGeometry.Scheme.PartialIso.ofIso f = { source := ⊤, dense_source := ⋯, target := ⊤, dense_target := ⋯, iso := X.topIso ≪≫ f ≪≫ Y.topIso.symm }

@[simp]

theorem AlgebraicGeometry.Scheme.PartialIso.ofIso_iso {X Y : Scheme} (f : X ≅ Y) : (ofIso f).iso = X.topIso ≪≫ f ≪≫ Y.topIso.symm

@[simp]

theorem AlgebraicGeometry.Scheme.PartialIso.ofIso_target {X Y : Scheme} (f : X ≅ Y) : (ofIso f).target = ⊤

@[simp]

theorem AlgebraicGeometry.Scheme.PartialIso.ofIso_source {X Y : Scheme} (f : X ≅ Y) : (ofIso f).source = ⊤

def AlgebraicGeometry.Scheme.Birational (X Y : Scheme) : Prop

X and Y are birational if there exists a partial isomorphism between them.

Equations

• X.Birational Y = Nonempty (X.PartialIso Y)

noncomputable def AlgebraicGeometry.Scheme.Birational.partialIso {X Y : Scheme} (h : X.Birational Y) : X.PartialIso Y

Choose a partial isomorphism witnessing that X and Y are birational.

Equations

• h.partialIso = Classical.choice h

theorem AlgebraicGeometry.Scheme.Birational.refl (X : Scheme) : X.Birational X

theorem AlgebraicGeometry.Scheme.Birational.symm {X Y : Scheme} (h : X.Birational Y) : Y.Birational X

theorem AlgebraicGeometry.Scheme.Birational.trans {X Y Z : Scheme} (h₁ : X.Birational Y) (h₂ : Y.Birational Z) : X.Birational Z

def AlgebraicGeometry.Scheme.BirationalOver {S X Y : Scheme} (sX : X ⟶ S) (sY : Y ⟶ S) : Prop

X and Y are birational over S if there exists a partial isomorphism between them that is compatible with the structure maps to S.

Equations

• AlgebraicGeometry.Scheme.BirationalOver sX sY = ∃ (f : X.PartialIso Y), AlgebraicGeometry.Scheme.PartialIso.IsOver sX sY f

noncomputable def AlgebraicGeometry.Scheme.BirationalOver.partialIso {S X Y : Scheme} (sX : X ⟶ S) (sY : Y ⟶ S) (h : BirationalOver sX sY) : X.PartialIso Y

Choose a partial isomorphism witnessing that X and Y are birational over S.

Equations

• AlgebraicGeometry.Scheme.BirationalOver.partialIso sX sY h = Exists.choose h

theorem AlgebraicGeometry.Scheme.BirationalOver.partialIso_isOver {S X Y : Scheme} (sX : X ⟶ S) (sY : Y ⟶ S) (h : BirationalOver sX sY) : PartialIso.IsOver sX sY (partialIso sX sY h)

theorem AlgebraicGeometry.Scheme.BirationalOver.refl {S X : Scheme} (sX : X ⟶ S) : BirationalOver sX sX

theorem AlgebraicGeometry.Scheme.BirationalOver.symm {S X Y : Scheme} {sX : X ⟶ S} {sY : Y ⟶ S} (h : BirationalOver sX sY) : BirationalOver sY sX

theorem AlgebraicGeometry.Scheme.BirationalOver.trans {S X Y Z : Scheme} {sX : X ⟶ S} {sY : Y ⟶ S} {sZ : Z ⟶ S} (h₁ : BirationalOver sX sY) (h₂ : BirationalOver sY sZ) : BirationalOver sX sZ

class AlgebraicGeometry.Scheme.IsRationalOver {S X : Scheme} (sX : X ⟶ S) : Prop

X is rational over S (or S-rational) if it is birational over S to some affine space 𝔸(n; S). Note that we do not require n to be finite here.

• exists_birationalOver_affineSpace : ∃ (n : Type u), BirationalOver sX (AffineSpace n S ↘ S)

theorem AlgebraicGeometry.Scheme.isRationalOver_iff {S X : Scheme} (sX : X ⟶ S) : IsRationalOver sX ↔ ∃ (n : Type u), BirationalOver sX (AffineSpace n S ↘ S)

instance AlgebraicGeometry.Scheme.instIsRationalOverOverAffineSpaceInferInstanceOverClass (S : Scheme) (n : Type u) : IsRationalOver (AffineSpace n S ↘ S)

theorem AlgebraicGeometry.Scheme.BirationalOver.isRationalOver {S X Y : Scheme} (sX : X ⟶ S) (sY : Y ⟶ S) [IsRationalOver sY] (h : BirationalOver sX sY) : IsRationalOver sX

If a scheme X is S-birational to an S-rational scheme Y, then X is S-rational.

def AlgebraicGeometry.Scheme.Opens.partialIsoOfDense {X : Scheme} (U : X.Opens) (hU : Dense ↑U) : (↑U).PartialIso X

A dense open set U : Opens X induces a partial isomorphism between U and X.

Equations

• U.partialIsoOfDense hU = { source := ⊤, dense_source := ⋯, target := U, dense_target := hU, iso := (↑U).topIso }

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.partialIsoOfDense_iso {X : Scheme} (U : X.Opens) (hU : Dense ↑U) : (U.partialIsoOfDense hU).iso = (↑U).topIso

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.partialIsoOfDense_source {X : Scheme} (U : X.Opens) (hU : Dense ↑U) : (U.partialIsoOfDense hU).source = ⊤

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.partialIsoOfDense_target {X : Scheme} (U : X.Opens) (hU : Dense ↑U) : (U.partialIsoOfDense hU).target = U

theorem AlgebraicGeometry.Scheme.Opens.birational_of_dense {X : Scheme} (U : X.Opens) (hU : Dense ↑U) : (↑U).Birational X

A dense open set U : Opens X is birational to X.

theorem AlgebraicGeometry.Scheme.Opens.birationalOver_of_dense {X S : Scheme} (U : X.Opens) (sX : X ⟶ S) (hU : Dense ↑U) : BirationalOver (CategoryTheory.CategoryStruct.comp U.ι sX) sX

A dense open set U : Opens X of a scheme X over S is S-birational to X.

theorem AlgebraicGeometry.Scheme.Opens.isRationalOver_of_dense {X S : Scheme} (U : X.Opens) (sX : X ⟶ S) (hU : Dense ↑U) [IsRationalOver sX] : IsRationalOver (CategoryTheory.CategoryStruct.comp U.ι sX)

A dense open set U : Opens X of a S-rational scheme X is S-rational.

noncomputable def AlgebraicGeometry.Scheme.Hom.partialIso {X U : Scheme} (f : U ⟶ X) [IsOpenImmersion f] [IsDominant f] : U.PartialIso X

A dominant open immersion f : U ⟶ X induces a partial isomorphism between U and X.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.partialIso_target {X U : Scheme} (f : U ⟶ X) [IsOpenImmersion f] [IsDominant f] : (partialIso f).target = opensRange f

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.partialIso_source {X U : Scheme} (f : U ⟶ X) [IsOpenImmersion f] [IsDominant f] : (partialIso f).source = ⊤

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.partialIso_iso {X U : Scheme} (f : U ⟶ X) [IsOpenImmersion f] [IsDominant f] : (partialIso f).iso = U.topIso ≪≫ isoOpensRange f

theorem AlgebraicGeometry.Scheme.Hom.birational {X U : Scheme} (f : U ⟶ X) [IsOpenImmersion f] [IsDominant f] : U.Birational X

theorem AlgebraicGeometry.Scheme.Hom.birationalOver {X U S : Scheme} (f : U ⟶ X) [IsOpenImmersion f] [IsDominant f] (sX : X ⟶ S) (sU : U ⟶ S) (hf : CategoryTheory.CategoryStruct.comp f sX = sU) : BirationalOver sU sX