Module

UnpointedGroup.lean

Nyll.JacobianVarieties.Picard.UnpointedGroup

2 declarations indexed from sourceView source ↗

Module documentation

The group law on an unpointed Picard descent

The group law comes from the actual tensor-product group of unrigidified classes, using the proved equivalence between descended scheme points and matching local classes. No group law or comparison is assumed on the descended carrier.

Imports4

Nyll.JacobianVarieties.Picard.UnpointedDescent
Nyll.AlgebraicCurves.Geometry.Picard.UnrigidifiedGroup
Nyll.AlgebraicCurves.Geometry.Descent.GroupOfMatching
Mathlib.AlgebraicGeometry.Sites.Fpqc

Imported by2

def

groupLawOfPicardDescent

L41 ↗

JacobianVarieties.Picard.Unpointed.groupLawOfPicardDescent

Documentation

The actual relative group law on the same descended Picard carrier.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
open AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {K : Type u} [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
  (L : Type u) [Field L] [Algebra K L]
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of L))) (baseChange K c L))
  {D : RelativePic0Designation L (baseChange K c L)}
  (h : RepresentsRelSubPic (baseChange K c L) ε (algEquivZeroCut (baseChange K c L) ε) D)
  {P : Scheme.{u}} (p : P ⟶ Spec (CommRingCat.of K))
  (e : pullback p (specMap K L) ≅ D.P)
  (he : e.hom ≫ D.toBase = pullback.snd p (specMap K L))
  (hc : DescentAction.eRel (specMap K L) D.toBase p e he ≫ (descentAction c L ε h).act =
    (DescentAction.canonical (specMap K L) p).act ≫ e.hom)

Lean source · statement

def groupLawOfPicardDescent : RelativeGroupLaw K p

theorem

groupLawOfPicardDescent_commutative

L45 ↗

JacobianVarieties.Picard.Unpointed.groupLawOfPicardDescent_commutative