NYLL
Module

ProjectiveLineConstancy.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.ProjectiveLineConstancy
6 declarations indexed from sourceView source ↗

Module documentation

Morphisms from the projective line to an abelian variety are constant

Each standard chart is the actual affine line. Their constant values agree at the common rational point with homogeneous coordinates (1,1).

Imports7
Imported by1

Declarations

abbrev

otherUnique

L38 ↗
GoodReductionJacobian.ProjectiveLineConstancy.otherUnique
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry HomogeneousLocalization Polynomial
open AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace
  (awayChartEquiv awayChartEquiv_X)
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GoodReductionJacobian
namespace ProjectiveLineConstancy
variable (k : Type u) [Field k]
Lean source · full declaration
abbrev otherUnique (i : Fin 2) : Unique {j : Fin 2 // j ≠ i} where
  default := ⟨⟨1 - i.val, by omega⟩, by
    intro h
    have h' := congrArg Fin.val h
    change 1 - i.val = i.val at h'
    have hi := i.isLt
    omega⟩
  uniq j := by
    apply Subtype.ext
    apply Fin.ext
    have hi := i.isLt
    have hj := j.val.isLt
    have hne : j.val.val ≠ i.val := fun h => j.property (Fin.ext h)
    change j.val.val = 1 - i.val
    omega
def

chartEquiv

L54 ↗
GoodReductionJacobian.ProjectiveLineConstancy.chartEquiv
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry HomogeneousLocalization Polynomial
open AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace
  (awayChartEquiv awayChartEquiv_X)
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GoodReductionJacobian
namespace ProjectiveLineConstancy
variable (k : Type u) [Field k]
Lean source · statement
def chartEquiv (i : Fin 2) :
    k[X] ≃ₐ[k] Away (MvPolynomial.homogeneousSubmodule (Fin 2) k) (MvPolynomial.X i)
def

ones

L60 ↗
GoodReductionJacobian.ProjectiveLineConstancy.ones
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry HomogeneousLocalization Polynomial
open AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace
  (awayChartEquiv awayChartEquiv_X)
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GoodReductionJacobian
namespace ProjectiveLineConstancy
variable (k : Type u) [Field k]
Lean source · statement
def ones (i : Fin 2) :
    Away (MvPolynomial.homogeneousSubmodule (Fin 2) k) (MvPolynomial.X i) →ₐ[k] k
lemma

ones_ratio

L65 ↗
GoodReductionJacobian.ProjectiveLineConstancy.ones_ratio
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry HomogeneousLocalization Polynomial
open AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace
  (awayChartEquiv awayChartEquiv_X)
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GoodReductionJacobian
namespace ProjectiveLineConstancy
variable (k : Type u) [Field k]
Lean source · statement
lemma ones_ratio (i j : Fin 2) : ones k i (ProjSpace.ratio k 1 i j) = 1
lemma

ones_chart_eq

L74 ↗
GoodReductionJacobian.ProjectiveLineConstancy.ones_chart_eq
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry HomogeneousLocalization Polynomial
open AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace
  (awayChartEquiv awayChartEquiv_X)
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GoodReductionJacobian
namespace ProjectiveLineConstancy
variable (k : Type u) [Field k]
Lean source · statement
lemma ones_chart_eq (i j : Fin 2) :
    Spec.map (CommRingCat.ofHom (ones k i).toRingHom) ≫
      Proj.awayι (MvPolynomial.homogeneousSubmodule (Fin 2) k) (MvPolynomial.X i)
        (ProjSpace.X_mem_one k 1 i) one_pos =
    Spec.map (CommRingCat.ofHom (ones k j).toRingHom) ≫
      Proj.awayι (MvPolynomial.homogeneousSubmodule (Fin 2) k) (MvPolynomial.X j)
        (ProjSpace.X_mem_one k 1 j) one_pos
theorem

exists_eq_const_of_projectiveLine

L89 ↗
GoodReductionJacobian.exists_eq_const_of_projectiveLine
Documentation

Every morphism over a field from the projective line to an abelian variety is constant.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry HomogeneousLocalization Polynomial
open AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace
  (awayChartEquiv awayChartEquiv_X)
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GoodReductionJacobian
open ProjectiveLineConstancy in
Lean source · statement
theorem exists_eq_const_of_projectiveLine
    (k : Type u) [Field k] {A : Scheme.{u}} {fA : A ⟶ Spec (CommRingCat.of k)}
    (hA : AbelianSchemePropertyBundle k fA)
    (q : Proj (MvPolynomial.homogeneousSubmodule (Fin 2) k) ⟶ A)
    (hq : q ≫ fA = ProjSpace.π k 1) :
    ∃ a : Spec (CommRingCat.of k) ⟶ A,
      a ≫ fA = 𝟙 _ ∧ q = ProjSpace.π k 1 ≫ a

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