NYLL
Module

Module.lean

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Module
12 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — coefficient rings — prime-power completed group algebra — module

The principal declarations in this module are:

  • primePowerCompletedCoeffToGroupAlgebra

The coefficient inverse limit maps canonically into the completed group algebra by taking the stagewise scalar units.

  • primePowerCompletedGroupAlgebraTransition_algebraMap

Finite-stage transitions send scalar coefficients through the reduced coefficient algebra map.

  • primePowerCompletedGroupAlgebraStageAugmentation_algebraMap

The finite-stage prime-power augmentation agrees with the scalar algebra map on coefficients.

  • primePowerCompletedGroupAlgebraProjection_coeffToGroupAlgebra

The prime-power completed group-algebra projection on coefficients is computed by the corresponding group-algebra coordinate map.

Imports1
Imported by2

Declarations

theorem

primePowerCompletedGroupAlgebraTransition_algebraMap

L48 ↗
FoxDifferential.primePowerCompletedGroupAlgebraTransition_algebraMap
Documentation

Finite-stage transitions send scalar coefficients through the reduced coefficient algebra map.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffStage
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffFamily
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraTransition_algebraMap
    {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j)
    (a : ZMod (ℓ ^ j.1)) :
    primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
        (algebraMap (ZMod (ℓ ^ j.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G j) a) =
      algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
        (modNCompletedCoeffMap
          (n := ℓ ^ i.1) (m := ℓ ^ j.1)
          (primePow_dvd_primePow (ℓ := ℓ) hij.1) a)
theorem

primePowerCompletedGroupAlgebraStageAugmentation_algebraMap

L66 ↗
FoxDifferential.primePowerCompletedGroupAlgebraStageAugmentation_algebraMap
Documentation

The finite-stage prime-power augmentation agrees with the scalar algebra map on coefficients.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffStage
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffFamily
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraStageAugmentation_algebraMap
    (i : PrimePowerCompletedGroupAlgebraIndex G) (a : ZMod (ℓ ^ i.1)) :
    modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
        (algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i) a) = a
def

primePowerCompletedCoeffToGroupAlgebra

L78 ↗
FoxDifferential.primePowerCompletedCoeffToGroupAlgebra
Documentation

The coefficient inverse limit maps canonically into the completed group algebra by taking the stagewise scalar units.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffStage
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffFamily
Lean source · full declaration
def primePowerCompletedCoeffToGroupAlgebra :
    PrimePowerCompletedCoeff ℓ G →+* PrimePowerCompletedGroupAlgebra ℓ G where
  toFun a := ⟨fun i =>
      algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
        (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a), by
    intro i j hij
    change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
        (algebraMap (ZMod (ℓ ^ j.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G j)
          (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) j a)) =
      algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
        (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a)
    rw [primePowerCompletedGroupAlgebraTransition_algebraMap]
    exact congrArg
      (algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i))
      (a.2 i j hij)⟩
  map_one' := by
    apply (primePowerCompletedGroupAlgebraSystem ℓ G).ext
    intro i
    change algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
        (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (1 : PrimePowerCompletedCoeff ℓ G))
      = 1
    rw [primePowerCompletedCoeffProjection_one]
    exact map_one (algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i))
  map_mul' := by
    intro a b
    apply (primePowerCompletedGroupAlgebraSystem ℓ G).ext
    intro i
    change algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
        (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (a * b)) =
      algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
        (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) *
      algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
        (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b)
    rw [primePowerCompletedCoeffProjection_mul]
    exact
      map_mul
        (algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i))
        (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a)
        (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b)
  map_zero' := by
    apply (primePowerCompletedGroupAlgebraSystem ℓ G).ext
    intro i
    change algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
        (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (0 : PrimePowerCompletedCoeff ℓ G))
      = 0
    rw [primePowerCompletedCoeffProjection_zero]
    exact map_zero (algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i))
  map_add' := by
    intro a b
    apply (primePowerCompletedGroupAlgebraSystem ℓ G).ext
    intro i
    change algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
        (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (a + b)) =
      algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
        (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) +
      algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
        (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b)
    rw [primePowerCompletedCoeffProjection_add]
    exact
      map_add
        (algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i))
        (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a)
        (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b)
theorem

primePowerCompletedGroupAlgebraProjection_coeffToGroupAlgebra

L148 ↗
FoxDifferential.primePowerCompletedGroupAlgebraProjection_coeffToGroupAlgebra
Documentation

The prime-power completed group-algebra projection on coefficients is computed by the corresponding group-algebra coordinate map.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffStage
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffFamily
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraProjection_coeffToGroupAlgebra
    (i : PrimePowerCompletedGroupAlgebraIndex G) (a : PrimePowerCompletedCoeff ℓ G) :
    primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
        (primePowerCompletedCoeffToGroupAlgebra (ℓ := ℓ) (G := G) a) =
      algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
        (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a)
theorem

primePowerCompletedGroupAlgebraTransition_smul

L162 ↗
FoxDifferential.primePowerCompletedGroupAlgebraTransition_smul
Documentation

Finite-stage transitions commute with scalar multiplication after reducing the scalar coefficient.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffStage
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffFamily
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraTransition_smul
    {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j)
    (a : ZMod (ℓ ^ j.1))
    (x : PrimePowerCompletedGroupAlgebraStage ℓ G j) :
    primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij (a • x) =
      (modNCompletedCoeffMap
          (n := ℓ ^ i.1) (m := ℓ ^ j.1)
          (primePow_dvd_primePow (ℓ := ℓ) hij.1) a) •
        primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij x
instance

instSMulPrimePowerCompletedCoeffPrimePowerCompletedGroupAlgebraFamily

L178 ↗
FoxDifferential.instSMulPrimePowerCompletedCoeffPrimePowerCompletedGroupAlgebraFamily
Documentation

The ambient family of prime-power group-algebra stages carries pointwise scalar multiplication, using the projection of a completed coefficient at each index.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffStage
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffFamily
Lean source · full declaration
instance instSMulPrimePowerCompletedCoeffPrimePowerCompletedGroupAlgebraFamily :
    SMul (PrimePowerCompletedCoeff ℓ G)
      ((i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedGroupAlgebraSystem ℓ G).X i) where
  smul a x := fun i =>
    (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
      (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i)
instance

instModulePrimePowerCompletedCoeffPrimePowerCompletedGroupAlgebraFamily

L190 ↗
FoxDifferential.instModulePrimePowerCompletedCoeffPrimePowerCompletedGroupAlgebraFamily
Documentation

The prime-power completed group-algebra family is a module over the prime-power completed coefficient ring.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffStage
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffFamily
Lean source · full declaration
instance instModulePrimePowerCompletedCoeffPrimePowerCompletedGroupAlgebraFamily :
    Module (PrimePowerCompletedCoeff ℓ G)
      ((i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedGroupAlgebraSystem ℓ G).X i) where
  one_smul x := by
    funext i
    change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
        (1 : PrimePowerCompletedCoeff ℓ G)) •
          (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i) =
        (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i)
    rw [primePowerCompletedCoeffProjection_one, one_smul]
  mul_smul a b x := by
    funext i
    change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (a * b)) •
        (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i) =
      (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
        ((primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b) •
          (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i))
    rw [primePowerCompletedCoeffProjection_mul, mul_smul]
  smul_zero a := by
    funext i
    change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
        (0 : PrimePowerCompletedGroupAlgebraStage ℓ G i) = 0
    rw [smul_zero]
  smul_add a x y := by
    funext i
    change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
        ((show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i) +
          (show PrimePowerCompletedGroupAlgebraStage ℓ G i from y i)) =
      (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
          (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i) +
        (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
          (show PrimePowerCompletedGroupAlgebraStage ℓ G i from y i)
    rw [smul_add]
  add_smul a b x := by
    funext i
    change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (a + b)) •
        (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i) =
      (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
          (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i) +
        (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b) •
          (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i)
    rw [primePowerCompletedCoeffProjection_add, add_smul]
  zero_smul x := by
    funext i
    change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
        (0 : PrimePowerCompletedCoeff ℓ G)) •
          (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i) = 0
    rw [primePowerCompletedCoeffProjection_zero, zero_smul]
instance

instSMulPrimePowerCompletedCoeffPrimePowerCompletedGroupAlgebra

L244 ↗
FoxDifferential.instSMulPrimePowerCompletedCoeffPrimePowerCompletedGroupAlgebra
Documentation

The completed group algebra carries coefficient-ring scalar multiplication by applying the scalar action at every finite quotient stage.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffStage
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffFamily
Lean source · full declaration
instance instSMulPrimePowerCompletedCoeffPrimePowerCompletedGroupAlgebra :
    SMul (PrimePowerCompletedCoeff ℓ G)
      (PrimePowerCompletedGroupAlgebra ℓ G) where
  smul a x := ⟨fun i =>
      (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
        (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i), by
    intro i j hij
    calc
      primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
          ((primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) j a) •
            (show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j)) =
      (modNCompletedCoeffMap
          (n := ℓ ^ i.1) (m := ℓ ^ j.1)
          (primePow_dvd_primePow (ℓ := ℓ) hij.1)
          (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) j a)) •
        primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
          (show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j) := by
            simpa using
              primePowerCompletedGroupAlgebraTransition_smul
                (ℓ := ℓ) (G := G) hij
                (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) j a)
                (show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j)
      _ =
      (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
        (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) := by
            exact congrArg₂ HSMul.hSMul (a.2 i j hij) (x.2 i j hij)⟩
theorem

coe_smul_primePowerCompletedGroupAlgebra

L274 ↗
FoxDifferential.coe_smul_primePowerCompletedGroupAlgebra
Documentation

The inclusion of the prime-power completed group algebra preserves scalar multiplication.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffStage
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffFamily
omit [Fact (0 < ℓ)] in
Lean source · full declaration
theorem coe_smul_primePowerCompletedGroupAlgebra
    (a : PrimePowerCompletedCoeff ℓ G)
    (x : PrimePowerCompletedGroupAlgebra ℓ G) :
    letI := instSMulPrimePowerCompletedCoeffPrimePowerCompletedGroupAlgebra
      (ℓ := ℓ) (G := G)
    ((a • x : PrimePowerCompletedGroupAlgebra ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedGroupAlgebraSystem ℓ G).X i) =
      a • (x :
        (i : PrimePowerCompletedGroupAlgebraIndex G) →
          (primePowerCompletedGroupAlgebraSystem ℓ G).X i) := by
  funext i
  change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
      (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) =
    (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
      (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i)
  rfl
theorem

primePowerCompletedGroupAlgebraProjection_smul

L295 ↗
FoxDifferential.primePowerCompletedGroupAlgebraProjection_smul
Documentation

The finite-stage projection is compatible with scalar multiplication.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffStage
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffFamily
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraProjection_smul
    (i : PrimePowerCompletedGroupAlgebraIndex G)
    (a : PrimePowerCompletedCoeff ℓ G)
    (x : PrimePowerCompletedGroupAlgebra ℓ G) :
    primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i (a • x) =
      (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
        primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x
instance

instModulePrimePowerCompletedCoeffPrimePowerCompletedGroupAlgebra

L308 ↗
FoxDifferential.instModulePrimePowerCompletedCoeffPrimePowerCompletedGroupAlgebra
Documentation

The prime-power completed group algebra is a module over the prime-power completed coefficient ring.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffStage
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffFamily
Lean source · statement
instance instModulePrimePowerCompletedCoeffPrimePowerCompletedGroupAlgebra :
    Module (PrimePowerCompletedCoeff ℓ G)
      (PrimePowerCompletedGroupAlgebra ℓ G)
theorem

primePowerCompletedGroupAlgebraAugmentation_coeffToGroupAlgebra

L323 ↗
FoxDifferential.primePowerCompletedGroupAlgebraAugmentation_coeffToGroupAlgebra
Documentation

The prime-power completed augmentation is left inverse to the coefficient-to-group-algebra map.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffStage
attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffFamily
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraAugmentation_coeffToGroupAlgebra
    (i : PrimePowerCompletedGroupAlgebraIndex G) (a : PrimePowerCompletedCoeff ℓ G) :
    modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
        (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
          (primePowerCompletedCoeffToGroupAlgebra (ℓ := ℓ) (G := G) a)) =
      primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.