NYLL
Module

OpenNormal.lean

Nyll.ProCGroups.ProP.Zassenhaus.OpenNormal
4 declarations indexed from sourceView source ↗

Module documentation

Deep finite open quotients and lifts

Iterating the open power--commutator core produces open normal subgroups inside arbitrary closed augmentation degrees. Applying an actual compact surjective homomorphism to such a source subgroup gives a target open normal subgroup whose elements have source lifts of the required depth.

Imports8
Imported by2

Declarations

theorem

closedPowerCommutator_map_le_zassenhaus_double

L38 ↗
ClassFieldTower.ProP.closedPowerCommutator_map_le_zassenhaus_double
Source context 7 commands

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

open scoped commutatorElement
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC ProCGroups.FiniteGeneration
noncomputable section
universe u v
variable (p : ℕ) [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem closedPowerCommutator_map_le_zassenhaus_double
    (H : Subgroup G) (n : ℕ) (hH : H ≤ zassenhausSubgroup p G n) :
    (closedPowerCommutator p H).map H.subtype ≤ zassenhausSubgroup p G (2 * n)
theorem

exists_openNormal_le_zassenhausSubgroup

L60 ↗
ClassFieldTower.ProP.exists_openNormal_le_zassenhausSubgroup
Documentation

Every prescribed augmentation depth contains an actual open normal subgroup.

Source context 7 commands

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

open scoped commutatorElement
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC ProCGroups.FiniteGeneration
noncomputable section
universe u v
variable (p : ℕ) [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem exists_openNormal_le_zassenhausSubgroup
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hfg : TopologicallyFinitelyGenerated G) (n : ℕ) :
    ∃ U : OpenNormalSubgroup G, (U : Subgroup G) ≤ zassenhausSubgroup p G n
theorem

isOpen_zassenhausSubgroup

L95 ↗
ClassFieldTower.ProP.isOpen_zassenhausSubgroup
Documentation

The closed augmentation filtration is open at every finite degree for a finitely generated profinite group.

Source context 7 commands

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

open scoped commutatorElement
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC ProCGroups.FiniteGeneration
noncomputable section
universe u v
variable (p : ℕ) [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem isOpen_zassenhausSubgroup
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hfg : TopologicallyFinitelyGenerated G) (n : ℕ) :
    IsOpen (zassenhausSubgroup p G n : Set G)
theorem

exists_openNormal_with_zassenhaus_lifts

L104 ↗
ClassFieldTower.ProP.exists_openNormal_with_zassenhaus_lifts
Documentation

Selecting a finite quotient through the image of a deep source subgroup provides actual source lifts with the same lower depth bound.

Source context 7 commands

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

open scoped commutatorElement
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC ProCGroups.FiniteGeneration
noncomputable section
universe u v
variable (p : ℕ) [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem exists_openNormal_with_zassenhaus_lifts
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H]
    (hfg : TopologicallyFinitelyGenerated G) (q : G →ₜ* H)
    (hq : Function.Surjective q) (n : ℕ) :
    ∃ U : OpenNormalSubgroup H, ∀ g : H, g ∈ U →
      ∃ f : G, q f = g ∧ ZassenhausDepthAtLeast p n f

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