NYLL
Module

ProperH1CoprimeCoefficient.lean

Nyll.EtaleFundamentalGroups.Cohomology.ProperH1CoprimeCoefficient
2 declarations indexed from sourceView source ↗

Module documentation

Finite coefficients coprime to the actual covering index

Imports3
Imported by3

Declarations

theorem

pointedCoverOpenSubgroup_index_pos

L21 ↗
EtaleFundamentalGroups.Cohomology.pointedCoverOpenSubgroup_index_pos
Documentation

The actual covering stabilizer has positive finite index, proved from its finite geometric orbit.

Source context 3 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry
namespace EtaleFundamentalGroups.Cohomology
Lean source · statement
theorem pointedCoverOpenSubgroup_index_pos
    {S : Scheme} [ConnectedSpace S] (A : FiniteEtale S)
    {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (geom : Spec (.of Ω) ⟶ A.left) :
    0 < (pointedCoverOpenSubgroup A geom).toSubgroup.index
theorem

exists_rootsOfUnity_coefficient_coprime_index

L37 ↗
EtaleFundamentalGroups.Cohomology.exists_rootsOfUnity_coefficient_coprime_index
Documentation

Nontrivial roots-of-unity coefficients can always be chosen coprime to the actual covering index; no prime-existence or coprimality hypothesis is left to the geometric application.

Source context 3 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory AlgebraicGeometry
namespace EtaleFundamentalGroups.Cohomology
Lean source · statement
theorem exists_rootsOfUnity_coefficient_coprime_index
    (K : Type) [Field K] [IsAlgClosed K] [CharZero K]
    {S : Scheme} [ConnectedSpace S] (A : FiniteEtale S)
    {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (geom : Spec (.of Ω) ⟶ A.left) :
    ∃ n : ℕ+, 1 < (n : ℕ) ∧
      (Nat.card (Multiplicative
        (AddCommGrpCat.of (Additive (rootsOfUnity (n : ℕ) K))))).Coprime
          (pointedCoverOpenSubgroup A geom).toSubgroup.index

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.