NYLL
Module

PadicH1Comparison.lean

Nyll.EtaleFundamentalGroups.Cohomology.PadicH1Comparison
21 declarations indexed from sourceView source ↗

Module documentation

Classical integral ℓ-adic H¹ and p-adic continuous characters

Compatible finite characters determine actual p-adic integers, whose topology is detected by reduction at every level. Consequently their pointwise limit is continuous. Combined with the finite-coefficient étale H¹ comparison this identifies classical integral ℓ-adic H¹ with continuous p-adic characters of the actual étale fundamental group. Connectedness and a geometric point are the only geometric assumptions.

Imports4
Imported by2

Declarations

instance

finiteCoefficientTopology

L37 ↗
EtaleFundamentalGroups.Cohomology.finiteCoefficientTopology
Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open LocalFieldTheory.PadicResidues
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}}
  {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
  (ℓ : ℕ) [Fact ℓ.Prime]
Lean source · statement
instance finiteCoefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ellPowerCoefficients.{u} ℓ n))
instance

finiteCoefficientDiscrete

L39 ↗
EtaleFundamentalGroups.Cohomology.finiteCoefficientDiscrete
Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open LocalFieldTheory.PadicResidues
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}}
  {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
  (ℓ : ℕ) [Fact ℓ.Prime]
local instance finiteCoefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⊥
Lean source · statement
instance finiteCoefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (ellPowerCoefficients.{u} ℓ n))
instance

residueTopology

L41 ↗
EtaleFundamentalGroups.Cohomology.residueTopology
Source context 9 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open LocalFieldTheory.PadicResidues
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}}
  {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
  (ℓ : ℕ) [Fact ℓ.Prime]
local instance finiteCoefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⊥
local instance finiteCoefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⟨rfl⟩
Lean source · statement
instance residueTopology (n : ℕ) : TopologicalSpace (ZMod (ℓ ^ n))
instance

residueDiscrete

L42 ↗
EtaleFundamentalGroups.Cohomology.residueDiscrete
Source context 10 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open LocalFieldTheory.PadicResidues
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}}
  {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
  (ℓ : ℕ) [Fact ℓ.Prime]
local instance finiteCoefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⊥
local instance finiteCoefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⟨rfl⟩
local instance residueTopology (n : ℕ) : TopologicalSpace (ZMod (ℓ ^ n)) := ⊥
Lean source · statement
instance residueDiscrete (n : ℕ) : DiscreteTopology (ZMod (ℓ ^ n))
abbrev

padicCharacters

L45 ↗
EtaleFundamentalGroups.Cohomology.padicCharacters
Documentation

Continuous characters into the actual additive p-adic integers.

Source context 11 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open LocalFieldTheory.PadicResidues
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}}
  {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
  (ℓ : ℕ) [Fact ℓ.Prime]
local instance finiteCoefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⊥
local instance finiteCoefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⟨rfl⟩
local instance residueTopology (n : ℕ) : TopologicalSpace (ZMod (ℓ ^ n)) := ⊥
local instance residueDiscrete (n : ℕ) : DiscreteTopology (ZMod (ℓ ^ n)) := ⟨rfl⟩
Lean source · statement
abbrev padicCharacters : Type (u + 1)
def

characterResidues

L48 ↗
EtaleFundamentalGroups.Cohomology.characterResidues
Source context 11 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open LocalFieldTheory.PadicResidues
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}}
  {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
  (ℓ : ℕ) [Fact ℓ.Prime]
local instance finiteCoefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⊥
local instance finiteCoefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⟨rfl⟩
local instance residueTopology (n : ℕ) : TopologicalSpace (ZMod (ℓ ^ n)) := ⊥
local instance residueDiscrete (n : ℕ) : DiscreteTopology (ZMod (ℓ ^ n)) := ⟨rfl⟩
Lean source · statement
def characterResidues (χ : compatibleFiniteCharacters ξ ℓ)
    (g : Aut (FiniteEtale.fiber ξ)) : compatibleResidues ℓ
def

characterLimit

L63 ↗
EtaleFundamentalGroups.Cohomology.characterLimit
Source context 11 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open LocalFieldTheory.PadicResidues
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}}
  {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
  (ℓ : ℕ) [Fact ℓ.Prime]
local instance finiteCoefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⊥
local instance finiteCoefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⟨rfl⟩
local instance residueTopology (n : ℕ) : TopologicalSpace (ZMod (ℓ ^ n)) := ⊥
local instance residueDiscrete (n : ℕ) : DiscreteTopology (ZMod (ℓ ^ n)) := ⟨rfl⟩
Lean source · statement
def characterLimit (χ : compatibleFiniteCharacters ξ ℓ)
    (g : Aut (FiniteEtale.fiber ξ)) : ℤ_[ℓ]
theorem

characterLimit_spec

L67 ↗
EtaleFundamentalGroups.Cohomology.characterLimit_spec
Source context 11 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open LocalFieldTheory.PadicResidues
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}}
  {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
  (ℓ : ℕ) [Fact ℓ.Prime]
local instance finiteCoefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⊥
local instance finiteCoefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⟨rfl⟩
local instance residueTopology (n : ℕ) : TopologicalSpace (ZMod (ℓ ^ n)) := ⊥
local instance residueDiscrete (n : ℕ) : DiscreteTopology (ZMod (ℓ ^ n)) := ⟨rfl⟩
Lean source · statement
theorem characterLimit_spec (χ : compatibleFiniteCharacters ξ ℓ)
    (g : Aut (FiniteEtale.fiber ξ)) (n : ℕ) :
    PadicInt.toZModPow (n + 1) (characterLimit ξ ℓ χ g) =
      ((χ.val n).toMul g).toAdd.down
theorem

padic_ext_positive

L73 ↗
EtaleFundamentalGroups.Cohomology.padic_ext_positive
Source context 11 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open LocalFieldTheory.PadicResidues
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}}
  {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
  (ℓ : ℕ) [Fact ℓ.Prime]
local instance finiteCoefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⊥
local instance finiteCoefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⟨rfl⟩
local instance residueTopology (n : ℕ) : TopologicalSpace (ZMod (ℓ ^ n)) := ⊥
local instance residueDiscrete (n : ℕ) : DiscreteTopology (ZMod (ℓ ^ n)) := ⟨rfl⟩
Lean source · statement
theorem padic_ext_positive {a b : ℤ_[ℓ]}
    (h : ∀ n, PadicInt.toZModPow (n + 1) a = PadicInt.toZModPow (n + 1) b) : a = b
theorem

characterLimit_mul

L83 ↗
EtaleFundamentalGroups.Cohomology.characterLimit_mul
Source context 11 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open LocalFieldTheory.PadicResidues
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}}
  {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
  (ℓ : ℕ) [Fact ℓ.Prime]
local instance finiteCoefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⊥
local instance finiteCoefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⟨rfl⟩
local instance residueTopology (n : ℕ) : TopologicalSpace (ZMod (ℓ ^ n)) := ⊥
local instance residueDiscrete (n : ℕ) : DiscreteTopology (ZMod (ℓ ^ n)) := ⟨rfl⟩
Lean source · statement
theorem characterLimit_mul (χ : compatibleFiniteCharacters ξ ℓ)
    (g h : Aut (FiniteEtale.fiber ξ)) :
    characterLimit ξ ℓ χ (g * h) = characterLimit ξ ℓ χ g + characterLimit ξ ℓ χ h
theorem

characterLimit_one

L92 ↗
EtaleFundamentalGroups.Cohomology.characterLimit_one
Source context 11 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open LocalFieldTheory.PadicResidues
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}}
  {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
  (ℓ : ℕ) [Fact ℓ.Prime]
local instance finiteCoefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⊥
local instance finiteCoefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⟨rfl⟩
local instance residueTopology (n : ℕ) : TopologicalSpace (ZMod (ℓ ^ n)) := ⊥
local instance residueDiscrete (n : ℕ) : DiscreteTopology (ZMod (ℓ ^ n)) := ⟨rfl⟩
Lean source · statement
theorem characterLimit_one (χ : compatibleFiniteCharacters ξ ℓ) :
    characterLimit ξ ℓ χ 1 = 0
theorem

continuous_characterLimit

L100 ↗
EtaleFundamentalGroups.Cohomology.continuous_characterLimit
Source context 11 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open LocalFieldTheory.PadicResidues
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}}
  {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
  (ℓ : ℕ) [Fact ℓ.Prime]
local instance finiteCoefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⊥
local instance finiteCoefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⟨rfl⟩
local instance residueTopology (n : ℕ) : TopologicalSpace (ZMod (ℓ ^ n)) := ⊥
local instance residueDiscrete (n : ℕ) : DiscreteTopology (ZMod (ℓ ^ n)) := ⟨rfl⟩
Lean source · statement
theorem continuous_characterLimit (χ : compatibleFiniteCharacters ξ ℓ) :
    Continuous (characterLimit ξ ℓ χ)
def

compatibleCharacterLimit

L121 ↗
EtaleFundamentalGroups.Cohomology.compatibleCharacterLimit
Documentation

The continuous p-adic character obtained by taking actual residue limits.

Source context 11 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open LocalFieldTheory.PadicResidues
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}}
  {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
  (ℓ : ℕ) [Fact ℓ.Prime]
local instance finiteCoefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⊥
local instance finiteCoefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⟨rfl⟩
local instance residueTopology (n : ℕ) : TopologicalSpace (ZMod (ℓ ^ n)) := ⊥
local instance residueDiscrete (n : ℕ) : DiscreteTopology (ZMod (ℓ ^ n)) := ⟨rfl⟩
Lean source · statement
def compatibleCharacterLimit (χ : compatibleFiniteCharacters ξ ℓ) : padicCharacters ξ ℓ
def

padicCharacterReduction

L130 ↗
EtaleFundamentalGroups.Cohomology.padicCharacterReduction
Documentation

Reduction of a continuous p-adic character at a positive finite level.

Source context 11 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open LocalFieldTheory.PadicResidues
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}}
  {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
  (ℓ : ℕ) [Fact ℓ.Prime]
local instance finiteCoefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⊥
local instance finiteCoefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⟨rfl⟩
local instance residueTopology (n : ℕ) : TopologicalSpace (ZMod (ℓ ^ n)) := ⊥
local instance residueDiscrete (n : ℕ) : DiscreteTopology (ZMod (ℓ ^ n)) := ⟨rfl⟩
Lean source · statement
def padicCharacterReduction (n : ℕ) (χ : padicCharacters ξ ℓ) :
    finiteLevelCharacters ξ ℓ n
def

padicCharacterResidues

L153 ↗
EtaleFundamentalGroups.Cohomology.padicCharacterResidues
Documentation

Simultaneous finite reductions of a p-adic character, as an additive homomorphism.

Source context 11 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open LocalFieldTheory.PadicResidues
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}}
  {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
  (ℓ : ℕ) [Fact ℓ.Prime]
local instance finiteCoefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⊥
local instance finiteCoefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⟨rfl⟩
local instance residueTopology (n : ℕ) : TopologicalSpace (ZMod (ℓ ^ n)) := ⊥
local instance residueDiscrete (n : ℕ) : DiscreteTopology (ZMod (ℓ ^ n)) := ⟨rfl⟩
Lean source · full declaration
def padicCharacterResidues : padicCharacters ξ ℓ →+ compatibleFiniteCharacters ξ ℓ where
  toFun χ := ⟨fun n => padicCharacterReduction ξ ℓ n χ, fun n => by
    apply ContinuousMonoidHom.ext
    intro g
    exact congrArg (fun z => Multiplicative.ofAdd (ULift.up.{u} z))
      (congrArg (fun f : ℤ_[ℓ] →+* ZMod (ℓ ^ (n + 1)) => f (χ.toMul g).toAdd)
        (PadicInt.zmod_cast_comp_toZModPow (n + 1) (n + 2) (Nat.le_succ (n + 1))))⟩
  map_zero' := by
    apply Subtype.ext
    funext n
    apply ContinuousMonoidHom.ext
    intro g
    exact congrArg (fun z => Multiplicative.ofAdd (ULift.up.{u} z))
      (PadicInt.toZModPow (n + 1)).map_zero
  map_add' χ ψ := by
    apply Subtype.ext
    funext n
    apply ContinuousMonoidHom.ext
    intro g
    exact congrArg (fun z => Multiplicative.ofAdd (ULift.up.{u} z))
      ((PadicInt.toZModPow (n + 1)).map_add (χ.toMul g).toAdd (ψ.toMul g).toAdd)
theorem

padicCharacterResidues_injective

L175 ↗
EtaleFundamentalGroups.Cohomology.padicCharacterResidues_injective
Source context 11 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open LocalFieldTheory.PadicResidues
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}}
  {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
  (ℓ : ℕ) [Fact ℓ.Prime]
local instance finiteCoefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⊥
local instance finiteCoefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⟨rfl⟩
local instance residueTopology (n : ℕ) : TopologicalSpace (ZMod (ℓ ^ n)) := ⊥
local instance residueDiscrete (n : ℕ) : DiscreteTopology (ZMod (ℓ ^ n)) := ⟨rfl⟩
Lean source · statement
theorem padicCharacterResidues_injective :
    Function.Injective (padicCharacterResidues ξ ℓ)
theorem

padicCharacterResidues_limit

L186 ↗
EtaleFundamentalGroups.Cohomology.padicCharacterResidues_limit
Source context 11 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open LocalFieldTheory.PadicResidues
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}}
  {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
  (ℓ : ℕ) [Fact ℓ.Prime]
local instance finiteCoefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⊥
local instance finiteCoefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⟨rfl⟩
local instance residueTopology (n : ℕ) : TopologicalSpace (ZMod (ℓ ^ n)) := ⊥
local instance residueDiscrete (n : ℕ) : DiscreteTopology (ZMod (ℓ ^ n)) := ⟨rfl⟩
Lean source · statement
theorem padicCharacterResidues_limit (χ : compatibleFiniteCharacters ξ ℓ) :
    padicCharacterResidues ξ ℓ (compatibleCharacterLimit ξ ℓ χ) = χ
def

padicCompatibleCharacterEquiv

L196 ↗
EtaleFundamentalGroups.Cohomology.padicCompatibleCharacterEquiv
Documentation

Actual continuous p-adic characters are exactly compatible finite characters.

Source context 11 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open LocalFieldTheory.PadicResidues
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}}
  {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
  (ℓ : ℕ) [Fact ℓ.Prime]
local instance finiteCoefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⊥
local instance finiteCoefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⟨rfl⟩
local instance residueTopology (n : ℕ) : TopologicalSpace (ZMod (ℓ ^ n)) := ⊥
local instance residueDiscrete (n : ℕ) : DiscreteTopology (ZMod (ℓ ^ n)) := ⟨rfl⟩
Lean source · statement
def padicCompatibleCharacterEquiv :
    padicCharacters ξ ℓ ≃+ compatibleFiniteCharacters ξ ℓ
def

ellAdicH1PadicCharacterEquiv

L204 ↗
EtaleFundamentalGroups.Cohomology.ellAdicH1PadicCharacterEquiv
Documentation

Classical integral ℓ-adic H¹ of any connected scheme is the additive group of continuous ℤℓ-valued characters of its étale fundamental group.

Source context 11 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open LocalFieldTheory.PadicResidues
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}}
  {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
  (ℓ : ℕ) [Fact ℓ.Prime]
local instance finiteCoefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⊥
local instance finiteCoefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⟨rfl⟩
local instance residueTopology (n : ℕ) : TopologicalSpace (ZMod (ℓ ^ n)) := ⊥
local instance residueDiscrete (n : ℕ) : DiscreteTopology (ZMod (ℓ ^ n)) := ⟨rfl⟩
Lean source · statement
def ellAdicH1PadicCharacterEquiv [ConnectedSpace X] [IsSepClosed Ω] :
    ellAdicCohomology X ℓ 1 ≃+ padicCharacters ξ ℓ
def

padicAbelianCharacterEquiv

L210 ↗
EtaleFundamentalGroups.Cohomology.padicAbelianCharacterEquiv
Documentation

Restriction along the closed-commutator quotient identifies p-adic characters of the actual topological abelianization with fundamental-group characters.

Source context 11 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open LocalFieldTheory.PadicResidues
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}}
  {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
  (ℓ : ℕ) [Fact ℓ.Prime]
local instance finiteCoefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⊥
local instance finiteCoefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⟨rfl⟩
local instance residueTopology (n : ℕ) : TopologicalSpace (ZMod (ℓ ^ n)) := ⊥
local instance residueDiscrete (n : ℕ) : DiscreteTopology (ZMod (ℓ ^ n)) := ⟨rfl⟩
Lean source · full declaration
def padicAbelianCharacterEquiv :
    Additive (TopologicalAbelianization (Aut (FiniteEtale.fiber ξ)) →ₜ*
      Multiplicative ℤ_[ℓ]) ≃+ padicCharacters ξ ℓ where
  toFun χ := Additive.ofMul (χ.toMul.comp
    (ProCGroups.Abelian.TopologicalAbelianization.mkₜ _))
  invFun χ := Additive.ofMul (ProCGroups.Abelian.TopologicalAbelianization.lift χ.toMul)
  left_inv χ := by
    apply ProCGroups.Abelian.TopologicalAbelianization.hom_ext
    intro g
    rfl
  right_inv χ := ContinuousMonoidHom.ext fun _ => rfl
  map_add' χ ψ := ContinuousMonoidHom.ext fun _ => rfl
def

ellAdicH1AbelianPadicCharacterEquiv

L225 ↗
EtaleFundamentalGroups.Cohomology.ellAdicH1AbelianPadicCharacterEquiv
Documentation

Classical integral ℓ-adic H¹ is the group of continuous p-adic characters of the fundamental group's quotient by its closed commutator subgroup.

Source context 11 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
open LocalFieldTheory.PadicResidues
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}}
  {Ω : Type u} [Field Ω] (ξ : Spec (.of Ω) ⟶ X)
  (ℓ : ℕ) [Fact ℓ.Prime]
local instance finiteCoefficientTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⊥
local instance finiteCoefficientDiscrete (n : ℕ) :
    DiscreteTopology (Multiplicative (ellPowerCoefficients.{u} ℓ n)) := ⟨rfl⟩
local instance residueTopology (n : ℕ) : TopologicalSpace (ZMod (ℓ ^ n)) := ⊥
local instance residueDiscrete (n : ℕ) : DiscreteTopology (ZMod (ℓ ^ n)) := ⟨rfl⟩
Lean source · statement
def ellAdicH1AbelianPadicCharacterEquiv [ConnectedSpace X] [IsSepClosed Ω] :
    ellAdicCohomology X ℓ 1 ≃+
      Additive (TopologicalAbelianization (Aut (FiniteEtale.fiber ξ)) →ₜ*
        Multiplicative ℤ_[ℓ])

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