Nyll.EtaleFundamentalGroups.FiniteEtale.CechKernelBaseChangeSurjectivity

Module documentation

Actual section surjectivity and the Čech kernel comparison

The affine-cochain tensor equivalence has an explicit formula in terms of the pullback adjunction unit. Using that formula and actual sheaf gluing, surjectivity of the pullback map on sections supplies surjectivity of the canonical degree-zero kernel base-change map.

theorem

surjective_kerBaseChangeHom_of_surjective_pullbackUnit

L31 ↗

AlgebraicGeometry.OModulePresheaf.surjective_kerBaseChangeHom_of_surjective_pullbackUnit

Documentation

The actual pullback map on global sections supplies the surjectivity hypothesis of the finite free H⁰ model.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicGeometry.OModulePresheaf
universe u

Lean source · statement

theorem surjective_kerBaseChangeHom_of_surjective_pullbackUnit
    {R : Type u} [CommRing R] {X : Scheme.{u}}
    (f : X ⟶ Spec (CommRingCat.of R)) [IsSeparated f]
    (M : X.Modules) (𝒰 : X.OrderedAffineCover)
    (htriv : ∀ x : X, ∃ U : X.Opens, x ∈ U ∧
      Nonempty ((Scheme.Modules.pullback U.ι).obj M ≅
        SheafOfModules.unit U.toScheme.ringCatSheaf))
    (A : Type u) [CommRing A] [Algebra R A]
    (hSurjective : Function.Surjective
      (((Scheme.Modules.pullbackPushforwardAdjunction
        (pullback.fst f (Scheme.TwoAffineOpenCover.specMap R A))).unit.app M).app ⊤)) :
    Function.Surjective
      (TwoChartCech.kerBaseChangeHom ((ofModules f M).d 𝒰 0) A)

Module documentation

Actual section surjectivity and the Čech kernel comparison

Declarations

surjective_kerBaseChangeHom_of_surjective_pullbackUnit