NYLL
Module

CyclicDetection.lean

Nyll.AnabelianGeometry.CuspidalInertia.CyclicDetection
2 declarations indexed from sourceView source ↗

Module documentation

Closed cyclic subgroups and relative abelianization tests

The closure of the powers of an element is commutative. Compact character separation therefore detects that element in an open relative abelianization unless its closed cyclic subgroup meets the prescribed family nontrivially.

Imports1
Imported by1

Declarations

theorem

exists_openSubgroup_cyclic_detects

L27 ↗
AnabelianGeometry.CuspidalInertia.exists_openSubgroup_cyclic_detects
Documentation

If a nontrivial closed cyclic subgroup meets the compact family only at one, an open relative abelianization detects its generator.

Source context 4 commands

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

namespace AnabelianGeometry.CuspidalInertia
open scoped IsMulCommutative
universe u
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
theorem exists_openSubgroup_cyclic_detects (z : G) (hz : z ≠ 1)
    {S : Set G} (hS : IsCompact S)
    (hinter : ∀ x ∈ (Subgroup.zpowers z).topologicalClosure, x ∈ S → x = 1) :
    ∃ (V : OpenSubgroup G) (hzV : z ∈ V),
      (⟨z, hzV⟩ : V) ∉
        (Subgroup.closure {s : (V : Subgroup G) | (s : G) ∈ S} ⊔
          commutator (V : Subgroup G)).topologicalClosure
theorem

exists_nontrivial_cyclic_intersection_of_relative_tests

L51 ↗
AnabelianGeometry.CuspidalInertia.exists_nontrivial_cyclic_intersection_of_relative_tests
Documentation

Passing every relative abelianization test forces a nontrivial intersection of the closed cyclic subgroup with the compact family.

Source context 4 commands

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

namespace AnabelianGeometry.CuspidalInertia
open scoped IsMulCommutative
universe u
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
theorem exists_nontrivial_cyclic_intersection_of_relative_tests
    (z : G) (hz : z ≠ 1) {S : Set G} (hS : IsCompact S)
    (htest : ∀ (V : OpenSubgroup G) (hzV : z ∈ V),
      (⟨z, hzV⟩ : V) ∈
        (Subgroup.closure {s : (V : Subgroup G) | (s : G) ∈ S} ⊔
          commutator (V : Subgroup G)).topologicalClosure) :
    ∃ x ∈ (Subgroup.zpowers z).topologicalClosure, x ∈ S ∧ x ≠ 1

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