Module

ZeroSection.lean

Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.ZeroSection

4 declarations indexed from sourceView source ↗

Module documentation

The zero section of the projective line

Evaluation at zero gives a morphism from Spec R to the standard affine chart of the projective line. The kernel of this evaluation is generated by the affine coordinate, so its affine image is its zero locus. The irrelevant-ideal condition puts every projective zero of T₀ inside the chart T₁ ≠ 0. Thus the image of the actual scheme morphism is exactly the homogeneous zero locus of T₀, over any commutative ring.

This section and its image are used to construct the primitive integral sections in Lemma 2.3 of Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers.

Imports17

Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.FieldSectionPoint
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.StandardAffineChart
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.TwoSectionComplement
Mathlib.Algebra.MvPolynomial.Basic
Mathlib.Algebra.Polynomial.Basic
Mathlib.Algebra.Polynomial.Eval.Defs
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Mathlib.AlgebraicGeometry.Scheme
Mathlib.Data.Set.Image
Mathlib.Data.Set.Insert
Mathlib.RingTheory.MvPolynomial.Homogeneous
Mathlib.RingTheory.Polynomial.Ideal
Mathlib.RingTheory.Spectrum.Prime.Basic
Mathlib.RingTheory.Spectrum.Prime.RingHom
Mathlib.RingTheory.Spectrum.Prime.Topology

Imported by3

def

zeroSection

L51 ↗

ShimizuYamaguchi26BranchedCoverings.zeroSection

Documentation

The zero section, constructed by polynomial evaluation in the standard chart.

Source context 5 commands

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

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

Lean source · statement

def zeroSection (R : Type u) [CommRing R] :
    Spec (CommRingCat.of R) ⟶ ProjectiveLine R

theorem

standardChartEmbedding_X_zero_mem_iff

L55 ↗

ShimizuYamaguchi26BranchedCoverings.standardChartEmbedding_X_zero_mem_iff

Source context 5 commands

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

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

Lean source · statement

theorem standardChartEmbedding_X_zero_mem_iff
    (R : Type u) [CommRing R] (q : PrimeSpectrum (Polynomial R)) :
    MvPolynomial.X (0 : Fin 2) ∈ (standardChartEmbedding R q).asHomogeneousIdeal ↔
      Polynomial.X ∈ q.asIdeal

theorem

mem_range_affineZeroSection_iff

L72 ↗

ShimizuYamaguchi26BranchedCoverings.mem_range_affineZeroSection_iff

Source context 5 commands

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

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

Lean source · statement

theorem mem_range_affineZeroSection_iff
    (R : Type u) [CommRing R] (q : PrimeSpectrum (Polynomial R)) :
    q ∈ Set.range (Spec.map (CommRingCat.ofHom (Polynomial.evalRingHom (0 : R)))) ↔
      Polynomial.X ∈ q.asIdeal

theorem

range_zeroSection

L85 ↗

ShimizuYamaguchi26BranchedCoverings.range_zeroSection

Documentation

The image of the zero section is exactly its homogeneous linear zero locus.

Source context 5 commands

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

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

Lean source · statement

theorem range_zeroSection (R : Type u) [CommRing R] :
    Set.range (zeroSection R) =
      ProjectiveSpectrum.zeroLocus (MvPolynomial.homogeneousSubmodule (Fin 2) R)
        {linearSectionEquation (0 : R) 1}

Module documentation

The zero section of the projective line

Declarations

zeroSection

standardChartEmbedding_X_zero_mem_iff

mem_range_affineZeroSection_iff

range_zeroSection