Module

baseChange_relativeGroupLaw_mul_compat.lean

Nyll.JacobianVarieties.Picard.baseChange_relativeGroupLaw_mul_compat

3 declarations indexed from sourceView source ↗

Module documentation

Compatibility of relative Picard multiplication with base change

The comparison of Poincaré bundles under base change identifies the multiplication laws on points of the two representing schemes.

Imports18

Imported by3

def

pullbackAlongComp

L65 ↗

JacobianVarieties.Picard.Proofs.BaseChangeGroupLaw.GrpBCLawSol.pullbackAlongComp

Documentation

Comparison of iterated pullback with pullback along the composite base morphism.

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.BaseChangeGroupLaw
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard.BaseChange
open scoped CategoryTheory.MonObj
namespace GrpBCLawSol
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}

Lean source · statement

def pullbackAlongComp {T T' T'' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t' : T' ⟶ Spec (CommRingCat.of R)} {t'' : T'' ⟶ Spec (CommRingCat.of R)}
    (M : RigidifiedLineBundle c ε t) (φ : SchemeHomOver t' t) (ψ : SchemeHomOver t'' t') :
    ((M.pullbackAlong φ).pullbackAlong ψ).L ≅ (M.pullbackAlong (postComp φ ψ)).L

def

pullbackAlongCongr

L73 ↗

JacobianVarieties.Picard.Proofs.BaseChangeGroupLaw.GrpBCLawSol.pullbackAlongCongr

Documentation

Equal underlying base morphisms induce isomorphic pulled-back line bundles.

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.BaseChangeGroupLaw
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard.BaseChange
open scoped CategoryTheory.MonObj
namespace GrpBCLawSol
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}

Lean source · statement

def pullbackAlongCongr {T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t' : T' ⟶ Spec (CommRingCat.of R)} (M : RigidifiedLineBundle c ε t) {φ ψ : SchemeHomOver t' t}
    (e : φ.1 = ψ.1) : (M.pullbackAlong φ).L ≅ (M.pullbackAlong ψ).L

theorem