NYLL
Module

IntegralSectionStalk.lean

Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.IntegralSectionStalk
2 declarations indexed from sourceView source ↗

Module documentation

The actual ideal of an integral section in a projective stalk

A primitive section has a reduced kernel ideal sheaf. On the infinity chart, its support is the zero locus of v-u*w. Restriction to the open chart preserves radical ideals, so equality of these zero loci identifies the actual chart ideal with the principal equation ideal.

The ideal-sheaf stalk and the inverse stalk map of the chart then identify the section's actual projective stalk ideal with the ideal generated by the polynomial germ. This supplies the scheme-theoretic equation comparison used in Lemma 2.3 of Shimizu and Yamaguchi, On branched coverings of the projective line over the integers.

Imports29
Imported by5

Declarations

theorem

integralSection_infinityChart_ideal_top

L63 ↗
ShimizuYamaguchi26BranchedCoverings.integralSection_infinityChart_ideal_top
Documentation

On the infinity chart, the actual kernel ideal of a primitive section is obtained from its polynomial equation ideal by the canonical section-ring map.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem integralSection_infinityChart_ideal_top
    (u v a b : ℤ) (hab : a * u + b * v = 1) :
    (((integralSection u v a b hab).ker.comap (infinityChartEmbedding ℤ)).ideal
        ⟨⊤, isAffineOpen_top (Spec (CommRingCat.of ℤ[X]))⟩) =
      (infinitySectionIdeal u v).map
        (Scheme.ΓSpecIso (CommRingCat.of ℤ[X])).inv.hom
theorem

integralSection_stalkIdeal_eq

L128 ↗
ShimizuYamaguchi26BranchedCoverings.integralSection_stalkIdeal_eq
Documentation

At every infinity-chart point, the actual section ideal is generated by its primitive polynomial equation under the actual projective germ map.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem integralSection_stalkIdeal_eq
    (u v a b : ℤ) (hab : a * u + b * v = 1)
    (q : Spec (CommRingCat.of ℤ[X])) :
    (integralSection u v a b hab).ker.stalkIdeal (infinityChartEmbedding ℤ q) =
      (infinitySectionIdeal u v).map (infinityChartGermAt ℤ q)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.