Module

GroupGlobalRepresentation.lean

Nyll.AlgebraicCurves.Geometry.Descent.GroupGlobalRepresentation

2 declarations indexed from sourceView source ↗

Module documentation

The group law of the descended global representation

The global classifying equivalence preserves the operations constructed on matching local points. Equality is checked after the actual descent cover using separatedness.

Imports3

Nyll.AlgebraicCurves.Geometry.Descent.GlobalRepresentation
Nyll.AlgebraicCurves.Geometry.Descent.GroupOfMatching
Mathlib.CategoryTheory.Sites.IsSheafFor

Imported by2

theorem

globalRepresentation_mul

L41 ↗

AlgebraicGeometry.DescentAction.globalRepresentation_mul

Documentation

The class of the product is the product of the two global classes.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
open NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.DescentAction
variable {R : Type u} [CommRing R]
  {S' : Scheme.{u}} (s : S' ⟶ Spec (CommRingCat.of R))
  (G : (Over (Spec (CommRingCat.of R)))ᵒᵖ ⥤ CommGrpCat.{u + 1})
  {X' : Scheme.{u}} (x' : X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G ⋙ forget CommGrpCat).RepresentableBy (Over.mk x'))
  {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R)) (e : pullback f s ≅ X')
  (he : e.hom ≫ x' = pullback.snd f s)
  (hG : ∀ T : Over (Spec (CommRingCat.of R)),
    Presieve.IsSheafFor (G ⋙ forget CommGrpCat) (Presieve.singleton (coverT s T)))
  (hc : eRel s x' f e he ≫ repAct s (G ⋙ forget CommGrpCat) x' hX' =
    (canonical s f).act ≫ e.hom)
  [∀ T : Over (Spec (CommRingCat.of R)), EffectiveEpi (pullback.fst T.hom s)]

Lean source · statement

theorem globalRepresentation_mul {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver t f) :
    (globalRepresentation s (G ⋙ forget CommGrpCat) x' hX' f e he hG hc).homEquiv
        (schemeHomOverToOverHom ((relativeGroupLawOfMatching s G x' hX' f e he hc).mul t x y)) =
      (globalRepresentation s (G ⋙ forget CommGrpCat) x' hX' f e he hG hc).homEquiv
        (schemeHomOverToOverHom x) *
      (globalRepresentation s (G ⋙ forget CommGrpCat) x' hX' f e he hG hc).homEquiv
        (schemeHomOverToOverHom y)

theorem

globalRepresentation_one

L69 ↗

AlgebraicGeometry.DescentAction.globalRepresentation_one