Module

AugmentationFiltration.lean

Nyll.ProCGroups.ProP.Zassenhaus.AugmentationFiltration

12 declarations indexed from sourceView source ↗

Module documentation

The closed augmentation filtration over `ZMod p`

This file specializes the completed group algebra already provided by ProCGroups to finite p-group quotients and packages the closures of the powers of its canonical augmentation ideal. The elementary multiplicative lemmas are stated once here so later Zassenhaus files need no repeated two-sided-ideal instances.

Imports3

Mathlib.Topology.Algebra.Ring.Ideal
Nyll.ProCGroups.CompletedGroupAlgebra.Augmentation.Functoriality
Nyll.ProCGroups.FiniteGroups.StandardClasses

Imported by5

abbrev

ModPCompletedGroupAlgebra

L35 ↗

ClassFieldTower.ProP.ModPCompletedGroupAlgebra

Documentation

The mod-p completed group algebra formed from finite p-group quotients.

Source context 7 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]

Lean source · statement

abbrev ModPCompletedGroupAlgebra

theorem

modPCompletedGroupAlgebraCharP

L42 ↗

ClassFieldTower.ProP.modPCompletedGroupAlgebraCharP

Documentation

The mod-p completed group algebra has characteristic p.

The proof uses the canonical augmentation as a retraction to ZMod p; no global characteristic instance is installed.

Source context 7 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]

Lean source · full declaration

theorem modPCompletedGroupAlgebraCharP :
    CharP (ModPCompletedGroupAlgebra p G) p where
  cast_eq_zero_iff n := by
    constructor
    · intro hn
      have haug := congrArg
        (CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationInClass
          (R := ZMod p) (G := G) (ProCGroups.FiniteGroupClass.pGroup p)) hn
      have hnZMod : (n : ZMod p) = 0 := by
        simpa using haug
      exact (CharP.cast_eq_zero_iff (ZMod p) p n).mp hnZMod
    · intro hn
      have hnZMod : (n : ZMod p) = 0 :=
        (CharP.cast_eq_zero_iff (ZMod p) p n).mpr hn
      calc
        (n : ModPCompletedGroupAlgebra p G) =
            algebraMap (ZMod p) (ModPCompletedGroupAlgebra p G) (n : ZMod p) := by
              simp
        _ = 0 := by rw [hnZMod, map_zero]

abbrev

modPAugmentationIdeal

L63 ↗

ClassFieldTower.ProP.modPAugmentationIdeal

Documentation

The canonical augmentation ideal in the mod-p completed group algebra.

Source context 7 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]

Lean source · statement

abbrev modPAugmentationIdeal : Ideal (ModPCompletedGroupAlgebra p G)

def

closedAugmentationPower

L68 ↗

ClassFieldTower.ProP.closedAugmentationPower

Documentation

The closure of the n-th power of the mod-p augmentation ideal.

Source context 7 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]

Lean source · statement

def closedAugmentationPower (n : ℕ) : Ideal (ModPCompletedGroupAlgebra p G)

theorem

closedAugmentationPower_antitone

L72 ↗

ClassFieldTower.ProP.closedAugmentationPower_antitone

Documentation

Closed augmentation powers decrease with the exponent.

Source context 7 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]

Lean source · statement

theorem closedAugmentationPower_antitone : Antitone (closedAugmentationPower p G)

theorem

mul_mem_idealClosure_mul

L80 ↗

ClassFieldTower.ProP.mul_mem_idealClosure_mul

Documentation

Multiplication of points in two ideal closures lands in the closure of the ideal product.

Source context 7 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]

Lean source · statement

theorem mul_mem_idealClosure_mul
    {R : Type*} [Ring R] [TopologicalSpace R] [IsTopologicalRing R]
    {I J : Ideal R} {x y : R} (hx : x ∈ I.closure) (hy : y ∈ J.closure) :
    x * y ∈ (I * J).closure

theorem

modPAugmentationIdeal_isTwoSided

L95 ↗

ClassFieldTower.ProP.modPAugmentationIdeal_isTwoSided

Documentation

The canonical augmentation ideal is two-sided.

Source context 7 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]

Lean source · statement

theorem modPAugmentationIdeal_isTwoSided :
    (modPAugmentationIdeal p G).IsTwoSided

theorem

closedAugmentationPower_mul_mem

L104 ↗

ClassFieldTower.ProP.closedAugmentationPower_mul_mem

Documentation

Closed augmentation powers multiply with additive exponents.

Source context 7 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]

Lean source · statement

theorem closedAugmentationPower_mul_mem
    {m n : ℕ} {x y : ModPCompletedGroupAlgebra p G}
    (hx : x ∈ closedAugmentationPower p G m)
    (hy : y ∈ closedAugmentationPower p G n) :
    x * y ∈ closedAugmentationPower p G (m + n)

theorem

pow_mem_closedAugmentationPower

L117 ↗

ClassFieldTower.ProP.pow_mem_closedAugmentationPower

Documentation

A power of a point in the n-th closed augmentation layer belongs to the n*k-th layer.

Source context 7 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]

Lean source · statement

theorem pow_mem_closedAugmentationPower
    {n : ℕ} {x : ModPCompletedGroupAlgebra p G}
    (hx : x ∈ closedAugmentationPower p G n) (k : ℕ) :
    x ^ k ∈ closedAugmentationPower p G (n * k)

theorem

ringHom_mem_ideal_pow

L134 ↗

ClassFieldTower.ProP.ringHom_mem_ideal_pow

Documentation

A ring homomorphism taking I to J takes I^n to J^n.

Source context 7 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]

Lean source · statement

theorem ringHom_mem_ideal_pow
    {R S : Type*} [Ring R] [Ring S] (f : R →+* S)
    {I : Ideal R} {J : Ideal S}
    (hmap : ∀ x ∈ I, f x ∈ J) (n : ℕ) {x : R} (hx : x ∈ I ^ n) :
    f x ∈ J ^ n

theorem

idealClosure_isTwoSided

L154 ↗

ClassFieldTower.ProP.idealClosure_isTwoSided

Documentation

The closure of a two-sided ideal remains two-sided in a topological ring.

Source context 7 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]

Lean source · statement

theorem idealClosure_isTwoSided
    {R : Type*} [Ring R] [TopologicalSpace R] [IsTopologicalRing R]
    (I : Ideal R) [I.IsTwoSided] : I.closure.IsTwoSided

theorem

closedAugmentationPower_isTwoSided

L163 ↗

ClassFieldTower.ProP.closedAugmentationPower_isTwoSided

Documentation

Every closed augmentation power is two-sided.

Source context 7 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]

Lean source · statement

theorem closedAugmentationPower_isTwoSided (n : ℕ) :
    (closedAugmentationPower p G n).IsTwoSided

Module documentation

The closed augmentation filtration over ZMod p

Declarations

The closed augmentation filtration over `ZMod p`