Module

IntegralSectionIdeal.lean

Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.IntegralSectionIdeal

2 declarations indexed from sourceView source ↗

Module documentation

The ideal sheaf of an integral section

The section constructed from a primitive integer pair has reduced source Spec ℤ. Its scheme-theoretic image therefore has the reduced induced structure on its closed image. The actual kernel ideal sheaf is consequently the vanishing ideal of the homogeneous equation's zero locus.

For a rational point, this identifies the section's ideal sheaf with the vanishing ideal of the Zariski closure of the original rational point, as in Lemma 2.3 of Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers. This statement identifies the reduced closed subscheme; identifying its ideal on a chart with the principal linear-equation ideal additionally uses the radicality of that concrete polynomial ideal.

Imports17

Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.IntegralSection
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.RationalSection
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.RationalSectionSupport
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.StandardAffineChart
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.TwoSectionComplement
Mathlib.Algebra.Category.Ring.Basic
Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Mathlib.AlgebraicGeometry.Properties
Mathlib.AlgebraicGeometry.Spec
Mathlib.Data.Set.Image
Mathlib.LinearAlgebra.Projectivization.Basic
Mathlib.RingTheory.MvPolynomial.Homogeneous
Mathlib.Topology.Closure
Mathlib.Topology.Sets.Closeds

Imported by3

theorem

integralSection_ker_eq_vanishingIdeal

L52 ↗

ShimizuYamaguchi26BranchedCoverings.integralSection_ker_eq_vanishingIdeal

Documentation

The kernel of the actual integral section is the reduced ideal sheaf of the zero locus of its primitive homogeneous equation.

Source context 4 commands

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

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

Lean source · statement

theorem integralSection_ker_eq_vanishingIdeal
    (u v a b : ℤ) (hab : a * u + b * v = 1) :
    (integralSection u v a b hab).ker =
      Scheme.IdealSheafData.vanishingIdeal
        ⟨ProjectiveSpectrum.zeroLocus (MvPolynomial.homogeneousSubmodule (Fin 2) ℤ)
            {linearSectionEquation u v},
          ProjectiveSpectrum.isClosed_zeroLocus _ _⟩

theorem

rationalSection_ker_eq_vanishingIdeal_closure

L76 ↗

ShimizuYamaguchi26BranchedCoverings.rationalSection_ker_eq_vanishingIdeal_closure