Module

IntegerSectionParameters.lean

Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.IntegerSectionParameters

4 declarations indexed from sourceView source ↗

Module documentation

Parameters supplied by two integral section equations

The concrete equations w and v-u*w form a weakly regular sequence in ℤ[w] when v is nonzero: modulo w, multiplication by the second equation is multiplication by the nonzero integer v. When p divides v, both equations lie in (p,w), so their images form a regular sequence in that localization and then in the actual projective stalk.

If v_p(v)=1, the previously calculated intersection quotient has length one. Its ideal is therefore the maximal ideal of the local ring. The two actual equation germs consequently form a regular system of parameters.

This is the normalized two-section local calculation needed for the normal-crossings assertion in Lemma 2.3 of Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers. The finite-divisor criterion and its comparison with base change to ℤ_p are separate assertions.

Imports27

Nyll.SchemeTheory.Divisors.Basic
Nyll.ShimizuYamaguchi26BranchedCoverings.Arithmetic.IntegerLocalizationValuation
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.InfinityChartStalk
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.InfinityIntersection
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.IntegerChartLocalization
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.IntegerProjectiveIntersection
Mathlib.Algebra.Module.Equiv.Defs
Mathlib.Algebra.Polynomial.Basic
Mathlib.Algebra.Polynomial.Coeff
Mathlib.Algebra.Polynomial.Div
Mathlib.Algebra.Ring.CompTypeclasses
Mathlib.Algebra.Ring.Equiv
Mathlib.Algebra.Ring.Hom.Defs
Mathlib.Data.Fin.VecNotation
Mathlib.Data.List.OfFn
Mathlib.Data.Set.Image
Mathlib.NumberTheory.Padics.PadicVal.Basic
Mathlib.RingTheory.Ideal.Maps
Mathlib.RingTheory.Ideal.Operations
Mathlib.RingTheory.Ideal.Span
Mathlib.RingTheory.Length
Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Mathlib.RingTheory.Localization.AtPrime.Basic
Mathlib.RingTheory.Regular.Flat
Mathlib.RingTheory.Regular.IsSMulRegular
Mathlib.RingTheory.Regular.RegularSequence
Mathlib.RingTheory.SimpleModule.Basic

Imported by2

theorem

integerSectionEquations_isWeaklyRegular

L61 ↗

ShimizuYamaguchi26BranchedCoverings.integerSectionEquations_isWeaklyRegular

Source context 3 commands

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

noncomputable section
open scoped Polynomial Pointwise
namespace ShimizuYamaguchi26BranchedCoverings

Lean source · statement

theorem integerSectionEquations_isWeaklyRegular
    (u v : ℤ) (hv : v ≠ 0) :
    RingTheory.Sequence.IsWeaklyRegular ℤ[X]
      [Polynomial.X, Polynomial.C v - Polynomial.C u * Polynomial.X]

theorem

integerInfinityChartSectionEquations_isRegular

L88 ↗

ShimizuYamaguchi26BranchedCoverings.integerInfinityChartSectionEquations_isRegular

Source context 3 commands

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

noncomputable section
open scoped Polynomial Pointwise
namespace ShimizuYamaguchi26BranchedCoverings

Lean source · statement

theorem integerInfinityChartSectionEquations_isRegular
    (p : ℕ) [Fact p.Prime] (u v : ℤ) (hv : v ≠ 0) (hpv : (p : ℤ) ∣ v) :
    RingTheory.Sequence.IsRegular (IntegerInfinityChartLocalRing p)
      [algebraMap ℤ[X] (IntegerInfinityChartLocalRing p) Polynomial.X,
        algebraMap ℤ[X] (IntegerInfinityChartLocalRing p)
          (Polynomial.C v - Polynomial.C u * Polynomial.X)]

theorem

integerProjectiveInfinitySectionEquations_isRegular

L115 ↗

ShimizuYamaguchi26BranchedCoverings.integerProjectiveInfinitySectionEquations_isRegular

Documentation

The germs of w and v-u*w at (p,w) form a regular sequence when v is nonzero and divisible by p.

Source context 3 commands

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

noncomputable section
open scoped Polynomial Pointwise
namespace ShimizuYamaguchi26BranchedCoverings

Lean source · statement

theorem integerProjectiveInfinitySectionEquations_isRegular
    (p : ℕ) [Fact p.Prime] (u v : ℤ) (hv : v ≠ 0) (hpv : (p : ℤ) ∣ v) :
    RingTheory.Sequence.IsRegular (IntegerProjectiveInfinityLocalRing p)
      ([infinityChartGermAt ℤ (integerInfinityChartPoint p) Polynomial.X,
        infinityChartGermAt ℤ (integerInfinityChartPoint p)
          (Polynomial.C v - Polynomial.C u * Polynomial.X)] :
        List (IntegerProjectiveInfinityLocalRing p))

theorem

integerProjectiveInfinitySection_isRegularSystemOfParameters

L157 ↗

ShimizuYamaguchi26BranchedCoverings.integerProjectiveInfinitySection_isRegularSystemOfParameters

Documentation

When the local intersection multiplicity is one, the two concrete section equations are a regular system of parameters in the actual integral projective stalk.

Source context 3 commands

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

noncomputable section
open scoped Polynomial Pointwise
namespace ShimizuYamaguchi26BranchedCoverings

Lean source · statement

theorem integerProjectiveInfinitySection_isRegularSystemOfParameters
    (p : ℕ) [Fact p.Prime] (u v : ℤ) (hv : v ≠ 0) (hval : padicValInt p v = 1) :
    AlgebraicGeometry.Scheme.IsRegularSystemOfParameters
      (![infinityChartGermAt ℤ (integerInfinityChartPoint p) Polynomial.X,
        infinityChartGermAt ℤ (integerInfinityChartPoint p)
          (Polynomial.C v - Polynomial.C u * Polynomial.X)] :
        Fin 2 → IntegerProjectiveInfinityLocalRing p)

Module documentation

Parameters supplied by two integral section equations

Declarations

integerSectionEquations_isWeaklyRegular

integerInfinityChartSectionEquations_isRegular

integerProjectiveInfinitySectionEquations_isRegular

integerProjectiveInfinitySection_isRegularSystemOfParameters