Module

GenericPointCharacterDetection.lean

Nyll.EtaleFundamentalGroups.Cohomology.GenericPointCharacterDetection

2 declarations indexed from sourceView source ↗

Module documentation

Detecting actual finite H¹ classes at a separably closed generic point

The closure is arbitrary. This allows a geometric comparison made in the chosen constant-field extension to determine the actual global H¹ class.

Imports2

Imported by4

theorem

genericFieldAction_surjective

L26 ↗

AlgebraicGeometry.FiniteEtale.genericFieldAction_surjective

Documentation

Every automorphism of the geometric generic fibre of a normal integral scheme comes from a field automorphism of its chosen separable closure.

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry
open TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale

Lean source · full declaration

theorem genericFieldAction_surjective
    (X : Scheme) [IsIntegral X] [IsNormalIntegral X]
    (Ω : Type) [Field Ω] [Algebra X.functionField Ω]
    [IsSepClosed Ω] [IsSepClosure X.functionField Ω] :
    Function.Surjective (fun σ : Ω ≃ₐ[X.functionField] Ω =>
      fundamentalGroupHom (X.fromSpecStalk (genericPoint X))
        (Spec.map (CommRingCat.ofHom (algebraMap X.functionField Ω)))
        (toAut (fib X.functionField Ω) (Ω ≃ₐ[X.functionField] Ω) σ)) := by
  let j := X.fromSpecStalk (genericPoint X)
  let η := Spec.map (CommRingCat.ofHom (algebraMap X.functionField Ω))
  have : QuasiCompact j :=
    { isCompact_preimage := fun U _ _ => (Set.toFinite (j ⁻¹' U)).isCompact }
  have : IsDominant j := by
    rw [isDominant_iff, DenseRange, dense_iff_closure_eq]
    apply Set.eq_univ_of_forall
    intro x
    apply (genericPoint_specializes x).mem_closed isClosed_closure
    exact subset_closure ⟨IsLocalRing.closedPoint (CommRingCat.of X.functionField),
      Scheme.fromSpecStalk_closedPoint (X := X) (x := genericPoint X)⟩
  have hj := fundamentalGroupHom_surjective_of_isPreimmersion_of_isDominant j η
  have ha : Function.Surjective
      (toAut (fib X.functionField Ω) (Ω ≃ₐ[X.functionField] Ω)) := by
    intro g
    obtain ⟨σ, hσ⟩ :=
      (toAutHomeo (fib X.functionField Ω) (Ω ≃ₐ[X.functionField] Ω)).surjective g
    exact ⟨σ, (toAutHomeo_apply _ σ).symm.trans hσ⟩
  exact hj.comp ha

theorem

finiteH1_ext_genericFieldAction

L60 ↗

EtaleFundamentalGroups.Cohomology.finiteH1_ext_genericFieldAction