Module

RationalSectionSupport.lean

Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.RationalSectionSupport

2 declarations indexed from sourceView source ↗

Module documentation

Homogeneous supports of rational sections

The support is the actual homogeneous zero locus of the primitive equation v*T₀-u*T₁ in the integral projective line. Pulling it back along the coefficient morphism computes the same equation over the new coefficient ring. This supplies one common geometric definition for Lemmas 2.3 and 2.4 of Shimizu and Yamaguchi, On branched coverings of the projective line over the integers.

Imports10

Nyll.ShimizuYamaguchi26BranchedCoverings.Arithmetic.RationalProjectiveCoordinates
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.StandardAffineChart
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.TwoSectionComplement
Nyll.SchemeTheory.ProjectiveSpace.Basic
Mathlib.Algebra.MvPolynomial.Eval
Mathlib.Data.Int.Cast.Lemmas
Mathlib.Data.Set.Insert
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Mathlib.LinearAlgebra.Projectivization.Basic

Imported by6

def

rationalSectionSupport

L39 ↗

ShimizuYamaguchi26BranchedCoverings.rationalSectionSupport

Documentation

The support of the integral section with the given rational projective point, as the zero locus of its primitive homogeneous equation.

Source context 4 commands

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

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

Lean source · statement

def rationalSectionSupport (a : Projectivization ℚ (ℚ × ℚ)) :
    Set (ProjectiveLine ℤ)

theorem

mem_rationalSectionSupport_baseChange_iff

L46 ↗

ShimizuYamaguchi26BranchedCoverings.mem_rationalSectionSupport_baseChange_iff