NYLL
Module

FieldSectionPoint.lean

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

Module documentation

The projective point of a nonzero coordinate pair over a field

The homogeneous core of the kernel of evaluation at (u,v) is a homogeneous prime ideal. A nonzero coordinate prevents this ideal from containing the irrelevant ideal, so it defines a point of the actual projective scheme. Membership of a homogeneous polynomial is exactly vanishing at (u,v). In particular, the equation t*T₀-s*T₁ vanishes at this point if and only if t*u-s*v = 0.

This constructs the points used in the first assertion of Lemma 2.3 of Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers. The uniqueness, closedness, and intersection-length comparisons are separate results.

Imports12
Imported by6

Declarations

theorem

projectiveLine_not_both_coordinates_mem

L47 ↗
ShimizuYamaguchi26BranchedCoverings.projectiveLine_not_both_coordinates_mem
Documentation

Both homogeneous coordinates cannot belong to a projective point's ideal.

Source context 5 commands

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

noncomputable section
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R]
Lean source · statement
theorem projectiveLine_not_both_coordinates_mem (x : ProjectiveLine R)
    (hzero : MvPolynomial.X (0 : Fin 2) ∈ x.asHomogeneousIdeal)
    (hone : MvPolynomial.X (1 : Fin 2) ∈ x.asHomogeneousIdeal) : False
def

fieldSectionEvaluation

L63 ↗
ShimizuYamaguchi26BranchedCoverings.fieldSectionEvaluation
Documentation

Evaluation at the ordered pair of homogeneous coordinates (u,v).

Source context 6 commands

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

noncomputable section
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R]
variable {k : Type u} [Field k]
Lean source · statement
def fieldSectionEvaluation (u v : k) : MvPolynomial (Fin 2) k →+* k
theorem

fieldSectionEvaluation_X_zero

L67 ↗
ShimizuYamaguchi26BranchedCoverings.fieldSectionEvaluation_X_zero
Documentation

Evaluation of the first homogeneous coordinate.

Source context 6 commands

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

noncomputable section
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R]
variable {k : Type u} [Field k]
Lean source · statement
theorem fieldSectionEvaluation_X_zero (u v : k) :
    fieldSectionEvaluation u v (MvPolynomial.X 0) = u
theorem

fieldSectionEvaluation_X_one

L73 ↗
ShimizuYamaguchi26BranchedCoverings.fieldSectionEvaluation_X_one
Documentation

Evaluation of the second homogeneous coordinate.

Source context 6 commands

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

noncomputable section
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R]
variable {k : Type u} [Field k]
Lean source · statement
theorem fieldSectionEvaluation_X_one (u v : k) :
    fieldSectionEvaluation u v (MvPolynomial.X 1) = v
theorem

fieldSectionEvaluation_linearSectionEquation

L79 ↗
ShimizuYamaguchi26BranchedCoverings.fieldSectionEvaluation_linearSectionEquation
Documentation

Evaluation of a homogeneous linear section equation.

Source context 6 commands

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

noncomputable section
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R]
variable {k : Type u} [Field k]
Lean source · statement
theorem fieldSectionEvaluation_linearSectionEquation (u v s t : k) :
    fieldSectionEvaluation u v (linearSectionEquation s t) = t * u - s * v
def

fieldSectionPoint

L87 ↗
ShimizuYamaguchi26BranchedCoverings.fieldSectionPoint
Documentation

The actual projective-scheme point determined by a nonzero coordinate pair. Its homogeneous ideal is the homogeneous core of the evaluation kernel.

Source context 6 commands

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

noncomputable section
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R]
variable {k : Type u} [Field k]
Lean source · full declaration
def fieldSectionPoint (u v : k) (huv : u ≠ 0 ∨ v ≠ 0) : ProjectiveLine k where
  asHomogeneousIdeal :=
    (RingHom.ker (fieldSectionEvaluation u v)).homogeneousCore
      (MvPolynomial.homogeneousSubmodule (Fin 2) k)
  isPrime := (RingHom.ker_isPrime (fieldSectionEvaluation u v)).homogeneousCore
  not_irrelevant_le := by
    intro hle
    have hcoordinates : ∀ i : Fin 2, fieldSectionEvaluation u v (MvPolynomial.X i) = 0 := by
      intro i
      have hmem : MvPolynomial.X i ∈ RingHom.ker (fieldSectionEvaluation u v) :=
        Ideal.toIdeal_homogeneousCore_le
          (MvPolynomial.homogeneousSubmodule (Fin 2) k)
          (RingHom.ker (fieldSectionEvaluation u v))
          (hle (HomogeneousIdeal.mem_irrelevant_of_mem _ one_pos
            (AlgebraicGeometry.ProjSpace.X_mem_one k 1 i)))
      exact RingHom.mem_ker.mp hmem
    rcases huv with hu | hv
    · exact hu ((fieldSectionEvaluation_X_zero u v).symm.trans (hcoordinates 0))
    · exact hv ((fieldSectionEvaluation_X_one u v).symm.trans (hcoordinates 1))
theorem

homogeneous_mem_fieldSectionPoint_iff

L109 ↗
ShimizuYamaguchi26BranchedCoverings.homogeneous_mem_fieldSectionPoint_iff
Documentation

A homogeneous polynomial belongs to the constructed point exactly when its evaluation at the original coordinates is zero.

Source context 6 commands

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

noncomputable section
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R]
variable {k : Type u} [Field k]
Lean source · statement
theorem homogeneous_mem_fieldSectionPoint_iff
    (u v : k) (huv : u ≠ 0 ∨ v ≠ 0)
    (f : MvPolynomial (Fin 2) k) {n : ℕ}
    (hf : f ∈ MvPolynomial.homogeneousSubmodule (Fin 2) k n) :
    f ∈ (fieldSectionPoint u v huv).asHomogeneousIdeal ↔
      fieldSectionEvaluation u v f = 0
theorem

linearSectionEquation_mem_fieldSectionPoint_iff

L130 ↗
ShimizuYamaguchi26BranchedCoverings.linearSectionEquation_mem_fieldSectionPoint_iff
Documentation

The linear equation of (s,t) contains the constructed point of (u,v) exactly when their coordinate determinant vanishes.

Source context 6 commands

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

noncomputable section
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R]
variable {k : Type u} [Field k]
Lean source · statement
theorem linearSectionEquation_mem_fieldSectionPoint_iff
    (u v s t : k) (huv : u ≠ 0 ∨ v ≠ 0) :
    linearSectionEquation s t ∈ (fieldSectionPoint u v huv).asHomogeneousIdeal ↔
      t * u - s * v = 0
theorem

linearSectionEquation_mem_fieldSectionPoint

L139 ↗
ShimizuYamaguchi26BranchedCoverings.linearSectionEquation_mem_fieldSectionPoint
Documentation

The constructed point lies on its own homogeneous section equation.

Source context 6 commands

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

noncomputable section
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
variable {R : Type u} [CommRing R]
variable {k : Type u} [Field k]
Lean source · statement
theorem linearSectionEquation_mem_fieldSectionPoint
    (u v : k) (huv : u ≠ 0 ∨ v ≠ 0) :
    linearSectionEquation u v ∈ (fieldSectionPoint u v huv).asHomogeneousIdeal

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