NYLL
Module

RepresentsRelSubPic_nonempty_pullbackAlong_mul_iso_tensor_ofInvertible_norm_pullback_poincare.lean

Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_nonempty_pullbackAlong_mul_iso_tensor_ofInvertible_norm_pullback_poincare
7 declarations indexed from sourceView source ↗

Module documentation

Multiplication and the rigidified norm of the Poincare bundle

The supplied norm comparisons commute with base change and tensor products. After rigidification, these comparisons give the tensor law for pullback along multiplication on the represented relative Picard group.

Imports31
Imported by1

Declarations

theorem

isFinite_curveChange'

L83 ↗
JacobianVarieties.Picard.Proofs.NormTensorMultiplication.ModularCurve.PrimBody.isFinite_curveChange'
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.NormTensorMultiplication
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ModularCurve
namespace PrimBody
open _root_.AlgebraicGeometry.Scheme.Modules
variable {R : Type} [CommRing R] {C C' : Scheme.{0}}
  {c : C ⟶ Spec (CommRingCat.of R)} {c' : C' ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem isFinite_curveChange' (π : C' ⟶ C) (hπ : π ≫ c = c') [IsFinite π] {T : Scheme.{0}}
    (t : T ⟶ Spec (CommRingCat.of R)) :
    IsFinite (curveChange π hπ t)
theorem

surjective_curveChange'

L90 ↗
JacobianVarieties.Picard.Proofs.NormTensorMultiplication.ModularCurve.PrimBody.surjective_curveChange'
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.NormTensorMultiplication
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ModularCurve
namespace PrimBody
open _root_.AlgebraicGeometry.Scheme.Modules
variable {R : Type} [CommRing R] {C C' : Scheme.{0}}
  {c : C ⟶ Spec (CommRingCat.of R)} {c' : C' ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem surjective_curveChange' (π : C' ⟶ C) (hπ : π ≫ c = c') [Surjective π] {T : Scheme.{0}}
    (t : T ⟶ Spec (CommRingCat.of R)) :
    Surjective (curveChange π hπ t)
theorem

isPullback_curveChange_baseChangeSnd

L99 ↗
JacobianVarieties.Picard.Proofs.NormTensorMultiplication.ModularCurve.PrimBody.isPullback_curveChange_baseChangeSnd
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.NormTensorMultiplication
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ModularCurve
namespace PrimBody
open _root_.AlgebraicGeometry.Scheme.Modules
variable {R : Type} [CommRing R] {C C' : Scheme.{0}}
  {c : C ⟶ Spec (CommRingCat.of R)} {c' : C' ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem isPullback_curveChange_baseChangeSnd (π : C' ⟶ C) (hπ : π ≫ c = c')
    {T T' : Scheme.{0}} {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
    (ψ : SchemeHomOver t' t) :
    IsPullback (baseChangeSnd c' ψ) (curveChange π hπ t')
      (curveChange π hπ t) (baseChangeSnd c ψ)
theorem

flat_baseChangeSnd

L123 ↗
JacobianVarieties.Picard.Proofs.NormTensorMultiplication.ModularCurve.PrimBody.flat_baseChangeSnd
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.NormTensorMultiplication
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ModularCurve
namespace PrimBody
open _root_.AlgebraicGeometry.Scheme.Modules
variable {R : Type} [CommRing R] {C C' : Scheme.{0}}
  {c : C ⟶ Spec (CommRingCat.of R)} {c' : C' ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem flat_baseChangeSnd {T T' : Scheme.{0}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t' : T' ⟶ Spec (CommRingCat.of R)} (ψ : SchemeHomOver t' t) [Flat ψ.1] : Flat (baseChangeSnd c
      ψ)
def

shuffle

L131 ↗
JacobianVarieties.Picard.Proofs.NormTensorMultiplication.ModularCurve.PrimBody.shuffle
Documentation

Reorder four tensor factors using the associator and the symmetry.

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.NormTensorMultiplication
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ModularCurve
namespace PrimBody
open _root_.AlgebraicGeometry.Scheme.Modules
variable {R : Type} [CommRing R] {C C' : Scheme.{0}}
  {c : C ⟶ Spec (CommRingCat.of R)} {c' : C' ⟶ Spec (CommRingCat.of R)}
Lean source · statement
def shuffle {V : Type 1} [Category.{0} V] [MonoidalCategory V] [SymmetricCategory V] (A B X Y : V) :
    (A ⊗ B) ⊗ (X ⊗ Y) ≅ (A ⊗ X) ⊗ (B ⊗ Y)
theorem

nonempty_rigidify_tensor_iso

L136 ↗
JacobianVarieties.Picard.Proofs.NormTensorMultiplication.ModularCurve.PrimBody.nonempty_rigidify_tensor_iso
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.NormTensorMultiplication
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry.Scheme.Modules
namespace ModularCurve
namespace PrimBody
open _root_.AlgebraicGeometry.Scheme.Modules
variable {R : Type} [CommRing R] {C C' : Scheme.{0}}
  {c : C ⟶ Spec (CommRingCat.of R)} {c' : C' ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem nonempty_rigidify_tensor_iso {T P : Scheme.{0}} (σ : T ⟶ P) (q : P ⟶ T) {A B : P.Modules}
    (hA : Scheme.Modules.IsInvertible A) (hB : Scheme.Modules.IsInvertible B) :
    Nonempty (Scheme.Modules.rigidify σ q (A ⊗ B) ≅ Scheme.Modules.rigidify σ q A ⊗
      Scheme.Modules.rigidify σ q B)
theorem

nonempty_pullbackAlong_mul_iso_tensor_ofInvertible_norm_pullback_poincare

L164 ↗
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.nonempty_pullbackAlong_mul_iso_tensor_ofInvertible_norm_pullback_poincare
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicGeometry.RelPicard.RepresentsRelSubPic
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry.Scheme.Modules
open JacobianVarieties.Picard.Proofs.NormTensorMultiplication
open ModularCurve.PrimBody in
Lean source · statement
theorem nonempty_pullbackAlong_mul_iso_tensor_ofInvertible_norm_pullback_poincare
    (R : Type) [CommRing R]
    {C C' : Scheme.{0}} (c : C ⟶ Spec (CommRingCat.of R)) (c' : C' ⟶ Spec (CommRingCat.of R))
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    (π₁ π₂ : SchemeHomOver c' c) [IsFinite π₂.1] [Surjective π₂.1]
    (D : RelativePic0Designation R c)
    (hD : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
    [IsIntegral ↑(pullback c' D.toBase)] [IsIntegral ↑(pullback c D.toBase)]
    (hnorm : ∀ U : (pullback c D.toBase).Opens, IsAffineOpen U →
      IsIntegrallyClosed Γ(pullback c D.toBase, U))
    [Flat D.toBase] [LocallyOfFiniteType D.toBase]
    [IsIntegral ↑(pullback c' (pullback.fst D.toBase D.toBase ≫ D.toBase))]
    [IsIntegral ↑(pullback c (pullback.fst D.toBase D.toBase ≫ D.toBase))]
    (hnorm₂ : ∀ U : (pullback c (pullback.fst D.toBase D.toBase ≫ D.toBase)).Opens, IsAffineOpen U →
      IsIntegrallyClosed Γ(pullback c (pullback.fst D.toBase D.toBase ≫ D.toBase), U))
    (Nm : ∀ ⦃X Y : Scheme.{0}⦄, (X ⟶ Y) → X.Modules → Y.Modules)
    (hNm :
      ∀ ⦃X Y : Scheme.{0}⦄ (π : X ⟶ Y) [IsFinite π] [Surjective π] [IsIntegral X] [IsIntegral Y],
        (∀ U : Y.Opens, IsAffineOpen U → IsIntegrallyClosed Γ(Y, U)) →
        (∀ L : X.Modules, Scheme.Modules.IsInvertible L → Scheme.Modules.IsInvertible (Nm π L)) ∧
        (∀ L L' : X.Modules, Scheme.Modules.IsInvertible L → Nonempty (L ≅ L') →
          Nonempty (Nm π L ≅ Nm π L')) ∧
        (∀ L L' : X.Modules, Scheme.Modules.IsInvertible L → Scheme.Modules.IsInvertible L' →
          Nonempty (Nm π (L ⊗ L') ≅ Nm π L ⊗ Nm π L')) ∧
        Nonempty (Nm π (𝟙_ X.Modules) ≅ 𝟙_ Y.Modules) ∧
        (∀ ⦃X' Y' : Scheme.{0}⦄ (g : Y' ⟶ Y) (π' : X' ⟶ Y') (g' : X' ⟶ X), IsPullback g' π' π g →
          ∀ [Flat g] [IsIntegral X'] [IsIntegral Y'],
          (∀ U : Y'.Opens, IsAffineOpen U → IsIntegrallyClosed Γ(Y', U)) →
          ∀ L : X.Modules, Scheme.Modules.IsInvertible L →
            Nonempty ((Scheme.Modules.pullback g).obj (Nm π L) ≅
              Nm π' ((Scheme.Modules.pullback g').obj L))) ∧
        (∀ (V : Y.Opens) (d : ℕ), Flat (π ∣_ V) → LocallyOfFinitePresentation (π ∣_ V) →
          (∀ y : V, (π ∣_ V).finrank y = d) →
          ∀ L : X.Modules, Scheme.Modules.IsInvertible L →
            Nonempty ((Scheme.Modules.pullback V.ι).obj (Nm π L) ≅
              Scheme.Modules.normModule (π ∣_ V) d ((Scheme.Modules.pullback (π ⁻¹ᵁ V).ι).obj L))))
    (hinv : Scheme.Modules.IsInvertible
      (Nm (curveChange π₂.1 π₂.2 D.toBase) ((Scheme.Modules.pullback (curveChange π₁.1 π₁.2
        D.toBase)).obj hD.poincare.L)))
    {T : Scheme.{0}} (s : T ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver s D.toBase) :
    Nonempty (((RigidifiedLineBundle.ofInvertible (ε := ε) (Nm (curveChange π₂.1 π₂.2 D.toBase)
      ((Scheme.Modules.pullback (curveChange π₁.1 π₁.2 D.toBase)).obj hD.poincare.L))
      hinv).pullbackAlong
        ((RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut _ _) hD).mul s x y)).L ≅
      (((RigidifiedLineBundle.ofInvertible (ε := ε) (Nm (curveChange π₂.1 π₂.2 D.toBase)
        ((Scheme.Modules.pullback (curveChange π₁.1 π₁.2 D.toBase)).obj hD.poincare.L))
        hinv).pullbackAlong x).tensor
        ((RigidifiedLineBundle.ofInvertible (ε := ε) (Nm (curveChange π₂.1 π₂.2 D.toBase)
          ((Scheme.Modules.pullback (curveChange π₁.1 π₁.2 D.toBase)).obj hD.poincare.L))
          hinv).pullbackAlong y)).L)

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