Documentation

Mathlib.AlgebraicGeometry.Birational.Dominant

Dominant rational maps #

This file defines RationalMap.IsDominant and establishes its connection to IsDominant on the underlying partial maps.

Main definition #

source
instance AlgebraicGeometry.Scheme.PartialMap.isDominant_restrict_hom {X Y : Scheme} (f : X.PartialMap Y) [IsDominant f.hom] (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.domain) :
IsDominant (f.restrict U hU hU').hom

Restricting a dominant partial map to a dense open yields a dominant partial map.

source
theorem AlgebraicGeometry.Scheme.PartialMap.isDominant_hom_of_isDominant_restrict_hom {X Y : Scheme} (f : X.PartialMap Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.domain) [H : IsDominant (f.restrict U hU hU').hom] :
IsDominant f.hom

If a restriction of f is dominant, then f is dominant.

source
theorem AlgebraicGeometry.Scheme.PartialMap.isDominant_hom_iff_isDominant_restrict_hom {X Y : Scheme} (f : X.PartialMap Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.domain) :
IsDominant f.hom ↔ IsDominant (f.restrict U hU hU').hom

f.hom is dominant iff any restriction of f is.

source
theorem AlgebraicGeometry.Scheme.PartialMap.isDominant_hom_iff_of_equiv {X Y : Scheme} (f g : X.PartialMap Y) (h : f.equiv g) :
IsDominant f.hom ↔ IsDominant g.hom

Dominance of the underlying morphism is invariant under equivalence of partial maps.

source
class AlgebraicGeometry.Scheme.RationalMap.IsDominant {X Y : Scheme} (f : X.RationalMap Y) :
Prop

A rational map is dominant if some (equivalently, any) representative partial map has dominant underlying morphism.

Instances
    source
    theorem AlgebraicGeometry.Scheme.RationalMap.isDominant_iff {X Y : Scheme} (f : X.RationalMap Y) :
    f.IsDominant ↔ Quotient.liftOn f (fun (g : X.PartialMap Y) => IsDominant g.hom) ⋯
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.PartialMap.isDominant_toRationalMap_iff {X Y : Scheme} (f : X.PartialMap Y) :
    f.toRationalMap.IsDominant ↔ IsDominant f.hom
    source
    instance AlgebraicGeometry.Scheme.instIsDominantToRationalMapOfIsDominantHom {X Y : Scheme} (f : X.PartialMap Y) [IsDominant f.hom] :
    f.toRationalMap.IsDominant
    source
    instance AlgebraicGeometry.Scheme.instIsDominantHomRepresentativeOfIsDominant {X Y : Scheme} (f : X.RationalMap Y) [f.IsDominant] :
    IsDominant f.representative.hom