NYLL
Module

PowerSeparation.lean

Nyll.AnabelianGeometry.KummerTheory.PowerSeparation
5 declarations indexed from sourceView source ↗

Module documentation

Separation by power quotients

In a finitely generated abelian group, an element divisible by every positive integer is trivial. Applying this to a quotient shows that every subgroup is the intersection of its enlargements by ambient power subgroups.

Imports2
  • Mathlib.GroupTheory.FiniteAbelian.Basic
  • Mathlib.Data.Int.Basic
Imported by3

Declarations

theorem

eq_one_of_forall_exists_pow

L24 ↗
AnabelianGeometry.KummerTheory.eq_one_of_forall_exists_pow
Documentation

A finitely generated abelian group has no nontrivial element divisible by every positive integer.

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_pow (x : G)
    (h : ∀ n : ℕ+, ∃ y : G, y ^ (n : ℕ) = x) : x = 1
theorem

mem_of_forall_mem_sup_powers

L60 ↗
AnabelianGeometry.KummerTheory.mem_of_forall_mem_sup_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_powers (H : Subgroup G) (x : G)
    (h : ∀ n : ℕ+, x ∈ H ⊔ (powMonoidHom (α := G) (n : ℕ)).range) : x ∈ H
theorem

iInf_sup_powers_eq

L76 ↗
AnabelianGeometry.KummerTheory.iInf_sup_powers_eq
Documentation

A subgroup of a finitely generated abelian group is recovered from all its finite power quotients.

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 iInf_sup_powers_eq (H : Subgroup G) :
    (⨅ n : ℕ+, H ⊔ (powMonoidHom (α := G) (n : ℕ)).range) = H
theorem

zpowers_eq_of_forall_sup_powers_eq

L85 ↗
AnabelianGeometry.KummerTheory.zpowers_eq_of_forall_sup_powers_eq
Documentation

Equal cyclic subgroups in every power quotient determine the same cyclic subgroup in the original finitely generated abelian group.

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 zpowers_eq_of_forall_sup_powers_eq (a b : G)
    (h : ∀ n : ℕ+,
      Subgroup.zpowers a ⊔ (powMonoidHom (α := G) (n : ℕ)).range =
      Subgroup.zpowers b ⊔ (powMonoidHom (α := G) (n : ℕ)).range) :
    Subgroup.zpowers a = Subgroup.zpowers b
theorem

mem_of_forall_mem_sup_powers_of_saturated

L97 ↗
AnabelianGeometry.KummerTheory.mem_of_forall_mem_sup_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_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 : ∀ n : ℕ+, x ∈ H ⊔ (powMonoidHom (α := G) (n : ℕ)).range) : x ∈ H

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