NYLL
Module

ConstantPullbackSections.lean

Nyll.EtaleFundamentalGroups.Cohomology.ConstantPullbackSections
9 declarations indexed from sourceView source ↗

Module documentation

Constant sections under actual inverse image

The constant-sheaf comparison is the unique comparison of left adjoints. Its adjoint carries each constant section to the same section on the base-changed étale object. In particular it preserves the integer section used to construct the torsor of an actual derived H¹ extension.

Imports5
Imported by2

Declarations

def

constantAbelianPullbackAdjoint

L33 ↗
EtaleFundamentalGroups.Cohomology.constantAbelianPullbackAdjoint
Documentation

Adjoint of the existing constant-coefficient inverse-image comparison.

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)
Lean source · statement
def constantAbelianPullbackAdjoint (A : AddCommGrpCat.{u}) :
    (constantSheaf Y.smallEtaleTopology AddCommGrpCat.{u}).obj A ⟶
      (etaleAbelianPushforward f).obj
        ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj A)
theorem

constantAbelianPullbackAdjoint_unit

L41 ↗
EtaleFundamentalGroups.Cohomology.constantAbelianPullbackAdjoint_unit
Documentation

The adjoint of constant inverse image preserves every constant 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)
Lean source · statement
theorem constantAbelianPullbackAdjoint_unit (A : AddCommGrpCat.{u}) (U : Y.Etale) :
    (toSheafify Y.smallEtaleTopology ((Functor.const Y.Etaleᵒᵖ).obj A)).app (op U) ≫
        (constantAbelianPullbackAdjoint f A).hom.app (op U) =
      (toSheafify X.smallEtaleTopology ((Functor.const X.Etaleᵒᵖ).obj A)).app
        (op ((etaleBaseChange f).obj U))
theorem

constantAbelianPullbackAdjoint_unit_apply

L79 ↗
EtaleFundamentalGroups.Cohomology.constantAbelianPullbackAdjoint_unit_apply
Documentation

Pointwise form of constant-section compatibility, retaining the coefficient type.

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)
Lean source · statement
theorem constantAbelianPullbackAdjoint_unit_apply (A : AddCommGrpCat.{u})
    (U : Y.Etale) (a : A) :
    (constantAbelianPullbackAdjoint f A).hom.app (op U)
        ((toSheafify Y.smallEtaleTopology ((Functor.const Y.Etaleᵒᵖ).obj A)).app (op U) a) =
      (toSheafify X.smallEtaleTopology ((Functor.const X.Etaleᵒᵖ).obj A)).app
        (op ((etaleBaseChange f).obj U)) a
theorem

integerUnitSection_constantPullbackAdjoint_app

L89 ↗
EtaleFundamentalGroups.Cohomology.integerUnitSection_constantPullbackAdjoint_app
Documentation

The particular quotient section defining H¹ torsors is preserved by the adjoint of the actual constant integer comparison.

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)
Lean source · statement
theorem integerUnitSection_constantPullbackAdjoint_app (U : Y.Etaleᵒᵖ) (z : PUnit) :
    (constantAbelianPullbackAdjoint f (AddCommGrpCat.of (ULift.{u} ℤ))).hom.app U
        ((integerUnitSection Y).app U z) =
      (integerUnitSection X).app (op ((etaleBaseChange f).obj U.unop)) PUnit.unit
def

integerUnitSheafSection

L98 ↗
EtaleFundamentalGroups.Cohomology.integerUnitSheafSection
Documentation

The integer section as a morphism of actual set-valued sheaves.

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)
Lean source · statement
def integerUnitSheafSection (Z : Scheme.{u}) :
    extensionFiberTerminal Z ⟶
      (sheafCompose Z.smallEtaleTopology (forget AddCommGrpCat.{u})).obj
        ((constantSheaf Z.smallEtaleTopology AddCommGrpCat.{u}).obj
          (AddCommGrpCat.of (ULift.{u} ℤ)))
theorem

integerUnitSheafSection_pushforward_comp

L105 ↗
EtaleFundamentalGroups.Cohomology.integerUnitSheafSection_pushforward_comp
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)
Lean source · statement
theorem integerUnitSheafSection_pushforward_comp
    (a : extensionFiberTerminal Y ⟶
      (etaleSetPushforward f).obj (extensionFiberTerminal X))
    (U : Y.Etaleᵒᵖ) (z : PUnit) :
    (a ≫ (etaleSetPushforward f).map (integerUnitSheafSection X)).hom.app U z =
      (integerUnitSection X).app (op ((etaleBaseChange f).obj U.unop)) PUnit.unit
theorem

integerUnitSheafSection_comp_adjoint

L112 ↗
EtaleFundamentalGroups.Cohomology.integerUnitSheafSection_comp_adjoint
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)
Lean source · statement
theorem integerUnitSheafSection_comp_adjoint
    (a : extensionFiberTerminal Y ⟶
      (etaleSetPushforward f).obj (extensionFiberTerminal X)) :
    integerUnitSheafSection Y ≫
        (sheafCompose Y.smallEtaleTopology (forget AddCommGrpCat.{u})).map
          (constantAbelianPullbackAdjoint f (AddCommGrpCat.of (ULift.{u} ℤ))) =
      a ≫ (etaleSetPushforward f).map (integerUnitSheafSection X)
theorem

integerUnitSheafSection_pullback

L129 ↗
EtaleFundamentalGroups.Cohomology.integerUnitSheafSection_pullback
Documentation

The canonical underlying comparison and the constant coefficient comparison carry the original integer section to the original 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)
Lean source · statement
theorem integerUnitSheafSection_pullback :
    (etaleSetPullback f).map (integerUnitSheafSection Y) ≫
        (abelianPullbackUnderlyingComparison f).app
          ((constantSheaf Y.smallEtaleTopology AddCommGrpCat.{u}).obj
            (AddCommGrpCat.of (ULift.{u} ℤ))) ≫
          (sheafCompose X.smallEtaleTopology (forget AddCommGrpCat.{u})).map
            ((etaleAbelianPullbackConstantIso f).hom.app
              (AddCommGrpCat.of (ULift.{u} ℤ))) =
      (extensionFiberTerminalPullbackIso f).hom ≫ integerUnitSheafSection X
theorem

integerUnitSheafSection_pullback_inv

L158 ↗
EtaleFundamentalGroups.Cohomology.integerUnitSheafSection_pullback_inv
Documentation

Explicitly transporting the integer section through inverse image leaves it equal to the distinguished section defining the H¹ extension torsor.

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)
Lean source · statement
theorem integerUnitSheafSection_pullback_inv :
    (extensionFiberTerminalPullbackIso f).inv ≫
      (etaleSetPullback f).map (integerUnitSheafSection Y) ≫
        (abelianPullbackUnderlyingComparison f).app
          ((constantSheaf Y.smallEtaleTopology AddCommGrpCat.{u}).obj
            (AddCommGrpCat.of (ULift.{u} ℤ))) ≫
          (sheafCompose X.smallEtaleTopology (forget AddCommGrpCat.{u})).map
            ((etaleAbelianPullbackConstantIso f).hom.app
              (AddCommGrpCat.of (ULift.{u} ℤ))) =
      integerUnitSheafSection X

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