Birational maps and the Cremona group

13 fully proved6 ready to prove

Scheme

StructureBirational map#✓fully proved

Let \(X\) and \(Y\) be irreducible schemes. A birational map from \(X\) to \(Y\) consists of dominant rational maps \(f \colon X \dashrightarrow Y\) and \(g \colon Y \dashrightarrow X\) that are mutually inverse: \(g \circ f\) is the identity rational map of \(X\) and \(f \circ g\) is the identity rational map of \(Y\).

structure BirationalMap (X Y : Scheme.{u}) [IrreducibleSpace X] [IrreducibleSpace Y] where
  /-- The forward rational map of a birational map. -/
  hom : X ⤏ Y
  [isDominant_hom : hom.IsDominant]
  /-- The inverse rational map of a birational map. -/
  inv : Y ⤏ X
  [isDominant_inv : inv.IsDominant]
  hom_comp_inv_id : hom.comp inv = .id X := by grind
  inv_comp_hom_id : inv.comp hom = .id Y := by grind

Used by 10

Used byBirational automorphisms over a base · Cremona group · Cremona group generated by pseudo-regularizable elements · Birational maps over a base · Pseudo-regularizable birational automorphism · Pseudo-regularization of a birational automorphism · Identity birational map · Inverse birational map · Birational map of a partial isomorphism · Composition of birational maps

Birational Map

DefinitionIdentity birational map#✓fully proved

For an irreducible scheme \(X\), the identity birational map of \(X\) has the identity rational map of \(X\) as both its forward and its inverse map.

@[simps]
def refl : X.BirationalMap X where
  hom := RationalMap.id X
  inv := RationalMap.id X

Uses 1 · Used by 3

Statement usesBirational map

Used byBirational automorphisms over a base · Cremona group · Cremona group generated by pseudo-regularizable elements

DefinitionInverse birational map#✓fully proved

Let \(X\) and \(Y\) be irreducible schemes. The inverse of a birational map from \(X\) to \(Y\) is the birational map from \(Y\) to \(X\) whose forward map is the inverse rational map of the original and whose inverse map is its forward rational map.

@[simps]
def symm (f : X.BirationalMap Y) : Y.BirationalMap X where
  hom := f.inv
  inv := f.hom

Uses 1 · Used by 4

Statement usesBirational map

Used byBirational automorphisms over a base · Cremona group · Cremona group generated by pseudo-regularizable elements · Pseudo-regularization of a birational automorphism

DefinitionComposition of birational maps#✓fully proved

Let \(X\), \(Y\) and \(Z\) be irreducible schemes, let \(f\) be a birational map from \(X\) to \(Y\) and let \(g\) be a birational map from \(Y\) to \(Z\). The composite of \(f\) and \(g\) is the birational map from \(X\) to \(Z\) whose forward rational map is the forward map of \(f\) followed by the forward map of \(g\), and whose inverse rational map is the inverse of \(g\) followed by the inverse of \(f\).

@[simps]
noncomputable def trans (f : X.BirationalMap Y) (g : Y.BirationalMap Z) :
    BirationalMap X Z where
  hom := f.hom.comp g.hom
  inv := g.inv.comp f.inv

Uses 1 · Used by 4

Statement usesBirational map

Used byBirational automorphisms over a base · Cremona group · Cremona group generated by pseudo-regularizable elements · Pseudo-regularization of a birational automorphism

AbbreviationBirational maps over a base#✓fully proved

Let \(X\) and \(Y\) be irreducible schemes over a scheme \(S\). A birational map from \(X\) to \(Y\) is over \(S\) when its forward rational map \(X \dashrightarrow Y\) is compatible with the structure maps to \(S\).

Its inverse rational map is then compatible with the structure maps to \(S\) as well.

abbrev IsOver (S : Scheme.{u}) [X.Over S] [Y.Over S] (f : X.BirationalMap Y) : Prop :=
  f.hom.IsOver S

Uses 1 · Used by 2

Statement usesBirational map

Used byBirational automorphisms over a base · Pseudo-regularization of a birational automorphism

Scheme

DefinitionBirational automorphisms over a base#✓fully proved

Let \(X\) be an irreducible scheme over a scheme \(S\). The birational automorphisms of \(X\) over \(S\) form the subgroup of the group of birational self-maps of \(X\) consisting of those birational maps whose forward rational map \(X \dashrightarrow X\) is compatible with the structure maps to \(S\).

def birationalAutOver (S : Scheme.{u}) [X.Over S] : Subgroup (X.BirationalMap X) where
  carrier := { f | f.IsOver S }
  one_mem' := inferInstanceAs ((RationalMap.id X).IsOver S)
  mul_mem' {f g} (_ : f.IsOver S) (_ : g.IsOver S) := inferInstanceAs ((f.hom.comp g.hom).IsOver S)
  inv_mem' {f} (_ : f.IsOver S) := inferInstanceAs (f.inv.IsOver S)

Uses 5 · Used by 2

Statement usesBirational map · Birational maps over a base · Identity birational map · Inverse birational map · Composition of birational maps

Used byCremona group · Cremona group generated by pseudo-regularizable elements

DefinitionBirational map of a partial isomorphism#✓fully proved

Let \(X\) and \(Y\) be irreducible schemes and let \(f\) be a partial isomorphism from \(X\) to \(Y\), that is, an isomorphism from a dense open subscheme of \(X\) onto a dense open subscheme of \(Y\). The birational map from \(X\) to \(Y\) given by \(f\) has as forward map the rational map \(X \dashrightarrow Y\) represented by \(f\), and as inverse the rational map \(Y \dashrightarrow X\) represented by the inverse of \(f\).

@[simps]
def PartialIso.toBirationalMap (f : X.PartialIso Y) : X.BirationalMap Y where
  hom := f.toRationalMap
  inv := f.symm.toRationalMap
  hom_comp_inv_id := by
    rw [RationalMap.toRationalMap_comp, PartialMap.toRationalMap_eq_iff,
      PartialIso.toPartialMap_comp_symm]
    apply PartialMap.restrict_equiv
  inv_comp_hom_id := by
    rw [RationalMap.toRationalMap_comp, PartialMap.toRationalMap_eq_iff,
      PartialIso.symm_toPartialMap_comp]
    apply PartialMap.restrict_equiv

Uses 1 · Used by 1

Statement usesBirational map

Used byPseudo-regularization of a birational automorphism

Motivic Invariants

ClassIntegral variety over a field#✓fully proved

Let \(k\) be a field. A variety over \(k\) in this sense is a scheme \(X\) together with a morphism \(X \to \operatorname{Spec} k\) such that \(X\) is integral (irreducible and reduced) and the morphism is separated and of finite type (locally of finite type and quasi-compact).

class Variety (X : Scheme) where
  [over : X.Over (Spec (.of 𝕜))]
  [isIntegral : IsIntegral X]
  [isSeparated : IsSeparated (X ↘ Spec (.of 𝕜))]
  [locallyOfFiniteType: LocallyOfFiniteType (X ↘ Spec (.of 𝕜))]
  [quasicompact : QuasiCompact (X ↘ Spec (.of 𝕜))]

Used by 7

Used byCremona group · Cremona group generated by pseudo-regularizable elements · Pseudo-regularizable birational automorphism · Pseudo-regularization of a birational automorphism · \(\mathrm{Cr}_3\) of a function field over a number field is not generated by pseudo-regularizable elements · \(\mathrm{Cr}_3\) of a function field over a finite field is not generated by pseudo-regularizable elements · \(\mathrm{Cr}_3\) of a function field over an algebraically closed field is not generated by pseudo-regularizable elements

StructurePseudo-isomorphism#✓fully proved

Let \(X\) and \(Y\) be schemes. A partial isomorphism from \(X\) to \(Y\), that is, an isomorphism \(U \cong V\) between dense open subschemes \(U \subseteq X\) and \(V \subseteq Y\), is a pseudo-isomorphism if it is an isomorphism in codimension one: every point of \(X\) outside \(U\) and every point of \(Y\) outside \(V\) has coheight at least \(2\) in the specialization order of points.

structure IsPseudoIso
    {X Y : Scheme.{u}} (i : PartialIso X Y) : Prop where
  codim_source : ∀ x ∉ i.source, 2 ≤ Order.coheight x
  codim_target : ∀ y ∉ i.target, 2 ≤ Order.coheight y

Used by 1

Used byPseudo-regularization of a birational automorphism

StructurePseudo-regularization of a birational automorphism#✓fully proved

Let \(X\) be a variety over a field \(k\) and let \(\varphi\) be a birational automorphism of \(X\). A pseudo-regularization of \(\varphi\) consists of a variety \(X'\) over \(k\), a birational map \(\alpha \colon X \dashrightarrow X'\) over \(k\), and a partial isomorphism \(\gamma\) from \(X'\) to itself over \(k\) that is a pseudo-isomorphism, such that \(\varphi = \alpha^{-1} \circ \gamma \circ \alpha\), where \(\gamma\) is viewed as a birational map.

structure PseudoRegularization {X : Scheme} [Variety 𝕜 X] (φ : BirationalMap X X) where
  /-- An irreducible scheme birational to `X`. -/
  X' : Scheme
  /-- The scheme is a variety. -/
  [variety : Variety 𝕜 X']
  /-- The birational map `α : X ⤏ X'`. -/
  α : BirationalMap X X'
  [isOver_α : α.IsOver (Spec (.of 𝕜))]
  /-- The pseudo-automorphism of `X'`, namely an isomorphism in codimension one. -/
  γ : PartialIso X' X'
  [isOver_γ : γ.IsOver (X' ↘ (Spec (.of 𝕜))) (X' ↘ (Spec (.of 𝕜)))]
  isPseudoIso : IsPseudoIso γ
  cond : φ = (α.trans γ.toBirationalMap).trans α.symm

Uses 7 · Used by 1

Statement usesBirational map · Birational maps over a base · Inverse birational map · Composition of birational maps · Birational map of a partial isomorphism · Pseudo-isomorphism · Integral variety over a field

Used byPseudo-regularizable birational automorphism

AbbreviationPseudo-regularizable birational automorphism#✓fully proved

Let \(X\) be a variety over a field \(k\). A birational automorphism \(\varphi\) of \(X\) is pseudo-regularizable if there exist a variety \(X'\) over \(k\), a birational map \(\alpha \colon X \dashrightarrow X'\) over \(k\), and a partial isomorphism \(\gamma\) from \(X'\) to itself over \(k\) that is a pseudo-isomorphism (an isomorphism in codimension one), such that \(\varphi = \alpha^{-1} \circ \gamma \circ \alpha\), where \(\gamma\) is viewed as a birational map. The variety \(X'\) need not be smooth or projective.

abbrev IsPseudoRegularizable
    {X : Scheme} [Variety 𝕜 X] (φ : BirationalMap X X) : Prop :=
  Nonempty (PseudoRegularization 𝕜 φ)

Sources

• H.-Y. Lin and E. Shinder, Motivic invariants of birational maps, Definition 4.1.

Uses 3 · Used by 1

Statement usesBirational map · Pseudo-regularization of a birational automorphism · Integral variety over a field

Used byCremona group generated by pseudo-regularizable elements

AbbreviationCremona group#✓fully proved

For a field \(k\) and \(n \in \mathbb{N}\), the Cremona group \(\mathrm{Cr}_n(k)\) is the group of birational automorphisms of affine \(n\)-space \(\mathbb{A}^n_k\) over \(\operatorname{Spec} k\).

abbrev Cr (n : ℕ) : Type := 𝔸(Fin n; Spec (.of 𝕜)).birationalAutOver (Spec (.of 𝕜))

Uses 6 · Used by 1

Statement usesBirational map · Identity birational map · Inverse birational map · Composition of birational maps · Birational automorphisms over a base · Integral variety over a field

Used byCremona group generated by pseudo-regularizable elements

AbbreviationCremona group generated by pseudo-regularizable elements#✓fully proved

For a field \(k\) and \(n \in \mathbb{N}\), this is the proposition that the Cremona group \(\mathrm{Cr}_n(k)\) is generated, as a group, by its pseudo-regularizable elements.

abbrev GenByPseudoRegularizable (n : ℕ) : Prop :=
  Subgroup.closure { f : Cr 𝕜 n | IsPseudoRegularizable 𝕜 f.1 } = ⊤

Uses 8 · Used by 6

Statement usesBirational map · Identity birational map · Inverse birational map · Composition of birational maps · Birational automorphisms over a base · Cremona group · Pseudo-regularizable birational automorphism · Integral variety over a field

Used by\(\mathrm{Cr}_3\) of a number field is not generated by pseudo-regularizable elements · \(\mathrm{Cr}_3\) of a function field over a number field is not generated by pseudo-regularizable elements · \(\mathrm{Cr}_3\) of a function field over a finite field is not generated by pseudo-regularizable elements · \(\mathrm{Cr}_3\) of a function field over an algebraically closed field is not generated by pseudo-regularizable elements · \(\mathrm{Cr}_n\) of a subfield of \(\mathbb{C}\) is not generated by pseudo-regularizable elements for \(n \ge 4\) · \(\mathrm{Cr}_n\) of an infinite field is not generated by pseudo-regularizable elements for \(n \ge 5\)

Theorem\(\mathrm{Cr}_3\) of a number field is not generated by pseudo-regularizable elements#●ready to prove

Let \(k\) be a number field. The Cremona group \(\mathrm{Cr}_3(k)\), the group of birational automorphisms of affine \(3\)-space over \(k\), is not generated by its pseudo-regularizable elements.

This is Theorem 1.2 (1) (a) of Lin and Shinder.

public theorem_wanted theorem_1_2_1_a [NumberField 𝕜] :
    ¬ GenByPseudoRegularizable 𝕜 3

Sources

• H.-Y. Lin and E. Shinder, Motivic invariants of birational maps, Annals of Math, 199 (1) 2024. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_motivic_invariants of the lean-eval benchmark.

Uses 1

Statement usesCremona group generated by pseudo-regularizable elements

Theorem\(\mathrm{Cr}_3\) of a function field over a number field is not generated by pseudo-regularizable elements#●ready to prove

\(\mathrm{Cr}_3\) of a function field over a number field is not generated by pseudo-regularizable elements. Let \(F\) be a number field and let \(X\) be a variety over \(F\) of positive dimension, with function field \(F(X)\). The Cremona group \(\mathrm{Cr}_3(F(X))\), the group of birational automorphisms of affine \(3\)-space over \(F(X)\), is not generated by its pseudo-regularizable elements.

This is Theorem 1.2 (1) (b) of Lin and Shinder.

public theorem_wanted theorem_1_2_1_b [NumberField 𝔽] (X : Scheme) [Variety 𝔽 X]
    (hX : 0 < topologicalKrullDim X) :
    ¬ GenByPseudoRegularizable X.functionField 3

Sources

• H.-Y. Lin and E. Shinder, Motivic invariants of birational maps, Annals of Math, 199 (1) 2024. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_motivic_invariants of the lean-eval benchmark.

Uses 2

Statement usesCremona group generated by pseudo-regularizable elements · Integral variety over a field

Theorem\(\mathrm{Cr}_3\) of a function field over a finite field is not generated by pseudo-regularizable elements#●ready to prove

\(\mathrm{Cr}_3\) of a function field over a finite field is not generated by pseudo-regularizable elements. Let \(F\) be a finite field and let \(X\) be a variety over \(F\) of positive dimension, with function field \(F(X)\). The Cremona group \(\mathrm{Cr}_3(F(X))\), the group of birational automorphisms of affine \(3\)-space over \(F(X)\), is not generated by its pseudo-regularizable elements.

This is Theorem 1.2 (1) (c) of Lin and Shinder.

public theorem_wanted theorem_1_2_1_c [Finite 𝔽] (X : Scheme) [Variety 𝔽 X]
    (hX : 0 < topologicalKrullDim X) :
    ¬ GenByPseudoRegularizable X.functionField 3

Sources

• H.-Y. Lin and E. Shinder, Motivic invariants of birational maps, Annals of Math, 199 (1) 2024. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_motivic_invariants of the lean-eval benchmark.

Uses 2

Statement usesCremona group generated by pseudo-regularizable elements · Integral variety over a field

Theorem\(\mathrm{Cr}_3\) of a function field over an algebraically closed field is not generated by pseudo-regularizable elements#●ready to prove

\(\mathrm{Cr}_3\) of a function field over an algebraically closed field is not generated by pseudo-regularizable elements. Let \(F\) be an algebraically closed field and let \(X\) be a variety over \(F\) of positive dimension, with function field \(F(X)\). The Cremona group \(\mathrm{Cr}_3(F(X))\), the group of birational automorphisms of affine \(3\)-space over \(F(X)\), is not generated by its pseudo-regularizable elements.

This is Theorem 1.2 (1) (d) of Lin and Shinder.

public theorem_wanted theorem_1_2_1_d [IsAlgClosed 𝔽] (X : Scheme) [Variety 𝔽 X]
    (hX : 0 < topologicalKrullDim X) :
    ¬ GenByPseudoRegularizable X.functionField 3

Sources

• H.-Y. Lin and E. Shinder, Motivic invariants of birational maps, Annals of Math, 199 (1) 2024. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_motivic_invariants of the lean-eval benchmark.

Uses 2

Statement usesCremona group generated by pseudo-regularizable elements · Integral variety over a field

Theorem\(\mathrm{Cr}_n\) of a subfield of \(\mathbb{C}\) is not generated by pseudo-regularizable elements for \(n \ge 4\)#●ready to prove

\(\mathrm{Cr}_n\) of a subfield of \(\mathbb{C}\) is not generated by pseudo-regularizable elements for \(n \ge 4\). Let \(k\) be a subfield of \(\mathbb{C}\) and let \(n \ge 4\). The Cremona group \(\mathrm{Cr}_n(k)\), the group of birational automorphisms of affine \(n\)-space over \(k\), is not generated by its pseudo-regularizable elements.

This is Theorem 1.2 (2) of Lin and Shinder.

public theorem_wanted theorem_1_2_2 {n : ℕ} (hn : 4 ≤ n) (𝕜 : Subfield ℂ) :
    ¬ GenByPseudoRegularizable 𝕜 n

Sources

• H.-Y. Lin and E. Shinder, Motivic invariants of birational maps, Annals of Math, 199 (1) 2024. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_motivic_invariants of the lean-eval benchmark.

Uses 1

Statement usesCremona group generated by pseudo-regularizable elements

Theorem\(\mathrm{Cr}_n\) of an infinite field is not generated by pseudo-regularizable elements for \(n \ge 5\)#●ready to prove

\(\mathrm{Cr}_n\) of an infinite field is not generated by pseudo-regularizable elements for \(n \ge 5\). Let \(k\) be an infinite field and let \(n \ge 5\). The Cremona group \(\mathrm{Cr}_n(k)\), the group of birational automorphisms of affine \(n\)-space over \(k\), is not generated by its pseudo-regularizable elements.

This is Theorem 1.2 (3) of Lin and Shinder.

public theorem_wanted theorem_1_2_3 {n : ℕ} (hn : 5 ≤ n) [Infinite 𝕜] :
    ¬ GenByPseudoRegularizable 𝕜 n

Sources

• H.-Y. Lin and E. Shinder, Motivic invariants of birational maps, Annals of Math, 199 (1) 2024. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_motivic_invariants of the lean-eval benchmark.

Uses 1

Statement usesCremona group generated by pseudo-regularizable elements

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.