NYLL
Module

Nonempty_invModule_prodKerGraph_tensor_module_pow_iso_pointsSubBasepointModule.lean

Nyll.JacobianVarieties.Picard.Nonempty_invModule_prodKerGraph_tensor_module_pow_iso_pointsSubBasepointModule
6 declarations indexed from sourceView source ↗

Module documentation

Relative Picard varieties and fibre cohomology

Identify the tensor product of graph-ideal inverse modules and basepoint factors with the point- difference line bundle.

Imports6
Imported by5

Declarations

def

shuffle

L56 ↗
JacobianVarieties.Picard.Proofs.Nonempty_invModule_prodKerGraph_tensor_module_pow_iso_pointsSubBasepointModule.AlgebraicGeometry.RelPicard.TensorList.shuffle
Documentation

Interchange the middle factors in a tensor product of four sheaf modules.

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs
namespace Nonempty_invModule_prodKerGraph_tensor_module_pow_iso_pointsSubBasepointModule
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
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace TensorList
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard.Scheme
open _root_.AlgebraicGeometry.Scheme
variable {k : Type u} [Field k] {A : Scheme.{u}} {a : A ⟶ Spec (CommRingCat.of k)}
  [IsSeparated a] [SmoothOfRelativeDimension 1 a]
Lean source · statement
def shuffle {X : Scheme.{u}} (X₁ X₂ Y₁ Y₂ : X.Modules) :
    (X₁ ⊗ X₂) ⊗ (Y₁ ⊗ Y₂) ≅ (X₁ ⊗ Y₁) ⊗ (X₂ ⊗ Y₂)
lemma

isInvertible_ker

L62 ↗
JacobianVarieties.Picard.Proofs.Nonempty_invModule_prodKerGraph_tensor_module_pow_iso_pointsSubBasepointModule.AlgebraicGeometry.RelPicard.TensorList.isInvertible_ker
Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs
namespace Nonempty_invModule_prodKerGraph_tensor_module_pow_iso_pointsSubBasepointModule
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
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace TensorList
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard.Scheme
open _root_.AlgebraicGeometry.Scheme
variable {k : Type u} [Field k] {A : Scheme.{u}} {a : A ⟶ Spec (CommRingCat.of k)}
  [IsSeparated a] [SmoothOfRelativeDimension 1 a]
Lean source · statement
lemma isInvertible_ker (P : Spec (CommRingCat.of k) ⟶ A) (hP : P ≫ a = 𝟙 _) :
    (graphOver a P hP).ker.IsInvertible
lemma

isInvertible_prodKerGraph

L75 ↗
JacobianVarieties.Picard.Proofs.Nonempty_invModule_prodKerGraph_tensor_module_pow_iso_pointsSubBasepointModule.AlgebraicGeometry.RelPicard.TensorList.isInvertible_prodKerGraph
Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs
namespace Nonempty_invModule_prodKerGraph_tensor_module_pow_iso_pointsSubBasepointModule
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
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace TensorList
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard.Scheme
open _root_.AlgebraicGeometry.Scheme
variable {k : Type u} [Field k] {A : Scheme.{u}} {a : A ⟶ Spec (CommRingCat.of k)}
  [IsSeparated a] [SmoothOfRelativeDimension 1 a]
Lean source · statement
lemma isInvertible_prodKerGraph {r : ℕ} (P : Fin r → (Spec (CommRingCat.of k) ⟶ A)) (hP : ∀ i,
  P i ≫ a = 𝟙 _) :
    (prodKerGraph a P hP).IsInvertible
lemma

isInvertible_pow

L84 ↗
JacobianVarieties.Picard.Proofs.Nonempty_invModule_prodKerGraph_tensor_module_pow_iso_pointsSubBasepointModule.AlgebraicGeometry.RelPicard.TensorList.isInvertible_pow
Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs
namespace Nonempty_invModule_prodKerGraph_tensor_module_pow_iso_pointsSubBasepointModule
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
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace TensorList
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard.Scheme
open _root_.AlgebraicGeometry.Scheme
variable {k : Type u} [Field k] {A : Scheme.{u}} {a : A ⟶ Spec (CommRingCat.of k)}
  [IsSeparated a] [SmoothOfRelativeDimension 1 a]
Lean source · statement
lemma isInvertible_pow {X : Scheme.{u}} {I : X.IdealSheafData} (hI : I.IsInvertible) (n : ℕ) :
    (I ^ n).IsInvertible
theorem

main

L90 ↗
JacobianVarieties.Picard.Proofs.Nonempty_invModule_prodKerGraph_tensor_module_pow_iso_pointsSubBasepointModule.AlgebraicGeometry.RelPicard.TensorList.main
Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs
namespace Nonempty_invModule_prodKerGraph_tensor_module_pow_iso_pointsSubBasepointModule
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
namespace RelPicard
open _root_.AlgebraicGeometry.RelPicard
namespace TensorList
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard.Scheme
open _root_.AlgebraicGeometry.Scheme
variable {k : Type u} [Field k] {A : Scheme.{u}} {a : A ⟶ Spec (CommRingCat.of k)}
  [IsSeparated a] [SmoothOfRelativeDimension 1 a]
Lean source · full declaration
theorem main (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) a) {r : ℕ}
    (P : Fin r → (Spec (CommRingCat.of k) ⟶ A)) (hP : ∀ i, P i ≫ a = 𝟙 _) :
    Nonempty ((prodKerGraph a P hP).invModule ⊗ ((RelEffCartierDiv.ofPoint a ε.1 ε.2).I ^
      r).module ≅
      pointsSubBasepointModule (a := a) ε
        (List.ofFn fun i => (⟨P i, hP i⟩ : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) a))) := by
  induction r with
  | zero =>
    have h1 : prodKerGraph a P hP = ⊤ := prodKerGraph_zero a P hP
    have h2 : (RelEffCartierDiv.ofPoint a ε.1 ε.2).I ^ 0 = ⊤ := by rw [pow_zero,
      Scheme.IdealSheafData.one_eq_top]
    rw [List.ofFn_zero, pointsSubBasepointModule_nil, h1, h2]
    exact Scheme.IdealSheafData.IsInvertible.nonempty_invModule_tensor_module_iso
      IdealSheafData.isInvertible_top
  | succ r ih =>
    let I₀ := (graphOver a (P 0) (hP 0)).ker
    let J := prodKerGraph a (fun i => P i.succ) (fun i => hP i.succ)
    let Iε := (RelEffCartierDiv.ofPoint a ε.1 ε.2).I
    have hprod : prodKerGraph a P hP = I₀ * J := by
      simp only [I₀, J, prodKerGraph_eq_prod]
      rw [Fin.prod_univ_succ]
    have hpow : Iε ^ (r + 1) = Iε * Iε ^ r := pow_succ' Iε r
    have hI₀ : I₀.IsInvertible := isInvertible_ker (P 0) (hP 0)
    have hJ : J.IsInvertible := isInvertible_prodKerGraph _ _
    have hIε : Iε.IsInvertible := isInvertible_ker ε.1 ε.2
    have hIεr : (Iε ^ r).IsInvertible := isInvertible_pow hIε r
    obtain ⟨e₁⟩ := Scheme.IdealSheafData.IsInvertible.nonempty_mul_invModule_iso_tensor hI₀ hJ
    obtain ⟨e₂⟩ := Scheme.IdealSheafData.IsInvertible.nonempty_mul_module_iso_tensor hIε hIεr
    obtain ⟨e₃⟩ := ih (fun i => P i.succ) (fun i => hP i.succ)
    rw [List.ofFn_succ, pointsSubBasepointModule_cons]
    have c₁ : (prodKerGraph a P hP).invModule ≅ (I₀ * J).invModule := eqToIso (by rw [hprod])
    have c₂ : ((RelEffCartierDiv.ofPoint a ε.1 ε.2).I ^ (r + 1)).module ≅ (Iε * Iε ^ r).module :=
      eqToIso
        (by rw [show (RelEffCartierDiv.ofPoint a ε.1 ε.2).I ^ (r + 1) = Iε * Iε ^ r from hpow])
    exact ⟨(c₁ ⊗ᵢ c₂) ≪≫ (e₁ ⊗ᵢ e₂) ≪≫ shuffle _ _ _ _ ≪≫ whiskerLeftIso _ e₃⟩
theorem

nonempty_invModule_prodKerGraph_tensor_module_pow_iso_pointsSubBasepointModule

L133 ↗
AlgebraicGeometry.RelPicard.nonempty_invModule_prodKerGraph_tensor_module_pow_iso_pointsSubBasepointModule
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs
namespace Nonempty_invModule_prodKerGraph_tensor_module_pow_iso_pointsSubBasepointModule
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
with_weak_namespace _root_.JacobianVarieties.Picard.Proofs
with_weak_namespace Nonempty_invModule_prodKerGraph_tensor_module_pow_iso_pointsSubBasepointModule
with_weak_namespace AlgebraicGeometry
open RelPicard in
with_weak_namespace _root_.AlgebraicGeometry.RelPicard
Lean source · full declaration
theorem nonempty_invModule_prodKerGraph_tensor_module_pow_iso_pointsSubBasepointModule
    {k : Type u} [Field k] {A : Scheme.{u}} {a : A ⟶ Spec (CommRingCat.of k)}
    [IsSeparated a] [SmoothOfRelativeDimension 1 a]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) a) {r : ℕ}
    (P : Fin r → (Spec (CommRingCat.of k) ⟶ A)) (hP : ∀ i, P i ≫ a = 𝟙 _) :
    Nonempty ((prodKerGraph a P hP).invModule ⊗ ((RelEffCartierDiv.ofPoint a ε.1 ε.2).I ^
      r).module ≅
      pointsSubBasepointModule (a := a) ε
        (List.ofFn fun i => (⟨P i, hP i⟩ : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) a))) :=
  TensorList.main ε P hP

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