Module

Depth.lean

Nyll.ProCGroups.ProP.Zassenhaus.Depth

9 declarations indexed from sourceView source ↗

Module documentation

Zassenhaus depth predicates

Depth is exposed through at least, exactly, and infinite predicates. This avoids assigning an arbitrary finite value to elements lying in every filtration layer, and gives the later relation-counting API a decidable finite-index predicate without installing new data instances.

Imports1

Nyll.ProCGroups.ProP.Zassenhaus.Functoriality

Imported by5

def

ZassenhausDepthAtLeast

L31 ↗

ClassFieldTower.ProP.ZassenhausDepthAtLeast

Documentation

An element has Zassenhaus depth at least n when it belongs to Dₙ.

Source context 7 commands

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

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

Lean source · statement

def ZassenhausDepthAtLeast (n : ℕ) (g : G) : Prop

def

ZassenhausDepthExactly

L36 ↗

ClassFieldTower.ProP.ZassenhausDepthExactly

Documentation

An element has exact finite depth n when it belongs to Dₙ but not Dₙ₊₁.

Source context 7 commands

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

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

Lean source · statement

def ZassenhausDepthExactly (n : ℕ) (g : G) : Prop

def

ZassenhausDepthInfinite

L40 ↗

ClassFieldTower.ProP.ZassenhausDepthInfinite

Documentation

An element has infinite depth when it belongs to every Zassenhaus layer.

Source context 7 commands

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

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

Lean source · statement

def ZassenhausDepthInfinite (g : G) : Prop

theorem

zassenhausDepthAtLeast_mono

L44 ↗

ClassFieldTower.ProP.zassenhausDepthAtLeast_mono

Documentation

A lower depth bound can be weakened.

Source context 7 commands

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

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

Lean source · statement

theorem zassenhausDepthAtLeast_mono {m n : ℕ} (hmn : m ≤ n) {g : G}
    (hg : ZassenhausDepthAtLeast p n g) :
    ZassenhausDepthAtLeast p m g

theorem

zassenhausDepthAtLeast_one

L50 ↗

ClassFieldTower.ProP.zassenhausDepthAtLeast_one

Documentation

Every group element has depth at least one.

Source context 7 commands

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

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

Lean source · statement

theorem zassenhausDepthAtLeast_one (g : G) :
    ZassenhausDepthAtLeast p 1 g

theorem

zassenhausDepthInfinite_one

L55 ↗

ClassFieldTower.ProP.zassenhausDepthInfinite_one

Documentation

The identity lies in every Zassenhaus layer.

Source context 7 commands

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

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

Lean source · statement

theorem zassenhausDepthInfinite_one :
    ZassenhausDepthInfinite p (1 : G)

theorem

zassenhausDepthExactly_unique

L62 ↗

ClassFieldTower.ProP.zassenhausDepthExactly_unique

Documentation

Exact finite Zassenhaus depth is unique.

Source context 7 commands

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

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

Lean source · statement

theorem zassenhausDepthExactly_unique {m n : ℕ} {g : G}
    (hm : ZassenhausDepthExactly p m g)
    (hn : ZassenhausDepthExactly p n g) : m = n

theorem

zassenhausDepthAtLeast_map

L74 ↗

ClassFieldTower.ProP.zassenhausDepthAtLeast_map

Documentation

Continuous homomorphisms do not decrease a proved lower depth bound.

Source context 7 commands

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

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

Lean source · statement

theorem zassenhausDepthAtLeast_map (f : G →ₜ* H) (n : ℕ) {g : G}
    (hg : ZassenhausDepthAtLeast p n g) :
    ZassenhausDepthAtLeast p n (f g)

theorem

zassenhausDepthInfinite_map

L80 ↗

ClassFieldTower.ProP.zassenhausDepthInfinite_map

Documentation

Continuous homomorphisms preserve infinite depth.

Source context 7 commands

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

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

Lean source · statement

theorem zassenhausDepthInfinite_map (f : G →ₜ* H) {g : G}
    (hg : ZassenhausDepthInfinite p g) :
    ZassenhausDepthInfinite p (f g)

Module documentation

Zassenhaus depth predicates

Declarations