NYLL
Module

FiniteSums.lean

Nyll.JacobianVarieties.Albanese.FiniteSums
16 declarations indexed from sourceView source ↗

Module documentation

Finite sums towards the Albanese construction

A morphism from a scheme to a relative group defines a sum morphism on every finite power of the source. Its action on test schemes is natural. Over an arbitrary field, properness and geometric integrality of the target imply permutation invariance: commutativity is deduced from the existing geometric theorem, not assumed. The list sum therefore descends to multisets of test-scheme points, naturally in the test scheme. This is a quotient of point families, not an assertion of a scheme quotient.

The construction does not require a rational point or algebraic closedness of the field. It does not yet assert invariance under linear equivalence or descent to a Jacobian.

Imports5
Imported by10

Declarations

def

sumList

L40 ↗
GoodReductionJacobian.RelativeGroupLaw.sumList
Documentation

Add an ordered finite list of relative points using the given group law.

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 GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)}
Lean source · statement
def sumList (G : RelativeGroupLaw R f) {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of R)) (xs : List (SchemeHomOver t f)) :
    SchemeHomOver t f
theorem

sumList_nil

L46 ↗
GoodReductionJacobian.RelativeGroupLaw.sumList_nil
Documentation

The sum of an empty list is the identity point.

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 GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem sumList_nil (G : RelativeGroupLaw R f) {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of R)) : G.sumList t [] = G.one t
theorem

sumList_cons

L51 ↗
GoodReductionJacobian.RelativeGroupLaw.sumList_cons
Documentation

Adding a head to a list multiplies its value by the sum of the tail.

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 GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem sumList_cons (G : RelativeGroupLaw R f) {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of R)) (x : SchemeHomOver t f)
    (xs : List (SchemeHomOver t f)) :
    G.sumList t (x :: xs) = G.mul t x (G.sumList t xs)
theorem

sumList_append

L58 ↗
GoodReductionJacobian.RelativeGroupLaw.sumList_append
Documentation

Concatenating two lists adds their sums.

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 GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem sumList_append (G : RelativeGroupLaw R f) {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of R)) (xs ys : List (SchemeHomOver t f)) :
    G.sumList t (xs ++ ys) = G.mul t (G.sumList t xs) (G.sumList t ys)
theorem

sumList_natural

L67 ↗
GoodReductionJacobian.RelativeGroupLaw.sumList_natural
Documentation

The finite sum commutes with pullback along a morphism of test schemes.

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 GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem sumList_natural (G : RelativeGroupLaw R f) {T T' : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of R)) (t' : T' ⟶ Spec (CommRingCat.of R))
    (ψ : T' ⟶ T) (hψ : ψ ≫ t = t') (xs : List (SchemeHomOver t f)) :
    GoodReductionJacobian.schemeHomOverComp ψ hψ (G.sumList t xs) =
      G.sumList t' (xs.map (GoodReductionJacobian.schemeHomOverComp ψ hψ))
def

sumFamily

L78 ↗
GoodReductionJacobian.RelativeGroupLaw.sumFamily
Documentation

The sum of a finite family of morphisms to the relative group, as an actual morphism.

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 GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)}
Lean source · statement
def sumFamily (G : RelativeGroupLaw R f) (T : Over (Spec (CommRingCat.of R)))
    {n : ℕ} (xs : Fin n → (T ⟶ Over.mk f)) : T ⟶ Over.mk f
theorem

sumFamily_natural

L84 ↗
GoodReductionJacobian.RelativeGroupLaw.sumFamily_natural
Documentation

The finite-family sum is natural in the test scheme.

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 GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)}
Lean source · full declaration
theorem sumFamily_natural (G : RelativeGroupLaw R f)
    {T T' : Over (Spec (CommRingCat.of R))} (ψ : T' ⟶ T)
    {n : ℕ} (xs : Fin n → (T ⟶ Over.mk f)) :
    ψ ≫ G.sumFamily T xs = G.sumFamily T' (fun i => ψ ≫ xs i) := by
  apply (overHomEquivSchemeHomOver T' f).injective
  change GoodReductionJacobian.schemeHomOverComp ψ.left (Over.w ψ)
    (G.sumList T.hom (List.ofFn fun i => overHomEquivSchemeHomOver T f (xs i))) =
      G.sumList T'.hom
        (List.ofFn fun i => overHomEquivSchemeHomOver T' f (ψ ≫ xs i))
  rw [G.sumList_natural, List.map_ofFn]
  rfl
def

finiteSumMap

L102 ↗
GoodReductionJacobian.RelativeGroupLaw.finiteSumMap
Documentation

Add the images of the coordinates on the existing finite fibre power of the source 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.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)}
section Field
variable {K : Type u} [Field K] {B : Scheme.{u}}
  {b : B ⟶ Spec (CommRingCat.of K)}
Lean source · statement
def finiteSumMap (G : RelativeGroupLaw K b) {C : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K)) (q : SchemeHomOver c b) (n : ℕ) :
    SchemeHomOver (finFibrePow.toBase c n) b
theorem

finiteSumMap_evaluate

L110 ↗
GoodReductionJacobian.RelativeGroupLaw.finiteSumMap_evaluate
Documentation

Evaluating the sum morphism at a family of points adds their images.

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.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)}
section Field
variable {K : Type u} [Field K] {B : Scheme.{u}}
  {b : B ⟶ Spec (CommRingCat.of K)}
Lean source · full declaration
theorem finiteSumMap_evaluate (G : RelativeGroupLaw K b) {C T : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K)) (q : SchemeHomOver c b) {n : ℕ}
    (t : T ⟶ Spec (CommRingCat.of K)) (xs : Fin n → SchemeHomOver t c) :
    GoodReductionJacobian.schemeHomOverComp
        (WidePullback.lift t (fun i => (xs i).1) (fun i => (xs i).2))
        (WidePullback.lift_base _ _ _ _) (G.finiteSumMap c q n) =
      G.sumList t (List.ofFn fun i => NeronModelInfra.schemeHomOverComp (xs i) q) := by
  rw [finiteSumMap, sumList_natural, List.map_ofFn]
  congr 1
  apply congrArg List.ofFn
  funext i
  apply Subtype.ext
  change WidePullback.lift t (fun j => (xs j).1) (fun j => (xs j).2) ≫
    (finFibrePow.proj c n i ≫ q.1) = (xs i).1 ≫ q.1
  exact WidePullback.lift_π_assoc _ _ _ _ _ _
theorem

sumList_perm

L129 ↗
GoodReductionJacobian.RelativeGroupLaw.sumList_perm
Documentation

Proper geometrically integral group targets make list sums invariant under permutation.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)}
section Field
variable {K : Type u} [Field K] {B : Scheme.{u}}
  {b : B ⟶ Spec (CommRingCat.of K)}
variable [IsProper b] [GeometricallyIntegral b]
Lean source · statement
theorem sumList_perm (G : RelativeGroupLaw K b) {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of K)) {xs ys : List (SchemeHomOver t b)}
    (h : xs.Perm ys) : G.sumList t xs = G.sumList t ys
theorem

sumFamily_perm

L142 ↗
GoodReductionJacobian.RelativeGroupLaw.sumFamily_perm
Documentation

A finite-family sum over an arbitrary field is unchanged by reindexing its coordinates.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)}
section Field
variable {K : Type u} [Field K] {B : Scheme.{u}}
  {b : B ⟶ Spec (CommRingCat.of K)}
variable [IsProper b] [GeometricallyIntegral b]
Lean source · statement
theorem sumFamily_perm (G : RelativeGroupLaw K b)
    (T : Over (Spec (CommRingCat.of K))) {n : ℕ}
    (xs : Fin n → (T ⟶ Over.mk b)) (σ : Equiv.Perm (Fin n)) :
    G.sumFamily T (xs ∘ σ) = G.sumFamily T xs
theorem

finiteSumMap_permute

L151 ↗
GoodReductionJacobian.RelativeGroupLaw.finiteSumMap_permute
Documentation

The actual sum morphism is invariant under the existing action on the finite fibre power.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)}
section Field
variable {K : Type u} [Field K] {B : Scheme.{u}}
  {b : B ⟶ Spec (CommRingCat.of K)}
variable [IsProper b] [GeometricallyIntegral b]
Lean source · statement
theorem finiteSumMap_permute (G : RelativeGroupLaw K b) {C : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K)) (q : SchemeHomOver c b) {n : ℕ}
    (σ : Equiv.Perm (Fin n)) :
    (finFibrePow.permAct c n σ).hom ≫ (G.finiteSumMap c q n).1 =
      (G.finiteSumMap c q n).1
def

sumMultiset

L182 ↗
GoodReductionJacobian.RelativeGroupLaw.sumMultiset
Documentation

Add an unordered finite family of test-scheme points. The value is independent of the representing list by geometric commutativity.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)}
section Field
variable {K : Type u} [Field K] {B : Scheme.{u}}
  {b : B ⟶ Spec (CommRingCat.of K)}
variable [IsProper b] [GeometricallyIntegral b]
Lean source · statement
def sumMultiset (G : RelativeGroupLaw K b) {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of K)) (xs : Multiset (SchemeHomOver t b)) :
    SchemeHomOver t b
theorem

sumMultiset_coe

L188 ↗
GoodReductionJacobian.RelativeGroupLaw.sumMultiset_coe
Documentation

The sum of a list represents its unordered sum.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)}
section Field
variable {K : Type u} [Field K] {B : Scheme.{u}}
  {b : B ⟶ Spec (CommRingCat.of K)}
variable [IsProper b] [GeometricallyIntegral b]
Lean source · statement
theorem sumMultiset_coe (G : RelativeGroupLaw K b) {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of K)) (xs : List (SchemeHomOver t b)) :
    G.sumMultiset t (xs : Multiset (SchemeHomOver t b)) = G.sumList t xs
theorem

sumMultiset_natural

L194 ↗
GoodReductionJacobian.RelativeGroupLaw.sumMultiset_natural
Documentation

Pulling an unordered family back to another test scheme commutes with its sum.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)}
section Field
variable {K : Type u} [Field K] {B : Scheme.{u}}
  {b : B ⟶ Spec (CommRingCat.of K)}
variable [IsProper b] [GeometricallyIntegral b]
Lean source · statement
theorem sumMultiset_natural (G : RelativeGroupLaw K b) {T T' : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of K)) (t' : T' ⟶ Spec (CommRingCat.of K))
    (ψ : T' ⟶ T) (hψ : ψ ≫ t = t') (xs : Multiset (SchemeHomOver t b)) :
    GoodReductionJacobian.schemeHomOverComp ψ hψ (G.sumMultiset t xs) =
      G.sumMultiset t' (xs.map (GoodReductionJacobian.schemeHomOverComp ψ hψ))
theorem

sumMultiset_add

L204 ↗
GoodReductionJacobian.RelativeGroupLaw.sumMultiset_add
Documentation

Union of unordered families adds their sums.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian.RelativeGroupLaw
variable {R : Type u} [CommRing R] {A : Scheme.{u}}
  {f : A ⟶ Spec (CommRingCat.of R)}
section Field
variable {K : Type u} [Field K] {B : Scheme.{u}}
  {b : B ⟶ Spec (CommRingCat.of K)}
variable [IsProper b] [GeometricallyIntegral b]
Lean source · statement
theorem sumMultiset_add (G : RelativeGroupLaw K b) {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of K)) (xs ys : Multiset (SchemeHomOver t b)) :
    G.sumMultiset t (xs + ys) = G.mul t (G.sumMultiset t xs) (G.sumMultiset t ys)

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