Module

FppfSiteCohomology.lean

Nyll.AlgebraicCurves.Cohomology.Sheaves.FppfSiteCohomology

61 declarations indexed from sourceView source ↗

Module documentation

The small fppf site and its abelian sheaf cohomology.

Imports16

Mathlib.AlgebraicGeometry.Sites.Fpqc
Mathlib.AlgebraicGeometry.Sites.Etale
Mathlib.AlgebraicGeometry.Sites.Small
Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Mathlib.AlgebraicGeometry.Morphisms.Flat
Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
Mathlib.CategoryTheory.Sites.ConstantSheaf
Mathlib.CategoryTheory.Sites.Over
Mathlib.CategoryTheory.Limits.MorphismProperty
Mathlib.CategoryTheory.MorphismProperty.Limits
Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf
Mathlib.CategoryTheory.Abelian.GrothendieckCategory.HasExt
Mathlib.CategoryTheory.Adjunction.Additive
Mathlib.Algebra.Category.Grp.AB
Mathlib.Algebra.Category.Grp.Ulift
Mathlib.Algebra.Category.Grp.ForgetCorepresentable

Imported by1

Nyll.AlgebraicCurves.Cohomology.Sheaves.All

instance

(anonymous instance)

L38 ↗

Source context 3 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme

Lean source · full declaration

instance : MorphismProperty.IsMultiplicative @LocallyOfFinitePresentation where
  id_mem _ := inferInstance

abbrev

fppfProperty

L42 ↗

AlgebraicGeometry.Scheme.fppfProperty

Documentation

The morphism property of being flat and locally of finite presentation.

Source context 3 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme

Lean source · statement

abbrev fppfProperty : MorphismProperty Scheme.{u}

theorem

fppfProperty_isStableUnderBaseChange

L44 ↗

AlgebraicGeometry.Scheme.fppfProperty_isStableUnderBaseChange

Source context 3 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme

Lean source · statement

theorem fppfProperty_isStableUnderBaseChange :
    fppfProperty.{u}.IsStableUnderBaseChange

theorem

fppfProperty_isMultiplicative

L49 ↗

AlgebraicGeometry.Scheme.fppfProperty_isMultiplicative

Source context 3 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme

Lean source · statement

theorem fppfProperty_isMultiplicative : fppfProperty.{u}.IsMultiplicative

theorem

fppfProperty_isStableUnderComposition

L53 ↗

AlgebraicGeometry.Scheme.fppfProperty_isStableUnderComposition

Source context 3 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme

Lean source · statement

theorem fppfProperty_isStableUnderComposition :
    fppfProperty.{u}.IsStableUnderComposition

theorem

fppfProperty_respectsIso

L56 ↗

AlgebraicGeometry.Scheme.fppfProperty_respectsIso

Source context 3 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme

Lean source · statement

theorem fppfProperty_respectsIso : fppfProperty.{u}.RespectsIso

theorem

fppfProperty_containsIdentities

L63 ↗

AlgebraicGeometry.Scheme.fppfProperty_containsIdentities

Source context 3 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme

Lean source · statement

theorem fppfProperty_containsIdentities : fppfProperty.{u}.ContainsIdentities

theorem

fppfProperty_hasPullbacks

L65 ↗

AlgebraicGeometry.Scheme.fppfProperty_hasPullbacks

Source context 3 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme

Lean source · statement

theorem fppfProperty_hasPullbacks : fppfProperty.{u}.HasPullbacks

theorem

fppfPrecoverage_eq_precoverage_fppfProperty

L74 ↗

AlgebraicGeometry.Scheme.fppfPrecoverage_eq_precoverage_fppfProperty

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks

Lean source · statement

theorem fppfPrecoverage_eq_precoverage_fppfProperty :
    fppfPrecoverage.{u} = Scheme.precoverage fppfProperty

instance

(anonymous instance)

L77 ↗

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks

Lean source · statement

instance : fppfPrecoverage.{u}.HasIsos

instance

(anonymous instance)

L80 ↗

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks

Lean source · statement

instance : fppfPrecoverage.{u}.HasPullbacks

def

fppfPretopology

L84 ↗

AlgebraicGeometry.Scheme.fppfPretopology

Documentation

The pretopology generated by jointly surjective fppf covering families.

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks

Lean source · statement

def fppfPretopology : Pretopology Scheme.{u}

theorem

fppfTopology_eq_grothendieckTopology

L86 ↗

AlgebraicGeometry.Scheme.fppfTopology_eq_grothendieckTopology

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks

Lean source · statement

theorem fppfTopology_eq_grothendieckTopology :
    fppfTopology.{u} = Scheme.grothendieckTopology fppfProperty

theorem

fppfTopology_eq_toGrothendieck_fppfPretopology

L89 ↗

AlgebraicGeometry.Scheme.fppfTopology_eq_toGrothendieck_fppfPretopology

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks

Lean source · statement

theorem fppfTopology_eq_toGrothendieck_fppfPretopology :
    fppfTopology.{u} = fppfPretopology.toGrothendieck

theorem

etale_le_fppfProperty

L93 ↗

AlgebraicGeometry.Scheme.etale_le_fppfProperty

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks

Lean source · statement

theorem etale_le_fppfProperty : @Etale ≤ fppfProperty.{u}

theorem

etalePrecoverage_le_fppfPrecoverage

L98 ↗

AlgebraicGeometry.Scheme.etalePrecoverage_le_fppfPrecoverage

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks

Lean source · statement

theorem etalePrecoverage_le_fppfPrecoverage : etalePrecoverage.{u} ≤ fppfPrecoverage

theorem

etaleTopology_le_fppfTopology

L101 ↗

AlgebraicGeometry.Scheme.etaleTopology_le_fppfTopology

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks

Lean source · statement

theorem etaleTopology_le_fppfTopology : etaleTopology.{u} ≤ fppfTopology

theorem

zariskiTopology_le_fppfTopology

L104 ↗

AlgebraicGeometry.Scheme.zariskiTopology_le_fppfTopology

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks

Lean source · statement

theorem zariskiTopology_le_fppfTopology : zariskiTopology.{u} ≤ fppfTopology

def

Fppf

L110 ↗

AlgebraicGeometry.Scheme.Fppf

Documentation

The category of flat, locally finitely presented schemes over the base.

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks

Lean source · statement

def Fppf (S : Scheme.{u}) : Type (u + 1)

instance

(anonymous instance)

L112 ↗

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks

Lean source · statement

instance (S : Scheme.{u}) : Category.{u} S.Fppf

instance

(anonymous instance)

L119 ↗

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
namespace Fppf
variable (S : Scheme.{u})

Lean source · statement

instance (U : S.Fppf) : Flat U.hom

instance

(anonymous instance)

L120 ↗

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
namespace Fppf
variable (S : Scheme.{u})

Lean source · statement

instance (U : S.Fppf) : LocallyOfFinitePresentation U.hom

def

mk

L124 ↗

AlgebraicGeometry.Scheme.Fppf.mk

Documentation

View a flat, locally finitely presented morphism as an object of the small fppf site.

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
namespace Fppf
variable (S : Scheme.{u})
variable {S} in

Lean source · statement

def mk {X : Scheme.{u}} (f : X ⟶ S) [Flat f]
    [LocallyOfFinitePresentation f] : S.Fppf

def

forget

L129 ↗

AlgebraicGeometry.Scheme.Fppf.forget

Documentation

Forget the flatness and finite-presentation conditions on a scheme over the base.

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
namespace Fppf
variable (S : Scheme.{u})
variable {S} in

Lean source · statement

def forget : S.Fppf ⥤ Over S

instance

(anonymous instance)

L131 ↗

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
namespace Fppf
variable (S : Scheme.{u})
variable {S} in

Lean source · statement

instance : (Fppf.forget S).Full

instance

(anonymous instance)

L134 ↗

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
namespace Fppf
variable (S : Scheme.{u})
variable {S} in

Lean source · statement

instance : (Fppf.forget S).Faithful

def

smallFppfTopology

L140 ↗

AlgebraicGeometry.Scheme.smallFppfTopology

Documentation

The Grothendieck topology on the small fppf site of a scheme.

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks

Lean source · statement

def smallFppfTopology (S : Scheme.{u}) : GrothendieckTopology S.Fppf

theorem

overGrothendieckTopology_fppfProperty_eq

L143 ↗

AlgebraicGeometry.Scheme.overGrothendieckTopology_fppfProperty_eq

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks

Lean source · statement

theorem overGrothendieckTopology_fppfProperty_eq (S : Scheme.{u}) :
    S.overGrothendieckTopology fppfProperty = fppfTopology.over S

instance

(anonymous instance)

L146 ↗

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks

Lean source · statement

instance (S : Scheme.{u}) :
    (Fppf.forget S).LocallyCoverDense (fppfTopology.over S)

theorem

smallFppfTopology_eq_restrictedTopology

L152 ↗

AlgebraicGeometry.Scheme.smallFppfTopology_eq_restrictedTopology

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks

Lean source · statement

theorem smallFppfTopology_eq_restrictedTopology (S : Scheme.{u}) :
    smallFppfTopology S = (Fppf.forget S).restrictedTopology (fppfTopology.over S)

instance

(anonymous instance)

L155 ↗

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks

Lean source · statement

instance (S : Scheme.{u}) :
    (Fppf.forget S).IsCocontinuous (smallFppfTopology S) (fppfTopology.over S)

def

fppfTerminal

L166 ↗

AlgebraicGeometry.Scheme.fppfTerminal

Documentation

The identity morphism, as an object of the small fppf site.

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks

Lean source · statement

def fppfTerminal (S : Scheme.{u}) : S.Fppf

def

fppfTerminalIsTerminal

L170 ↗

AlgebraicGeometry.Scheme.fppfTerminalIsTerminal

Documentation

The identity morphism is terminal in the small fppf site.

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks

Lean source · statement

def fppfTerminalIsTerminal (S : Scheme.{u}) : IsTerminal (fppfTerminal S)

instance

(anonymous instance)

L173 ↗

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks

Lean source · statement

instance (S : Scheme.{u}) : HasTerminal S.Fppf

instance

hasSheafify_smallFppfTopology

L178 ↗

AlgebraicGeometry.Scheme.hasSheafify_smallFppfTopology

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
variable (S : Scheme.{u})

Lean source · statement

instance hasSheafify_smallFppfTopology : HasSheafify (smallFppfTopology S) Ab.{u + 1}

instance

abelian_sheaf_smallFppfTopology

L181 ↗

AlgebraicGeometry.Scheme.abelian_sheaf_smallFppfTopology

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
variable (S : Scheme.{u})

Lean source · statement

instance abelian_sheaf_smallFppfTopology :
    Abelian (Sheaf (smallFppfTopology S) Ab.{u + 1})

instance

isGrothendieckAbelian_sheaf_smallFppfTopology

L186 ↗

AlgebraicGeometry.Scheme.isGrothendieckAbelian_sheaf_smallFppfTopology

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
variable (S : Scheme.{u})

Lean source · statement

instance isGrothendieckAbelian_sheaf_smallFppfTopology :
    IsGrothendieckAbelian.{u + 1} (Sheaf (smallFppfTopology S) Ab.{u + 1})

instance

hasExt_sheaf_smallFppfTopology

L193 ↗

AlgebraicGeometry.Scheme.hasExt_sheaf_smallFppfTopology

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
variable (S : Scheme.{u})

Lean source · statement

instance hasExt_sheaf_smallFppfTopology :
    HasExt.{u + 1} (Sheaf (smallFppfTopology S) Ab.{u + 1})

def

fppfCohomology

L198 ↗

AlgebraicGeometry.Scheme.fppfCohomology

Documentation

The degree n cohomology of an abelian sheaf on the small fppf site.

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
variable (S : Scheme.{u})

Lean source · statement

def fppfCohomology (F : Sheaf (smallFppfTopology S) Ab.{u + 1}) (n : ℕ) :
    Type (u + 1)

instance

(anonymous instance)

L202 ↗

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
variable (S : Scheme.{u})

Lean source · statement

instance (F : Sheaf (smallFppfTopology S) Ab.{u + 1}) (n : ℕ) :
    AddCommGroup (fppfCohomology S F n)

instance

(anonymous instance)

L206 ↗

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
variable (S : Scheme.{u})

Lean source · full declaration

instance : (Functor.const (S.Fppf)ᵒᵖ : Ab.{u + 1} ⥤ ((S.Fppf)ᵒᵖ ⥤ Ab.{u + 1})).Additive where
  map_add := by intros; ext; rfl

instance

(anonymous instance)

L209 ↗

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
variable (S : Scheme.{u})

Lean source · statement

instance : (constantSheaf (smallFppfTopology S) Ab.{u + 1}).Additive

def

homULiftIntAddEquiv

L215 ↗

AlgebraicGeometry.Scheme.homULiftIntAddEquiv

Documentation

Identify morphisms from the lifted integers with elements of an abelian group.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
variable (S : Scheme.{u})
universe w in

Lean source · statement

def homULiftIntAddEquiv (A : Ab.{w}) :
    (AddCommGrpCat.of (ULift.{w} ℤ) ⟶ A) ≃+ A

def

sheafHZeroAddEquiv

L227 ↗

AlgebraicGeometry.Scheme.sheafHZeroAddEquiv

Documentation

Identify degree-zero sheaf cohomology with sections on the terminal object.

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
variable (S : Scheme.{u})
universe w in
open Abelian in

Lean source · statement

def sheafHZeroAddEquiv (F : Sheaf (smallFppfTopology S) Ab.{u + 1}) :
    F.H 0 ≃+ F.obj.obj (op (fppfTerminal S))

def

fppfCohomologyZeroAddEquiv

L235 ↗

AlgebraicGeometry.Scheme.fppfCohomologyZeroAddEquiv

Documentation

Identify degree-zero fppf cohomology with global sections.

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
variable (S : Scheme.{u})
universe w in
open Abelian in

Lean source · statement

def fppfCohomologyZeroAddEquiv (F : Sheaf (smallFppfTopology S) Ab.{u + 1}) :
    fppfCohomology S F 0 ≃+ F.obj.obj (op (fppfTerminal S))

def

sheafHMap

L241 ↗

AlgebraicGeometry.Scheme.sheafHMap

Documentation

The additive map on sheaf cohomology induced by a sheaf morphism.

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
variable (S : Scheme.{u})
universe w in
open Abelian in

Lean source · statement

def sheafHMap {F G : Sheaf (smallFppfTopology S) Ab.{u + 1}} (φ : F ⟶ G)
    (n : ℕ) : F.H n →+ G.H n

def

fppfCohomologyMap

L248 ↗

AlgebraicGeometry.Scheme.fppfCohomologyMap

Documentation

The map on fppf cohomology induced by a morphism of abelian sheaves.

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
variable (S : Scheme.{u})
universe w in
open Abelian in

Lean source · statement

def fppfCohomologyMap {F G : Sheaf (smallFppfTopology S) Ab.{u + 1}} (φ : F ⟶ G)
    (n : ℕ) : fppfCohomology S F n →+ fppfCohomology S G n

theorem

sheafHMap_id

L253 ↗

AlgebraicGeometry.Scheme.sheafHMap_id

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
variable (S : Scheme.{u})
universe w in
open Abelian in

Lean source · statement

theorem sheafHMap_id {F : Sheaf (smallFppfTopology S) Ab.{u + 1}} (n : ℕ)
    (α : F.H n) :
    sheafHMap S (𝟙 F) n α = α

theorem

fppfCohomologyMap_id

L260 ↗

AlgebraicGeometry.Scheme.fppfCohomologyMap_id

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
variable (S : Scheme.{u})
universe w in
open Abelian in

Lean source · statement

theorem fppfCohomologyMap_id {F : Sheaf (smallFppfTopology S) Ab.{u + 1}} (n : ℕ)
    (α : fppfCohomology S F n) :
    fppfCohomologyMap S (𝟙 F) n α = α

theorem

sheafHMap_comp

L266 ↗

AlgebraicGeometry.Scheme.sheafHMap_comp

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
variable (S : Scheme.{u})
universe w in
open Abelian in

Lean source · statement

theorem sheafHMap_comp {F G H' : Sheaf (smallFppfTopology S) Ab.{u + 1}}
    (φ : F ⟶ G) (ψ : G ⟶ H') (n : ℕ) (α : F.H n) :
    sheafHMap S (φ ≫ ψ) n α = sheafHMap S ψ n (sheafHMap S φ n α)

theorem

fppfCohomologyMap_comp

L274 ↗

AlgebraicGeometry.Scheme.fppfCohomologyMap_comp

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
variable (S : Scheme.{u})
universe w in
open Abelian in

Lean source · statement

theorem fppfCohomologyMap_comp {F G H' : Sheaf (smallFppfTopology S) Ab.{u + 1}}
    (φ : F ⟶ G) (ψ : G ⟶ H') (n : ℕ) (α : fppfCohomology S F n) :
    fppfCohomologyMap S (φ ≫ ψ) n α = fppfCohomologyMap S ψ n (fppfCohomologyMap S φ n α)

def

fppfCohomologyFunctor

L280 ↗

AlgebraicGeometry.Scheme.fppfCohomologyFunctor

Documentation

Degree n fppf cohomology as a functor to abelian groups.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
variable (S : Scheme.{u})
universe w in

Lean source · statement

def fppfCohomologyFunctor (n : ℕ) :
    Sheaf (smallFppfTopology S) Ab.{u + 1} ⥤ Ab.{u + 1}

theorem

fppfCohomologyFunctor_obj_carrier

L284 ↗

AlgebraicGeometry.Scheme.fppfCohomologyFunctor_obj_carrier

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
variable (S : Scheme.{u})
universe w in

Lean source · statement

theorem fppfCohomologyFunctor_obj_carrier (n : ℕ) (F : Sheaf (smallFppfTopology S) Ab.{u + 1}) :
    ((fppfCohomologyFunctor S n).obj F : Type (u + 1)) = F.H n

def

fppfBigToOverRestriction

L289 ↗

AlgebraicGeometry.Scheme.fppfBigToOverRestriction

Documentation

Restrict a sheaf on the big fppf site to schemes over the fixed base.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
variable (S : Scheme.{u})
universe w in

Lean source · statement

def fppfBigToOverRestriction :
    Sheaf fppfTopology.{u} Ab.{u + 1} ⥤ Sheaf (fppfTopology.{u}.over S) Ab.{u + 1}

def

fppfSmallToOverPushforward

L294 ↗

AlgebraicGeometry.Scheme.fppfSmallToOverPushforward

Documentation

Push a sheaf on the small fppf site to the fppf over-site.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
variable (S : Scheme.{u})
universe w in

Lean source · statement

def fppfSmallToOverPushforward :
    Sheaf (smallFppfTopology S) Ab.{u + 1} ⥤ Sheaf (fppfTopology.{u}.over S) Ab.{u + 1}

theorem

gate_zero_sheaf_subsingleton

L300 ↗

AlgebraicGeometry.Scheme.gate_zero_sheaf_subsingleton

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
variable (S : Scheme.{u})
universe w in
open ZeroObject in

Lean source · statement

theorem gate_zero_sheaf_subsingleton (n : ℕ) :
    Subsingleton (fppfCohomology S (0 : Sheaf (smallFppfTopology S) Ab.{u + 1}) n)

theorem

gate_H0_nontrivial_of_sections_nontrivial

L305 ↗

AlgebraicGeometry.Scheme.gate_H0_nontrivial_of_sections_nontrivial

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
variable (S : Scheme.{u})
universe w in

Lean source · statement

theorem gate_H0_nontrivial_of_sections_nontrivial (F : Sheaf (smallFppfTopology S) Ab.{u + 1})
    (h : Nontrivial (F.obj.obj (op (fppfTerminal S)))) :
    Nontrivial (fppfCohomology S F 0)

theorem

gate_H0_equiv_fires_on_zero_sheaf

L311 ↗

AlgebraicGeometry.Scheme.gate_H0_equiv_fires_on_zero_sheaf

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
variable (S : Scheme.{u})
universe w in
open ZeroObject in

Lean source · statement

theorem gate_H0_equiv_fires_on_zero_sheaf :
    Subsingleton
      (((0 : Sheaf (smallFppfTopology S) Ab.{u + 1}).obj.obj (op (fppfTerminal S))) :
        Type (u + 1))

abbrev

specInt

L323 ↗

AlgebraicGeometry.Scheme.specInt

Documentation

The spectrum of the integers.

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
variable (S : Scheme.{u})
universe w in
section SpecInt

Lean source · statement

abbrev specInt : Scheme.{0}

def

fppfCohomologySpecIntZeroAddEquiv

L331 ↗

AlgebraicGeometry.Scheme.fppfCohomologySpecIntZeroAddEquiv

Documentation

Identify degree-zero fppf cohomology over the integers with global sections.

Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
variable (S : Scheme.{u})
universe w in
section SpecInt
open Abelian in

Lean source · statement

def fppfCohomologySpecIntZeroAddEquiv
    (F : Sheaf (smallFppfTopology specInt) Ab.{1}) :
    fppfCohomology specInt F 0 ≃+ F.obj.obj (op (fppfTerminal specInt))

theorem

gate_specInt_H1_zero_sheaf_subsingleton

L337 ↗

AlgebraicGeometry.Scheme.gate_specInt_H1_zero_sheaf_subsingleton

Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.Scheme
attribute [instance] fppfProperty_isStableUnderBaseChange fppfProperty_isMultiplicative
  fppfProperty_isStableUnderComposition fppfProperty_respectsIso
  fppfProperty_containsIdentities fppfProperty_hasPullbacks
variable (S : Scheme.{u})
universe w in
section SpecInt
open ZeroObject in

Lean source · statement

theorem gate_specInt_H1_zero_sheaf_subsingleton :
    Subsingleton (fppfCohomology specInt (0 : Sheaf (smallFppfTopology specInt) Ab.{1}) 1)

Module documentation

Declarations