Module

RepresentsRelSubPicBaseChange.lean

Nyll.JacobianVarieties.Picard.RepresentsRelSubPicBaseChange

1 declaration indexed from sourceView source ↗

Module documentation

Relative Picard varieties and fibre cohomology

Restrict a representing relative Picard designation along a base change.

Imports9

Imported by37

def

representableByRestrict

L41 ↗

AlgebraicGeometry.RelPicard.BaseChange.representableByRestrict

Documentation

Restrict the base-changed representing designation through the canonical relative sub- Picard presheaf isomorphism.

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
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 representableByRestrict {D' : RelativePic0Designation R' (baseChange R c R')}
    (h' : RepresentsRelSubPic (baseChange R c R') (sectionBaseChange R' ε)
      (algEquivZeroCut (baseChange R c R') (sectionBaseChange R' ε)) D') :
    ((Over.map (specMap R R')).op ⋙ relSubPicPresheaf c ε (algEquivZeroCut c ε)).RepresentableBy
      (Over.mk D'.toBase)

Module documentation

Relative Picard varieties and fibre cohomology

Declarations

representableByRestrict