NYLL
Module

FieldSectionPointUniqueness.lean

Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.FieldSectionPointUniqueness
9 declarations indexed from sourceView source ↗

Module documentation

The unique closed point of a homogeneous linear equation over a field

The equation v*T₀-u*T₁ for a nonzero pair (u,v) has exactly the point constructed by homogeneous evaluation as its zero locus in the actual projective scheme. If v is nonzero, relevance forces the zero locus into the standard affine chart, where the equation generates the maximal ideal of evaluation at u/v. A coordinate exchange treats the point at infinity. The singleton is closed because it is this projective zero locus.

This proves the field-fibre uniqueness underlying the first assertion of Lemma 2.3 of Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers.

Imports20
Imported by2

Declarations

theorem

coordinate_mem_of_scaled_mem

L55 ↗
ShimizuYamaguchi26BranchedCoverings.coordinate_mem_of_scaled_mem
Source context 6 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
variable {k : Type u} [Field k]
Lean source · statement
theorem coordinate_mem_of_scaled_mem (x : ProjectiveLine k)
    (c : k) (hc : c ≠ 0) (i : Fin 2)
    (h : MvPolynomial.C c * MvPolynomial.X i ∈ x.asHomogeneousIdeal) :
    MvPolynomial.X i ∈ x.asHomogeneousIdeal
theorem

linearSection_mem_infinityComplement

L63 ↗
ShimizuYamaguchi26BranchedCoverings.linearSection_mem_infinityComplement
Source context 6 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
variable {k : Type u} [Field k]
Lean source · statement
theorem linearSection_mem_infinityComplement (u v : k) (hv : v ≠ 0)
    (x : ProjectiveLine k) (h : linearSectionEquation u v ∈ x.asHomogeneousIdeal) :
    x ∈ infinityComplement k
theorem

affinePrime_eq_evalKer

L76 ↗
ShimizuYamaguchi26BranchedCoverings.affinePrime_eq_evalKer
Source context 6 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
variable {k : Type u} [Field k]
Lean source · statement
theorem affinePrime_eq_evalKer (u v : k) (hv : v ≠ 0)
    (q : PrimeSpectrum (Polynomial k))
    (hq : Polynomial.C v * Polynomial.X - Polynomial.C u ∈ q.asIdeal) :
    q.asIdeal = RingHom.ker (Polynomial.evalRingHom (u / v))
theorem

affineLinear_mem_of_section_mem

L95 ↗
ShimizuYamaguchi26BranchedCoverings.affineLinear_mem_of_section_mem
Source context 6 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
variable {k : Type u} [Field k]
Lean source · statement
theorem affineLinear_mem_of_section_mem (u v : k)
    (q : PrimeSpectrum (Polynomial k))
    (h : linearSectionEquation u v ∈
      (standardChartEmbedding k q).asHomogeneousIdeal) :
    Polynomial.C v * Polynomial.X - Polynomial.C u ∈ q.asIdeal
theorem

eq_of_linearSection_mem_of_snd_ne_zero

L111 ↗
ShimizuYamaguchi26BranchedCoverings.eq_of_linearSection_mem_of_snd_ne_zero
Source context 6 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
variable {k : Type u} [Field k]
Lean source · statement
theorem eq_of_linearSection_mem_of_snd_ne_zero
    (u v : k) (hv : v ≠ 0) (x y : ProjectiveLine k)
    (hx : linearSectionEquation u v ∈ x.asHomogeneousIdeal)
    (hy : linearSectionEquation u v ∈ y.asHomogeneousIdeal) : x = y
theorem

eq_of_linearSection_mem

L132 ↗
ShimizuYamaguchi26BranchedCoverings.eq_of_linearSection_mem
Source context 6 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
variable {k : Type u} [Field k]
Lean source · statement
theorem eq_of_linearSection_mem
    (u v : k) (huv : u ≠ 0 ∨ v ≠ 0) (x y : ProjectiveLine k)
    (hx : linearSectionEquation u v ∈ x.asHomogeneousIdeal)
    (hy : linearSectionEquation u v ∈ y.asHomogeneousIdeal) : x = y
theorem

eq_fieldSectionPoint_of_linearSection_mem

L163 ↗
ShimizuYamaguchi26BranchedCoverings.eq_fieldSectionPoint_of_linearSection_mem
Documentation

A point of the projective line containing the nonzero homogeneous linear equation is the point constructed by evaluation at its coordinates.

Source context 6 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
variable {k : Type u} [Field k]
Lean source · statement
theorem eq_fieldSectionPoint_of_linearSection_mem
    (u v : k) (huv : u ≠ 0 ∨ v ≠ 0) (x : ProjectiveLine k)
    (h : linearSectionEquation u v ∈ x.asHomogeneousIdeal) :
    x = fieldSectionPoint u v huv
theorem

zeroLocus_linearSectionEquation_eq_singleton

L171 ↗
ShimizuYamaguchi26BranchedCoverings.zeroLocus_linearSectionEquation_eq_singleton
Documentation

The zero locus of a nonzero homogeneous linear equation is exactly its rational point.

Source context 6 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
variable {k : Type u} [Field k]
Lean source · statement
theorem zeroLocus_linearSectionEquation_eq_singleton
    (u v : k) (huv : u ≠ 0 ∨ v ≠ 0) :
    ProjectiveSpectrum.zeroLocus (MvPolynomial.homogeneousSubmodule (Fin 2) k)
      {linearSectionEquation u v} = {fieldSectionPoint u v huv}
theorem

isClosed_singleton_fieldSectionPoint

L188 ↗
ShimizuYamaguchi26BranchedCoverings.isClosed_singleton_fieldSectionPoint
Documentation

The actual projective-scheme point supplied by a nonzero field-valued pair is closed.

Source context 6 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
variable {k : Type u} [Field k]
Lean source · statement
theorem isClosed_singleton_fieldSectionPoint (u v : k) (huv : u ≠ 0 ∨ v ≠ 0) :
    IsClosed ({fieldSectionPoint u v huv} : Set (ProjectiveLine k))

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