Module

FiberPullbackTranslation.lean

Nyll.EtaleFundamentalGroups.Cohomology.FiberPullbackTranslation

2 declarations indexed from sourceView source ↗

Module documentation

Coefficient equivariance of geometric pullback of H¹ lift sheaves

Translations on the fiber over one are restrictions of additive shears. Their compatibility with inverse image therefore follows from the genuine abelian inverse-image functor and its constant-coefficient comparison.

Imports2

Imported by2

instance

extensionFiberInclusion_mono

L26 ↗

EtaleFundamentalGroups.Cohomology.extensionFiberInclusion_mono

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

instance extensionFiberInclusion_mono {X : Scheme.{u}}
    (S : ShortComplex (Sheaf X.smallEtaleTopology AddCommGrpCat.{u}))
    (t : (Functor.const X.Etaleᵒᵖ).obj PUnit ⟶ S.X₃.obj ⋙ forget AddCommGrpCat.{u}) :
    Mono (extensionFiberInclusion S t) where
  right_cancellation {B} a b hab := by
    apply Sheaf.hom_ext
    apply NatTrans.ext
    funext U
    apply ConcreteCategory.hom_ext
    intro z
    apply Subtype.ext
    exact congrArg (fun k => k.hom.app U z) hab

theorem

schemePullbackH1Extension_fiberIso_translation

L48 ↗

EtaleFundamentalGroups.Cohomology.schemePullbackH1Extension_fiberIso_translation

Documentation

The actual lift-sheaf comparison preserves translation by every original coefficient, without any imposed equivariance hypothesis.

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 Y : Scheme.{u}} (f : X ⟶ Y) (A : AddCommGrpCat.{u})
  {E : Sheaf Y.smallEtaleTopology AddCommGrpCat.{u}}
  (i : (constantSheaf Y.smallEtaleTopology AddCommGrpCat.{u}).obj A ⟶ E)
  (p : E ⟶ (constantSheaf Y.smallEtaleTopology AddCommGrpCat.{u}).obj
    (AddCommGrpCat.of (ULift.{u} ℤ)))
  (h : i ≫ p = 0)

Lean source · statement

theorem schemePullbackH1Extension_fiberIso_translation (a : A) :
    (etaleSetPullback f).map
        (constantFiberTranslation A i p h (integerUnitSection Y) a) ≫
      (schemePullbackH1Extension_fiberIso f A i p h).hom =
    (schemePullbackH1Extension_fiberIso f A i p h).hom ≫
      constantFiberTranslation A (schemePullbackH1Extension f A i p h).f
        (schemePullbackH1Extension f A i p h).g
        (schemePullbackH1Extension f A i p h).zero (integerUnitSection X) a

Module documentation

Coefficient equivariance of geometric pullback of H¹ lift sheaves

Declarations

extensionFiberInclusion_mono

schemePullbackH1Extension_fiberIso_translation