Module

FiberTranslation.lean

Nyll.EtaleFundamentalGroups.Cohomology.FiberTranslation

3 declarations indexed from sourceView source ↗

Module documentation

Constant coefficient translations on the sheaf of lifts

Every original coefficient acts by a morphism of the actual fiber sheaf. On a geometric stalk this is translation by the same coefficient under the canonical constant-stalk isomorphism. Naturality of these sheaf morphisms will give commutation with geometric monodromy.

Imports3

Nyll.EtaleFundamentalGroups.Cohomology.ConstantStalk
Nyll.EtaleFundamentalGroups.Cohomology.FiberStalkComparison
Mathlib.CategoryTheory.Sites.Sheafification

Imported by5

abbrev

constantSection

L34 ↗

EtaleFundamentalGroups.Cohomology.constantSection

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} (A : AddCommGrpCat.{u})
  {E Q : Sheaf X.smallEtaleTopology AddCommGrpCat.{u}}
  (i : (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj A ⟶ E)
  (p : E ⟶ Q) (h : i ≫ p = 0)
  (t : (Functor.const X.Etaleᵒᵖ).obj PUnit ⟶ Q.obj ⋙ forget AddCommGrpCat.{u})

Lean source · statement

abbrev constantSection (U : X.Etaleᵒᵖ) (a : A)

def

constantFiberTranslation

L39 ↗

EtaleFundamentalGroups.Cohomology.constantFiberTranslation

Documentation

Adding the image of a constant coefficient defines an endomorphism of the fiber sheaf itself, before any geometric point or monodromy is chosen.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} (A : AddCommGrpCat.{u})
  {E Q : Sheaf X.smallEtaleTopology AddCommGrpCat.{u}}
  (i : (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj A ⟶ E)
  (p : E ⟶ Q) (h : i ≫ p = 0)
  (t : (Functor.const X.Etaleᵒᵖ).obj PUnit ⟶ Q.obj ⋙ forget AddCommGrpCat.{u})

Lean source · full declaration

def constantFiberTranslation (a : A) :
    extensionFiber (ShortComplex.mk i p h) t ⟶
      extensionFiber (ShortComplex.mk i p h) t where
  hom :=
    { app := fun U => ↾fun (e : {b : E.obj.obj U // p.hom.app U b = t.app U PUnit.unit}) =>
        ⟨i.hom.app U (constantSection A U a) + e.val, by
        change p.hom.app U (i.hom.app U (constantSection A U a) + e.val) =
          t.app U PUnit.unit
        rw [map_add]
        have hz := ConcreteCategory.congr_hom
          (congrArg (fun k : (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj A ⟶ Q =>
            k.hom.app U) h) (constantSection A U a)
        change p.hom.app U (i.hom.app U (constantSection A U a)) = 0 at hz
        rw [hz, zero_add]
        exact e.property⟩
      naturality := fun U V f => by
        apply ConcreteCategory.hom_ext
        intro (e : {b : E.obj.obj U // p.hom.app U b = t.app U PUnit.unit})
        apply Subtype.ext
        symm
        change E.obj.map f (i.hom.app U (constantSection A U a) + e.val) =
          i.hom.app V (constantSection A V a) + E.obj.map f e.val
        rw [map_add]
        apply congrArg (· + E.obj.map f e.val)
        have hi := ConcreteCategory.congr_hom (i.hom.naturality f) (constantSection A U a)
        have ha := ConcreteCategory.congr_hom
          ((toSheafify X.smallEtaleTopology ((Functor.const X.Etaleᵒᵖ).obj A)).naturality f) a
        exact hi.symm.trans (congrArg (i.hom.app V) ha.symm) }

theorem

constantFiberTranslation_stalk

L72 ↗

EtaleFundamentalGroups.Cohomology.constantFiberTranslation_stalk

Documentation

The stalk action of a constant translation uses the original inclusion and the actual coefficient, not a separately reconstructed stalk structure.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} (A : AddCommGrpCat.{u})
  {E Q : Sheaf X.smallEtaleTopology AddCommGrpCat.{u}}
  (i : (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj A ⟶ E)
  (p : E ⟶ Q) (h : i ≫ p = 0)
  (t : (Functor.const X.Etaleᵒᵖ).obj PUnit ⟶ Q.obj ⋙ forget AddCommGrpCat.{u})
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)

Lean source · statement

theorem constantFiberTranslation_stalk (a : A)
    (q : (Scheme.pointSmallEtale ξ).sheafFiber.obj
      (extensionFiber (ShortComplex.mk i p h) t)) :
    (extensionFiberStalkEquiv (ShortComplex.mk i p h) t ξ
      ((Scheme.pointSmallEtale ξ).sheafFiber.map (constantFiberTranslation A i p h t a) q)).val =
      (Scheme.pointSmallEtale ξ).sheafFiber.map i ((constantAbelianStalkIso ξ A).inv a) +
        (extensionFiberStalkEquiv (ShortComplex.mk i p h) t ξ q).val

Module documentation

Constant coefficient translations on the sheaf of lifts

Declarations

constantSection

constantFiberTranslation

constantFiberTranslation_stalk