Module

FppfGmRepresentable.lean

Nyll.AlgebraicCurves.Geometry.Descent.FppfGmRepresentable

57 declarations indexed from sourceView source ↗

Module documentation

Fppf Gm Representable

Imports7

Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Mathlib.AlgebraicGeometry.AffineSpace
Mathlib.AlgebraicGeometry.Limits
Mathlib.CategoryTheory.Sites.SubcanonicalOver
Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_
Mathlib.Algebra.Category.Grp.Adjunctions
Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup

Imported by2

theorem

isSheaf_fppf_of_isRepresentable

L36 ↗

FppfRepresentableGroupSchemeSheaf.isSheaf_fppf_of_isRepresentable

Source context 6 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section TypeValued

Lean source · statement

theorem isSheaf_fppf_of_isRepresentable (P : Scheme.{u}ᵒᵖ ⥤ Type u) [P.IsRepresentable] :
    Presheaf.IsSheaf Scheme.fppfTopology P

theorem

isSheaf_fpqc_of_isRepresentable

L41 ↗

FppfRepresentableGroupSchemeSheaf.isSheaf_fpqc_of_isRepresentable

Source context 6 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section TypeValued

Lean source · statement

theorem isSheaf_fpqc_of_isRepresentable (P : Scheme.{u}ᵒᵖ ⥤ Type u) [P.IsRepresentable] :
    Presheaf.IsSheaf Scheme.fpqcTopology P

theorem

isSheaf_fppf_yoneda

L46 ↗

FppfRepresentableGroupSchemeSheaf.isSheaf_fppf_yoneda

Source context 6 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section TypeValued

Lean source · statement

theorem isSheaf_fppf_yoneda (G : Scheme.{u}) :
    Presheaf.IsSheaf Scheme.fppfTopology (yoneda.obj G)

theorem

isSheaf_fppf_of_representableBy

L50 ↗

FppfRepresentableGroupSchemeSheaf.isSheaf_fppf_of_representableBy

Source context 6 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section TypeValued

Lean source · statement

theorem isSheaf_fppf_of_representableBy (P : Scheme.{u}ᵒᵖ ⥤ Type u) {G : Scheme.{u}}
    (h : P.RepresentableBy G) :
    Presheaf.IsSheaf Scheme.fppfTopology P

theorem

presieve_isSheaf_fppf_of_isRepresentable

L56 ↗

FppfRepresentableGroupSchemeSheaf.presieve_isSheaf_fppf_of_isRepresentable

Source context 6 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section TypeValued

Lean source · statement

theorem presieve_isSheaf_fppf_of_isRepresentable (P : Scheme.{u}ᵒᵖ ⥤ Type u)
    [P.IsRepresentable] : Presieve.IsSheaf Scheme.fppfTopology P

theorem

isSheaf_fppf_monCat_of_forget_isRepresentable

L64 ↗

FppfRepresentableGroupSchemeSheaf.isSheaf_fppf_monCat_of_forget_isRepresentable

Source context 6 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section StructuredValues

Lean source · statement

theorem isSheaf_fppf_monCat_of_forget_isRepresentable (F : Scheme.{u}ᵒᵖ ⥤ MonCat.{u})
    [(F ⋙ forget MonCat).IsRepresentable] :
    Presheaf.IsSheaf Scheme.fppfTopology F

theorem

isSheaf_fppf_grpCat_of_forget_isRepresentable

L70 ↗

FppfRepresentableGroupSchemeSheaf.isSheaf_fppf_grpCat_of_forget_isRepresentable

Source context 6 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section StructuredValues

Lean source · statement

theorem isSheaf_fppf_grpCat_of_forget_isRepresentable (F : Scheme.{u}ᵒᵖ ⥤ GrpCat.{u})
    [(F ⋙ forget GrpCat).IsRepresentable] :
    Presheaf.IsSheaf Scheme.fppfTopology F

theorem

isSheaf_fppf_commGrpCat_of_forget_isRepresentable

L76 ↗

FppfRepresentableGroupSchemeSheaf.isSheaf_fppf_commGrpCat_of_forget_isRepresentable

Source context 6 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section StructuredValues

Lean source · statement

theorem isSheaf_fppf_commGrpCat_of_forget_isRepresentable (F : Scheme.{u}ᵒᵖ ⥤ CommGrpCat.{u})
    [(F ⋙ forget CommGrpCat).IsRepresentable] :
    Presheaf.IsSheaf Scheme.fppfTopology F

theorem

isSheaf_fppf_ab_of_forget_isRepresentable

L82 ↗

FppfRepresentableGroupSchemeSheaf.isSheaf_fppf_ab_of_forget_isRepresentable

Source context 6 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section StructuredValues

Lean source · statement

theorem isSheaf_fppf_ab_of_forget_isRepresentable (F : Scheme.{u}ᵒᵖ ⥤ AddCommGrpCat.{u})
    [(F ⋙ forget AddCommGrpCat).IsRepresentable] :
    Presheaf.IsSheaf Scheme.fppfTopology F

theorem

isSheaf_fppf_yonedaGrpObj

L94 ↗

FppfRepresentableGroupSchemeSheaf.isSheaf_fppf_yonedaGrpObj

Source context 7 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section GroupSchemeOverZ
variable (G : Scheme.{u}) [GrpObj G]

Lean source · statement

theorem isSheaf_fppf_yonedaGrpObj :
    Presheaf.IsSheaf Scheme.fppfTopology (yonedaGrpObj G)

def

fppfGrpSheaf

L101 ↗

FppfRepresentableGroupSchemeSheaf.fppfGrpSheaf

Documentation

The fppf sheaf of groups represented by the group scheme.

Source context 7 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section GroupSchemeOverZ
variable (G : Scheme.{u}) [GrpObj G]

Lean source · statement

def fppfGrpSheaf : Sheaf Scheme.fppfTopology GrpCat.{u}

def

yonedaCommGrpObj

L107 ↗

FppfRepresentableGroupSchemeSheaf.yonedaCommGrpObj

Documentation

The commutative-group-valued functor of points of the commutative group scheme.

Source context 8 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section GroupSchemeOverZ
variable (G : Scheme.{u}) [GrpObj G]
variable [IsCommMonObj G]

Lean source · full declaration

def yonedaCommGrpObj : Scheme.{u}ᵒᵖ ⥤ CommGrpCat.{u} where
  obj T := CommGrpCat.of (unop T ⟶ G)
  map φ := CommGrpCat.ofHom ((yonedaGrpObj G).map φ).hom
  map_id _ := CommGrpCat.hom_ext (MonoidHom.ext fun g => Category.id_comp g)
  map_comp φ ψ := CommGrpCat.hom_ext (MonoidHom.ext fun g => Category.assoc ψ.unop φ.unop g)

def

yonedaCommGrpObjRepresentableBy

L114 ↗

FppfRepresentableGroupSchemeSheaf.yonedaCommGrpObjRepresentableBy

Documentation

The representation of the underlying functor of points by the commutative group scheme.

Source context 8 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section GroupSchemeOverZ
variable (G : Scheme.{u}) [GrpObj G]
variable [IsCommMonObj G]

Lean source · full declaration

def yonedaCommGrpObjRepresentableBy :
    (yonedaCommGrpObj G ⋙ forget CommGrpCat).RepresentableBy G where
  homEquiv := Equiv.refl _
  homEquiv_comp _ _ := rfl

theorem

isSheaf_fppf_yonedaCommGrpObj

L119 ↗

FppfRepresentableGroupSchemeSheaf.isSheaf_fppf_yonedaCommGrpObj

Source context 8 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section GroupSchemeOverZ
variable (G : Scheme.{u}) [GrpObj G]
variable [IsCommMonObj G]

Lean source · statement

theorem isSheaf_fppf_yonedaCommGrpObj :
    Presheaf.IsSheaf Scheme.fppfTopology (yonedaCommGrpObj G)

def

fppfCommGrpSheaf

L126 ↗

FppfRepresentableGroupSchemeSheaf.fppfCommGrpSheaf

Documentation

The fppf sheaf of commutative groups represented by the commutative group scheme.

Source context 8 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section GroupSchemeOverZ
variable (G : Scheme.{u}) [GrpObj G]
variable [IsCommMonObj G]

Lean source · statement

def fppfCommGrpSheaf : Sheaf Scheme.fppfTopology CommGrpCat.{u}

def

yonedaAddCommGrpObj

L130 ↗

FppfRepresentableGroupSchemeSheaf.yonedaAddCommGrpObj

Documentation

The functor of points of the commutative group scheme written additively.

Source context 8 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section GroupSchemeOverZ
variable (G : Scheme.{u}) [GrpObj G]
variable [IsCommMonObj G]

Lean source · statement

def yonedaAddCommGrpObj : Scheme.{u}ᵒᵖ ⥤ AddCommGrpCat.{u}

theorem

isSheaf_fppf_yonedaAddCommGrpObj

L133 ↗

FppfRepresentableGroupSchemeSheaf.isSheaf_fppf_yonedaAddCommGrpObj

Source context 8 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section GroupSchemeOverZ
variable (G : Scheme.{u}) [GrpObj G]
variable [IsCommMonObj G]

Lean source · statement

theorem isSheaf_fppf_yonedaAddCommGrpObj :
    Presheaf.IsSheaf Scheme.fppfTopology (yonedaAddCommGrpObj G)

def

fppfAbelianSheaf

L139 ↗

FppfRepresentableGroupSchemeSheaf.fppfAbelianSheaf

Documentation

The abelian fppf sheaf associated with the commutative group scheme.

Source context 8 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section GroupSchemeOverZ
variable (G : Scheme.{u}) [GrpObj G]
variable [IsCommMonObj G]

Lean source · statement

def fppfAbelianSheaf : Sheaf Scheme.fppfTopology AddCommGrpCat.{u}

def

fppfGrpSheafSectionsMulEquiv

L149 ↗

FppfRepresentableGroupSchemeSheaf.fppfGrpSheafSectionsMulEquiv

Documentation

The multiplicative equivalence between sheaf sections and points of the group scheme.

Source context 7 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section SectionsIdentification
variable (G : Scheme.{u}) [GrpObj G]

Lean source · statement

def fppfGrpSheafSectionsMulEquiv (T : Scheme.{u}) :
    ((fppfGrpSheaf G).obj.obj (op T)) ≃* (T ⟶ G)

def

fppfCommGrpSheafSectionsMulEquiv

L156 ↗

FppfRepresentableGroupSchemeSheaf.fppfCommGrpSheafSectionsMulEquiv

Documentation

The multiplicative equivalence between sections and points of the commutative group scheme.

Source context 8 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section SectionsIdentification
variable (G : Scheme.{u}) [GrpObj G]
variable [IsCommMonObj G]

Lean source · statement

def fppfCommGrpSheafSectionsMulEquiv (T : Scheme.{u}) :
    ((fppfCommGrpSheaf G).obj.obj (op T)) ≃* (T ⟶ G)

def

fppfAbelianSheafSectionsAddEquiv

L162 ↗

FppfRepresentableGroupSchemeSheaf.fppfAbelianSheafSectionsAddEquiv

Documentation

The additive equivalence between abelian sheaf sections and group-scheme points written additively.

Source context 8 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section SectionsIdentification
variable (G : Scheme.{u}) [GrpObj G]
variable [IsCommMonObj G]

Lean source · statement

def fppfAbelianSheafSectionsAddEquiv (T : Scheme.{u}) :
    ((fppfAbelianSheaf G).obj.obj (op T)) ≃+ Additive (T ⟶ G)

def

fppfAbelianSheafGlobalSectionsAddEquiv

L167 ↗

FppfRepresentableGroupSchemeSheaf.fppfAbelianSheafGlobalSectionsAddEquiv

Documentation

The identification of global abelian sheaf sections with points over the terminal scheme.

Source context 8 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section SectionsIdentification
variable (G : Scheme.{u}) [GrpObj G]
variable [IsCommMonObj G]

Lean source · statement

def fppfAbelianSheafGlobalSectionsAddEquiv :
    ((fppfAbelianSheaf G).obj.obj (op (𝟙_ Scheme.{u}))) ≃+ Additive (𝟙_ Scheme.{u} ⟶ G)

abbrev

fppfTopologyOver

L178 ↗

FppfRepresentableGroupSchemeSheaf.fppfTopologyOver

Documentation

The fppf topology on the category of schemes over the specified base.

Source context 7 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section GroupSchemeOverBase
variable (S : Scheme.{u})

Lean source · statement

abbrev fppfTopologyOver : GrothendieckTopology (Over S)

theorem

isSheaf_fppfOver_yonedaGrpObj

L185 ↗

FppfRepresentableGroupSchemeSheaf.isSheaf_fppfOver_yonedaGrpObj

Source context 8 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section GroupSchemeOverBase
variable (S : Scheme.{u})
variable (G : Over S) [GrpObj G]

Lean source · statement

theorem isSheaf_fppfOver_yonedaGrpObj :
    Presheaf.IsSheaf (fppfTopologyOver S) (yonedaGrpObj G)

def

fppfOverGrpSheaf

L194 ↗

FppfRepresentableGroupSchemeSheaf.fppfOverGrpSheaf

Documentation

The group-valued fppf sheaf represented by the group object over the base.

Source context 8 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section GroupSchemeOverBase
variable (S : Scheme.{u})
variable (G : Over S) [GrpObj G]

Lean source · statement

def fppfOverGrpSheaf : Sheaf (fppfTopologyOver S) GrpCat.{u}

def

yonedaCommGrpObjOver

L200 ↗

FppfRepresentableGroupSchemeSheaf.yonedaCommGrpObjOver

Documentation

The commutative-group-valued functor of points over the base scheme.

Source context 9 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section GroupSchemeOverBase
variable (S : Scheme.{u})
variable (G : Over S) [GrpObj G]
variable [IsCommMonObj G]

Lean source · full declaration

def yonedaCommGrpObjOver : (Over S)ᵒᵖ ⥤ CommGrpCat.{u} where
  obj T := CommGrpCat.of (unop T ⟶ G)
  map φ := CommGrpCat.ofHom ((yonedaGrpObj G).map φ).hom
  map_id _ := CommGrpCat.hom_ext (MonoidHom.ext fun g => Category.id_comp g)
  map_comp φ ψ := CommGrpCat.hom_ext (MonoidHom.ext fun g => Category.assoc ψ.unop φ.unop g)

def

yonedaCommGrpObjOverRepresentableBy

L207 ↗

FppfRepresentableGroupSchemeSheaf.yonedaCommGrpObjOverRepresentableBy

Documentation

The representation of the relative functor of points by the commutative group object.

Source context 9 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section GroupSchemeOverBase
variable (S : Scheme.{u})
variable (G : Over S) [GrpObj G]
variable [IsCommMonObj G]

Lean source · full declaration

def yonedaCommGrpObjOverRepresentableBy :
    (yonedaCommGrpObjOver S G ⋙ forget CommGrpCat).RepresentableBy G where
  homEquiv := Equiv.refl _
  homEquiv_comp _ _ := rfl

theorem

isSheaf_fppfOver_yonedaCommGrpObjOver

L212 ↗

FppfRepresentableGroupSchemeSheaf.isSheaf_fppfOver_yonedaCommGrpObjOver

Source context 9 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section GroupSchemeOverBase
variable (S : Scheme.{u})
variable (G : Over S) [GrpObj G]
variable [IsCommMonObj G]

Lean source · statement

theorem isSheaf_fppfOver_yonedaCommGrpObjOver :
    Presheaf.IsSheaf (fppfTopologyOver S) (yonedaCommGrpObjOver S G)

def

yonedaAddCommGrpObjOver

L221 ↗

FppfRepresentableGroupSchemeSheaf.yonedaAddCommGrpObjOver

Documentation

The relative functor of points of the commutative group object written additively.

Source context 9 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section GroupSchemeOverBase
variable (S : Scheme.{u})
variable (G : Over S) [GrpObj G]
variable [IsCommMonObj G]

Lean source · statement

def yonedaAddCommGrpObjOver : (Over S)ᵒᵖ ⥤ AddCommGrpCat.{u}

theorem

isSheaf_fppfOver_yonedaAddCommGrpObjOver

L224 ↗

FppfRepresentableGroupSchemeSheaf.isSheaf_fppfOver_yonedaAddCommGrpObjOver

Source context 9 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section GroupSchemeOverBase
variable (S : Scheme.{u})
variable (G : Over S) [GrpObj G]
variable [IsCommMonObj G]

Lean source · statement

theorem isSheaf_fppfOver_yonedaAddCommGrpObjOver :
    Presheaf.IsSheaf (fppfTopologyOver S) (yonedaAddCommGrpObjOver S G)

def

fppfOverAbelianSheaf

L230 ↗

FppfRepresentableGroupSchemeSheaf.fppfOverAbelianSheaf

Documentation

The abelian fppf sheaf represented by the commutative group object over the base.

Source context 9 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section GroupSchemeOverBase
variable (S : Scheme.{u})
variable (G : Over S) [GrpObj G]
variable [IsCommMonObj G]

Lean source · statement

def fppfOverAbelianSheaf : Sheaf (fppfTopologyOver S) AddCommGrpCat.{u}

def

fppfOverAbelianSheafSectionsAddEquiv

L234 ↗

FppfRepresentableGroupSchemeSheaf.fppfOverAbelianSheafSectionsAddEquiv

Documentation

The identification of relative abelian sheaf sections with points written additively.

Source context 9 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section GroupSchemeOverBase
variable (S : Scheme.{u})
variable (G : Over S) [GrpObj G]
variable [IsCommMonObj G]

Lean source · statement

def fppfOverAbelianSheafSectionsAddEquiv (T : Over S) :
    ((fppfOverAbelianSheaf S G).obj.obj (op T)) ≃+ Additive (T ⟶ G)

def

unitsPresheaf

L245 ↗

FppfRepresentableGroupSchemeSheaf.unitsPresheaf

Documentation

The presheaf of unit groups of a presheaf of commutative rings.

Source context 7 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section UnitsDescent
variable {C : Type u₁} [Category.{v₁} C]

Lean source · statement

def unitsPresheaf (O : Cᵒᵖ ⥤ CommRingCat.{w}) : Cᵒᵖ ⥤ CommGrpCat.{w}

theorem

presieve_isSheaf_units

L248 ↗

FppfRepresentableGroupSchemeSheaf.presieve_isSheaf_units

Source context 7 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section UnitsDescent
variable {C : Type u₁} [Category.{v₁} C]

Lean source · statement

theorem presieve_isSheaf_units {J : GrothendieckTopology C} {O : Cᵒᵖ ⥤ CommRingCat.{w}}
    (hO : Presieve.IsSheaf J (O ⋙ forget CommRingCat)) :
    Presieve.IsSheaf J (unitsPresheaf O ⋙ forget CommGrpCat)

abbrev

affineLineOverZ

L299 ↗

FppfRepresentableGroupSchemeSheaf.affineLineOverZ

Documentation

The affine line over the integers, with the specified universe lift.

Source context 6 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section Instances

Lean source · statement

abbrev affineLineOverZ : Scheme.{u}

def

gammaRepresentableBy

L303 ↗

FppfRepresentableGroupSchemeSheaf.gammaRepresentableBy

Documentation

The representation of the global-sections functor by the affine line over the integers.

Source context 6 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section Instances

Lean source · full declaration

def gammaRepresentableBy :
    (Scheme.Γ.{u} ⋙ forget CommRingCat).RepresentableBy affineLineOverZ.{u} where
  homEquiv {X} := (AffineSpace.toSpecMvPolyIntEquiv PUnit.{u + 1} (X := X)).trans
    (Equiv.funUnique PUnit.{u + 1} _)
  homEquiv_comp f g := by
    change AffineSpace.toSpecMvPolyIntEquiv _ (f ≫ g) PUnit.unit = _
    rw [AffineSpace.toSpecMvPolyIntEquiv_comp]
    rfl

theorem

presieve_isSheaf_fppf_gammaForget

L312 ↗

FppfRepresentableGroupSchemeSheaf.presieve_isSheaf_fppf_gammaForget

Source context 6 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section Instances

Lean source · statement

theorem presieve_isSheaf_fppf_gammaForget :
    Presieve.IsSheaf Scheme.fppfTopology.{u} (Scheme.Γ ⋙ forget CommRingCat)

def

Gm

L319 ↗

FppfRepresentableGroupSchemeSheaf.Gm

Documentation

The multiplicative-group presheaf of units in global sections.

Source context 6 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section Instances

Lean source · statement

def Gm : Scheme.{u}ᵒᵖ ⥤ CommGrpCat.{u}

theorem

isSheaf_fppf_Gm

L322 ↗

FppfRepresentableGroupSchemeSheaf.isSheaf_fppf_Gm

Source context 6 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section Instances

Lean source · statement

theorem isSheaf_fppf_Gm : Presheaf.IsSheaf Scheme.fppfTopology.{u} Gm.{u}

def

GmSheaf

L328 ↗

FppfRepresentableGroupSchemeSheaf.GmSheaf

Documentation

The multiplicative group as an fppf sheaf of commutative groups.

Source context 6 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section Instances

Lean source · statement

def GmSheaf : Sheaf Scheme.fppfTopology.{u} CommGrpCat.{u}

def

GmSectionsMulEquiv

L332 ↗

FppfRepresentableGroupSchemeSheaf.GmSectionsMulEquiv

Documentation

The identification of multiplicative-group sections with units in the global section ring.

Source context 6 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section Instances

Lean source · statement

def GmSectionsMulEquiv (X : Scheme.{u}) :
    ((Gm.{u}).obj (op X) : Type u) ≃* ((Γ(X, ⊤) : Type u))ˣ

def

GmAbelianSheaf

L337 ↗

FppfRepresentableGroupSchemeSheaf.GmAbelianSheaf

Documentation

The multiplicative group as an abelian fppf sheaf, written additively.

Source context 6 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section Instances

Lean source · statement

def GmAbelianSheaf : Sheaf Scheme.fppfTopology.{u} AddCommGrpCat.{u}

def

mu

L343 ↗

FppfRepresentableGroupSchemeSheaf.mu

Documentation

The presheaf of homomorphisms from the cyclic group into the multiplicative group.

Source context 6 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section Instances

Lean source · statement

def mu (n : ℕ) : Scheme.{u}ᵒᵖ ⥤ Type u

theorem

presieve_isSheaf_fppf_mu

L346 ↗

FppfRepresentableGroupSchemeSheaf.presieve_isSheaf_fppf_mu

Source context 6 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section Instances

Lean source · statement

theorem presieve_isSheaf_fppf_mu (n : ℕ) :
    Presieve.IsSheaf Scheme.fppfTopology.{u} (mu.{u} n)

theorem

mu_obj

L350 ↗

FppfRepresentableGroupSchemeSheaf.mu_obj

Source context 6 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section Instances

Lean source · statement

theorem mu_obj (n : ℕ) (X : Scheme.{u}) :
    (mu.{u} n).obj (op X) =
      (CommGrpCat.of (ULift.{u} (Multiplicative (ZMod n))) ⟶ Gm.{u}.obj (op X))

instance

(anonymous instance)

L359 ↗

Source context 8 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section Instances
section ConstantZMod
variable (n : ℕ)

Lean source · statement

instance : TopologicalSpace (ZMod n)

instance

(anonymous instance)

L361 ↗

Source context 9 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section Instances
section ConstantZMod
variable (n : ℕ)
local instance : TopologicalSpace (ZMod n) := ⊥

Lean source · statement

instance : DiscreteTopology (ZMod n)

instance

(anonymous instance)

L363 ↗

Source context 10 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section Instances
section ConstantZMod
variable (n : ℕ)
local instance : TopologicalSpace (ZMod n) := ⊥
local instance : DiscreteTopology (ZMod n) := ⟨rfl⟩

Lean source · full declaration

instance : IsTopologicalAddGroup (ZMod n) where
  continuous_add := continuous_of_discreteTopology
  continuous_neg := continuous_of_discreteTopology

def

constantZMod

L368 ↗

FppfRepresentableGroupSchemeSheaf.constantZMod

Documentation

The presheaf of locally constant functions with values in the additive group ZMod n.

Source context 11 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section Instances
section ConstantZMod
variable (n : ℕ)
local instance : TopologicalSpace (ZMod n) := ⊥
local instance : DiscreteTopology (ZMod n) := ⟨rfl⟩
local instance : IsTopologicalAddGroup (ZMod n) where
  continuous_add := continuous_of_discreteTopology
  continuous_neg := continuous_of_discreteTopology

Lean source · statement

def constantZMod : Scheme.{u}ᵒᵖ ⥤ AddCommGrpCat.{u}

theorem

isSheaf_fppf_constantZMod

L371 ↗

FppfRepresentableGroupSchemeSheaf.isSheaf_fppf_constantZMod

Source context 11 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section Instances
section ConstantZMod
variable (n : ℕ)
local instance : TopologicalSpace (ZMod n) := ⊥
local instance : DiscreteTopology (ZMod n) := ⟨rfl⟩
local instance : IsTopologicalAddGroup (ZMod n) where
  continuous_add := continuous_of_discreteTopology
  continuous_neg := continuous_of_discreteTopology

Lean source · statement

theorem isSheaf_fppf_constantZMod :
    Presheaf.IsSheaf Scheme.fppfTopology.{u} (constantZMod.{u} n)

def

constantZModSheaf

L377 ↗

FppfRepresentableGroupSchemeSheaf.constantZModSheaf

Documentation

The fppf sheaf of locally constant functions with values in ZMod n.

Source context 11 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section Instances
section ConstantZMod
variable (n : ℕ)
local instance : TopologicalSpace (ZMod n) := ⊥
local instance : DiscreteTopology (ZMod n) := ⟨rfl⟩
local instance : IsTopologicalAddGroup (ZMod n) where
  continuous_add := continuous_of_discreteTopology
  continuous_neg := continuous_of_discreteTopology

Lean source · statement

def constantZModSheaf : Sheaf Scheme.fppfTopology.{u} AddCommGrpCat.{u}

instance

(anonymous instance)

L386 ↗

Source context 6 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section Gates

Lean source · full declaration

instance : IsCommMonObj (𝟙_ Scheme.{u}) where
  mul_comm := isTerminalTensorUnit.hom_ext _ _

def

gateTrivialGroupSchemeAbelianSheaf

L390 ↗

FppfRepresentableGroupSchemeSheaf.gateTrivialGroupSchemeAbelianSheaf

Documentation

The abelian fppf sheaf associated to the trivial group scheme.

Source context 6 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section Gates

Lean source · statement

def gateTrivialGroupSchemeAbelianSheaf : Sheaf Scheme.fppfTopology AddCommGrpCat.{u}

instance

gateTrivialSheafSectionsSubsingleton

L393 ↗

FppfRepresentableGroupSchemeSheaf.gateTrivialSheafSectionsSubsingleton

Source context 6 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section Gates

Lean source · statement

instance gateTrivialSheafSectionsSubsingleton (T : Scheme.{u}) :
    Subsingleton ((gateTrivialGroupSchemeAbelianSheaf.{u}).obj.obj (op T))

theorem

gate_singleton_generates_fppf_cover

L400 ↗

FppfRepresentableGroupSchemeSheaf.gate_singleton_generates_fppf_cover

Source context 6 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section Gates

Lean source · statement

theorem gate_singleton_generates_fppf_cover {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f]
    [Surjective f] [LocallyOfFinitePresentation f] :
    Sieve.generate (Presieve.singleton f) ∈ Scheme.fppfTopology Y

def

gateGmSectionsSpecZ

L409 ↗

FppfRepresentableGroupSchemeSheaf.gateGmSectionsSpecZ

Documentation

The multiplicative equivalence from sections of the multiplicative group over Spec ℤ to units of ℤ.

Source context 6 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section Gates

Lean source · statement

def gateGmSectionsSpecZ :
    ((Gm.{0}).obj (op (Spec (CommRingCat.of ℤ))) : Type 0) ≃* ℤˣ

theorem

gate_Gm_sections_nontrivial

L414 ↗

FppfRepresentableGroupSchemeSheaf.gate_Gm_sections_nontrivial

Source context 6 commands

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

noncomputable section
namespace FppfRepresentableGroupSchemeSheaf
open CategoryTheory AlgebraicGeometry Limits Opposite MonoidalCategory CartesianMonoidalCategory
open scoped CategoryTheory.MonObj
universe w v₁ u₁ u
section Gates

Lean source · statement

theorem gate_Gm_sections_nontrivial :
    Nontrivial ((Gm.{0}).obj (op (Spec (CommRingCat.of ℤ))) : Type 0)

Module documentation

Fppf Gm Representable

Declarations