NYLL
Module

RelEffCartierDiv_isAlgEquivZero_twistModule_fibre.lean

Nyll.JacobianVarieties.Picard.RelEffCartierDiv_isAlgEquivZero_twistModule_fibre
9 declarations indexed from sourceView source ↗

Module documentation

Relative Picard varieties and fibre cohomology

Show that effective-divisor twist modules have algebraically trivial fibres.

Imports26
Imported by4

Declarations

theorem

ker_comap_fst_eq_ofPoint_I

L63 ↗
JacobianVarieties.Picard.Proofs.RelEffCartierDiv_isAlgEquivZero_twistModule_fibre.AlgebraicGeometry.K2Aux.ker_comap_fst_eq_ofPoint_I
Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RelEffCartierDiv_isAlgEquivZero_twistModule_fibre
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
Lean source · statement
theorem K2Aux.ker_comap_fst_eq_ofPoint_I {A B : Scheme.{u}} (a : A ⟶ B) [IsSeparated a]
    (P : B ⟶ A) (hP : P ≫ a = 𝟙 B) :
    P.ker.comap (pullback.fst a (𝟙 B)) = (RelEffCartierDiv.ofPoint a P hP).I
theorem

nonempty_iso_unit_of_subsingleton

L79 ↗
JacobianVarieties.Picard.Proofs.RelEffCartierDiv_isAlgEquivZero_twistModule_fibre.AlgebraicGeometry.K2Aux.nonempty_iso_unit_of_subsingleton
Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RelEffCartierDiv_isAlgEquivZero_twistModule_fibre
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
Lean source · statement
theorem K2Aux.nonempty_iso_unit_of_subsingleton {X : Scheme.{u}} [Subsingleton X] [Nonempty X]
    {N : X.Modules} (hN : Scheme.Modules.IsInvertible N) :
    Nonempty (N ≅ 𝟙_ X.Modules)
def

fibrePt

L100 ↗
JacobianVarieties.Picard.Proofs.RelEffCartierDiv_isAlgEquivZero_twistModule_fibre.AlgebraicGeometry.K2Aux.fibrePt
Documentation

The point of the fibre obtained by the graph of a point above the given base point.

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RelEffCartierDiv_isAlgEquivZero_twistModule_fibre
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section Fibre
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
  {k : Type u} [Field k] (x : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
Lean source · statement
def K2Aux.fibrePt (q : Spec (CommRingCat.of k) ⟶ C) (hq : q ≫ c = x) :
    SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) (pullback.snd c x)
def

fibreBasePt

L105 ↗
JacobianVarieties.Picard.Proofs.RelEffCartierDiv_isAlgEquivZero_twistModule_fibre.AlgebraicGeometry.K2Aux.fibreBasePt
Documentation

The distinguished point of the fibre induced by the rigidifying section.

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RelEffCartierDiv_isAlgEquivZero_twistModule_fibre
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section Fibre
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
  {k : Type u} [Field k] (x : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
Lean source · statement
def K2Aux.fibreBasePt : SchemeHomOver (𝟙 (Spec (CommRingCat.of k)))
  (pullback.snd c x)
theorem

nonempty_pullback_point_iso

L109 ↗
JacobianVarieties.Picard.Proofs.RelEffCartierDiv_isAlgEquivZero_twistModule_fibre.AlgebraicGeometry.K2Aux.nonempty_pullback_point_iso
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RelEffCartierDiv_isAlgEquivZero_twistModule_fibre
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section Fibre
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
  {k : Type u} [Field k] (x : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
Lean source · statement
theorem K2Aux.nonempty_pullback_point_iso (q : Spec (CommRingCat.of k) ⟶ C) (hq : q ≫ c = x) :
    Nonempty ((Scheme.Modules.pullback (pullback.fst (pullback.snd c x) (𝟙 _))).obj
        ((graphOver c q hq).ker.invModule ⊗ (RelPicard.sectionIdeal c ε x).module) ≅
      pointSubBasepointModule (a := pullback.snd c x) (K2Aux.fibrePt c x q hq)
        (K2Aux.fibreBasePt c ε x))
theorem

nonempty_pullback_prod_iso

L146 ↗
JacobianVarieties.Picard.Proofs.RelEffCartierDiv_isAlgEquivZero_twistModule_fibre.AlgebraicGeometry.K2Aux.nonempty_pullback_prod_iso
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RelEffCartierDiv_isAlgEquivZero_twistModule_fibre
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
section Fibre
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
  {k : Type u} [Field k] (x : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
Lean source · full declaration
theorem K2Aux.nonempty_pullback_prod_iso (n : ℕ) (b : Fin n → (Spec (CommRingCat.of k) ⟶ C))
    (hb : ∀ i, b i ≫ c = x) :
    Nonempty ((Scheme.Modules.pullback (pullback.fst (pullback.snd c x) (𝟙 _))).obj
        ((prodKerGraph c b hb).invModule ⊗ ((RelPicard.sectionIdeal c ε x) ^ n).module) ≅
      pointsSubBasepointModule (a := pullback.snd c x) (K2Aux.fibreBasePt c ε x)
        (List.ofFn fun i => K2Aux.fibrePt c x (b i) (hb i))) := by
  induction n with
  | zero =>
    have h0 : prodKerGraph c b hb = ⊤ := prodKerGraph_zero c b hb
    have hJ : (RelPicard.sectionIdeal c ε x) ^ 0 = ⊤ := by
      rw [pow_zero, Scheme.IdealSheafData.one_eq_top]
    obtain ⟨e1⟩ := Scheme.IdealSheafData.IsInvertible.nonempty_invModule_tensor_module_iso
      (Scheme.IdealSheafData.isInvertible_top (X := pullback c x))
    rw [List.ofFn_zero, pointsSubBasepointModule_nil]
    exact ⟨(Scheme.Modules.pullback _).mapIso
        ((eqToIso (congrArg Scheme.IdealSheafData.invModule h0) ⊗ᵢ
          eqToIso (congrArg Scheme.IdealSheafData.module hJ)) ≪≫ e1) ≪≫
      Scheme.Modules.pullbackTensorUnitObjIso _⟩
  | succ n ih =>
    obtain ⟨etail⟩ := ih (fun i => b i.succ) (fun i => hb i.succ)
    obtain ⟨ehead⟩ := K2Aux.nonempty_pullback_point_iso c ε x (b 0) (hb 0)
    have hsucc := prodKerGraph_succ c b hb
    have hJ : (RelPicard.sectionIdeal c ε x) ^ (n + 1) =
        RelPicard.sectionIdeal c ε x * (RelPicard.sectionIdeal c ε x) ^ n := pow_succ' _ _
    have hK0 : (graphOver c (b 0) (hb 0)).ker.IsInvertible :=
      RelEffCartierDiv.isInvertible_I (RelEffCartierDiv.ofPoint c (b 0) (hb 0))
    have hK' : (prodKerGraph c (fun i => b i.succ) (fun i => hb i.succ)).IsInvertible := by
      obtain ⟨D', hD'⟩ := RelEffCartierDiv.exists_I_eq_prodKerGraph (f := c)
        (fun i => b i.succ) (fun i => hb i.succ)
      exact hD' ▸ RelEffCartierDiv.isInvertible_I D'
    have hJ1 : (RelPicard.sectionIdeal c ε x).IsInvertible :=
      RelEffCartierDiv.isInvertible_I
        (RelEffCartierDiv.ofPoint c (x ≫ ε.1) (by rw [Category.assoc, ε.2, Category.comp_id]))
    have hJn : ((RelPicard.sectionIdeal c ε x) ^ n).IsInvertible := hJ1.pow n
    obtain ⟨i1⟩ := Scheme.IdealSheafData.IsInvertible.nonempty_mul_invModule_iso_tensor hK0 hK'
    obtain ⟨i2⟩ := Scheme.IdealSheafData.IsInvertible.nonempty_mul_module_iso_tensor hJ1 hJn
    rw [List.ofFn_succ, pointsSubBasepointModule_cons]
    exact ⟨(Scheme.Modules.pullback _).mapIso
        ((eqToIso (congrArg Scheme.IdealSheafData.invModule hsucc) ⊗ᵢ
            eqToIso (congrArg Scheme.IdealSheafData.module hJ)) ≪≫
          (i1 ⊗ᵢ i2) ≪≫ Scheme.Modules.tensorTensorTensorComm _ _ _ _) ≪≫
      Scheme.Modules.pullbackTensorObjIso _ _ _ ≪≫ (ehead ⊗ᵢ etail)⟩
theorem

isAlgEquivZero_twistModule_of_isAlgClosed

L191 ↗
JacobianVarieties.Picard.Proofs.RelEffCartierDiv_isAlgEquivZero_twistModule_fibre.AlgebraicGeometry.K2Aux.isAlgEquivZero_twistModule_of_isAlgClosed
Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RelEffCartierDiv_isAlgEquivZero_twistModule_fibre
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
Lean source · statement
theorem K2Aux.isAlgEquivZero_twistModule_of_isAlgClosed
    {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    [IsSeparated c] [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) {r : ℕ}
    {k : Type u} [Field k] [IsAlgClosed k] (x : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
    (D : RelEffCartierDiv c r x) :
    IsAlgEquivZero (pullback.snd c x) (D.twistModule c ε)
theorem

isAlgEquivZero_twistModule_fibre'

L234 ↗
JacobianVarieties.Picard.Proofs.RelEffCartierDiv_isAlgEquivZero_twistModule_fibre.AlgebraicGeometry.K2Aux.isAlgEquivZero_twistModule_fibre'
Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RelEffCartierDiv_isAlgEquivZero_twistModule_fibre
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
Lean source · statement
theorem K2Aux.isAlgEquivZero_twistModule_fibre'
    {R : Type u} [CommRing R] [IsNoetherianRing R] {C : Scheme.{u}} (c : C ⟶ Spec
      (CommRingCat.of R))
    [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    {r : ℕ} {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} (D : RelEffCartierDiv c r t)
    (k : Type u) [Field k] [IsAlgClosed k] (s : Spec (CommRingCat.of k) ⟶ T) :
    IsAlgEquivZero (fibreAt c t s)
      ((Scheme.Modules.pullback (pullback.fst (pullback.snd c t) s)).obj (D.twistModule c ε))
theorem

isAlgEquivZero_twistModule_fibre

L260 ↗
AlgebraicGeometry.RelEffCartierDiv.isAlgEquivZero_twistModule_fibre
Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RelEffCartierDiv_isAlgEquivZero_twistModule_fibre
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
Lean source · statement
theorem _root_.AlgebraicGeometry.RelEffCartierDiv.isAlgEquivZero_twistModule_fibre
    {R : Type u} [CommRing R] [IsNoetherianRing R] {C : Scheme.{u}} (c : C ⟶ Spec
      (CommRingCat.of R))
    [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    {r : ℕ} {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} (D : RelEffCartierDiv c r t)
    (k : Type u) [Field k] [IsAlgClosed k] (s : Spec (CommRingCat.of k) ⟶ T) :
    IsAlgEquivZero (fibreAt c t s)
      ((Scheme.Modules.pullback (pullback.fst (pullback.snd c t) s)).obj (D.twistModule c ε))

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