Module

EndDegree.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.GroupLaw.EndDegree

17 declarations indexed from sourceView source ↗

Module documentation

End Degree

Imports4

Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Nyll.AlgebraicCurves.Geometry.Picard.RelativeGroupLaw
Nyll.AlgebraicCurves.Geometry.AbelianSchemes.GroupLaw.Kernel
Nyll.AlgebraicCurves.Geometry.Schemes.SchemeHomOver

Imported by16

def

schemeHomOverNpow

L33 ↗

NeronModelInfra.schemeHomOverNpow

Documentation

The iterated composition of a scheme endomorphism over its base.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace NeronModelInfra
variable {B X : Scheme.{u}} {f : X ⟶ B}

Lean source · full declaration

def schemeHomOverNpow (β : SchemeHomOver f f) : ℕ → SchemeHomOver f f
  | 0 => schemeHomOverId f
  | i + 1 => schemeHomOverComp (schemeHomOverNpow β i) β

theorem

schemeHomOverNpow_zero

L37 ↗

NeronModelInfra.schemeHomOverNpow_zero

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace NeronModelInfra
variable {B X : Scheme.{u}} {f : X ⟶ B}

Lean source · statement

theorem schemeHomOverNpow_zero (β : SchemeHomOver f f) :
    schemeHomOverNpow β 0 = schemeHomOverId f

theorem

schemeHomOverNpow_succ

L40 ↗

NeronModelInfra.schemeHomOverNpow_succ

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace NeronModelInfra
variable {B X : Scheme.{u}} {f : X ⟶ B}

Lean source · statement

theorem schemeHomOverNpow_succ (β : SchemeHomOver f f) (i : ℕ) :
    schemeHomOverNpow β (i + 1) = schemeHomOverComp (schemeHomOverNpow β i) β

def

pointCommGroup

L54 ↗

GoodReductionJacobian.RelativeGroupLaw.pointCommGroup

Documentation

The commutative group structure on points supplied by the relative group law.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section General
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}

Lean source · statement

def pointCommGroup (G : RelativeGroupLaw R f) (hc : G.IsCommutative) {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of R)) : CommGroup (SchemeHomOver t f)

def

endAeval

L59 ↗

GoodReductionJacobian.RelativeGroupLaw.endAeval

Documentation

Evaluation of an integral polynomial at an endomorphism using the point group law.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section General
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}

Lean source · statement

def endAeval (G : RelativeGroupLaw R f) (hc : G.IsCommutative) (β : SchemeHomOver f f)
    (p : Polynomial ℤ) : SchemeHomOver f f

theorem

endAeval_X

L64 ↗

GoodReductionJacobian.RelativeGroupLaw.endAeval_X

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section General
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}

Lean source · statement

theorem endAeval_X (G : RelativeGroupLaw R f) (hc : G.IsCommutative) (β : SchemeHomOver f f) :
    G.endAeval hc β Polynomial.X = β

abbrev

endKer

L74 ↗

GoodReductionJacobian.RelativeGroupLaw.endKer

Documentation

The scheme theoretic kernel of an endomorphism for the relative group law.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section General
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}

Lean source · statement

abbrev endKer (G : RelativeGroupLaw R f) (β : SchemeHomOver f f) : Scheme.{u}

abbrev

endKerStr

L78 ↗

GoodReductionJacobian.RelativeGroupLaw.endKerStr

Documentation

The structure morphism of the endomorphism kernel to the base spectrum.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section General
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}

Lean source · statement

abbrev endKerStr (G : RelativeGroupLaw R f) (β : SchemeHomOver f f) :
    G.endKer β ⟶ Spec (CommRingCat.of R)

abbrev

endKerι

L83 ↗

GoodReductionJacobian.RelativeGroupLaw.endKerι

Documentation

The canonical inclusion of the endomorphism kernel into the group scheme.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section General
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}

Lean source · statement

abbrev endKerι (G : RelativeGroupLaw R f) (β : SchemeHomOver f f) : G.endKer β ⟶ A

theorem

endKer_nsmul_idPoint

L86 ↗

GoodReductionJacobian.RelativeGroupLaw.endKer_nsmul_idPoint

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section General
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}

Lean source · statement

theorem endKer_nsmul_idPoint (G : RelativeGroupLaw R f) (n : ℕ) :
    G.endKer (G.nsmul f n idPoint) = G.schemeKer n

theorem

endKerι_comp

L90 ↗

GoodReductionJacobian.RelativeGroupLaw.endKerι_comp

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section General
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}

Lean source · statement

theorem endKerι_comp (G : RelativeGroupLaw R f) (β : SchemeHomOver f f) :
    G.endKerι β ≫ β.1 = G.endKerStr β ≫ (G.one (𝟙 (Spec (CommRingCat.of R)))).1

theorem

endKerι_comp_base

L94 ↗

GoodReductionJacobian.RelativeGroupLaw.endKerι_comp_base

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section General
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}

Lean source · statement

theorem endKerι_comp_base (G : RelativeGroupLaw R f) (β : SchemeHomOver f f) :
    G.endKerι β ≫ f = G.endKerStr β

def

endDegree

L108 ↗

GoodReductionJacobian.RelativeGroupLaw.endDegree

Documentation

The finite rank of the endomorphism kernel, with value zero when it is not finite.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section Field
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}

Lean source · statement

def endDegree (G : RelativeGroupLaw K f) (β : SchemeHomOver f f) : ℕ

theorem

endDegree_of_isFinite

L112 ↗

GoodReductionJacobian.RelativeGroupLaw.endDegree_of_isFinite

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section Field
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}

Lean source · statement

theorem endDegree_of_isFinite (G : RelativeGroupLaw K f) (β : SchemeHomOver f f)
    [h : IsFinite (G.endKerStr β)] :
    G.endDegree β = (G.endKerStr β).finrank (IsLocalRing.closedPoint K)

theorem

endDegree_of_not_isFinite

L117 ↗

GoodReductionJacobian.RelativeGroupLaw.endDegree_of_not_isFinite

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section Field
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}

Lean source · statement

theorem endDegree_of_not_isFinite (G : RelativeGroupLaw K f) (β : SchemeHomOver f f)
    (h : ¬ IsFinite (G.endKerStr β)) : G.endDegree β = 0

instance

isIso_endKerStr_schemeHomOverId

L121 ↗

GoodReductionJacobian.RelativeGroupLaw.isIso_endKerStr_schemeHomOverId

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section Field
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}

Lean source · statement

instance isIso_endKerStr_schemeHomOverId (G : RelativeGroupLaw K f) :
    IsIso (G.endKerStr (schemeHomOverId f))

theorem

endDegree_schemeHomOverId

L126 ↗

GoodReductionJacobian.RelativeGroupLaw.endDegree_schemeHomOverId

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
namespace RelativeGroupLaw
section Field
variable {K : Type u} [Field K] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of K)}

Lean source · statement

theorem endDegree_schemeHomOverId (G : RelativeGroupLaw K f) :
    G.endDegree (schemeHomOverId f) = 1

Module documentation

End Degree

Declarations