Rational maps between schemes #
Main definitions #
AlgebraicGeometry.Scheme.PartialMap
: A partial map fromX
toY
(X.PartialMap Y
) is a morphism intoY
defined on a dense open subscheme ofX
.AlgebraicGeometry.Scheme.PartialMap.equiv
: Two partial maps are equivalent if they are equal on a dense open subscheme.AlgebraicGeometry.Scheme.RationalMap
: A rational map fromX
toY
(X ⤏ Y
) is an equivalence class of partial maps.AlgebraicGeometry.Scheme.RationalMap.equivFunctionField
: GivenS
-schemesX
andY
such thatY
is locally of finite type andX
is integral,S
-morphismsSpec K(X) ⟶ Y
correspond bijectively toS
-rational maps fromX
toY
.
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.
Instances For
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 }
Instances For
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 }
Instances For
A scheme morphism as a partial map.
Equations
- f.toPartialMap = { domain := ⊤, dense_domain := ⋯, hom := CategoryTheory.CategoryStruct.comp X.topIso.hom f }
Instances For
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
Instances For
A partial map restricts to a map from Spec K(X)
.
Equations
- f.fromFunctionField = f.fromSpecStalkOfMem ⋯
Instances For
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 }
Instances For
Two partial maps are equivalent if they are equal on a dense open subscheme.
Equations
Instances For
Equations
- AlgebraicGeometry.Scheme.PartialMap.instSetoid = { r := AlgebraicGeometry.Scheme.PartialMap.equiv, iseqv := ⋯ }
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.
Instances For
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))
Instances For
A partial map as a rational map.
Equations
- f.toRationalMap = ⟦f⟧
Instances For
A scheme morphism as a rational map.
Equations
- f.toRationalMap = f.toPartialMap.toRationalMap
Instances For
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
Instances For
A rational map restricts to a map from Spec K(X)
.
Equations
- f.fromFunctionField = Quotient.lift AlgebraicGeometry.Scheme.PartialMap.fromFunctionField ⋯ f
Instances For
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
Instances For
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.