NYLL
Module

FiberCoefficientMap.lean

Nyll.EtaleFundamentalGroups.Cohomology.FiberCoefficientMap
2 declarations indexed from sourceView source ↗

Module documentation

Changing the coefficients of a lift sheaf

The map induced by a morphism of extensions carries translation by a constant coefficient to translation by its image. The coefficient comparison is the actual constant-sheaf functor map, with its sheafification unit naturality.

Imports3
Imported by2

Declarations

theorem

constantAbelianUnit_naturality

L28 ↗
EtaleFundamentalGroups.Cohomology.constantAbelianUnit_naturality
Documentation

Constant-sheaf units are natural in the original abelian coefficient group.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace EtaleFundamentalGroups.Cohomology
Lean source · statement
theorem constantAbelianUnit_naturality {X : Scheme.{u}}
    {A B : AddCommGrpCat.{u}} (α : A ⟶ B) (U : X.Etaleᵒᵖ) (a : A) :
    ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).map α).hom.app U
        ((toSheafify X.smallEtaleTopology ((Functor.const X.Etaleᵒᵖ).obj A)).app U a) =
      (toSheafify X.smallEtaleTopology ((Functor.const X.Etaleᵒᵖ).obj B)).app U (α a)
theorem

extensionFiberMap_changeCoefficients

L38 ↗
EtaleFundamentalGroups.Cohomology.extensionFiberMap_changeCoefficients
Documentation

Actual extension comparisons respect coefficient translations also for a nonidentity coefficient homomorphism.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace EtaleFundamentalGroups.Cohomology
Lean source · statement
theorem extensionFiberMap_changeCoefficients
    {X : Scheme.{u}} {A B : AddCommGrpCat.{u}} (α : A ⟶ B)
    {E₁ E₂ Q : Sheaf X.smallEtaleTopology AddCommGrpCat.{u}}
    (i₁ : (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj A ⟶ E₁)
    (p₁ : E₁ ⟶ Q) (z₁ : i₁ ≫ p₁ = 0)
    (i₂ : (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj B ⟶ E₂)
    (p₂ : E₂ ⟶ Q) (z₂ : i₂ ≫ p₂ = 0)
    (f : E₁ ⟶ E₂)
    (hi : i₁ ≫ f = (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).map α ≫ i₂)
    (hp : f ≫ p₂ = p₁)
    (t : (Functor.const X.Etaleᵒᵖ).obj PUnit ⟶ Q.obj ⋙ forget AddCommGrpCat.{u})
    (a : A) :
    constantFiberTranslation A i₁ p₁ z₁ t a ≫
        extensionFiberMap i₁ p₁ z₁ i₂ p₂ z₂ f hp t =
      extensionFiberMap i₁ p₁ z₁ i₂ p₂ z₂ f hp t ≫
        constantFiberTranslation B i₂ p₂ z₂ t (α a)

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