NYLL
Module

CohomologyPullbackFibers.lean

Nyll.JacobianVarieties.Kummer.CohomologyPullbackFibers
7 declarations indexed from sourceView source ↗

Module documentation

Actual extension fibers under scheme pullback

The inverse-image adjunction unit sends a lift of the integer section one to a lift in the actual inverse-image extension. Compatibility with the quotient comes from the unit's naturality and the proved constant-section comparison. This constructs the map of actual sheaves used to compare their geometric monodromy under a morphism of schemes.

Imports5
Imported by2

Declarations

theorem

pullbackExtension_unit_projection

L39 ↗
JacobianVarieties.Kummer.pullbackExtension_unit_projection
Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
open EtaleFundamentalGroups.Cohomology
namespace JacobianVarieties.Kummer
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 pullbackExtension_unit_projection :
    (etaleAbelianPullbackPushforwardAdjunction f).unit.app E ≫
        (etaleAbelianPushforward f).map (pullbackExtension f A i p h).g =
      p ≫ (etaleAbelianPullbackPushforwardAdjunction f).homEquiv _ _
        ((etaleAbelianPullbackConstantIso f).hom.app (AddCommGrpCat.of (ULift.{u} ℤ)))
theorem

pullbackExtension_unit_inclusion

L47 ↗
JacobianVarieties.Kummer.pullbackExtension_unit_inclusion
Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
open EtaleFundamentalGroups.Cohomology
namespace JacobianVarieties.Kummer
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 pullbackExtension_unit_inclusion :
    i ≫ (etaleAbelianPullbackPushforwardAdjunction f).unit.app E =
      (etaleAbelianPullbackPushforwardAdjunction f).homEquiv _ _
          ((etaleAbelianPullbackConstantIso f).hom.app A) ≫
        (etaleAbelianPushforward f).map (pullbackExtension f A i p h).f
def

fiberMap

L64 ↗
JacobianVarieties.Kummer.fiberMap
Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
open EtaleFundamentalGroups.Cohomology
namespace JacobianVarieties.Kummer
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 · full declaration
def fiberMap
    {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)
    (η : E ⟶ (etaleAbelianPushforward f).obj E')
    (q : (constantSheaf Y.smallEtaleTopology AddCommGrpCat.{u}).obj
        (AddCommGrpCat.of (ULift.{u} ℤ)) ⟶
      (etaleAbelianPushforward f).obj
        ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj
          (AddCommGrpCat.of (ULift.{u} ℤ))))
    (hp : η ≫ (etaleAbelianPushforward f).map p' = p ≫ q)
    (hq : ∀ U : Y.Etaleᵒᵖ,
      q.hom.app U ((integerUnitSection Y).app U PUnit.unit) =
        (integerUnitSection X).app (op ((etaleBaseChange f).obj U.unop)) PUnit.unit) :
    extensionFiber (ShortComplex.mk i p h) (integerUnitSection Y) ⟶
      (etaleSetPushforward f).obj
        (extensionFiber (ShortComplex.mk i' p' h') (integerUnitSection X)) where
  hom :=
    { app := fun U => ↾fun x => ⟨η.hom.app U x.val, by
        have he := ConcreteCategory.congr_hom
          (congrArg (fun m : E ⟶ (etaleAbelianPushforward f).obj
            ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj
              (AddCommGrpCat.of (ULift.{u} ℤ))) => m.hom.app U) hp) x.val
        exact he.trans ((congrArg (q.hom.app U) x.property).trans (hq U))⟩
      naturality := fun U V k => by
        apply ConcreteCategory.hom_ext
        intro x
        apply Subtype.ext
        exact ConcreteCategory.congr_hom (η.hom.naturality k) x.val }
theorem

fiberMap_translation

L95 ↗
JacobianVarieties.Kummer.fiberMap_translation
Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
open EtaleFundamentalGroups.Cohomology
namespace JacobianVarieties.Kummer
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 fiberMap_translation
    {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)
    (η : E ⟶ (etaleAbelianPushforward f).obj E')
    (q : (constantSheaf Y.smallEtaleTopology AddCommGrpCat.{u}).obj
        (AddCommGrpCat.of (ULift.{u} ℤ)) ⟶
      (etaleAbelianPushforward f).obj
        ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj
          (AddCommGrpCat.of (ULift.{u} ℤ))))
    (hp : η ≫ (etaleAbelianPushforward f).map p' = p ≫ q)
    (hq : ∀ U : Y.Etaleᵒᵖ,
      q.hom.app U ((integerUnitSection Y).app U PUnit.unit) =
        (integerUnitSection X).app (op ((etaleBaseChange f).obj U.unop)) PUnit.unit)
    (qA : (constantSheaf Y.smallEtaleTopology AddCommGrpCat.{u}).obj A ⟶
      (etaleAbelianPushforward f).obj
        ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj A))
    (hi : i ≫ η = qA ≫ (etaleAbelianPushforward f).map i')
    (hc : ∀ (U : Y.Etaleᵒᵖ) (a : A), qA.hom.app U
      ((toSheafify Y.smallEtaleTopology ((Functor.const Y.Etaleᵒᵖ).obj A)).app U a) =
        (toSheafify X.smallEtaleTopology ((Functor.const X.Etaleᵒᵖ).obj A)).app
          (op ((etaleBaseChange f).obj U.unop)) a) (a : A) :
    constantFiberTranslation A i p h (integerUnitSection Y) a ≫
        fiberMap f A i p h i' p' h' η q hp hq =
      fiberMap f A i p h i' p' h' η q hp hq ≫
        (etaleSetPushforward f).map
          (constantFiberTranslation A i' p' h' (integerUnitSection X) a)
theorem

constantUnit_section

L144 ↗
JacobianVarieties.Kummer.constantUnit_section
Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
open EtaleFundamentalGroups.Cohomology
namespace JacobianVarieties.Kummer
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 constantUnit_section (B : AddCommGrpCat.{u}) (U : Y.Etaleᵒᵖ) (b : B) :
    ((etaleAbelianPullbackPushforwardAdjunction f).homEquiv _ _
      ((etaleAbelianPullbackConstantIso f).hom.app B)).hom.app U
        ((toSheafify Y.smallEtaleTopology ((Functor.const Y.Etaleᵒᵖ).obj B)).app U b) =
      (toSheafify X.smallEtaleTopology ((Functor.const X.Etaleᵒᵖ).obj B)).app
        (op ((etaleBaseChange f).obj U.unop)) b
def

pullbackExtensionFiberMap

L154 ↗
JacobianVarieties.Kummer.pullbackExtensionFiberMap
Documentation

The actual adjunction unit maps the original lift sheaf into the direct image of the lift sheaf of the actual inverse-image extension.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
open EtaleFundamentalGroups.Cohomology
namespace JacobianVarieties.Kummer
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
def pullbackExtensionFiberMap :
    extensionFiber (ShortComplex.mk i p h) (integerUnitSection Y) ⟶
      (etaleSetPushforward f).obj
        (extensionFiber (pullbackExtension f A i p h) (integerUnitSection X))
theorem

pullbackExtensionFiberMap_translation

L169 ↗
JacobianVarieties.Kummer.pullbackExtensionFiberMap_translation
Documentation

Pullback of an extension fiber preserves translation by each original constant coefficient, using the actual constant comparison.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite EtaleCohomology
open EtaleFundamentalGroups.Cohomology
namespace JacobianVarieties.Kummer
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 pullbackExtensionFiberMap_translation (a : A) :
    constantFiberTranslation A i p h (integerUnitSection Y) a ≫
        pullbackExtensionFiberMap f A i p h =
      pullbackExtensionFiberMap f A i p h ≫
        (etaleSetPushforward f).map
          (constantFiberTranslation A (pullbackExtension f A i p h).f
            (pullbackExtension f A i p h).g (pullbackExtension f A i p h).zero
            (integerUnitSection X) a)

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