Module

IntegerExtensionShear.lean

Nyll.EtaleFundamentalGroups.Cohomology.IntegerExtensionShear

5 declarations indexed from sourceView source ↗

Module documentation

Constant torsor translations as additive shears

On the fiber of an extension over the integer section one, translation by a coefficient is the restriction of the additive endomorphism e ↦ e + i(a p(e)). This realizes the torsor action using genuine abelian-sheaf morphisms, so its compatibility with inverse image follows from additivity and the naturality of the existing constant-coefficient comparison.

Imports6

Nyll.EtaleFundamentalGroups.Cohomology.ExtensionFiberSquare
Nyll.EtaleFundamentalGroups.Cohomology.FiberTranslation
Nyll.EtaleFundamentalGroups.Cohomology.H1FiniteCover
Nyll.EtaleFundamentalGroups.Cohomology.SchemePullback
Mathlib.Algebra.Category.Grp.ForgetCorepresentable
Mathlib.CategoryTheory.Sites.Sheafification

Imported by2

def

constantIntegerMultiple

EtaleFundamentalGroups.Cohomology.constantIntegerMultiple

Documentation

The constant-sheaf map sending one to the specified original coefficient.

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

def constantIntegerMultiple (X : Scheme.{u}) (A : AddCommGrpCat.{u}) (a : A) :
    (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj
        (AddCommGrpCat.of (ULift.{u} ℤ)) ⟶
      (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj A

theorem

constantIntegerMultiple_one

EtaleFundamentalGroups.Cohomology.constantIntegerMultiple_one

Documentation

This map sends the actual integer-one section to the original coefficient section.

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 constantIntegerMultiple_one (X : Scheme.{u}) (A : AddCommGrpCat.{u}) (a : A)
    (U : X.Etaleᵒᵖ) :
    (constantIntegerMultiple X A a).hom.app U ((integerUnitSection X).app U PUnit.unit) =
      (toSheafify X.smallEtaleTopology ((Functor.const X.Etaleᵒᵖ).obj A)).app U a

def

integerExtensionShear

EtaleFundamentalGroups.Cohomology.integerExtensionShear

Documentation

An additive middle-sheaf endomorphism realizing coefficient translation on the fiber over one.

Source context 5 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
variable {X : Scheme.{u}} (A : AddCommGrpCat.{u})
  {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} ℤ)))

Lean source · statement

def integerExtensionShear (a : A) : E ⟶ E

theorem

constantFiberTranslation_inclusion_eq_shear

EtaleFundamentalGroups.Cohomology.constantFiberTranslation_inclusion_eq_shear

Documentation

The original translation on the actual lift sheaf is the restriction of this additive shear.

Source context 5 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
variable {X : Scheme.{u}} (A : AddCommGrpCat.{u})
  {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} ℤ)))

Lean source · statement

theorem constantFiberTranslation_inclusion_eq_shear (h : i ≫ p = 0) (a : A) :
    constantFiberTranslation A i p h (integerUnitSection X) a ≫
        extensionFiberInclusion (ShortComplex.mk i p h) (integerUnitSection X) =
      extensionFiberInclusion (ShortComplex.mk i p h) (integerUnitSection X) ≫
        (sheafCompose X.smallEtaleTopology (forget AddCommGrpCat.{u})).map
          (integerExtensionShear A i p a)

theorem

integerExtensionShear_pullback

EtaleFundamentalGroups.Cohomology.integerExtensionShear_pullback

Documentation

The additive shear commutes with actual abelian inverse image and the original coefficient identifications.

Source context 6 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
variable {X : Scheme.{u}} (A : AddCommGrpCat.{u})
  {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} ℤ)))
variable {Y : Scheme.{u}} (f : Y ⟶ X)

Lean source · statement

theorem integerExtensionShear_pullback (h : i ≫ p = 0) (a : A) :
    (etaleAbelianPullback f).map (integerExtensionShear A i p a) =
      integerExtensionShear A (schemePullbackH1Extension f A i p h).f
        (schemePullbackH1Extension f A i p h).g a