Module

PolarisationRosati.lean

Nyll.AlgebraicCurves.Geometry.Picard.PolarisationRosati

12 declarations indexed from sourceView source ↗

Module documentation

Polarisation Rosati

Imports2

Imported by26

def

idPt

L33 ↗

AlgebraicGeometry.Polarisation.idPt

Documentation

The identity morphism regarded as a point of the scheme over its base.

Source context 5 commands

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

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

Lean source · statement

def idPt : SchemeHomOver f f

def

negMor

L36 ↗

AlgebraicGeometry.Polarisation.negMor

Documentation

The scheme morphism implementing inversion in the relative group law.

Source context 5 commands

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

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

Lean source · statement

def negMor : A ⟶ A

theorem

negMor_over

L38 ↗

AlgebraicGeometry.Polarisation.negMor_over

Source context 5 commands

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

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

Lean source · statement

theorem negMor_over : negMor f L ≫ f = f

def

addMor

L41 ↗

AlgebraicGeometry.Polarisation.addMor

Documentation

The scheme morphism implementing multiplication in the relative group law.

Source context 5 commands

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

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

Lean source · statement

def addMor : pullback f f ⟶ A

theorem

addMor_over

L45 ↗

AlgebraicGeometry.Polarisation.addMor_over

Source context 5 commands

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

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

Lean source · statement

theorem addMor_over : addMor f L ≫ f = pullback.fst f f ≫ f

def

LocIsoOnBase

L50 ↗

AlgebraicGeometry.Polarisation.LocIsoOnBase

Documentation

The module sheaves become isomorphic locally on the base spectrum.

Source context 5 commands

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

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

Lean source · statement

def LocIsoOnBase {S' : Type u} [CommRing S'] {X : Scheme.{u}} (g : X ⟶ Spec (CommRingCat.of S')) (M
  M' : X.Modules) : Prop

def

IsSymmetric

L57 ↗

AlgebraicGeometry.Polarisation.IsSymmetric

Documentation

The module sheaf is locally isomorphic on the base to its pullback under inversion.

Source context 5 commands

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

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

Lean source · statement

def IsSymmetric (𝓛 : A.Modules) : Prop

def

mumfordBundle

L61 ↗

AlgebraicGeometry.Polarisation.mumfordBundle

Documentation

The pullback under addition tensored with the duals pulled back from both factors.

Source context 5 commands

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

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

Lean source · statement

def mumfordBundle (𝓛 : A.Modules) : (pullback f f).Modules

def

sliceAt

L67 ↗

AlgebraicGeometry.Polarisation.sliceAt

Documentation

The morphism into the square of the scheme defined by a point in the second factor.

Source context 5 commands

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

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

Lean source · statement

def sliceAt {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of S)} (x : SchemeHomOver t f) :
    pullback f t ⟶ pullback f f

def

KernelTrivial

L73 ↗

AlgebraicGeometry.Polarisation.KernelTrivial

Documentation

Local triviality of the sliced Mumford bundle forces the point to be the identity.

Source context 5 commands

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

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

Lean source · statement

def KernelTrivial (𝓛 : A.Modules) : Prop

def

KernelIsTwoTorsion

L82 ↗

AlgebraicGeometry.Polarisation.KernelIsTwoTorsion

Documentation

Local triviality of the sliced Mumford bundle is equivalent to the point being two-torsion.

Source context 5 commands

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

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

Lean source · statement

def KernelIsTwoTorsion (𝓛 : A.Modules) : Prop

def

RosatiCompatible

L91 ↗

AlgebraicGeometry.Polarisation.RosatiCompatible

Documentation

The action and its adjoint give locally isomorphic pullbacks of the Mumford bundle.

Source context 5 commands

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

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

Lean source · statement

def RosatiCompatible (𝓛 : A.Modules) {I : Type v} (ι : I → (A ⟶ A)) (hι : ∀ b, ι b ≫ f = f) (star :
  I → I) : Prop

Module documentation

Polarisation Rosati

Declarations