Module

HenselianLocal.lean

Nyll.EtaleCohomology.Classical.HenselianLocal

5 declarations indexed from sourceView source ↗

Module documentation

Classical cohomology of a strictly local spectrum

The already constructed lifting of global sections supplies preservation of epimorphisms by the actual global-sections functor. Its constant-sheaf adjunction supplies preservation of kernels, hence exactness.

For abelian sheaves, the same maximal-covering-sieve result makes global sections preserve epimorphisms. The constant integer sheaf is therefore projective. Positive-degree Sheaf.H vanishes by the existing Ext theorem for a projective first argument. The coefficient-module statement uses the existing etaleCohomology definition, without a replacement cohomology or a comparison premise.

Imports25

Nyll.EtaleCohomology.Classical.Etale
Nyll.EtaleCohomology.Classical.ModuleCohomology
Nyll.EtaleCohomology.Sites.HenselianLocal
Mathlib.Algebra.Category.Grp.AB
Mathlib.Algebra.Category.Grp.Adjunctions
Mathlib.Algebra.Category.Grp.EpiMono
Mathlib.Algebra.Category.Grp.ForgetCorepresentable
Mathlib.Algebra.Category.ModuleCat.Basic
Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
Mathlib.AlgebraicGeometry.Sites.AffineEtale
Mathlib.CategoryTheory.Abelian.Exact
Mathlib.CategoryTheory.Abelian.GrothendieckCategory.HasExt
Mathlib.CategoryTheory.Adjunction.Limits
Mathlib.CategoryTheory.ConcreteCategory.Basic
Mathlib.CategoryTheory.Functor.EpiMono
Mathlib.CategoryTheory.Limits.MorphismProperty
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Mathlib.CategoryTheory.Preadditive.Projective.Basic
Mathlib.CategoryTheory.Sites.ConstantSheaf
Mathlib.CategoryTheory.Sites.EpiMono
Mathlib.CategoryTheory.Sites.LocallySurjective
Mathlib.CategoryTheory.Sites.Sheaf
Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
Mathlib.CategoryTheory.Sites.Whiskering

Imported by1

Nyll.EtaleCohomology.Classical.All

theorem

moduleGlobalSections_preservesHomology_of_henselianLocalRing

L62 ↗

EtaleCohomology.moduleGlobalSections_preservesHomology_of_henselianLocalRing

Documentation

Actual module-valued global sections on a strictly local spectrum preserve homology, and in particular preserve exact sequences.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable (R : Type u) [CommRing R] [HenselianLocalRing R]
  [IsSepClosed (IsLocalRing.ResidueField R)]

Lean source · statement

theorem moduleGlobalSections_preservesHomology_of_henselianLocalRing
    (Λ : Type u) [CommRing Λ] :
    ((sheafSections (Spec.{u} (CommRingCat.of R)).smallEtaleTopology (ModuleCat.{u} Λ)).obj
      (op (Scheme.Etale.mk (𝟙 (Spec.{u} (CommRingCat.of R)))))).PreservesHomology

theorem

abelianGlobalSections_preservesEpimorphisms

L80 ↗

EtaleCohomology.abelianGlobalSections_preservesEpimorphisms

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable (R : Type u) [CommRing R] [HenselianLocalRing R]
  [IsSepClosed (IsLocalRing.ResidueField R)]

Lean source · full declaration

theorem abelianGlobalSections_preservesEpimorphisms :
    ((sheafSections (Spec.{u} (CommRingCat.of R)).smallEtaleTopology AddCommGrpCat.{u}).obj
      (op (Scheme.Etale.mk (𝟙 (Spec.{u} (CommRingCat.of R)))))).PreservesEpimorphisms where
  preserves {F G} η _ := by
    apply (AddCommGrpCat.epi_iff_surjective _).mpr
    have : Sheaf.IsLocallySurjective η :=
      (Sheaf.isLocallySurjective_iff_epi'
        (J := (Spec.{u} (CommRingCat.of R)).smallEtaleTopology) AddCommGrpCat.{u} η).mpr
          inferInstance
    intro t
    have hS := sieve_eq_top_of_henselianLocalRing R
      (Presheaf.imageSieve η.hom t)
      (Presheaf.imageSieve_mem (Spec.{u} (CommRingCat.of R)).smallEtaleTopology η.hom t)
    have hid : Presheaf.imageSieve η.hom t
        (𝟙 (Scheme.Etale.mk (𝟙 (Spec.{u} (CommRingCat.of R))))) := by
      rw [hS]
      trivial
    obtain ⟨s, hs⟩ := hid
    refine ⟨s, ?_⟩
    have hmap : G.obj.map (𝟙 (op (Scheme.Etale.mk (𝟙 (Spec.{u} (CommRingCat.of R)))))) =
        𝟙 (G.obj.obj (op (Scheme.Etale.mk (𝟙 (Spec.{u} (CommRingCat.of R)))))) :=
      G.obj.map_id (op (Scheme.Etale.mk (𝟙 (Spec.{u} (CommRingCat.of R)))))
    exact hs.trans ((ConcreteCategory.congr_hom hmap t).trans (CategoryTheory.id_apply t))

theorem

etaleConstantInteger_projective_of_henselianLocalRing

L107 ↗

EtaleCohomology.etaleConstantInteger_projective_of_henselianLocalRing

Documentation

The actual constant integer sheaf on a strictly local spectrum is projective: global sections preserve epimorphisms, and the integer group corepresents the epimorphism-preserving forgetful functor.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable (R : Type u) [CommRing R] [HenselianLocalRing R]
  [IsSepClosed (IsLocalRing.ResidueField R)]

Lean source · statement

theorem etaleConstantInteger_projective_of_henselianLocalRing :
    Projective ((constantSheaf (Spec.{u} (CommRingCat.of R)).smallEtaleTopology
      AddCommGrpCat.{u}).obj (AddCommGrpCat.of (ULift.{u} ℤ)))

theorem

etaleAbelianCohomology_succ_subsingleton_of_henselianLocalRing

L124 ↗

EtaleCohomology.etaleAbelianCohomology_succ_subsingleton_of_henselianLocalRing

Documentation

Every abelian sheaf on a strictly local spectrum has zero classical étale cohomology in positive degrees. These are the existing Sheaf.H groups.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable (R : Type u) [CommRing R] [HenselianLocalRing R]
  [IsSepClosed (IsLocalRing.ResidueField R)]

Lean source · statement

theorem etaleAbelianCohomology_succ_subsingleton_of_henselianLocalRing
    (F : Sheaf (Spec.{u} (CommRingCat.of R)).smallEtaleTopology AddCommGrpCat.{u}) (n : ℕ) :
    Subsingleton (Sheaf.H.{u} F (n + 1))

theorem

etaleCohomology_succ_isZero_of_henselianLocalRing

L134 ↗

EtaleCohomology.etaleCohomology_succ_isZero_of_henselianLocalRing

Documentation

Every coefficient sheaf on a strictly local spectrum has zero positive-degree classical étale cohomology, for any commutative coefficient ring.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable (R : Type u) [CommRing R] [HenselianLocalRing R]
  [IsSepClosed (IsLocalRing.ResidueField R)]

Lean source · statement

theorem etaleCohomology_succ_isZero_of_henselianLocalRing
    (Λ : Type u) [CommRing Λ]
    (F : Sheaf (Spec.{u} (CommRingCat.of R)).smallEtaleTopology (ModuleCat.{u} Λ)) (n : ℕ) :
    IsZero (etaleCohomology (Spec.{u} (CommRingCat.of R)) Λ F (n + 1))

Module documentation

Classical cohomology of a strictly local spectrum

Declarations

moduleGlobalSections_preservesHomology_of_henselianLocalRing

abelianGlobalSections_preservesEpimorphisms

etaleConstantInteger_projective_of_henselianLocalRing

etaleAbelianCohomology_succ_subsingleton_of_henselianLocalRing

etaleCohomology_succ_isZero_of_henselianLocalRing