NYLL
Module

Designation.lean

Nyll.JacobianVarieties.Picard.Designation
4 declarations indexed from sourceView source ↗

Module documentation

Pointed carriers for the relative Picard construction

A relative Picard designation records a scheme over the base with a chosen zero section. The avatar bridge identifies an additive group with its points over a test scheme and records compatibility with the relative group law.

Imports4
Imported by25

Declarations

structure

RelativePic0Designation

L40 ↗
GoodReductionJacobian.RelativePic0Designation
Documentation

A chosen scheme over the base, equipped with a zero section.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section AbstractCarriers
variable (R : Type u) [CommRing R]
Lean source · full declaration
structure RelativePic0Designation {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) where
  /-- The scheme designated as the relative Picard carrier. -/
  P : Scheme.{u}
  /-- The structure morphism to the base scheme. -/
  toBase : P ⟶ Spec (CommRingCat.of R)
  /-- The chosen zero section of the structure morphism. -/
  zeroSection : Spec (CommRingCat.of R) ⟶ P
  /-- The zero section is a section of `toBase`. -/
  zeroSection_toBase : zeroSection ≫ toBase = 𝟙 (Spec (CommRingCat.of R))
def

trivialPic0Designation

L51 ↗
GoodReductionJacobian.trivialPic0Designation
Documentation

The designation whose carrier is the base itself and whose maps are identities.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section AbstractCarriers
variable (R : Type u) [CommRing R]
Lean source · full declaration
def trivialPic0Designation {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) :
    RelativePic0Designation R c where
  P := Spec (CommRingCat.of R)
  toBase := 𝟙 _
  zeroSection := 𝟙 _
  zeroSection_toBase := Category.comp_id _
structure

AvatarSchemeBridge

L66 ↗
GoodReductionJacobian.AvatarSchemeBridge
Documentation

An identification of an additive group with scheme points compatible with the group law.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section AvatarBridge
variable {R : Type u} [CommRing R]
variable {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
Lean source · full declaration
structure AvatarSchemeBridge (A : Type*) [AddCommGroup A]
    (D : RelativePic0Designation R c) (L : RelativeGroupLaw R D.toBase)
    {T : Scheme.{u}} (σ : T ⟶ Spec (CommRingCat.of R)) where
  /-- The equivalence from the additive group to points over the test scheme. -/
  pts : A ≃ SchemeHomOver σ D.toBase
  /-- Addition of avatar elements corresponds to multiplication in the relative group law. -/
  pts_add : ∀ x y : A, pts (x + y) = L.mul σ (pts x) (pts y)
  /-- The zero avatar point is induced by the designated zero section. -/
  pts_zero : (pts 0).1 = σ ≫ D.zeroSection
theorem

law_one_eq_pts_zero

L82 ↗
GoodReductionJacobian.AvatarSchemeBridge.law_one_eq_pts_zero
Source context 11 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section AvatarBridge
variable {R : Type u} [CommRing R]
variable {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
namespace AvatarSchemeBridge
variable {A : Type*} [AddCommGroup A]
variable {D : RelativePic0Designation R c} {L : RelativeGroupLaw R D.toBase}
variable {T : Scheme.{u}} {σ : T ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem law_one_eq_pts_zero (B : AvatarSchemeBridge A D L σ) :
    L.one σ = B.pts 0

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