Module

IntegerCharacters.lean

Nyll.AnabelianGeometry.KummerTheory.IntegerCharacters

2 declarations indexed from sourceView source ↗

Module documentation

Integer characters detecting non-torsion elements

The structure theorem for finitely generated abelian groups supplies an integer-valued character nonzero on any prescribed non-torsion element. Applying that character to a power relation yields an integral divisibility constraint on its exponent.

Imports1

Mathlib.GroupTheory.FiniteAbelian.Basic

Imported by2

theorem

exists_integer_character_ne_one

L26 ↗

AnabelianGeometry.KummerTheory.exists_integer_character_ne_one

Documentation

A non-torsion element of a finitely generated abelian group is detected by a homomorphism to the infinite cyclic group.

Source context 3 commands

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

noncomputable section
namespace AnabelianGeometry.KummerTheory
variable {G : Type*} [CommGroup G]

Lean source · statement

theorem exists_integer_character_ne_one [Group.FG G]
    (a : G) (ha : ¬ IsOfFinOrder a) :
    ∃ f : G →* Multiplicative ℤ, f a ≠ 1

theorem

integer_character_dvd_of_zpow_eq_pow

L55 ↗

AnabelianGeometry.KummerTheory.integer_character_dvd_of_zpow_eq_pow