Rational maps between schemes

Main definitions

• AlgebraicGeometry.Scheme.PartialMap: A partial map from X to Y (X.PartialMap Y) is a morphism into Y defined on a dense open subscheme of X.
• AlgebraicGeometry.Scheme.PartialMap.equiv: Two partial maps are equivalent if they are equal on a dense open subscheme.
• AlgebraicGeometry.Scheme.RationalMap: A rational map from X to Y (X ⤏ Y) is an equivalence class of partial maps.
• AlgebraicGeometry.Scheme.RationalMap.equivFunctionField: Given S-schemes X and Y such that Y is locally of finite type and X is integral, S-morphisms Spec K(X) ⟶ Y correspond bijectively to S-rational maps from X to Y.

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

A partial map from X to Y (X.PartialMap Y) is a morphism into Y defined on a dense open subscheme of X.

• domain : X.Opens

  The domain of definition of a partial map.

• dense_domain : Dense ↑self.domain
• hom : ↑self.domain ⟶ Y

  The underlying morphism of a partial map.

theorem AlgebraicGeometry.Scheme.PartialMap.ext_iff {X Y : AlgebraicGeometry.Scheme} (f g : X.PartialMap Y) : f = g ↔ ∃ (e : f.domain = g.domain), f.hom = CategoryTheory.CategoryStruct.comp (X.isoOfEq e).hom g.hom

theorem AlgebraicGeometry.Scheme.PartialMap.ext {X Y : AlgebraicGeometry.Scheme} (f g : X.PartialMap Y) (e : f.domain = g.domain) (H : f.hom = CategoryTheory.CategoryStruct.comp (X.isoOfEq e).hom g.hom) : f = g

noncomputable def AlgebraicGeometry.Scheme.PartialMap.restrict {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.domain) : X.PartialMap Y

The restriction of a partial map to a smaller domain.

Equations

• f.restrict U hU hU' = { domain := U, dense_domain := hU, hom := CategoryTheory.CategoryStruct.comp (X.homOfLE hU') f.hom }

@[simp]

theorem AlgebraicGeometry.Scheme.PartialMap.restrict_hom {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.domain) : (f.restrict U hU hU').hom = CategoryTheory.CategoryStruct.comp (X.homOfLE hU') f.hom

theorem AlgebraicGeometry.Scheme.PartialMap.restrict_domain {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.domain) : (f.restrict U hU hU').domain = U

@[simp]

theorem AlgebraicGeometry.Scheme.PartialMap.restrict_id {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) : f.restrict f.domain ⋯ ⋯ = f

theorem AlgebraicGeometry.Scheme.PartialMap.restrict_id_hom {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) : (f.restrict f.domain ⋯ ⋯).hom = f.hom

@[simp]

theorem AlgebraicGeometry.Scheme.PartialMap.restrict_restrict {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.domain) (V : X.Opens) (hV : Dense ↑V) (hV' : V ≤ U) : (f.restrict U hU hU').restrict V hV hV' = f.restrict V hV ⋯

theorem AlgebraicGeometry.Scheme.PartialMap.restrict_restrict_hom {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.domain) (V : X.Opens) (hV : Dense ↑V) (hV' : V ≤ U) : ((f.restrict U hU hU').restrict V hV hV').hom = (f.restrict V hV ⋯).hom

def AlgebraicGeometry.Scheme.PartialMap.compHom {X Y Z : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (g : Y ⟶ Z) : X.PartialMap Z

The composition of a partial map and a morphism on the right.

Equations

• f.compHom g = { domain := f.domain, dense_domain := ⋯, hom := CategoryTheory.CategoryStruct.comp f.hom g }

@[simp]

theorem AlgebraicGeometry.Scheme.PartialMap.compHom_domain {X Y Z : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (g : Y ⟶ Z) : (f.compHom g).domain = f.domain

@[simp]

theorem AlgebraicGeometry.Scheme.PartialMap.compHom_hom {X Y Z : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (g : Y ⟶ Z) : (f.compHom g).hom = CategoryTheory.CategoryStruct.comp f.hom g

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

A scheme morphism as a partial map.

Equations

• f.toPartialMap = { domain := ⊤, dense_domain := ⋯, hom := CategoryTheory.CategoryStruct.comp X.topIso.hom f }

@[simp]

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

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.toPartialMap_hom {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) : f.toPartialMap.hom = CategoryTheory.CategoryStruct.comp X.topIso.hom f

noncomputable def AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) {x : ↑↑X.toPresheafedSpace} (hx : x ∈ f.domain) : AlgebraicGeometry.Spec (X.presheaf.stalk x) ⟶ Y

If x is in the domain of a partial map f, then f restricts to a map from Spec 𝒪_x.

Equations

• f.fromSpecStalkOfMem hx = CategoryTheory.CategoryStruct.comp (f.domain.fromSpecStalkOfMem x hx) f.hom

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Scheme.PartialMap.fromFunctionField {X Y : AlgebraicGeometry.Scheme} [IrreducibleSpace ↑↑X.toPresheafedSpace] (f : X.PartialMap Y) : AlgebraicGeometry.Spec X.functionField ⟶ Y

A partial map restricts to a map from Spec K(X).

Equations

• f.fromFunctionField = f.fromSpecStalkOfMem ⋯

theorem AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem_restrict {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) {U : X.Opens} (hU : Dense ↑U) (hU' : U ≤ f.domain) {x : ↑↑X.toPresheafedSpace} (hx : x ∈ U) : (f.restrict U hU hU').fromSpecStalkOfMem hx = f.fromSpecStalkOfMem ⋯

theorem AlgebraicGeometry.Scheme.PartialMap.fromFunctionField_restrict {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) [IrreducibleSpace ↑↑X.toPresheafedSpace] {U : X.Opens} (hU : Dense ↑U) (hU' : U ≤ f.domain) : (f.restrict U hU hU').fromFunctionField = f.fromFunctionField

noncomputable def AlgebraicGeometry.Scheme.PartialMap.ofFromSpecStalk {X Y S : AlgebraicGeometry.Scheme} (sX : X ⟶ S) (sY : Y ⟶ S) [IrreducibleSpace ↑↑X.toPresheafedSpace] [AlgebraicGeometry.LocallyOfFiniteType sY] {x : ↑↑X.toPresheafedSpace} [X.IsGermInjectiveAt x] (φ : AlgebraicGeometry.Spec (X.presheaf.stalk x) ⟶ Y) (h : CategoryTheory.CategoryStruct.comp φ sY = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) sX) : X.PartialMap Y

Given S-schemes X and Y such that Y is locally of finite type and X is irreducible germ-injective at x (e.g. when X is integral), any S-morphism Spec 𝒪ₓ ⟶ Y spreads out to a partial map from X to Y.

Equations

• AlgebraicGeometry.Scheme.PartialMap.ofFromSpecStalk sX sY φ h = { domain := ⋯.choose, dense_domain := ⋯, hom := ⋯.choose }

theorem AlgebraicGeometry.Scheme.PartialMap.ofFromSpecStalk_comp {X Y S : AlgebraicGeometry.Scheme} (sX : X ⟶ S) (sY : Y ⟶ S) [IrreducibleSpace ↑↑X.toPresheafedSpace] [AlgebraicGeometry.LocallyOfFiniteType sY] {x : ↑↑X.toPresheafedSpace} [X.IsGermInjectiveAt x] (φ : AlgebraicGeometry.Spec (X.presheaf.stalk x) ⟶ Y) (h : CategoryTheory.CategoryStruct.comp φ sY = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) sX) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.PartialMap.ofFromSpecStalk sX sY φ h).hom sY = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.PartialMap.ofFromSpecStalk sX sY φ h).domain.ι sX

theorem AlgebraicGeometry.Scheme.PartialMap.mem_domain_ofFromSpecStalk {X Y S : AlgebraicGeometry.Scheme} (sX : X ⟶ S) (sY : Y ⟶ S) [IrreducibleSpace ↑↑X.toPresheafedSpace] [AlgebraicGeometry.LocallyOfFiniteType sY] {x : ↑↑X.toPresheafedSpace} [X.IsGermInjectiveAt x] (φ : AlgebraicGeometry.Spec (X.presheaf.stalk x) ⟶ Y) (h : CategoryTheory.CategoryStruct.comp φ sY = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) sX) : x ∈ (AlgebraicGeometry.Scheme.PartialMap.ofFromSpecStalk sX sY φ h).domain

theorem AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem_ofFromSpecStalk {X Y S : AlgebraicGeometry.Scheme} (sX : X ⟶ S) (sY : Y ⟶ S) [IrreducibleSpace ↑↑X.toPresheafedSpace] [AlgebraicGeometry.LocallyOfFiniteType sY] {x : ↑↑X.toPresheafedSpace} [X.IsGermInjectiveAt x] (φ : AlgebraicGeometry.Spec (X.presheaf.stalk x) ⟶ Y) (h : CategoryTheory.CategoryStruct.comp φ sY = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) sX) : (AlgebraicGeometry.Scheme.PartialMap.ofFromSpecStalk sX sY φ h).fromSpecStalkOfMem ⋯ = φ

@[simp]

theorem AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem_compHom {X Y Z : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (g : Y ⟶ Z) (x : ↑↑X.toPresheafedSpace) (hx : x ∈ (f.compHom g).domain) : (f.compHom g).fromSpecStalkOfMem hx = CategoryTheory.CategoryStruct.comp (f.fromSpecStalkOfMem hx) g

@[simp]

theorem AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem_toPartialMap {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↑↑X.toPresheafedSpace) : (AlgebraicGeometry.Scheme.Hom.toPartialMap f).fromSpecStalkOfMem trivial = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) f

noncomputable def AlgebraicGeometry.Scheme.PartialMap.equiv {X Y : AlgebraicGeometry.Scheme} (f g : X.PartialMap Y) : Prop

Two partial maps are equivalent if they are equal on a dense open subscheme.

Equations

• f.equiv g = ∃ (W : X.Opens) (hW : Dense ↑W) (hWl : W ≤ f.domain) (hWr : W ≤ g.domain), (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom

theorem AlgebraicGeometry.Scheme.PartialMap.equivalence_rel {X Y : AlgebraicGeometry.Scheme} : Equivalence AlgebraicGeometry.Scheme.PartialMap.equiv

instance AlgebraicGeometry.Scheme.PartialMap.instSetoid {X Y : AlgebraicGeometry.Scheme} : Setoid (X.PartialMap Y)

Equations

• AlgebraicGeometry.Scheme.PartialMap.instSetoid = { r := AlgebraicGeometry.Scheme.PartialMap.equiv, iseqv := ⋯ }

theorem AlgebraicGeometry.Scheme.PartialMap.restrict_equiv {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.domain) : (f.restrict U hU hU').equiv f

theorem AlgebraicGeometry.Scheme.PartialMap.equiv_of_fromSpecStalkOfMem_eq {X Y : AlgebraicGeometry.Scheme} [IrreducibleSpace ↑↑X.toPresheafedSpace] {x : ↑↑X.toPresheafedSpace} [X.IsGermInjectiveAt x] (f g : X.PartialMap Y) (hxf : x ∈ f.domain) (hxg : x ∈ g.domain) (H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg) : f.equiv g

def AlgebraicGeometry.Scheme.RationalMap (X Y : AlgebraicGeometry.Scheme) : Type u

A rational map from X to Y (X ⤏ Y) is an equivalence class of partial maps, where two partial maps are equivalent if they are equal on a dense open subscheme.

Equations

• X.RationalMap Y = Quotient inferInstance

def AlgebraicGeometry.«term_⤏_» : Lean.TrailingParserDescr

The notation for rational maps.

Equations

• AlgebraicGeometry.«term_⤏_» = Lean.ParserDescr.trailingNode `AlgebraicGeometry.«term_⤏_» 10 11 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⤏ ") (Lean.ParserDescr.cat `term 11))

def AlgebraicGeometry.Scheme.PartialMap.toRationalMap {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) : X.RationalMap Y

A partial map as a rational map.

Equations

• f.toRationalMap = ⟦f⟧

@[reducible, inline]

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

A scheme morphism as a rational map.

Equations

• f.toRationalMap = f.toPartialMap.toRationalMap

theorem AlgebraicGeometry.Scheme.PartialMap.toRationalMap_surjective {X Y : AlgebraicGeometry.Scheme} : Function.Surjective AlgebraicGeometry.Scheme.PartialMap.toRationalMap

theorem AlgebraicGeometry.Scheme.RationalMap.exists_rep {X Y : AlgebraicGeometry.Scheme} (f : X.RationalMap Y) : ∃ (g : X.PartialMap Y), g.toRationalMap = f

theorem AlgebraicGeometry.Scheme.PartialMap.toRationalMap_eq_iff {X Y : AlgebraicGeometry.Scheme} {f g : X.PartialMap Y} : f.toRationalMap = g.toRationalMap ↔ f.equiv g

@[simp]

theorem AlgebraicGeometry.Scheme.PartialMap.restrict_toRationalMap {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.domain) : (f.restrict U hU hU').toRationalMap = f.toRationalMap

def AlgebraicGeometry.Scheme.RationalMap.compHom {X Y Z : AlgebraicGeometry.Scheme} (f : X.RationalMap Y) (g : Y ⟶ Z) : X.RationalMap Z

The composition of a rational map and a morphism on the right.

Equations

• f.compHom g = Quotient.map (fun (x : X.PartialMap Y) => x.compHom g) ⋯ f

@[simp]

theorem AlgebraicGeometry.Scheme.RationalMap.compHom_toRationalMap {X Y Z : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (g : Y ⟶ Z) : (f.compHom g).toRationalMap = f.toRationalMap.compHom g

noncomputable def AlgebraicGeometry.Scheme.RationalMap.fromFunctionField {X Y : AlgebraicGeometry.Scheme} [IrreducibleSpace ↑↑X.toPresheafedSpace] (f : X.RationalMap Y) : AlgebraicGeometry.Spec X.functionField ⟶ Y

A rational map restricts to a map from Spec K(X).

Equations

• f.fromFunctionField = Quotient.lift AlgebraicGeometry.Scheme.PartialMap.fromFunctionField ⋯ f

@[simp]

theorem AlgebraicGeometry.Scheme.RationalMap.fromFunctionField_toRationalMap {X Y : AlgebraicGeometry.Scheme} [IrreducibleSpace ↑↑X.toPresheafedSpace] (f : X.PartialMap Y) : f.toRationalMap.fromFunctionField = f.fromFunctionField

noncomputable def AlgebraicGeometry.Scheme.RationalMap.ofFunctionField {X Y S : AlgebraicGeometry.Scheme} (sX : X ⟶ S) (sY : Y ⟶ S) [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.LocallyOfFiniteType sY] (f : AlgebraicGeometry.Spec X.functionField ⟶ Y) (h : CategoryTheory.CategoryStruct.comp f sY = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk (genericPoint ↑↑X.toPresheafedSpace)) sX) : X.RationalMap Y

Given S-schemes X and Y such that Y is locally of finite type and X is integral, any S-morphism Spec K(X) ⟶ Y spreads out to a rational map from X to Y.

Equations

• AlgebraicGeometry.Scheme.RationalMap.ofFunctionField sX sY f h = (AlgebraicGeometry.Scheme.PartialMap.ofFromSpecStalk sX sY f h).toRationalMap

theorem AlgebraicGeometry.Scheme.RationalMap.fromFunctionField_ofFunctionField {X Y S : AlgebraicGeometry.Scheme} (sX : X ⟶ S) (sY : Y ⟶ S) [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.LocallyOfFiniteType sY] (f : AlgebraicGeometry.Spec X.functionField ⟶ Y) (h : CategoryTheory.CategoryStruct.comp f sY = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk (genericPoint ↑↑X.toPresheafedSpace)) sX) : (AlgebraicGeometry.Scheme.RationalMap.ofFunctionField sX sY f h).fromFunctionField = f

theorem AlgebraicGeometry.Scheme.RationalMap.eq_of_fromFunctionField_eq {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (f g : X.RationalMap Y) (H : f.fromFunctionField = g.fromFunctionField) : f = g

noncomputable def AlgebraicGeometry.Scheme.RationalMap.equivFunctionField {X Y S : AlgebraicGeometry.Scheme} (sX : X ⟶ S) (sY : Y ⟶ S) [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.LocallyOfFiniteType sY] : { f : AlgebraicGeometry.Spec X.functionField ⟶ Y // CategoryTheory.CategoryStruct.comp f sY = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk (genericPoint ↑↑X.toPresheafedSpace)) sX } ≃ { f : X.RationalMap Y // f.compHom sY = AlgebraicGeometry.Scheme.Hom.toRationalMap sX }

Given S-schemes X and Y such that Y is locally of finite type and X is integral, S-morphisms Spec K(X) ⟶ Y correspond bijectively to S-rational maps from X to Y.

Equations

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