Module

AbelianSchemePropertyBundle_exists_isInvertible_coeff_pos_forall_eulerChar_tensorPow_eq.lean

Nyll.JacobianVarieties.Picard.AbelianSchemePropertyBundle_exists_isInvertible_coeff_pos_forall_eulerChar_tensorPow_eq

1 declaration indexed from sourceView source ↗

Module documentation

A positive Euler characteristic coefficient on an abelian scheme

For an abelian scheme over an algebraically closed field, this file constructs an invertible sheaf whose tensor powers have polynomial Euler characteristic. The coefficient in the relative dimension is positive.

Imports14

Imported by2

theorem

exists_isInvertible_coeff_pos_forall_eulerChar_tensorPow_eq

L616 ↗

GoodReductionJacobian.AbelianSchemePropertyBundle.exists_isInvertible_coeff_pos_forall_eulerChar_tensorPow_eq

Documentation

An invertible sheaf has a positive leading Euler coefficient in the relative dimension.

Source context 10 commands

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

section ProofImplementation
namespace GoodReductionJacobian.AbelianSchemePropertyBundle
open _root_.JacobianVarieties.Picard.Proofs.AmpleEulerCoefficient
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u

Lean source · statement

theorem exists_isInvertible_coeff_pos_forall_eulerChar_tensorPow_eq
    (K : Type u) [Field K] [IsAlgClosed K] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of K))
    (hA : AbelianSchemePropertyBundle K f) (g : ℕ) [SmoothOfRelativeDimension g f]
    (𝒦 : A.OrderedAffineCover) :
    ∃ 𝓛 : A.Modules, Scheme.Modules.IsInvertible 𝓛 ∧ ∃ q : Polynomial ℚ, 0 < q.coeff g ∧
      ∀ m : ℕ, ((OModulePresheaf.ofModules f (𝓛.tensorPow m)).eulerChar 𝒦 : ℚ) =
        q.eval (m : ℚ)

Module documentation

A positive Euler characteristic coefficient on an abelian scheme

Declarations

exists_isInvertible_coeff_pos_forall_eulerChar_tensorPow_eq