Module

CountableRelatorFiniteWitness.lean

Nyll.ProCGroups.ProP.CountableRelatorFiniteWitness

5 declarations indexed from sourceView source ↗

Module documentation

A finite witness for a finite quotient by countably many relations

If a finitely generated pro-p group modulo a closed normal relator closure is finite, its open kernel is finitely generated. The finite Frattini quotient of that kernel then supplies a finite prefix with the same closed normal closure. No finite presentation of the countable quotient is an input.

Imports10

Nyll.ProCGroups.ProP.ClosedChainStabilization
Nyll.ProCGroups.FiniteGeneration.OpenSubgroups
Nyll.ProCGroups.Presentations.Profinite
Nyll.ProCGroups.ProC.Subgroups.Closed
Nyll.ProCGroups.FiniteGroups.StandardClasses
Mathlib.Algebra.Group.Subgroup.Pointwise
Mathlib.Algebra.Group.Subgroup.Map
Mathlib.Algebra.Group.Subgroup.Ker
Mathlib.GroupTheory.Index
Mathlib.Topology.Algebra.Group.ClosedSubgroup

Imported by2

theorem

prefix_closedNormalClosure_mono

L37 ↗

ClassFieldTower.ProP.prefix_closedNormalClosure_mono

Source context 5 commands

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

namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.Presentations ProCGroups.FiniteGeneration
universe u
section Closure
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]

Lean source · full declaration

theorem prefix_closedNormalClosure_mono (R₀ : Set F) (f : ℕ → F) :
    Monotone (fun n ↦ closedNormalClosure (R₀ ∪ f '' (Finset.range n : Set ℕ))) := by
  intro m n hmn
  apply closedNormalClosure_le_closed_normal (closedNormalClosure_isClosed _)
  apply Set.Subset.trans _ (subset_closedNormalClosure _)
  exact Set.union_subset_union_right R₀
    (Set.image_mono (by exact_mod_cast Finset.range_mono hmn))

theorem

prefix_closedNormalClosure_le

L45 ↗

ClassFieldTower.ProP.prefix_closedNormalClosure_le

Source context 5 commands

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

namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.Presentations ProCGroups.FiniteGeneration
universe u
section Closure
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]

Lean source · statement

theorem prefix_closedNormalClosure_le (R₀ : Set F) (f : ℕ → F) (n : ℕ) :
    closedNormalClosure (R₀ ∪ f '' (Finset.range n : Set ℕ)) ≤
      closedNormalClosure (R₀ ∪ Set.range f)

theorem

closedNormalClosure_countable_eq_closure_iSup

L54 ↗

ClassFieldTower.ProP.closedNormalClosure_countable_eq_closure_iSup

Documentation

The closed normal closure of countably many new relators is the closure of the increasing supremum of the finite-prefix normal closures.

Source context 5 commands

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

namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.Presentations ProCGroups.FiniteGeneration
universe u
section Closure
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]

Lean source · statement

theorem closedNormalClosure_countable_eq_closure_iSup (R₀ : Set F) (f : ℕ → F) :
    closedNormalClosure (R₀ ∪ Set.range f) =
      (⨆ n, closedNormalClosure (R₀ ∪ f '' (Finset.range n : Set ℕ))).topologicalClosure

theorem

exists_stage_eq_of_closed_sup

L78 ↗

ClassFieldTower.ProP.exists_stage_eq_of_closed_sup

Source context 3 commands

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

namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.Presentations ProCGroups.FiniteGeneration
universe u

Lean source · statement

theorem exists_stage_eq_of_closed_sup
    {p : ℕ} [Fact p.Prime]
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    (hpro : ProC.HasPGroupOpenNormalBasis p F)
    (R : Subgroup F) (hRclosed : IsClosed (R : Set F))
    (hRfg : TopologicallyFinitelyGenerated R)
    (H : ℕ → Subgroup F) (hmono : Monotone H)
    (hclosed : ∀ n, IsClosed (H n : Set F))
    (hle : ∀ n, H n ≤ R)
    (hclosure : (⨆ n, H n).topologicalClosure = R) :
    ∃ n, H n = R

theorem

exists_finitePrefix_eq_closedNormalClosure_of_finite_quotient

L125 ↗

ClassFieldTower.ProP.exists_finitePrefix_eq_closedNormalClosure_of_finite_quotient

Documentation

A finite quotient by a countable closed normal relator closure already has the same kernel after a finite prefix of the added relations.

Source context 3 commands

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

namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.Presentations ProCGroups.FiniteGeneration
universe u

Lean source · statement

theorem exists_finitePrefix_eq_closedNormalClosure_of_finite_quotient
    {p : ℕ} [Fact p.Prime]
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    (hpro : ProC.HasPGroupOpenNormalBasis p F)
    (hfg : TopologicallyFinitelyGenerated F)
    (R₀ : Set F) (f : ℕ → F)
    [Finite (F ⧸ closedNormalClosure (R₀ ∪ Set.range f))] :
    ∃ n, closedNormalClosure (R₀ ∪ f '' (Finset.range n : Set ℕ)) =
      closedNormalClosure (R₀ ∪ Set.range f)

Module documentation

A finite witness for a finite quotient by countably many relations

Declarations

prefix_closedNormalClosure_mono

prefix_closedNormalClosure_le

closedNormalClosure_countable_eq_closure_iSup

exists_stage_eq_of_closed_sup

exists_finitePrefix_eq_closedNormalClosure_of_finite_quotient