Module

FullTateModule.lean

Nyll.ProCGroups.Abelian.FullTateModule

21 declarations indexed from sourceView source ↗

Module documentation

The full Tate module of an additive commutative group

The full Tate module consists of actual torsion points indexed by positive integers, compatible under multiplication. It is torsion-free: if a positive integer annihilates a compatible family, compatibility with the levels multiplied by that integer makes every coordinate zero.

Each torsion level is given the discrete topology. The induced product subspace topology on the limit is Hausdorff and totally disconnected, and is compact when every actual torsion subgroup is finite.

Imports5

Mathlib.Algebra.Group.Subgroup.Basic
Mathlib.Algebra.Group.Torsion
Mathlib.Data.PNat.Basic
Mathlib.Topology.Algebra.Group.Subgroup
Mathlib.Topology.Connected.TotallyDisconnected

Imported by15

def

torsionLevel

L33 ↗

ProCGroups.torsionLevel

Documentation

The actual subgroup of points annihilated by a positive integer.

Source context 3 commands

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

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M]

Lean source · full declaration

def torsionLevel (n : ℕ+) : AddSubgroup M where
  carrier := {x : M | (n : ℕ) • x = 0}
  zero_mem' := nsmul_zero (n : ℕ)
  add_mem' := by
    intro x y hx hy
    change (n : ℕ) • (x + y) = 0
    rw [nsmul_add, hx, hy, zero_add]
  neg_mem' := by
    intro x hx
    change (n : ℕ) • (-x) = 0
    rw [smul_neg, hx, neg_zero]

def

torsionTransition

L46 ↗

ProCGroups.torsionTransition

Documentation

Multiplication by m maps the actual (n*m)-torsion into the n-torsion.

Source context 3 commands

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

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M]

Lean source · full declaration

def torsionTransition (n m : ℕ+) : torsionLevel M (n * m) →+ torsionLevel M n where
  toFun x := ⟨(m : ℕ) • x.val, by
    change (n : ℕ) • ((m : ℕ) • x.val) = 0
    rw [← mul_nsmul, Nat.mul_comm]
    exact x.property⟩
  map_zero' := by
    apply Subtype.ext
    exact nsmul_zero (m : ℕ)
  map_add' := by
    intro x y
    apply Subtype.ext
    exact nsmul_add x.val y.val (m : ℕ)

def

compatibleTorsionFamilies

L60 ↗

ProCGroups.compatibleTorsionFamilies

Documentation

The subgroup of the product satisfying every multiplication transition.

Source context 3 commands

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

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M]

Lean source · full declaration

def compatibleTorsionFamilies : AddSubgroup (∀ n : ℕ+, torsionLevel M n) where
  carrier := {x | ∀ n m : ℕ+, torsionTransition M n m (x (n * m)) = x n}
  zero_mem' := by
    intro n m
    exact (torsionTransition M n m).map_zero
  add_mem' := by
    intro x y hx hy n m
    change torsionTransition M n m (x (n * m) + y (n * m)) = x n + y n
    rw [map_add, hx n m, hy n m]
  neg_mem' := by
    intro x hx n m
    change torsionTransition M n m (-x (n * m)) = -x n
    rw [map_neg, hx n m]

def

FullTateModule

L75 ↗

ProCGroups.FullTateModule

Documentation

The full Tate module, realized as compatible actual torsion families.

Source context 3 commands

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

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M]

Lean source · statement

def FullTateModule : Type u

instance

(anonymous instance)

L79 ↗

Source context 4 commands

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

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M]
namespace FullTateModule

Lean source · statement

instance : AddCommGroup (FullTateModule M)

def

projection

L83 ↗

ProCGroups.FullTateModule.projection

Documentation

The canonical projection to an actual torsion subgroup.

Source context 4 commands

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

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M]
namespace FullTateModule

Lean source · full declaration

def projection (n : ℕ+) : FullTateModule M →+ torsionLevel M n where
  toFun x := x.val n
  map_zero' := rfl
  map_add' _ _ := rfl

def

evaluation

L89 ↗

ProCGroups.FullTateModule.evaluation

Documentation

The n-th torsion point, viewed in the original group.

Source context 4 commands

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

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M]
namespace FullTateModule

Lean source · statement

def evaluation (n : ℕ+) : FullTateModule M →+ M

theorem

ext

L95 ↗

ProCGroups.FullTateModule.ext

Documentation

Two full Tate elements agree when their actual torsion points agree.

Source context 5 commands

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

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M]
namespace FullTateModule
variable {M}

Lean source · statement

theorem ext {x y : FullTateModule M}
    (h : ∀ n : ℕ+, evaluation M n x = evaluation M n y) : x = y

theorem

evaluation_annihilated

L103 ↗

ProCGroups.FullTateModule.evaluation_annihilated

Documentation

Every projected point is annihilated by its index.

Source context 5 commands

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

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M]
namespace FullTateModule
variable {M}

Lean source · statement

theorem evaluation_annihilated (x : FullTateModule M) (n : ℕ+) :
    (n : ℕ) • evaluation M n x = 0

theorem

evaluation_compatible

L108 ↗

ProCGroups.FullTateModule.evaluation_compatible

Documentation

The compatibility equation holds in the original additive group.

Source context 5 commands

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

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M]
namespace FullTateModule
variable {M}

Lean source · statement

theorem evaluation_compatible (x : FullTateModule M) (n m : ℕ+) :
    (m : ℕ) • evaluation M (n * m) x = evaluation M n x

theorem

eq_zero_of_nsmul_eq_zero

L113 ↗

ProCGroups.FullTateModule.eq_zero_of_nsmul_eq_zero

Documentation

No nonzero positive-integer torsion occurs in the constructed full Tate module.

Source context 5 commands

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

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M]
namespace FullTateModule
variable {M}

Lean source · statement

theorem eq_zero_of_nsmul_eq_zero (x : FullTateModule M) {n : ℕ}
    (hn : 0 < n) (hx : n • x = 0) : x = 0

instance

(anonymous instance)

L125 ↗

Source context 5 commands

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

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M]
namespace FullTateModule
variable {M}

Lean source · full declaration

instance : IsAddTorsionFree (FullTateModule M) where
  nsmul_right_injective := by
    intro n hn x y hxy
    change n • x = n • y at hxy
    apply sub_eq_zero.mp
    apply eq_zero_of_nsmul_eq_zero (x - y) (Nat.pos_of_ne_zero hn)
    rw [nsmul_sub, hxy, sub_self]

def

torsionLevelTopology

L138 ↗

ProCGroups.FullTateModule.torsionLevelTopology

Documentation

The chosen topology at a torsion level is discrete, independently of any topology on the original group. It is installed only locally in this module.

Source context 6 commands

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

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M]
namespace FullTateModule
variable {M}
variable (M)

Lean source · statement

def torsionLevelTopology (n : ℕ+) : TopologicalSpace (torsionLevel M n)

instance

(anonymous instance)

L142 ↗

Source context 7 commands

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

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M]
namespace FullTateModule
variable {M}
variable (M)
attribute [local instance] torsionLevelTopology

Lean source · statement

instance (n : ℕ+) : DiscreteTopology (torsionLevel M n)

instance

(anonymous instance)

L146 ↗

Documentation

The full Tate topology is the subspace topology of the product of the discrete actual torsion levels.

Source context 8 commands

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

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M]
namespace FullTateModule
variable {M}
variable (M)
attribute [local instance] torsionLevelTopology
local instance (n : ℕ+) : DiscreteTopology (torsionLevel M n) := ⟨rfl⟩

Lean source · statement

instance : TopologicalSpace (FullTateModule M)

instance

(anonymous instance)

L149 ↗

Source context 8 commands

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

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M]
namespace FullTateModule
variable {M}
variable (M)
attribute [local instance] torsionLevelTopology
local instance (n : ℕ+) : DiscreteTopology (torsionLevel M n) := ⟨rfl⟩

Lean source · statement

instance : IsTopologicalAddGroup (FullTateModule M)

instance

(anonymous instance)

L152 ↗

Source context 8 commands

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

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M]
namespace FullTateModule
variable {M}
variable (M)
attribute [local instance] torsionLevelTopology
local instance (n : ℕ+) : DiscreteTopology (torsionLevel M n) := ⟨rfl⟩

Lean source · statement

instance : T2Space (FullTateModule M)

instance

(anonymous instance)

L155 ↗

Source context 8 commands

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

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M]
namespace FullTateModule
variable {M}
variable (M)
attribute [local instance] torsionLevelTopology
local instance (n : ℕ+) : DiscreteTopology (torsionLevel M n) := ⟨rfl⟩

Lean source · statement

instance : TotallyDisconnectedSpace (FullTateModule M)

theorem

continuous_projection

L159 ↗

ProCGroups.FullTateModule.continuous_projection

Documentation

Projection to every discrete torsion level is continuous.

Source context 8 commands

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

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M]
namespace FullTateModule
variable {M}
variable (M)
attribute [local instance] torsionLevelTopology
local instance (n : ℕ+) : DiscreteTopology (torsionLevel M n) := ⟨rfl⟩

Lean source · statement

theorem continuous_projection (n : ℕ+) : Continuous (projection M n)

theorem

isClosed_compatibleTorsionFamilies

L163 ↗

ProCGroups.FullTateModule.isClosed_compatibleTorsionFamilies

Documentation

Compatibility cuts out a closed subspace of the discrete-level product.

Source context 8 commands

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

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M]
namespace FullTateModule
variable {M}
variable (M)
attribute [local instance] torsionLevelTopology
local instance (n : ℕ+) : DiscreteTopology (torsionLevel M n) := ⟨rfl⟩

Lean source · statement

theorem isClosed_compatibleTorsionFamilies :
    IsClosed (compatibleTorsionFamilies M : Set (∀ n : ℕ+, torsionLevel M n))

instance

(anonymous instance)

L174 ↗

Documentation

Finite actual torsion levels make the full Tate module compact.

Source context 8 commands

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

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M]
namespace FullTateModule
variable {M}
variable (M)
attribute [local instance] torsionLevelTopology
local instance (n : ℕ+) : DiscreteTopology (torsionLevel M n) := ⟨rfl⟩

Lean source · statement

instance [∀ n : ℕ+, Finite (torsionLevel M n)] : CompactSpace (FullTateModule M)

Module documentation

The full Tate module of an additive commutative group

Declarations