Module

Functoriality.lean

Nyll.ProCGroups.ProP.Zassenhaus.Functoriality

5 declarations indexed from sourceView source ↗

Module documentation

Functoriality of the Zassenhaus filtration

A continuous group homomorphism induces the existing functorial map on class-indexed completed group algebras. Naturality of augmentation and continuity of that map show that every closed augmentation power, hence every Zassenhaus subgroup, is preserved.

Imports2

Imported by3

def

modPCompletedGroupAlgebraMap

L35 ↗

ClassFieldTower.ProP.modPCompletedGroupAlgebraMap

Documentation

The mod-p completed group-algebra map induced by a continuous group homomorphism.

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
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 modPCompletedGroupAlgebraMap (f : G →ₜ* H) :
    ModPCompletedGroupAlgebra p G →+* ModPCompletedGroupAlgebra p H

theorem

modPCompletedGroupAlgebraMap_groupLikeDifference

L45 ↗

ClassFieldTower.ProP.modPCompletedGroupAlgebraMap_groupLikeDifference

Documentation

The induced completed map sends a group-like difference to the difference of the image.

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
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 modPCompletedGroupAlgebraMap_groupLikeDifference
    (f : G →ₜ* H) (g : G) :
    modPCompletedGroupAlgebraMap p f (groupLikeDifference p G g) =
      groupLikeDifference p H (f g)

theorem

modPCompletedGroupAlgebraMap_mem_closedAugmentationPower

L55 ↗

ClassFieldTower.ProP.modPCompletedGroupAlgebraMap_mem_closedAugmentationPower

Documentation

Functorial completed group-algebra maps preserve every closed power of the augmentation ideal.

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
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 modPCompletedGroupAlgebraMap_mem_closedAugmentationPower
    (f : G →ₜ* H) (n : ℕ) {x : ModPCompletedGroupAlgebra p G}
    (hx : x ∈ closedAugmentationPower p G n) :
    modPCompletedGroupAlgebraMap p f x ∈ closedAugmentationPower p H n

theorem

map_mem_zassenhausSubgroup

L80 ↗

ClassFieldTower.ProP.map_mem_zassenhausSubgroup

Documentation

Continuous homomorphisms preserve membership in each Zassenhaus subgroup.

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
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 map_mem_zassenhausSubgroup
    (f : G →ₜ* H) (n : ℕ) {g : G}
    (hg : g ∈ zassenhausSubgroup p G n) :
    f g ∈ zassenhausSubgroup p H n

theorem

map_zassenhausSubgroup_le

L89 ↗

ClassFieldTower.ProP.Subgroup.map_zassenhausSubgroup_le

Documentation

The subgroup image of Dₙ(G) is contained in Dₙ(H).

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
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 Subgroup.map_zassenhausSubgroup_le
    (f : G →ₜ* H) (n : ℕ) :
    (zassenhausSubgroup p G n).map f ≤ zassenhausSubgroup p H n

Module documentation

Functoriality of the Zassenhaus filtration

Declarations

modPCompletedGroupAlgebraMap

modPCompletedGroupAlgebraMap_groupLikeDifference

modPCompletedGroupAlgebraMap_mem_closedAugmentationPower

map_mem_zassenhausSubgroup

map_zassenhausSubgroup_le