Module

FullTateCharacters.lean

Nyll.ProCGroups.Abelian.FullTateCharacters

4 declarations indexed from sourceView source ↗

Module documentation

Finite-exponent characters of the actual full Tate module

The kernel of evaluation at n is exactly n times the full Tate module. Division inside that kernel is given by shifting the compatible family to the levels multiplied by n. Thus every character killed by n factors through the actual n-torsion projection when that projection is surjective.

Imports1

Nyll.ProCGroups.Abelian.FullTateModule

Imported by2

theorem

exists_nsmul_eq_of_evaluation_eq_zero

L24 ↗

ProCGroups.FullTateModule.exists_nsmul_eq_of_evaluation_eq_zero

Documentation

A compatible family vanishing at n can be divided by n by shifting its coordinates; no divisibility assumption on M is needed.

Source context 2 commands

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

namespace ProCGroups.FullTateModule
variable {M : Type*} [AddCommGroup M]

Lean source · statement

theorem exists_nsmul_eq_of_evaluation_eq_zero (n : ℕ+)
    (x : FullTateModule M) (hx : evaluation M n x = 0) :
    ∃ y : FullTateModule M, (n : ℕ) • y = x

theorem

evaluation_eq_zero_iff_exists_nsmul

L44 ↗

ProCGroups.FullTateModule.evaluation_eq_zero_iff_exists_nsmul

Documentation

The kernel of the n-th evaluation is precisely the subgroup of n-multiples in the full Tate module.

Source context 2 commands

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

namespace ProCGroups.FullTateModule
variable {M : Type*} [AddCommGroup M]

Lean source · statement

theorem evaluation_eq_zero_iff_exists_nsmul (n : ℕ+) (x : FullTateModule M) :
    evaluation M n x = 0 ↔ ∃ y : FullTateModule M, (n : ℕ) • y = x

theorem

character_eq_of_projection_eq

L53 ↗

ProCGroups.FullTateModule.character_eq_of_projection_eq

Documentation

Characters annihilated by n agree on fibres of the n-th projection.

Source context 2 commands

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

namespace ProCGroups.FullTateModule
variable {M : Type*} [AddCommGroup M]

Lean source · statement

theorem character_eq_of_projection_eq
    {H : Type*} [AddCommGroup H] (n : ℕ+)
    (φ : FullTateModule M →+ H) (hH : ∀ a : H, (n : ℕ) • a = 0)
    {x y : FullTateModule M}
    (hxy : projection M n x = projection M n y) : φ x = φ y

theorem

character_factors_through_projection

L68 ↗

ProCGroups.FullTateModule.character_factors_through_projection

Documentation

Every finite-exponent character factors through the same torsion level if the actual projection is surjective. Continuity is not needed here.

Source context 2 commands

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

namespace ProCGroups.FullTateModule
variable {M : Type*} [AddCommGroup M]

Lean source · statement

theorem character_factors_through_projection
    {H : Type*} [AddCommGroup H] (n : ℕ+)
    (hsurj : Function.Surjective (projection M n))
    (φ : FullTateModule M →+ H) (hH : ∀ a : H, (n : ℕ) • a = 0) :
    ∃ ψ : torsionLevel M n →+ H, ψ.comp (projection M n) = φ

Module documentation

Finite-exponent characters of the actual full Tate module

Declarations

exists_nsmul_eq_of_evaluation_eq_zero

evaluation_eq_zero_iff_exists_nsmul

character_eq_of_projection_eq

character_factors_through_projection