NYLL
Module

RepresentsRelSubPic_relativeGroupLaw_mul_eq_baseChange_mul_of_nonempty_poincare_iso_ofR.lean

Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_relativeGroupLaw_mul_eq_baseChange_mul_of_nonempty_poincare_iso_ofR
4 declarations indexed from sourceView source ↗

Module documentation

Compatibility of the relative Picard group law with base change

The comparison between the Poincare bundles transports tensor products along base change. It identifies the multiplication represented after base change with the base-changed group law.

Imports12
Imported by1

Declarations

def

LAW_ofR_pullbackAlong_iso

L100 ↗
JacobianVarieties.Picard.Proofs.LawBC.AlgebraicGeometry.RelPicard.BaseChange.LAW_ofR_pullbackAlong_iso
Documentation

Base change of a rigidified line bundle commutes with pullback along points.

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LawBC
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
namespace AlgebraicGeometry
namespace RelPicard
namespace BaseChange
open _root_.AlgebraicGeometry.RelPicard.BaseChange
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
def LAW_ofR_pullbackAlong_iso {T T'' : Scheme.{u}} {t' : T ⟶ Spec (CommRingCat.of R')}
    {t'' : T'' ⟶ Spec (CommRingCat.of R')} (ψ : SchemeHomOver t'' t')
    (X : RigidifiedLineBundle c ε (t' ≫ specMap R R')) :
    ((ofR c ε R' X).pullbackAlong ψ).L ≅ (ofR c ε R' (X.pullbackAlong (overR R' ψ))).L
def

LAW_pullbackAlong_pullbackAlong_iso

L110 ↗
JacobianVarieties.Picard.Proofs.LawBC.AlgebraicGeometry.RelPicard.BaseChange.LAW_pullbackAlong_pullbackAlong_iso
Documentation

Iterated pullback of a rigidified line bundle agrees with pullback along the composite.

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LawBC
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
namespace AlgebraicGeometry
namespace RelPicard
namespace BaseChange
open _root_.AlgebraicGeometry.RelPicard.BaseChange
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
omit [Algebra R R'] in
Lean source · statement
def LAW_pullbackAlong_pullbackAlong_iso {X₀ X₁ X₂ : Scheme.{u}}
    {x₀ : X₀ ⟶ Spec (CommRingCat.of R)}
    {x₁ : X₁ ⟶ Spec (CommRingCat.of R)} {x₂ : X₂ ⟶ Spec (CommRingCat.of R)}
    (M : RigidifiedLineBundle c ε x₀) (φ : SchemeHomOver x₁ x₀) (ψ : SchemeHomOver x₂ x₁) :
    ((M.pullbackAlong φ).pullbackAlong ψ).L ≅ (M.pullbackAlong (postComp φ ψ)).L
def

LAW_transportIso

L119 ↗
JacobianVarieties.Picard.Proofs.LawBC.AlgebraicGeometry.RelPicard.BaseChange.LAW_transportIso
Documentation

Transport of a Poincare fibre back to the base through the given base-change comparison.

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LawBC
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
namespace AlgebraicGeometry
namespace RelPicard
namespace BaseChange
open _root_.AlgebraicGeometry.RelPicard.BaseChange
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
def LAW_transportIso {D : RelativePic0Designation R c}
    (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
    (h' : RepresentsRelSubPic (baseChange R c R') (sectionBaseChange R' ε)
        (algEquivZeroCut (baseChange R c R') (sectionBaseChange R' ε)) (D.baseChange R'))
    (e : h'.poincare.L ≅ (BaseChange.ofR c ε R'
        (h.poincare.pullbackAlong ⟨pullback.fst D.toBase (specMap R R'), pullback.condition⟩)).L)
    {T : Scheme.{u}} {t' : T ⟶ Spec (CommRingCat.of R')}
    (z : SchemeHomOver t' (D.baseChange R').toBase) :
    (toR c ε R' (h'.poincare.pullbackAlong z)).L ≅
      (h.poincare.pullbackAlong (RelativeGroupLaw.baseChangePointToBase (specMap R R') z)).L
theorem

relativeGroupLaw_mul_eq_baseChange_mul_of_nonempty_poincare_iso_ofR

L139 ↗
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.relativeGroupLaw_mul_eq_baseChange_mul_of_nonempty_poincare_iso_ofR
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.LawBC
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
open _root_.JacobianVarieties.Picard.Proofs.LawBC.AlgebraicGeometry.RelPicard.BaseChange in
with_weak_namespace _root_.AlgebraicGeometry.RelPicard.RepresentsRelSubPic
Lean source · statement
theorem relativeGroupLaw_mul_eq_baseChange_mul_of_nonempty_poincare_iso_ofR
    (R : Type u) [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    (D : RelativePic0Designation R c) (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
    (R' : Type u) [CommRing R'] [Algebra R R']
    (h' : RepresentsRelSubPic (baseChange R c R') (sectionBaseChange R' ε)
        (algEquivZeroCut (baseChange R c R') (sectionBaseChange R' ε)) (D.baseChange R'))
    (hP : Nonempty (h'.poincare.L ≅ (BaseChange.ofR c ε R'
        (h.poincare.pullbackAlong ⟨pullback.fst D.toBase (specMap R R'), pullback.condition⟩)).L)) :
    ∀ {T : Scheme.{u}} (t' : T ⟶ Spec (CommRingCat.of R'))
        (x y : SchemeHomOver t' (D.baseChange R').toBase),
      (RepresentsRelSubPic.relativeGroupLaw
          (P := algEquivZeroGroupCut (baseChange R c R') (sectionBaseChange R' ε)) h').mul t' x y =
        ((RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut c ε) h).baseChange
          (specMap R R')).mul t' x y

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