Module

FiberMap.lean

Nyll.EtaleFundamentalGroups.Cohomology.FiberMap

2 declarations indexed from sourceView source ↗

Module documentation

Functoriality of the actual sheaf of lifts

A morphism of extensions which is the identity on kernel and quotient induces a morphism of their lift sheaves. This morphism commutes with every constant coefficient translation, directly from the original additive sheaf morphism.

Imports1

Nyll.EtaleFundamentalGroups.Cohomology.FiberTranslation

Imported by3

def

extensionFiberMap

L32 ↗

EtaleFundamentalGroups.Cohomology.extensionFiberMap

Documentation

The actual morphism of lift sheaves induced by a quotient-compatible map.

Source context 5 commands

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

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

Lean source · full declaration

def extensionFiberMap :
    extensionFiber (ShortComplex.mk i₁ p₁ z₁) t ⟶
      extensionFiber (ShortComplex.mk i₂ p₂ z₂) t where
  hom :=
    { app := fun U => ↾fun e => ⟨f.hom.app U e.val, by
        have hh := ConcreteCategory.congr_hom
          (congrArg (fun k : E₁ ⟶ Q => k.hom.app U) hp) e.val
        exact hh.trans e.property⟩
      naturality := fun U V g => by
        apply ConcreteCategory.hom_ext
        intro e
        apply Subtype.ext
        exact ConcreteCategory.congr_hom (f.hom.naturality g) e.val }

theorem

extensionFiberMap_translation

L48 ↗

EtaleFundamentalGroups.Cohomology.extensionFiberMap_translation