Module

FiniteH1IsomorphismPullback.lean

Nyll.EtaleFundamentalGroups.Cohomology.FiniteH1IsomorphismPullback

3 declarations indexed from sourceView source ↗

Module documentation

Transporting actual finite H¹ along geometric isomorphisms

Imports1

Nyll.EtaleFundamentalGroups.Cohomology.FiniteH1PullbackIdentity

Imported by2

def

constantFiniteH1PullbackEquiv

L19 ↗

EtaleFundamentalGroups.Cohomology.constantFiniteH1PullbackEquiv

Documentation

The existing derived pullback along a scheme isomorphism is an additive equivalence, with inverse the actual inverse-morphism 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 · full declaration

def constantFiniteH1PullbackEquiv
    {X Y : Scheme} [ConnectedSpace X] [ConnectedSpace Y]
    (e : X ≅ Y) {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (geom : Spec (.of Ω) ⟶ X) (A : AddCommGrpCat.{0}) [Finite A] :
    Sheaf.H.{0} ((constantSheaf Y.smallEtaleTopology AddCommGrpCat.{0}).obj A) 1 ≃+
      Sheaf.H.{0} ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{0}).obj A) 1 where
  toFun := constantCohomologyPullback e.hom A 1
  invFun := constantCohomologyPullback e.inv A 1
  left_inv c := by
    rw [← constantFiniteH1Pullback_comp e.inv e.hom (geom ≫ e.hom) A c,
      e.inv_hom_id, constantFiniteH1Pullback_id (geom ≫ e.hom) A c]
  right_inv c := by
    rw [← constantFiniteH1Pullback_comp e.hom e.inv geom A c,
      e.hom_inv_id, constantFiniteH1Pullback_id geom A c]
  map_add' a b := map_add (constantCohomologyPullback e.hom A 1) a b

theorem

constantFiniteH1Pullback_eq_self_of_iso_square

L37 ↗

EtaleFundamentalGroups.Cohomology.constantFiniteH1Pullback_eq_self_of_iso_square

Documentation

Triviality of an actual endomorphism's H¹ action is preserved under an actual geometric isomorphism and a proved commuting square.

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_eq_self_of_iso_square
    {X Y : Scheme} [ConnectedSpace X] [ConnectedSpace Y]
    (e : X ≅ Y) {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (geom : Spec (.of Ω) ⟶ X) (A : AddCommGrpCat.{0}) [Finite A]
    (f : X ⟶ X) (g : Y ⟶ Y) (hfg : f ≫ e.hom = e.hom ≫ g)
    (hg : ∀ c, constantCohomologyPullback g A 1 c = c) :
    ∀ c, constantCohomologyPullback f A 1 c = c

theorem

constantFiniteH1Pullback_surjective_of_iso_square

L53 ↗

EtaleFundamentalGroups.Cohomology.constantFiniteH1Pullback_surjective_of_iso_square

Documentation

Surjectivity of actual derived finite H¹ pullback is invariant under a proved square of scheme isomorphisms.

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_surjective_of_iso_square
    {X Y X' Y' : Scheme} [ConnectedSpace X] [ConnectedSpace Y]
    [ConnectedSpace X'] [ConnectedSpace Y']
    (eX : X ≅ X') (eY : Y ≅ Y')
    {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (geom : Spec (.of Ω) ⟶ X) (A : AddCommGrpCat.{0}) [Finite A]
    (f : X ⟶ Y) (g : X' ⟶ Y')
    (hfg : f ≫ eY.hom = eX.hom ≫ g)
    (hg : Function.Surjective (constantCohomologyPullback g A 1)) :
    Function.Surjective (constantCohomologyPullback f A 1)

Module documentation

Transporting actual finite H¹ along geometric isomorphisms

Declarations

constantFiniteH1PullbackEquiv

constantFiniteH1Pullback_eq_self_of_iso_square

constantFiniteH1Pullback_surjective_of_iso_square