Module

H1FiberPullback.lean

Nyll.EtaleFundamentalGroups.Cohomology.H1FiberPullback

3 declarations indexed from sourceView source ↗

Module documentation

The actual H¹ lift cover commutes with geometric inverse image

After identifying both constant coefficients, the inverse image of the original lift sheaf is the lift sheaf over the original integer section on the new base. This is the lift sheaf of the extension representing the actual derived cohomology pullback, not an independently chosen replacement.

Imports2

Imported by2

theorem

schemePullbackH1Extension_fiber_isPullback

L36 ↗

EtaleFundamentalGroups.Cohomology.schemePullbackH1Extension_fiber_isPullback

Documentation

The pulled-back original lift cover has the fiber square for the geometric inverse-image extension with its original constant quotient.

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_fiber_isPullback :
    IsPullback
      ((etaleSetPullback f).map
          (extensionFiberInclusion (ShortComplex.mk i p h) (integerUnitSection Y)) ≫
        (abelianPullbackUnderlyingMateIso f).inv.app E)
      ((Sheaf.isTerminalTerminal X.smallEtaleTopology Types.isTerminalPUnit).from
        ((etaleSetPullback f).obj
          (extensionFiber (ShortComplex.mk i p h) (integerUnitSection Y))))
      ((sheafCompose X.smallEtaleTopology (forget AddCommGrpCat.{u})).map
        (schemePullbackH1Extension f A i p h).g)
      (extensionFiberSection (schemePullbackH1Extension f A i p h)
        (integerUnitSection X))

def

schemePullbackH1Extension_fiberIso

L73 ↗

EtaleFundamentalGroups.Cohomology.schemePullbackH1Extension_fiberIso

Documentation

The actual lift sheaf of an H¹ extension commutes with geometric pullback, including the identification of its distinguished integer section.

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

def schemePullbackH1Extension_fiberIso :
    (etaleSetPullback f).obj
        (extensionFiber (ShortComplex.mk i p h) (integerUnitSection Y)) ≅
      extensionFiber (schemePullbackH1Extension f A i p h) (integerUnitSection X)

theorem

schemePullbackH1Extension_fiberIso_hom_inclusion

L82 ↗

EtaleFundamentalGroups.Cohomology.schemePullbackH1Extension_fiberIso_hom_inclusion

Documentation

This comparison keeps the inclusion into the original inverse-image middle sheaf.

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_hom_inclusion :
    (schemePullbackH1Extension_fiberIso f A i p h).hom ≫
        extensionFiberInclusion (schemePullbackH1Extension f A i p h)
          (integerUnitSection X) =
      (etaleSetPullback f).map
          (extensionFiberInclusion (ShortComplex.mk i p h) (integerUnitSection Y)) ≫
        (abelianPullbackUnderlyingMateIso f).inv.app E

Module documentation

The actual H¹ lift cover commutes with geometric inverse image

Declarations

schemePullbackH1Extension_fiber_isPullback

schemePullbackH1Extension_fiberIso

schemePullbackH1Extension_fiberIso_hom_inclusion