Module

PrimePowerSeparation.lean

Nyll.AnabelianGeometry.KummerTheory.PrimePowerSeparation

3 declarations indexed from sourceView source ↗

Module documentation

Separation by prime-power quotients

Prime powers suffice to recover subgroups of finitely generated abelian groups. The saturated-subgroup version also applies to S-unit groups.

Imports1

Nyll.AnabelianGeometry.KummerTheory.PowerSeparation

Imported by2

theorem

eq_one_of_forall_exists_prime_pow

L22 ↗

AnabelianGeometry.KummerTheory.eq_one_of_forall_exists_prime_pow

Documentation

A finitely generated abelian group has no nontrivial element divisible by every power of every prime.

Source context 2 commands

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

namespace AnabelianGeometry.KummerTheory
variable {G : Type*} [CommGroup G] [Group.FG G]

Lean source · statement

theorem eq_one_of_forall_exists_prime_pow (x : G)
    (h : ∀ p : ℕ, p.Prime → ∀ r : ℕ, ∃ y : G, y ^ (p ^ r) = x) : x = 1

theorem

mem_of_forall_mem_sup_prime_powers

L58 ↗

AnabelianGeometry.KummerTheory.mem_of_forall_mem_sup_prime_powers

Documentation

Membership in every power enlargement already implies membership in the original subgroup. The ambient group is finitely generated and abelian.

Source context 2 commands

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

namespace AnabelianGeometry.KummerTheory
variable {G : Type*} [CommGroup G] [Group.FG G]

Lean source · statement

theorem mem_of_forall_mem_sup_prime_powers (H : Subgroup G) (x : G)
    (h : ∀ p : ℕ, p.Prime → ∀ r : ℕ,
      x ∈ H ⊔ (powMonoidHom (α := G) (p ^ r)).range) : x ∈ H

theorem

mem_of_forall_mem_sup_prime_powers_of_saturated

L76 ↗

AnabelianGeometry.KummerTheory.mem_of_forall_mem_sup_prime_powers_of_saturated

Documentation

Power separation can be checked in a finitely generated subgroup that contains every root of each of its elements.

Source context 3 commands

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

namespace AnabelianGeometry.KummerTheory
variable {G : Type*} [CommGroup G] [Group.FG G]
omit [Group.FG G] in

Lean source · statement

theorem mem_of_forall_mem_sup_prime_powers_of_saturated
    (S H : Subgroup G) [Group.FG S] (hHS : H ≤ S)
    (hsat : ∀ (n : ℕ+) (y : G), y ^ (n : ℕ) ∈ S → y ∈ S)
    (x : G) (hx : x ∈ S)
    (h : ∀ p : ℕ, p.Prime → ∀ r : ℕ,
      x ∈ H ⊔ (powMonoidHom (α := G) (p ^ r)).range) : x ∈ H

Module documentation

Separation by prime-power quotients

Declarations

eq_one_of_forall_exists_prime_pow

mem_of_forall_mem_sup_prime_powers

mem_of_forall_mem_sup_prime_powers_of_saturated