Module

PointedFiniteSums.lean

Nyll.JacobianVarieties.Albanese.PointedFiniteSums

2 declarations indexed from sourceView source ↗

Module documentation

Stabilization of pointed finite sums

Adjoining the rational basepoint defines an actual morphism between successive finite fibre powers. A morphism sending that basepoint to the identity has the same finite sum before and after this insertion. This works over any field and needs no commutativity.

This is degree stabilization, not invariance under principal divisors. It asserts neither an arbitrary-target Albanese factorization nor the existence of a symmetric-power quotient.

Imports7

Nyll.JacobianVarieties.Albanese.FiniteSums
Nyll.AlgebraicCurves.Geometry.Schemes.SchemeHomOver
Nyll.AlgebraicCurves.Geometry.Picard.RelativeGroupLaw
Nyll.AlgebraicCurves.Hilbert.SymmetricPowerData
Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Mathlib.Data.Fin.Tuple.Basic
Mathlib.Data.List.OfFn

Imported by1

Nyll.JacobianVarieties.Albanese.All

def

insertBasepoint

L36 ↗

AlgebraicGeometry.finFibrePow.insertBasepoint

Documentation

Adjoin the given rational basepoint as the first coordinate of a finite fibre power.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace AlgebraicGeometry.finFibrePow

Lean source · statement

def insertBasepoint {K : Type u} [Field K] {C : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K))
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c) (n : ℕ) :
    SchemeHomOver (toBase c n) (toBase c (n + 1))

theorem

finiteSumMap_insertBasepoint

L53 ↗

GoodReductionJacobian.RelativeGroupLaw.finiteSumMap_insertBasepoint