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.equivFunctionFieldOver: 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.
• AlgebraicGeometry.Scheme.RationalMap.toPartialMap: If X is integral and Y is separated, then any f : X ⤏ Y can be realized as a partial map on f.domain, the domain of definition of f.

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.

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.PartialMap.IsOver {X Y : AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [X.Over S] [Y.Over S] (f : X.PartialMap Y) : Prop

A partial map is a S-map if the underlying morphism is.

Equations

• AlgebraicGeometry.Scheme.PartialMap.IsOver S f = AlgebraicGeometry.Scheme.Hom.IsOver f.hom S

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

@[simp]

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

instance AlgebraicGeometry.Scheme.PartialMap.instIsOverRestrict {X Y S : AlgebraicGeometry.Scheme} [X.Over S] [Y.Over S] (f : X.PartialMap Y) [AlgebraicGeometry.Scheme.PartialMap.IsOver S f] (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.domain) : AlgebraicGeometry.Scheme.PartialMap.IsOver S (f.restrict U hU hU')

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_hom {X Y Z : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (g : Y ⟶ Z) : (f.compHom g).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

instance AlgebraicGeometry.Scheme.PartialMap.instIsOverCompHomOfIsOver {X Y Z S : AlgebraicGeometry.Scheme} [X.Over S] [Y.Over S] [Z.Over S] (f : X.PartialMap Y) (g : Y ⟶ Z) [AlgebraicGeometry.Scheme.PartialMap.IsOver S f] [AlgebraicGeometry.Scheme.Hom.IsOver g S] : AlgebraicGeometry.Scheme.PartialMap.IsOver S (f.compHom 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_hom {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) : f.toPartialMap.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 = ⊤

instance AlgebraicGeometry.Scheme.PartialMap.instIsOverToPartialMapOfIsOver {X Y S : AlgebraicGeometry.Scheme} [X.Over S] [Y.Over S] (f : X ⟶ Y) [AlgebraicGeometry.Scheme.Hom.IsOver f S] : AlgebraicGeometry.Scheme.PartialMap.IsOver S (AlgebraicGeometry.Scheme.Hom.toPartialMap f)

theorem AlgebraicGeometry.Scheme.PartialMap.isOver_iff {X Y S : AlgebraicGeometry.Scheme} [X.Over S] [Y.Over S] {f : X.PartialMap Y} : AlgebraicGeometry.Scheme.PartialMap.IsOver S f ↔ (f.compHom (Y ↘ S)).hom = CategoryTheory.CategoryStruct.comp f.domain.ι (X ↘ S)

theorem AlgebraicGeometry.Scheme.PartialMap.isOver_iff_eq_restrict {X Y S : AlgebraicGeometry.Scheme} [X.Over S] [Y.Over S] {f : X.PartialMap Y} : AlgebraicGeometry.Scheme.PartialMap.IsOver S f ↔ f.compHom (Y ↘ S) = (AlgebraicGeometry.Scheme.Hom.toPartialMap (X ↘ S)).restrict f.domain ⋯ ⋯

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

instance AlgebraicGeometry.Scheme.PartialMap.instIsReducedToScheme {X : AlgebraicGeometry.Scheme} (U : X.Opens) [AlgebraicGeometry.IsReduced X] : AlgebraicGeometry.IsReduced ↑U

theorem AlgebraicGeometry.Scheme.PartialMap.Opens.isDominant_ι {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : Dense ↑U) : AlgebraicGeometry.IsDominant U.ι

theorem AlgebraicGeometry.Scheme.PartialMap.Opens.isDominant_homOfLE {X : AlgebraicGeometry.Scheme} {U V : X.Opens} (hU : Dense ↑U) (hU' : U ≤ V) : AlgebraicGeometry.IsDominant (X.homOfLE hU')

theorem AlgebraicGeometry.Scheme.PartialMap.equiv_iff_of_isSeparated_of_le {X Y S : AlgebraicGeometry.Scheme} [X.Over S] [Y.Over S] [AlgebraicGeometry.IsReduced X] [AlgebraicGeometry.IsSeparated (Y ↘ S)] {f g : X.PartialMap Y} [AlgebraicGeometry.Scheme.PartialMap.IsOver S f] [AlgebraicGeometry.Scheme.PartialMap.IsOver S g] {W : X.Opens} (hW : Dense ↑W) (hWl : W ≤ f.domain) (hWr : W ≤ g.domain) : f.equiv g ↔ (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom

Two partial maps from reduced schemes to separated schemes are equivalent if and only if they are equal on any open dense subset.

theorem AlgebraicGeometry.Scheme.PartialMap.equiv_iff_of_isSeparated {X Y S : AlgebraicGeometry.Scheme} [X.Over S] [Y.Over S] [AlgebraicGeometry.IsReduced X] [AlgebraicGeometry.IsSeparated (Y ↘ S)] {f g : X.PartialMap Y} [AlgebraicGeometry.Scheme.PartialMap.IsOver S f] [AlgebraicGeometry.Scheme.PartialMap.IsOver S g] : f.equiv g ↔ (f.restrict (f.domain ⊓ g.domain) ⋯ ⋯).hom = (g.restrict (f.domain ⊓ g.domain) ⋯ ⋯).hom

Two partial maps from reduced schemes to separated schemes are equivalent if and only if they are equal on the intersection of the domains.

theorem AlgebraicGeometry.Scheme.PartialMap.equiv_iff_of_domain_eq_of_isSeparated {X Y S : AlgebraicGeometry.Scheme} [X.Over S] [Y.Over S] [AlgebraicGeometry.IsReduced X] [AlgebraicGeometry.IsSeparated (Y ↘ S)] {f g : X.PartialMap Y} (hfg : f.domain = g.domain) [AlgebraicGeometry.Scheme.PartialMap.IsOver S f] [AlgebraicGeometry.Scheme.PartialMap.IsOver S g] : f.equiv g ↔ f = g

Two partial maps from reduced schemes to separated schemes with the same domain are equivalent if and only if they are equal.

theorem AlgebraicGeometry.Scheme.PartialMap.equiv_toPartialMap_iff_of_isSeparated {X Y S : AlgebraicGeometry.Scheme} [X.Over S] [Y.Over S] [AlgebraicGeometry.IsReduced X] [AlgebraicGeometry.IsSeparated (Y ↘ S)] {f : X.PartialMap Y} {g : X ⟶ Y} [AlgebraicGeometry.Scheme.PartialMap.IsOver S f] [AlgebraicGeometry.Scheme.Hom.IsOver g S] : f.equiv (AlgebraicGeometry.Scheme.Hom.toPartialMap g) ↔ f.hom = CategoryTheory.CategoryStruct.comp f.domain.ι g

A partial map from a reduced scheme to a separated scheme is equivalent to a morphism if and only if it is equal to the restriction of the morphism.

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

class AlgebraicGeometry.Scheme.RationalMap.IsOver {X Y : AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [X.Over S] [Y.Over S] (f : X.RationalMap Y) : Prop

A rational map is a S-map if some partial map in the equivalence class is a S-map.

• exists_partialMap_over : ∃ (g : X.PartialMap Y), AlgebraicGeometry.Scheme.PartialMap.IsOver S g ∧ g.toRationalMap = f

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

instance AlgebraicGeometry.Scheme.instIsOverToRationalMapOfIsOver {X Y S : AlgebraicGeometry.Scheme} [X.Over S] [Y.Over S] (f : X.PartialMap Y) [AlgebraicGeometry.Scheme.PartialMap.IsOver S f] : AlgebraicGeometry.Scheme.RationalMap.IsOver S f.toRationalMap

theorem AlgebraicGeometry.Scheme.RationalMap.exists_partialMap_over {X Y : AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [X.Over S] [Y.Over S] (f : X.RationalMap Y) [AlgebraicGeometry.Scheme.RationalMap.IsOver S f] : ∃ (g : X.PartialMap Y), AlgebraicGeometry.Scheme.PartialMap.IsOver S g ∧ g.toRationalMap = f

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

instance AlgebraicGeometry.Scheme.instIsOverCompHomOfIsOver {X Y Z S : AlgebraicGeometry.Scheme} [X.Over S] [Y.Over S] [Z.Over S] (f : X.RationalMap Y) (g : Y ⟶ Z) [AlgebraicGeometry.Scheme.RationalMap.IsOver S f] [AlgebraicGeometry.Scheme.Hom.IsOver g S] : AlgebraicGeometry.Scheme.RationalMap.IsOver S (f.compHom g)

theorem AlgebraicGeometry.Scheme.PartialMap.exists_restrict_isOver {X Y : AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [X.Over S] [Y.Over S] (f : X.PartialMap Y) [AlgebraicGeometry.Scheme.RationalMap.IsOver S f.toRationalMap] : ∃ (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.domain), AlgebraicGeometry.Scheme.PartialMap.IsOver S (f.restrict U hU hU')

theorem AlgebraicGeometry.Scheme.RationalMap.isOver_iff {X Y S : AlgebraicGeometry.Scheme} [X.Over S] [Y.Over S] {f : X.RationalMap Y} : AlgebraicGeometry.Scheme.RationalMap.IsOver S f ↔ f.compHom (Y ↘ S) = AlgebraicGeometry.Scheme.Hom.toRationalMap (X ↘ S)

theorem AlgebraicGeometry.Scheme.PartialMap.isOver_toRationalMap_iff_of_isSeparated {X Y S : AlgebraicGeometry.Scheme} [X.Over S] [Y.Over S] [AlgebraicGeometry.IsReduced X] [S.IsSeparated] {f : X.PartialMap Y} : AlgebraicGeometry.Scheme.RationalMap.IsOver S f.toRationalMap ↔ AlgebraicGeometry.Scheme.PartialMap.IsOver S f

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.

noncomputable def AlgebraicGeometry.Scheme.RationalMap.equivFunctionFieldOver {X Y S : AlgebraicGeometry.Scheme} [X.Over S] [Y.Over S] [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.LocallyOfFiniteType (Y ↘ S)] : { f : AlgebraicGeometry.Spec X.functionField ⟶ Y // AlgebraicGeometry.Scheme.Hom.IsOver f S } ≃ { f : X.RationalMap Y // AlgebraicGeometry.Scheme.RationalMap.IsOver S f }

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.

def AlgebraicGeometry.Scheme.RationalMap.domain {X Y : AlgebraicGeometry.Scheme} (f : X.RationalMap Y) : X.Opens

The domain of definition of a rational map.

Equations

• f.domain = sSup {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x}

theorem AlgebraicGeometry.Scheme.PartialMap.le_domain_toRationalMap {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) : f.domain ≤ f.toRationalMap.domain

theorem AlgebraicGeometry.Scheme.RationalMap.mem_domain {X Y : AlgebraicGeometry.Scheme} {f : X.RationalMap Y} {x : ↑↑X.toPresheafedSpace} : x ∈ f.domain ↔ ∃ (g : X.PartialMap Y), x ∈ g.domain ∧ g.toRationalMap = f

theorem AlgebraicGeometry.Scheme.RationalMap.dense_domain {X Y : AlgebraicGeometry.Scheme} (f : X.RationalMap Y) : Dense ↑f.domain

noncomputable def AlgebraicGeometry.Scheme.RationalMap.openCoverDomain {X Y : AlgebraicGeometry.Scheme} (f : X.RationalMap Y) : (↑f.domain).OpenCover

The open cover of the domain of f : X ⤏ Y, consisting of all the domains of the partial maps in the equivalence class.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.RationalMap.toPartialMap {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsReduced X] [Y.IsSeparated] (f : X.RationalMap Y) : X.PartialMap Y

If f : X ⤏ Y is a rational map from a reduced scheme to a separated scheme, then f can be represented as a partial map on its domain of definition.

Equations

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

theorem AlgebraicGeometry.Scheme.PartialMap.toPartialMap_toRationalMap_restrict {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsReduced X] [Y.IsSeparated] (f : X.PartialMap Y) : (f.toRationalMap.toPartialMap.restrict f.domain ⋯ ⋯).hom = f.hom

@[simp]

theorem AlgebraicGeometry.Scheme.RationalMap.toRationalMap_toPartialMap {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsReduced X] [Y.IsSeparated] (f : X.RationalMap Y) : f.toPartialMap.toRationalMap = f

instance AlgebraicGeometry.Scheme.instIsOverToPartialMapOfIsSeparatedOfIsOver {X Y S : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsReduced X] [Y.IsSeparated] [S.IsSeparated] [X.Over S] [Y.Over S] (f : X.RationalMap Y) [AlgebraicGeometry.Scheme.RationalMap.IsOver S f] : AlgebraicGeometry.Scheme.PartialMap.IsOver S f.toPartialMap