NYLL
Module

AlbaneseSeparableDescent.lean

Nyll.JacobianVarieties.Albanese.AlbaneseSeparableDescent
6 declarations indexed from sourceView source ↗

Module documentation

Descent of an actual Albanese factorization

The factorization over a finite separable extension descends along its finite faithfully flat spectrum map. Equality on the overlap follows from actual geometric point classes and uniqueness among all scheme morphisms.

Imports29
Imported by2

Declarations

def

scalarLeg

L59 ↗
JacobianVarieties.Albanese.SeparableDescent.scalarLeg
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open NeronModelInfra GoodReductionJacobian
namespace JacobianVarieties.Albanese.SeparableDescent
variable {S S' T C P B : Scheme.{u}}
  (s : S' ⟶ S) (t : T ⟶ S) (v : T ⟶ S') (hv : v ≫ s = t)
  (p : P ⟶ S) (b : B ⟶ S)
Lean source · statement
def scalarLeg : pullback p t ⟶ pullback p s
def

factorAt

L63 ↗
JacobianVarieties.Albanese.SeparableDescent.factorAt
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open NeronModelInfra GoodReductionJacobian
namespace JacobianVarieties.Albanese.SeparableDescent
variable {S S' T C P B : Scheme.{u}}
  (s : S' ⟶ S) (t : T ⟶ S) (v : T ⟶ S') (hv : v ≫ s = t)
  (p : P ⟶ S) (b : B ⟶ S)
Lean source · statement
def factorAt
    (ψ : SchemeHomOver (pullback.snd p s) (pullback.snd b s)) :
    SchemeHomOver (pullback.snd p t) (pullback.snd b t)
theorem

scalarLeg_natural

L73 ↗
JacobianVarieties.Albanese.SeparableDescent.scalarLeg_natural
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open NeronModelInfra GoodReductionJacobian
namespace JacobianVarieties.Albanese.SeparableDescent
variable {S S' T C P B : Scheme.{u}}
  (s : S' ⟶ S) (t : T ⟶ S) (v : T ⟶ S') (hv : v ≫ s = t)
  (p : P ⟶ S) (b : B ⟶ S)
Lean source · statement
theorem scalarLeg_natural (c : C ⟶ S) (a : SchemeHomOver c p) :
    (fibreRestrictAlong t p c a).1 ≫ scalarLeg s t v hv p =
      scalarLeg s t v hv c ≫ (fibreRestrictAlong s p c a).1
theorem

factorAt_comp

L82 ↗
JacobianVarieties.Albanese.SeparableDescent.factorAt_comp
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open NeronModelInfra GoodReductionJacobian
namespace JacobianVarieties.Albanese.SeparableDescent
variable {S S' T C P B : Scheme.{u}}
  (s : S' ⟶ S) (t : T ⟶ S) (v : T ⟶ S') (hv : v ≫ s = t)
  (p : P ⟶ S) (b : B ⟶ S)
Lean source · statement
theorem factorAt_comp (c : C ⟶ S) (a : SchemeHomOver c p)
    (q : SchemeHomOver c b)
    (ψ : SchemeHomOver (pullback.snd p s) (pullback.snd b s))
    (hψ : (fibreRestrictAlong s p c a).1 ≫ ψ.1 = (fibreRestrictAlong s b c q).1) :
    (fibreRestrictAlong t p c a).1 ≫ (factorAt s t v hv p b ψ).1 =
      (fibreRestrictAlong t b c q).1
theorem

pointed_fibreRestrictAlong

L103 ↗
JacobianVarieties.Albanese.pointed_fibreRestrictAlong
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open NeronModelInfra GoodReductionJacobian
open AlgebraicGeometry.SmoothProperCurve
namespace JacobianVarieties.Albanese
Lean source · statement
theorem pointed_fibreRestrictAlong
    {K L : Type u} [Field K] [Field L] [Algebra K L] {C B : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K)) (b : B ⟶ Spec (CommRingCat.of K))
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
    (G : RelativeGroupLaw K b) (q : SchemeHomOver c b)
    (hq : NeronModelInfra.schemeHomOverComp ε q = G.one (𝟙 _)) :
    NeronModelInfra.schemeHomOverComp (sectionBaseChange L ε)
      (fibreRestrictAlong (specMap K L) b c q) =
        (G.baseChange (specMap K L)).one (𝟙 _)
theorem

exists_factorization_of_finite_separable_baseChange

L138 ↗
JacobianVarieties.Albanese.exists_factorization_of_finite_separable_baseChange
Documentation

A factorization obtained over an actual finite separable extension descends to the ground field. Compatibility on the overlap is proved from the actual geometric point classes and Abel--Jacobi uniqueness.

Source context 11 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open NeronModelInfra GoodReductionJacobian
open AlgebraicGeometry.SmoothProperCurve
open CategoryTheory.MonoidalCategory AlgebraicGeometry.RelPicard
open AlgebraicCurves.Geometry.Schemes.Proofs
open SchemeHomOver_ext_of_forall_algebraicClosure_point_of_isReduced_of_flat
namespace JacobianVarieties.Albanese
open SeparableDescent
open RigKerGeomPoints renaming ext_of_forall_geometric_point → geometricHomExt in
Lean source · statement
theorem exists_factorization_of_finite_separable_baseChange
    (K : Type u) [Field K] {C : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K)) [IsProper c]
    [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
    (D : RelativePic0Designation K c) [Smooth D.toBase] [IsProper D.toBase]
    [GeometricallyConnected D.toBase]
    (hD : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
    (aj : SchemeHomOver c D.toBase)
    (hclass : ∀ (F : Type u) [Field F]
      (t : Spec (CommRingCat.of F) ⟶ Spec (CommRingCat.of K))
      (x : SchemeHomOver t c),
      Nonempty ((hD.poincare.pullbackAlong
        ⟨x.1 ≫ aj.1, (Category.assoc _ _ _).trans
          ((congrArg (x.1 ≫ ·) aj.2).trans x.2)⟩).L ≅
        (RelEffCartierDiv.ofPoint c x.1 x.2).lineBundle ⊗
          (RelEffCartierDiv.ofPoint c (t ≫ ε.1)
            ((Category.assoc _ _ _).trans
              ((congrArg (t ≫ ·) ε.2).trans (Category.comp_id t)))).idealModule))
    {B : Scheme.{u}} (b : B ⟶ Spec (CommRingCat.of K)) [Smooth b] [IsProper b]
    [GeometricallyIntegral b] (G : RelativeGroupLaw K b) (q : SchemeHomOver c b)
    (hq : NeronModelInfra.schemeHomOverComp ε q = G.one (𝟙 _))
    (L : Type u) [Field L] [Algebra K L] [Module.Finite K L]
    [Algebra.IsSeparable K L]
    (ψ : SchemeHomOver (D.baseChange L).toBase (pullback.snd b (specMap K L)))
    (hψ : (fibreRestrictAlong (specMap K L) D.toBase c aj).1 ≫ ψ.1 =
      (fibreRestrictAlong (specMap K L) b c q).1) :
    ∃ φ : SchemeHomOver D.toBase b, aj.1 ≫ φ.1 = q.1

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