NYLL
Module

TateFiniteSubgroups.lean

Nyll.AnabelianGeometry.WeightFiltration.TateFiniteSubgroups
1 declaration indexed from sourceView source ↗

Module documentation

Finite point subgroups contain no nonzero compatible Tate family

This is the group-theoretic input for ruling out fixed Tate vectors after identifying fixed geometric points with a finite rational-point group. The geometric identification and finiteness are separate requirements.

Imports2
Imported by1

Declarations

theorem

fullTate_eq_zero_of_evaluation_mem_finite_subgroup

L26 ↗
AnabelianGeometry.WeightFiltration.fullTate_eq_zero_of_evaluation_mem_finite_subgroup
Documentation

A compatible family whose every coordinate lies in one finite subgroup vanishes. Finiteness separately at each level would not suffice.

Source context 3 commands

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

namespace AnabelianGeometry.WeightFiltration
open ProCGroups
variable {M : Type*} [AddCommGroup M]
Lean source · statement
theorem fullTate_eq_zero_of_evaluation_mem_finite_subgroup
    (S : AddSubgroup M) [Finite S] (x : FullTateModule M)
    (hx : ∀ n : ℕ+, FullTateModule.evaluation M n x ∈ S) : x = 0

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