NYLL
Module

LinearAdicH1Comparison.lean

Nyll.EtaleFundamentalGroups.Cohomology.LinearAdicH1Comparison
8 declarations indexed from sourceView source ↗

Module documentation

Linearity of the classical integral ℓ-adic H¹ comparison

The character group carries pointwise p-adic scalar multiplication. The comparison respects this actual action because finite-coefficient H¹ is natural for the scalar endomorphisms of its constant coefficient sheaf.

Imports3
Imported by2

Declarations

def

scalePadicCharacter

L30 ↗
EtaleFundamentalGroups.Cohomology.scalePadicCharacter
Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} {Ω : Type u} [Field Ω]
  (ξ : Spec (.of Ω) ⟶ X) (ℓ : ℕ) [Fact ℓ.Prime]
Lean source · statement
def scalePadicCharacter (c : ℤ_[ℓ]) (χ : padicCharacters ξ ℓ) :
    padicCharacters ξ ℓ
instance

padicCharactersModule

L43 ↗
EtaleFundamentalGroups.Cohomology.padicCharactersModule
Documentation

The canonical p-adic module structure on characters is pointwise multiplication.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} {Ω : Type u} [Field Ω]
  (ξ : Spec (.of Ω) ⟶ X) (ℓ : ℕ) [Fact ℓ.Prime]
Lean source · full declaration
instance padicCharactersModule : Module ℤ_[ℓ] (padicCharacters ξ ℓ) where
  smul := scalePadicCharacter ξ ℓ
  one_smul χ := ContinuousMonoidHom.ext fun g =>
    congrArg Multiplicative.ofAdd (one_mul (χ.toMul g).toAdd)
  mul_smul c d χ := ContinuousMonoidHom.ext fun g =>
    congrArg Multiplicative.ofAdd (mul_assoc c d (χ.toMul g).toAdd)
  smul_zero c := ContinuousMonoidHom.ext fun _ =>
    congrArg Multiplicative.ofAdd (mul_zero c)
  smul_add c χ ψ := ContinuousMonoidHom.ext fun g =>
    congrArg Multiplicative.ofAdd (mul_add c (χ.toMul g).toAdd (ψ.toMul g).toAdd)
  add_smul c d χ := ContinuousMonoidHom.ext fun g =>
    congrArg Multiplicative.ofAdd (add_mul c d (χ.toMul g).toAdd)
  zero_smul χ := ContinuousMonoidHom.ext fun g =>
    congrArg Multiplicative.ofAdd (zero_mul (χ.toMul g).toAdd)
theorem

padicCharacters_smul_apply

L59 ↗
EtaleFundamentalGroups.Cohomology.padicCharacters_smul_apply
Documentation

The scalar action on characters agrees with multiplication of their values.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} {Ω : Type u} [Field Ω]
  (ξ : Spec (.of Ω) ⟶ X) (ℓ : ℕ) [Fact ℓ.Prime]
Lean source · statement
theorem padicCharacters_smul_apply (c : ℤ_[ℓ]) (χ : padicCharacters ξ ℓ)
    (g : Aut (FiniteEtale.fiber ξ)) :
    ((c • χ).toMul g).toAdd = c * (χ.toMul g).toAdd
theorem

finiteComparison_smul

L67 ↗
EtaleFundamentalGroups.Cohomology.finiteComparison_smul
Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} {Ω : Type u} [Field Ω]
  (ξ : Spec (.of Ω) ⟶ X) (ℓ : ℕ) [Fact ℓ.Prime]
variable [ConnectedSpace X] [IsSepClosed Ω]
attribute [local instance] finiteCoefficientTopology finiteCoefficientDiscrete
Lean source · statement
theorem finiteComparison_smul (n : ℕ) (c : ℤ_[ℓ])
    (a : finiteLevelCohomology X ℓ n 1) (g : Aut (FiniteEtale.fiber ξ)) :
    ((finiteH1CharacterEquiv (ellPowerCoefficients ℓ n) ξ (c • a)).toMul g).toAdd.down =
      PadicInt.toZModPow (n + 1) c *
        ((finiteH1CharacterEquiv (ellPowerCoefficients ℓ n) ξ a).toMul g).toAdd.down
theorem

ellAdicH1PadicCharacterEquiv_reduction

L80 ↗
EtaleFundamentalGroups.Cohomology.ellAdicH1PadicCharacterEquiv_reduction
Documentation

Reduction of the integral comparison is the original finite-coefficient comparison.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} {Ω : Type u} [Field Ω]
  (ξ : Spec (.of Ω) ⟶ X) (ℓ : ℕ) [Fact ℓ.Prime]
variable [ConnectedSpace X] [IsSepClosed Ω]
attribute [local instance] finiteCoefficientTopology finiteCoefficientDiscrete
Lean source · statement
theorem ellAdicH1PadicCharacterEquiv_reduction (a : ellAdicCohomology X ℓ 1)
    (n : ℕ) (g : Aut (FiniteEtale.fiber ξ)) :
    PadicInt.toZModPow (n + 1) ((ellAdicH1PadicCharacterEquiv ξ ℓ a).toMul g).toAdd =
      ((finiteH1CharacterEquiv (ellPowerCoefficients ℓ n) ξ (a.val n)).toMul g).toAdd.down
theorem

ellAdicH1PadicCharacterEquiv_smul

L91 ↗
EtaleFundamentalGroups.Cohomology.ellAdicH1PadicCharacterEquiv_smul
Documentation

The integral H¹ comparison respects the actual coefficient-induced p-adic action.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} {Ω : Type u} [Field Ω]
  (ξ : Spec (.of Ω) ⟶ X) (ℓ : ℕ) [Fact ℓ.Prime]
variable [ConnectedSpace X] [IsSepClosed Ω]
attribute [local instance] finiteCoefficientTopology finiteCoefficientDiscrete
Lean source · statement
theorem ellAdicH1PadicCharacterEquiv_smul (c : ℤ_[ℓ]) (a : ellAdicCohomology X ℓ 1) :
    ellAdicH1PadicCharacterEquiv ξ ℓ (c • a) = c • ellAdicH1PadicCharacterEquiv ξ ℓ a
def

ellAdicH1PadicCharacterLinearEquiv

L114 ↗
EtaleFundamentalGroups.Cohomology.ellAdicH1PadicCharacterLinearEquiv
Documentation

Classical integral ℓ-adic H¹ and continuous p-adic characters are canonically isomorphic as modules over the actual p-adic integer ring.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} {Ω : Type u} [Field Ω]
  (ξ : Spec (.of Ω) ⟶ X) (ℓ : ℕ) [Fact ℓ.Prime]
variable [ConnectedSpace X] [IsSepClosed Ω]
attribute [local instance] finiteCoefficientTopology finiteCoefficientDiscrete
Lean source · full declaration
def ellAdicH1PadicCharacterLinearEquiv :
    ellAdicCohomology X ℓ 1 ≃ₗ[ℤ_[ℓ]] padicCharacters ξ ℓ where
  __ := ellAdicH1PadicCharacterEquiv ξ ℓ
  map_smul' := ellAdicH1PadicCharacterEquiv_smul ξ ℓ
def

rationalEllAdicH1TensorCharacterEquiv

L122 ↗
EtaleFundamentalGroups.Cohomology.rationalEllAdicH1TensorCharacterEquiv
Documentation

Rational classical H¹ is the scalar extension of the actual integral continuous character module. This does not discard integral torsion in order to claim reconstruction of the full profinite abelianization.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} {Ω : Type u} [Field Ω]
  (ξ : Spec (.of Ω) ⟶ X) (ℓ : ℕ) [Fact ℓ.Prime]
variable [ConnectedSpace X] [IsSepClosed Ω]
attribute [local instance] finiteCoefficientTopology finiteCoefficientDiscrete
Lean source · statement
def rationalEllAdicH1TensorCharacterEquiv :
    rationalEllAdicCohomology ℓ X 1 ≃ₗ[ℚ_[ℓ]]
      TensorProduct ℤ_[ℓ] ℚ_[ℓ] (padicCharacters ξ ℓ)

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