NYLL
Module

RationalH1Comparison.lean

Nyll.EtaleFundamentalGroups.Cohomology.RationalH1Comparison
15 declarations indexed from sourceView source ↗

Module documentation

Classical rational ℓ-adic H¹ and continuous characters

Compactness of the actual étale fundamental group gives a common integral denominator for each continuous Qℓ-valued character. Consequently its module of continuous Qℓ-valued characters is the scalar extension of its integral character module. This identifies ordinary rational ℓ-adic H¹ with actual continuous Qℓ-valued characters, without a pro-étale definition.

Imports5
Imported by1

Declarations

abbrev

rationalPadicCharacters

L35 ↗
EtaleFundamentalGroups.Cohomology.rationalPadicCharacters
Documentation

Continuous characters into the additive group of the actual p-adic field.

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
abbrev rationalPadicCharacters : Type (u + 1)
def

scaleRationalCharacter

L38 ↗
EtaleFundamentalGroups.Cohomology.scaleRationalCharacter
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 scaleRationalCharacter (c : ℚ_[ℓ]) (χ : rationalPadicCharacters ξ ℓ) :
    rationalPadicCharacters ξ ℓ
instance

rationalPadicCharactersModule

L51 ↗
EtaleFundamentalGroups.Cohomology.rationalPadicCharactersModule
Documentation

Rational scalars act on continuous characters by 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 rationalPadicCharactersModule : Module ℚ_[ℓ] (rationalPadicCharacters ξ ℓ) where
  smul := scaleRationalCharacter ξ ℓ
  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)
instance

rationalPadicCharactersIntegralModule

L67 ↗
EtaleFundamentalGroups.Cohomology.rationalPadicCharactersIntegralModule
Documentation

Integral scalars use the canonical inclusion of p-adic integers into their field.

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
instance rationalPadicCharactersIntegralModule :
    Module ℤ_[ℓ] (rationalPadicCharacters ξ ℓ)
instance

rationalPadicCharactersScalarTower

L72 ↗
EtaleFundamentalGroups.Cohomology.rationalPadicCharactersScalarTower
Documentation

The integral and rational actions use the same scalar 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 rationalPadicCharactersScalarTower :
    IsScalarTower ℤ_[ℓ] ℚ_[ℓ] (rationalPadicCharacters ξ ℓ) where
  smul_assoc c d χ := ContinuousMonoidHom.ext fun g =>
    congrArg Multiplicative.ofAdd (mul_assoc (c : ℚ_[ℓ]) d (χ.toMul g).toAdd)
def

integralCharacterInclusion

L78 ↗
EtaleFundamentalGroups.Cohomology.integralCharacterInclusion
Documentation

Inclusion of integral characters into rational characters, with the actual scalar actions.

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
def integralCharacterInclusion :
    padicCharacters ξ ℓ →ₗ[ℤ_[ℓ]] rationalPadicCharacters ξ ℓ where
  toFun χ := Additive.ofMul
    { toFun := fun g => Multiplicative.ofAdd ((χ.toMul g).toAdd : ℚ_[ℓ])
      map_one' := congrArg (fun z : Multiplicative ℤ_[ℓ] =>
        Multiplicative.ofAdd (z.toAdd : ℚ_[ℓ])) (map_one χ.toMul)
      map_mul' g h := congrArg (fun z : Multiplicative ℤ_[ℓ] =>
        Multiplicative.ofAdd (z.toAdd : ℚ_[ℓ])) (map_mul χ.toMul g h)
      continuous_toFun := continuous_ofAdd.comp
        (continuous_subtype_val.comp (continuous_toAdd.comp χ.toMul.continuous)) }
  map_add' _ _ := ContinuousMonoidHom.ext fun _ => rfl
  map_smul' _ _ := ContinuousMonoidHom.ext fun _ => rfl
theorem

integralCharacterInclusion_injective

L92 ↗
EtaleFundamentalGroups.Cohomology.integralCharacterInclusion_injective
Documentation

Inclusion of integral continuous characters is injective.

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 integralCharacterInclusion_injective :
    Function.Injective (integralCharacterInclusion ξ ℓ)
def

integralMultiple

L100 ↗
EtaleFundamentalGroups.Cohomology.integralMultiple
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 integralMultiple (χ : rationalPadicCharacters ξ ℓ) (n : ℕ)
    (hn : ∀ g, ‖(ℓ : ℚ_[ℓ]) ^ n * (χ.toMul g).toAdd‖ ≤ 1) :
    padicCharacters ξ ℓ
theorem

rationalCharacter_has_integral_multiple

L118 ↗
EtaleFundamentalGroups.Cohomology.rationalCharacter_has_integral_multiple
Documentation

Every rational continuous character has a common integral denominator.

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 rationalCharacter_has_integral_multiple (χ : rationalPadicCharacters ξ ℓ) :
    ∃ n : ℕ, ∃ ψ : padicCharacters ξ ℓ,
      ((ℓ : ℤ_[ℓ]) ^ n) • χ = integralCharacterInclusion ξ ℓ ψ
instance

integralCharacterInclusion_isLocalizedModule

L126 ↗
EtaleFundamentalGroups.Cohomology.integralCharacterInclusion_isLocalizedModule
Documentation

Rational continuous characters are the localization of integral continuous characters.

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 integralCharacterInclusion_isLocalizedModule :
    IsLocalizedModule (nonZeroDivisors ℤ_[ℓ]) (integralCharacterInclusion ξ ℓ) where
  map_units s := by
    rw [← (Algebra.lsmul ℤ_[ℓ] (A := ℚ_[ℓ]) ℤ_[ℓ]
      (rationalPadicCharacters ξ ℓ)).commutes]
    exact (IsLocalization.map_units ℚ_[ℓ] s).map _
  surj χ := by
    obtain ⟨n, ψ, hψ⟩ := rationalCharacter_has_integral_multiple ξ ℓ χ
    have hℓ : (ℓ : ℤ_[ℓ]) ≠ 0 := Nat.cast_ne_zero.mpr (Fact.out : ℓ.Prime).ne_zero
    exact ⟨(ψ, ⟨(ℓ : ℤ_[ℓ]) ^ n,
      mem_nonZeroDivisors_iff_ne_zero.mpr (pow_ne_zero n hℓ)⟩), hψ⟩
  exists_of_eq h := by
    have h' := integralCharacterInclusion_injective ξ ℓ h
    exact ⟨1, congrArg (fun χ : padicCharacters ξ ℓ => (1 : ℤ_[ℓ]) • χ) h'⟩
def

rationalCharacterTensorEquiv

L143 ↗
EtaleFundamentalGroups.Cohomology.rationalCharacterTensorEquiv
Documentation

Scalar extension of integral characters is the module of actual rational continuous characters; surjectivity follows from compactness, not an extra boundedness hypothesis.

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 rationalCharacterTensorEquiv :
    TensorProduct ℤ_[ℓ] ℚ_[ℓ] (padicCharacters ξ ℓ) ≃ₗ[ℚ_[ℓ]]
      rationalPadicCharacters ξ ℓ
theorem

rationalCharacterTensorEquiv_tmul

L151 ↗
EtaleFundamentalGroups.Cohomology.rationalCharacterTensorEquiv_tmul
Documentation

The tensor comparison sends a pure tensor to the corresponding scalar multiple of the included integral character.

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 rationalCharacterTensorEquiv_tmul (c : ℚ_[ℓ]) (χ : padicCharacters ξ ℓ) :
    rationalCharacterTensorEquiv ξ ℓ (c ⊗ₜ[ℤ_[ℓ]] χ) =
      c • integralCharacterInclusion ξ ℓ χ
def

rationalAbelianCharacterEquiv

L159 ↗
EtaleFundamentalGroups.Cohomology.rationalAbelianCharacterEquiv
Documentation

Rational characters of the actual closed-commutator quotient are exactly the rational characters of the fundamental group.

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
def rationalAbelianCharacterEquiv :
    Additive (TopologicalAbelianization (Aut (FiniteEtale.fiber ξ)) →ₜ*
      Multiplicative ℚ_[ℓ]) ≃+ rationalPadicCharacters ξ ℓ 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

rationalEllAdicH1CharacterEquiv

L176 ↗
EtaleFundamentalGroups.Cohomology.rationalEllAdicH1CharacterEquiv
Documentation

Ordinary rational ℓ-adic H¹ of a connected scheme is its continuous Qℓ-valued character module. No smoothness, properness, noetherian, or characteristic hypothesis is needed.

Source context 6 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 Ω]
Lean source · statement
def rationalEllAdicH1CharacterEquiv :
    rationalEllAdicCohomology ℓ X 1 ≃ₗ[ℚ_[ℓ]] rationalPadicCharacters ξ ℓ
def

rationalEllAdicH1AbelianCharacterEquiv

L183 ↗
EtaleFundamentalGroups.Cohomology.rationalEllAdicH1AbelianCharacterEquiv
Documentation

Ordinary rational ℓ-adic H¹ is the continuous rational character group of the actual topological abelianization. This statement does not assert that rational characters recover the torsion of that abelianization.

Source context 6 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 Ω]
Lean source · statement
def rationalEllAdicH1AbelianCharacterEquiv :
    rationalEllAdicCohomology ℓ 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.