Module

ProCIntegerPrimePower.lean

Nyll.ProCGroups.Completion.ProCIntegerPrimePower

10 declarations indexed from sourceView source ↗

Module documentation

Pro C Groups / Completion / Prime-Power pro-C Integer

This module specializes the pro-C integer construction to prime-power moduli and proves the pro-p density, generation, and procyclicity results.

Imports1

Nyll.ProCGroups.Completion.ProCInteger

Imported by4

def

pGroupPower

L25 ↗

ProCGroups.Completion.ProCIntegerIndex.pGroupPower

Documentation

The \(p^k\)-modulus coefficient index for the pro-\(p\) integer limit.

Source context 4 commands

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

namespace ProCGroups.Completion
noncomputable section
universe u
namespace ProCIntegerIndex

Lean source · full declaration

def pGroupPower (p k : ℕ) [Fact (Nat.Prime p)] :
    ProCIntegerIndex (FiniteGroupClass.pGroup p : FiniteGroupClass.{u}) where
  modulus := p ^ k
  positive := by
    exact Nat.pow_pos (show 0 < p from (Fact.out : Nat.Prime p).pos)
  cyclic_mem := by
    refine (FiniteGroupClass.memAcrossUniverses_ulift_iff
      (FiniteGroupClass.pGroup p : FiniteGroupClass.{u})
      (Multiplicative (ZMod (p ^ k)))).1 ?_
    apply FiniteGroupClass.memAcrossUniverses_of_mem
    let : NeZero (p ^ k) := ⟨Nat.ne_of_gt (Nat.pow_pos
      (show 0 < p from (Fact.out : Nat.Prime p).pos))⟩
    constructor
    · exact Finite.of_equiv (ZMod (p ^ k))
        (Multiplicative.ofAdd.trans Equiv.ulift.symm)
    · intro g
      refine ⟨k, ?_⟩
      cases g with
      | up g' =>
        apply ULift.ext
        change g' ^ p ^ k = 1
        cases g' with
        | ofAdd z =>
          change Multiplicative.ofAdd ((p ^ k) • z) = Multiplicative.ofAdd 0
          simp only [nsmul_eq_mul, CharP.cast_eq_zero, zero_mul, ofAdd_zero]

theorem

modulus_pGroupPower

L53 ↗

ProCGroups.Completion.ProCIntegerIndex.modulus_pGroupPower

Documentation

The prime-power coefficient index has modulus \(p ^ n\).

Source context 4 commands

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

namespace ProCGroups.Completion
noncomputable section
universe u
namespace ProCIntegerIndex

Lean source · statement

theorem modulus_pGroupPower (p k : ℕ) [Fact (Nat.Prime p)] :
    (pGroupPower p k :
      ProCIntegerIndex (FiniteGroupClass.pGroup p : FiniteGroupClass.{u})).modulus = p ^ k

theorem

modulus_dvd_pow_of_mem_pGroup

L59 ↗

ProCGroups.Completion.ProCIntegerIndex.modulus_dvd_pow_of_mem_pGroup

Documentation

Any coefficient index for the finite \(p\)-group class is dominated by a prime-power modulus.

Source context 4 commands

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

namespace ProCGroups.Completion
noncomputable section
universe u
namespace ProCIntegerIndex

Lean source · statement

theorem modulus_dvd_pow_of_mem_pGroup (p : ℕ) [Fact (Nat.Prime p)]
    (i : ProCIntegerIndex (FiniteGroupClass.pGroup p : FiniteGroupClass.{u})) :
    ∃ k, i.modulus ∣ p ^ k

theorem

directed_pGroup

L75 ↗

ProCGroups.Completion.ProCIntegerIndex.directed_pGroup

Documentation

The finite \(p\)-group coefficient indices for pro-\(C\) integers are directed.

Source context 4 commands

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

namespace ProCGroups.Completion
noncomputable section
universe u
namespace ProCIntegerIndex

Lean source · statement

theorem directed_pGroup (p : ℕ) [Fact (Nat.Prime p)] :
    Directed (· ≤ ·)
      (id : ProCIntegerIndex (FiniteGroupClass.pGroup p : FiniteGroupClass.{u}) →
        ProCIntegerIndex (FiniteGroupClass.pGroup p : FiniteGroupClass.{u}))

theorem

proCIntegerProj_pGroupPower_one

L90 ↗

ProCGroups.Completion.proCIntegerProj_pGroupPower_one

Documentation

The distinguished element \(1\) projects to \(1\) on every prime-power coordinate.

Source context 3 commands

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

namespace ProCGroups.Completion
noncomputable section
universe u

Lean source · statement

theorem proCIntegerProj_pGroupPower_one (p k : ℕ) [Fact (Nat.Prime p)] :
    proCIntegerProj
        (C := (FiniteGroupClass.pGroup p : FiniteGroupClass.{u}))
        (ProCIntegerIndex.pGroupPower p k)
        (proCIntegerOne
          (C := (FiniteGroupClass.pGroup p : FiniteGroupClass.{u}))).toAdd =
      (1 : ZMod (p ^ k))

theorem

denseRange_intToProCInteger_pGroup

L100 ↗

ProCGroups.Completion.denseRange_intToProCInteger_pGroup

Documentation

The ordinary integers are dense in the pro-\(p\) integer coefficient ring.

Source context 3 commands

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

namespace ProCGroups.Completion
noncomputable section
universe u

Lean source · statement

theorem denseRange_intToProCInteger_pGroup (p : ℕ) [Fact (Nat.Prime p)] :
    DenseRange (intToProCInteger
      (C := (FiniteGroupClass.pGroup p : FiniteGroupClass.{u})))

theorem

denseRange_multiplicativeIntToProCInteger_pGroup

L127 ↗

ProCGroups.Completion.denseRange_multiplicativeIntToProCInteger_pGroup

Documentation

The multiplicative infinite-cyclic map is dense in the pro-\(p\) integers.

Source context 3 commands

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

namespace ProCGroups.Completion
noncomputable section
universe u

Lean source · statement

theorem denseRange_multiplicativeIntToProCInteger_pGroup (p : ℕ) [Fact (Nat.Prime p)] :
    DenseRange
      (multiplicativeIntToProCInteger
        (C := (FiniteGroupClass.pGroup p : FiniteGroupClass.{u})))

theorem

topologicallyGenerates_singleton_proCIntegerOne_pGroup

L158 ↗

ProCGroups.Completion.topologicallyGenerates_singleton_proCIntegerOne_pGroup

Documentation

The distinguished element 1 topologically generates the pro-\(p\) integers.

Source context 3 commands

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

namespace ProCGroups.Completion
noncomputable section
universe u

Lean source · statement

theorem topologicallyGenerates_singleton_proCIntegerOne_pGroup
    (p : ℕ) [Fact (Nat.Prime p)] :
    ProCGroups.Generation.TopologicallyGenerates
      (G := Multiplicative
        (ProCIntegerLimitCarrier (FiniteGroupClass.pGroup p : FiniteGroupClass.{0})))
      ({(proCIntegerOne
        (C := (FiniteGroupClass.pGroup p : FiniteGroupClass.{0})))} : Set _)

theorem

hasPGroupOpenNormalBasis_multiplicative_proCInteger_pGroup

L172 ↗

ProCGroups.Completion.hasPGroupOpenNormalBasis_multiplicative_proCInteger_pGroup

Documentation

The pro-\(p\) integers have an open-normal basis of finite \(p\)-group quotients.

Source context 3 commands

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

namespace ProCGroups.Completion
noncomputable section
universe u

Lean source · statement

theorem hasPGroupOpenNormalBasis_multiplicative_proCInteger_pGroup (p : ℕ) [Fact (Nat.Prime p)] :
    ProCGroups.ProC.HasPGroupOpenNormalBasis p
      (Multiplicative
        (ProCIntegerLimitCarrier (FiniteGroupClass.pGroup p : FiniteGroupClass.{0})))

theorem

hasCyclicOpenNormalBasis_multiplicative_proCInteger_pGroup

L186 ↗

ProCGroups.Completion.hasCyclicOpenNormalBasis_multiplicative_proCInteger_pGroup

Documentation

The pro-\(p\) integers have a cyclic open-normal quotient basis.

Source context 3 commands

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

namespace ProCGroups.Completion
noncomputable section
universe u

Lean source · statement

theorem hasCyclicOpenNormalBasis_multiplicative_proCInteger_pGroup (p : ℕ) [Fact (Nat.Prime p)] :
    ProCGroups.ProC.HasCyclicOpenNormalBasis
      (Multiplicative
        (ProCIntegerLimitCarrier (FiniteGroupClass.pGroup p : FiniteGroupClass.{0})))

Module documentation

Pro C Groups / Completion / Prime-Power pro-C Integer

Declarations