Module

IntegralSectionCoordinateTransport.lean

Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.IntegralSectionCoordinateTransport

4 declarations indexed from sourceView source ↗

Module documentation

Transporting actual section ideals by the integral coordinate change

Pullback by the inverse of a scheme isomorphism agrees with pushforward by the isomorphism. Applied to reduced vanishing ideal sheaves, this identifies pullback with the vanishing ideal of the inverse image.

The explicit integral coordinate change therefore sends the actual kernel ideal of a second primitive section to that of the section with coordinates (-(a*u' + b*v'), u*v' - v*u'). The first section becomes the actual section at infinity. The only auxiliary data are Bezout coefficients for these primitive pairs, supplied by isCoprime_normalizedCoordinates. No comparison of section ideals is assumed.

These identities supply the coordinate transport in Lemma 2.3 of Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers.

Imports19

Nyll.ShimizuYamaguchi26BranchedCoverings.Arithmetic.Determinant
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.IntegralCoordinateChange
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.IntegralSection
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.IntegralSectionIdeal
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.StandardAffineChart
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.TwoSectionComplement
Mathlib.Algebra.Module.Submodule.Defs
Mathlib.Algebra.MvPolynomial.Basic
Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Mathlib.AlgebraicGeometry.Scheme
Mathlib.CategoryTheory.Iso
Mathlib.Data.Set.Image
Mathlib.RingTheory.MvPolynomial.Homogeneous
Mathlib.Topology.Closure
Mathlib.Topology.Homeomorph.Defs
Mathlib.Topology.Sets.Closeds

Imported by4

theorem

comap_inv_eq_map_hom

L54 ↗

ShimizuYamaguchi26BranchedCoverings.comap_inv_eq_map_hom

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace ShimizuYamaguchi26BranchedCoverings
attribute [local instance] MvPolynomial.gradedAlgebra

Lean source · statement

theorem comap_inv_eq_map_hom {X Y : Scheme} (e : X ≅ Y)
    (I : X.IdealSheafData) : I.comap e.inv = I.map e.hom

theorem

comap_inv_vanishingIdeal

L67 ↗

ShimizuYamaguchi26BranchedCoverings.comap_inv_vanishingIdeal

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace ShimizuYamaguchi26BranchedCoverings
attribute [local instance] MvPolynomial.gradedAlgebra

Lean source · statement

theorem comap_inv_vanishingIdeal {X Y : Scheme} (e : X ≅ Y)
    (Z : TopologicalSpace.Closeds X) :
    (Scheme.IdealSheafData.vanishingIdeal Z).comap e.inv =
      Scheme.IdealSheafData.vanishingIdeal (Z.preimage e.inv.continuous)

theorem

integralSection_ker_comap_coordinateChange_inv

L82 ↗

ShimizuYamaguchi26BranchedCoverings.integralSection_ker_comap_coordinateChange_inv

Documentation

The actual ideal of the second section transforms to the ideal of its explicit normalized primitive coordinates. The supplied Bezout identity can be obtained from isCoprime_normalizedCoordinates.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace ShimizuYamaguchi26BranchedCoverings
attribute [local instance] MvPolynomial.gradedAlgebra

Lean source · statement

theorem integralSection_ker_comap_coordinateChange_inv
    (u v a b u' v' c d c' d' : ℤ)
    (hab : a * u + b * v = 1) (hcd : c * u' + d * v' = 1)
    (hcd' : c' * (-(a * u' + b * v')) +
      d' * coordinateDeterminant u v u' v' = 1) :
    (integralSection u' v' c d hcd).ker.comap
        (integralCoordinateChange u v a b hab).inv =
      (integralSection (-(a * u' + b * v'))
        (coordinateDeterminant u v u' v') c' d' hcd').ker

theorem

integralSection_ker_comap_coordinateChange_inv_self

L132 ↗

ShimizuYamaguchi26BranchedCoverings.integralSection_ker_comap_coordinateChange_inv_self

Documentation

Pulling back the first section's actual ideal gives the actual section at infinity, including its scheme structure.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace ShimizuYamaguchi26BranchedCoverings
attribute [local instance] MvPolynomial.gradedAlgebra

Lean source · full declaration

theorem integralSection_ker_comap_coordinateChange_inv_self
    (u v a b : ℤ) (hab : a * u + b * v = 1) :
    (integralSection u v a b hab).ker.comap
        (integralCoordinateChange u v a b hab).inv =
      (integralSection 1 0 1 0 (by decide)).ker := by
  rw [integralSection_ker_eq_vanishingIdeal,
    integralSection_ker_eq_vanishingIdeal, comap_inv_vanishingIdeal]
  apply congrArg Scheme.IdealSheafData.vanishingIdeal
  apply SetLike.coe_injective
  change (integralCoordinateChange u v a b hab).inv ⁻¹'
      ProjectiveSpectrum.zeroLocus (MvPolynomial.homogeneousSubmodule (Fin 2) ℤ)
        {linearSectionEquation u v} =
    ProjectiveSpectrum.zeroLocus (MvPolynomial.homogeneousSubmodule (Fin 2) ℤ)
      {linearSectionEquation (1 : ℤ) 0}
  have hinfinity : Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin 2) ℤ)
      (linearSectionEquation (1 : ℤ) 0) = infinityComplement ℤ := by
    ext x
    change (linearSectionEquation (1 : ℤ) 0 ∉ x.asHomogeneousIdeal.toIdeal) ↔
      MvPolynomial.X (1 : Fin 2) ∉ x.asHomogeneousIdeal.toIdeal
    simp only [linearSectionEquation, map_zero, map_one, zero_mul, one_mul,
      zero_sub, x.asHomogeneousIdeal.toIdeal.neg_mem_iff]
  have hopen : (integralCoordinateChange u v a b hab).inv ⁻¹'
      (Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin 2) ℤ)
        (linearSectionEquation u v) : Set (ProjectiveLine ℤ))ᶜ =
      (Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin 2) ℤ)
        (linearSectionEquation (1 : ℤ) 0) : Set (ProjectiveLine ℤ))ᶜ :=
    congrArg (fun U : (ProjectiveLine ℤ).Opens => (U : Set (ProjectiveLine ℤ))ᶜ)
      ((integralCoordinateChange_inv_preimage_firstSection u v a b hab).trans
        hinfinity.symm)
  have hsource :
      (Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin 2) ℤ)
        (linearSectionEquation u v) : Set (ProjectiveLine ℤ))ᶜ =
      (ProjectiveSpectrum.zeroLocus (MvPolynomial.homogeneousSubmodule (Fin 2) ℤ)
        {linearSectionEquation u v} : Set (ProjectiveLine ℤ)) :=
    compl_eq_comm.mp (ProjectiveSpectrum.basicOpen_eq_zeroLocus_compl
      (MvPolynomial.homogeneousSubmodule (Fin 2) ℤ) (linearSectionEquation u v)).symm
  have htarget :
      (Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin 2) ℤ)
        (linearSectionEquation (1 : ℤ) 0) : Set (ProjectiveLine ℤ))ᶜ =
      (ProjectiveSpectrum.zeroLocus (MvPolynomial.homogeneousSubmodule (Fin 2) ℤ)
        {linearSectionEquation (1 : ℤ) 0} : Set (ProjectiveLine ℤ)) :=
    compl_eq_comm.mp (ProjectiveSpectrum.basicOpen_eq_zeroLocus_compl
      (MvPolynomial.homogeneousSubmodule (Fin 2) ℤ)
      (linearSectionEquation (1 : ℤ) 0)).symm
  exact (congrArg (fun Z : Set (ProjectiveLine ℤ) =>
    (integralCoordinateChange u v a b hab).inv ⁻¹' Z) hsource.symm).trans
      (hopen.trans htarget)

Module documentation

Transporting actual section ideals by the integral coordinate change

Declarations

comap_inv_eq_map_hom

comap_inv_vanishingIdeal

integralSection_ker_comap_coordinateChange_inv

integralSection_ker_comap_coordinateChange_inv_self