Module

Laws.lean

Nyll.ProCGroups.ProP.Zassenhaus.Laws

4 declarations indexed from sourceView source ↗

Module documentation

Commutator and power laws for the Zassenhaus filtration

The completed group-like commutator identity sends elements of filtration degrees i and j to degree i + j. In characteristic p, the completed group-like difference of a p-th power is a p-th power, giving degree p * i. The elementwise statements are promoted to the corresponding subgroup inclusions.

Imports1

Nyll.ProCGroups.ProP.Zassenhaus.Basic

Imported by2

theorem

commutator_mem_zassenhausSubgroup_add

L32 ↗

ClassFieldTower.ProP.commutator_mem_zassenhausSubgroup_add

Documentation

A commutator of elements of Zassenhaus degrees i and j has degree i + j.

Source context 6 commands

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

open scoped Topology commutatorElement
namespace ClassFieldTower.ProP
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem commutator_mem_zassenhausSubgroup_add
    {i j : ℕ} {g h : G}
    (hg : g ∈ zassenhausSubgroup p G i)
    (hh : h ∈ zassenhausSubgroup p G j) :
    ⁅g, h⁆ ∈ zassenhausSubgroup p G (i + j)

theorem

commutator_zassenhausSubgroup_le_add

L56 ↗

ClassFieldTower.ProP.commutator_zassenhausSubgroup_le_add

Documentation

The commutator subgroup of the i-th and j-th Zassenhaus subgroups is contained in degree i + j.

Source context 6 commands

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

open scoped Topology commutatorElement
namespace ClassFieldTower.ProP
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem commutator_zassenhausSubgroup_le_add (i j : ℕ) :
    ⁅zassenhausSubgroup p G i, zassenhausSubgroup p G j⁆ ≤
      zassenhausSubgroup p G (i + j)

theorem

pow_mem_zassenhausSubgroup_mul

L65 ↗

ClassFieldTower.ProP.pow_mem_zassenhausSubgroup_mul

Documentation

The p-th power of an element of Zassenhaus degree i has degree p * i.

Source context 6 commands

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

open scoped Topology commutatorElement
namespace ClassFieldTower.ProP
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem pow_mem_zassenhausSubgroup_mul
    {i : ℕ} {g : G} (hg : g ∈ zassenhausSubgroup p G i) :
    g ^ p ∈ zassenhausSubgroup p G (p * i)

theorem

powerSubgroup_map_le_zassenhausSubgroup_mul

L76 ↗

ClassFieldTower.ProP.powerSubgroup_map_le_zassenhausSubgroup_mul

Documentation

The subgroup generated by p-th powers in the i-th Zassenhaus subgroup, mapped into the ambient group, is contained in degree p * i.

Source context 6 commands

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

open scoped Topology commutatorElement
namespace ClassFieldTower.ProP
noncomputable section
universe u
variable (p : ℕ) [Fact p.Prime]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem powerSubgroup_map_le_zassenhausSubgroup_mul (i : ℕ) :
    (powerSubgroup p (zassenhausSubgroup p G i)).map
        (zassenhausSubgroup p G i).subtype ≤
      zassenhausSubgroup p G (p * i)

Module documentation

Commutator and power laws for the Zassenhaus filtration

Declarations

commutator_mem_zassenhausSubgroup_add

commutator_zassenhausSubgroup_le_add

pow_mem_zassenhausSubgroup_mul

powerSubgroup_map_le_zassenhausSubgroup_mul