NYLL
Module

GlobalRepresentation.lean

Nyll.AlgebraicCurves.Geometry.Descent.GlobalRepresentation
5 declarations indexed from sourceView source ↗

Module documentation

A compatible global representation after effective descent

The descended universal element is retained explicitly. Consequently its classifying equivalence agrees with the fixed local representation, a fact needed to compare group laws rather than merely isomorphism classes of representing objects.

Imports3
Imported by3

Declarations

theorem

isSheafFor_coverT_of_isRepresentable

L30 ↗
AlgebraicGeometry.DescentAction.isSheafFor_coverT_of_isRepresentable
Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
noncomputable section
namespace AlgebraicGeometry.DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S)
  (G : (Over S)ᵒᵖ ⥤ Type (u + 1))
Lean source · statement
theorem isSheafFor_coverT_of_isRepresentable
    [G.IsRepresentable] [Flat s] [Surjective s] [QuasiCompact s] (T : Over S) :
    Presieve.IsSheafFor G (Presieve.singleton (coverT s T))
def

globalUniversal

L49 ↗
AlgebraicGeometry.DescentAction.globalUniversal
Documentation

The actual descent of the local universal presheaf element.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
noncomputable section
namespace AlgebraicGeometry.DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S)
  (G : (Over S)ᵒᵖ ⥤ Type (u + 1))
variable {X' : Scheme.{u}} (x' : X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G).RepresentableBy (Over.mk x'))
  {X : Scheme.{u}} (f : X ⟶ S) (e : pullback f s ≅ X')
  (he : e.hom ≫ x' = pullback.snd f s)
  (hG : ∀ T : Over S, Presieve.IsSheafFor G (Presieve.singleton (coverT s T)))
  (hc : eRel s x' f e he ≫ repAct s G x' hX' = (canonical s f).act ≫ e.hom)
Lean source · statement
def globalUniversal : G.obj (op (Over.mk f))
theorem

globalUniversal_spec

L52 ↗
AlgebraicGeometry.DescentAction.globalUniversal_spec
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
noncomputable section
namespace AlgebraicGeometry.DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S)
  (G : (Over S)ᵒᵖ ⥤ Type (u + 1))
variable {X' : Scheme.{u}} (x' : X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G).RepresentableBy (Over.mk x'))
  {X : Scheme.{u}} (f : X ⟶ S) (e : pullback f s ≅ X')
  (he : e.hom ≫ x' = pullback.snd f s)
  (hG : ∀ T : Over S, Presieve.IsSheafFor G (Presieve.singleton (coverT s T)))
  (hc : eRel s x' f e he ≫ repAct s G x' hX' = (canonical s f).act ≫ e.hom)
Lean source · statement
theorem globalUniversal_spec :
    G.map (cover s f).op (globalUniversal s G x' hX' f e he hG hc) =
      univBC s G x' hX' f e he
def

globalRepresentation

L60 ↗
AlgebraicGeometry.DescentAction.globalRepresentation
Documentation

The global representation whose universal element is the actual descended one.

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
noncomputable section
namespace AlgebraicGeometry.DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S)
  (G : (Over S)ᵒᵖ ⥤ Type (u + 1))
variable {X' : Scheme.{u}} (x' : X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G).RepresentableBy (Over.mk x'))
  {X : Scheme.{u}} (f : X ⟶ S) (e : pullback f s ≅ X')
  (he : e.hom ≫ x' = pullback.snd f s)
  (hG : ∀ T : Over S, Presieve.IsSheafFor G (Presieve.singleton (coverT s T)))
  (hc : eRel s x' f e he ≫ repAct s G x' hX' = (canonical s f).act ≫ e.hom)
variable [∀ T : Over S, EffectiveEpi (pullback.fst T.hom s)]
Lean source · full declaration
def globalRepresentation : G.RepresentableBy (Over.mk f) where
  homEquiv {T} :=
    Equiv.ofBijective (fun m => G.map m.op (globalUniversal s G x' hX' f e he hG hc))
      ⟨fun _ _ h => map_ζ_injective s G x' hX' f e he
          (globalUniversal s G x' hX' f e he hG hc)
          (globalUniversal_spec s G x' hX' f e he hG hc) h,
        fun z => map_ζ_surjective s G x' hX' f e he
          (globalUniversal s G x' hX' f e he hG hc)
          (globalUniversal_spec s G x' hX' f e he hG hc) hc (hG T).isSeparatedFor z⟩
  homEquiv_comp g m := by
    change G.map (g ≫ m).op _ = G.map g.op (G.map m.op _)
    rw [op_comp, G.map_comp, types_comp_apply]
theorem

globalRepresentation_localPoint

L73 ↗
AlgebraicGeometry.DescentAction.globalRepresentation_localPoint
Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
noncomputable section
namespace AlgebraicGeometry.DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S)
  (G : (Over S)ᵒᵖ ⥤ Type (u + 1))
variable {X' : Scheme.{u}} (x' : X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G).RepresentableBy (Over.mk x'))
  {X : Scheme.{u}} (f : X ⟶ S) (e : pullback f s ≅ X')
  (he : e.hom ≫ x' = pullback.snd f s)
  (hG : ∀ T : Over S, Presieve.IsSheafFor G (Presieve.singleton (coverT s T)))
  (hc : eRel s x' f e he ≫ repAct s G x' hX' = (canonical s f).act ≫ e.hom)
variable [∀ T : Over S, EffectiveEpi (pullback.fst T.hom s)]
Lean source · statement
theorem globalRepresentation_localPoint {T : Over S} (m : T ⟶ Over.mk f) :
    G.map (coverT s T).op
        ((globalRepresentation s G x' hX' f e he hG hc).homEquiv m) =
      localPoint s G x' hX' f e he m

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