NYLL
Module

H1FiniteCover.lean

Nyll.EtaleFundamentalGroups.Cohomology.H1FiniteCover
2 declarations indexed from sourceView source ↗

Module documentation

Finite étale covers obtained from actual first cohomology classes

For finite abelian constant coefficients, the inverse image of the integer section 1 in an extension representing a cohomology class is represented by a finite étale scheme. Both the extension and the representer are constructed from existing theorems, with no comparison hypothesis on cohomology.

Imports4
Imported by5

Declarations

def

integerUnitSection

L30 ↗
EtaleFundamentalGroups.Cohomology.integerUnitSection
Documentation

The global section 1 of the actual constant integer sheaf.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
universe u
namespace EtaleFundamentalGroups.Cohomology
Lean source · full declaration
def integerUnitSection (X : Scheme.{u}) :
    (Functor.const X.Etaleᵒᵖ).obj PUnit ⟶
      ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj
        (AddCommGrpCat.of (ULift.{u} ℤ))).obj ⋙ forget AddCommGrpCat.{u} where
  app U := ↾fun _ =>
    (toSheafify X.smallEtaleTopology
      ((Functor.const X.Etaleᵒᵖ).obj (AddCommGrpCat.of (ULift.{u} ℤ)))).app U (ULift.up 1)
  naturality U V f := by
    apply ConcreteCategory.hom_ext
    intro a
    exact ConcreteCategory.congr_hom
      ((toSheafify X.smallEtaleTopology
        ((Functor.const X.Etaleᵒᵖ).obj (AddCommGrpCat.of (ULift.{u} ℤ)))).naturality f)
      (ULift.up 1)
theorem

exists_h1_finiteEtale_cover

L48 ↗
EtaleFundamentalGroups.Cohomology.exists_h1_finiteEtale_cover
Documentation

Every actual first étale cohomology class with finite constant coefficients has an extension whose fiber over 1 is an actual finite étale cover. The base scheme is arbitrary; connectedness and geometric points are not needed here.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
universe u
namespace EtaleFundamentalGroups.Cohomology
Lean source · statement
theorem exists_h1_finiteEtale_cover (X : Scheme.{u}) (A : AddCommGrpCat.{u}) [Finite A]
    (a : Sheaf.H.{u} ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj A) 1) :
    ∃ (E : Sheaf X.smallEtaleTopology AddCommGrpCat.{u})
      (i : (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj A ⟶ E)
      (p : E ⟶ (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj
        (AddCommGrpCat.of (ULift.{u} ℤ)))
      (h : i ≫ p = 0) (hs : (ShortComplex.mk i p h).ShortExact)
      (Y : FiniteEtale X), hs.extClass = a ∧
        Nonempty ((finiteEtaleSheaf X).obj Y ≅
          extensionFiber (ShortComplex.mk i p h) (integerUnitSection X))

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