Module

FiniteH1PullbackIdentity.lean

Nyll.EtaleFundamentalGroups.Cohomology.FiniteH1PullbackIdentity

2 declarations indexed from sourceView source ↗

Module documentation

Identity and isomorphism pullback on actual finite H¹

Imports2

Imported by3

theorem

constantFiniteH1Pullback_injective_of_fundamentalGroupHom_surjective

L20 ↗

EtaleFundamentalGroups.Cohomology.constantFiniteH1Pullback_injective_of_fundamentalGroupHom_surjective

Documentation

Surjectivity on actual fundamental groups implies injectivity of the already constructed derived H¹ pullback.

Source context 3 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
namespace EtaleFundamentalGroups.Cohomology

Lean source · statement

theorem constantFiniteH1Pullback_injective_of_fundamentalGroupHom_surjective
    {X Y : Scheme} [ConnectedSpace X] [ConnectedSpace Y]
    (f : X ⟶ Y) {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (geom : Spec (.of Ω) ⟶ X) (A : AddCommGrpCat.{0}) [Finite A]
    (hf : Function.Surjective (FiniteEtale.fundamentalGroupHom f geom)) :
    Function.Injective (constantCohomologyPullback f A 1)

theorem

constantFiniteH1Pullback_id

L37 ↗

EtaleFundamentalGroups.Cohomology.constantFiniteH1Pullback_id