ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.Core

43 Theorems | 13 Definitions | 6 Abbreviations | 13 Instances

The principal declarations in this module are:

ZCCoeff The pro-\(C\) integer coefficient ring. - ZCCompletedGroupAlgebraIndex The two-parameter finite-stage index for \(\mathbb{Z}_C\llbracket H\rrbracket\): a coefficient quotient of \(\mathbb{Z}_C\) and a finite \(C\)-quotient of \(H\). - zcCompletedGroupAlgebraTransition_of Evaluation of a pro-\(C\) transition on a group-like basis element. - zcCompletedGroupAlgebraTransition_single The transition map \(R[G/V] \to R[G/U]\) sends a singleton supported at a class of \(G/V\) to the singleton supported at its image in \(G/U\), with the same coefficient.

imports

Imported by

abbrev ZCCoeff (C : ProCGroups.FiniteGroupClass.{u}) : Type _ :=
  ProCIntegerLimitCarrier C

The pro-\(C\) integer coefficient ring.

Abbreviation FoxDifferential.ZCCompletedGroupAlgebraIndex

abbrev ZCCompletedGroupAlgebraIndex
    (C : ProCGroups.FiniteGroupClass.{u})
    (H : Type u) [Group H] [TopologicalSpace H] : Type u :=
  ProCIntegerIndex C × CompletedGroupAlgebraIndexInClass H C

The two-parameter finite-stage index for \(\mathbb{Z}_C\llbracket H\rrbracket\): a coefficient quotient of \(\mathbb{Z}_C\) and a finite \(C\)-quotient of \(H\).

Abbreviation FoxDifferential.ZCCompletedGroupAlgebraStage

abbrev ZCCompletedGroupAlgebraStage
    (C : ProCGroups.FiniteGroupClass.{u})
    (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (i : ZCCompletedGroupAlgebraIndex C H) : Type u :=
  ModNCompletedGroupAlgebraStageInClass i.1.modulus H C i.2

A finite stage \((\mathbb{Z}/n\mathbb{Z})[H/U]\) of the pro-\(C\) completed group algebra.

Definition FoxDifferential.zcCompletedGroupAlgebraTransition

def zcCompletedGroupAlgebraTransition
    (C : ProCGroups.FiniteGroupClass.{u})
    (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    {i j : ZCCompletedGroupAlgebraIndex C H} (hij : i ≤ j) :
    ZCCompletedGroupAlgebraStage C H j →+* ZCCompletedGroupAlgebraStage C H i := by
  letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
  letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
  exact
    (modNCompletedGroupAlgebraStageCoeffMapInClass
        (n := i.1.modulus) (m := j.1.modulus) (G := H) C i.2 hij.1).comp
      (modNCompletedGroupAlgebraTransitionInClass (n := j.1.modulus) (G := H) C hij.2)

Transition maps for the true pro-\(C\) completed group algebra. The coefficient direction is divisibility of allowed pro-\(C\) integer moduli, and the group direction is refinement of \(C\)-quotients.

Theorem FoxDifferential.zcCompletedGroupAlgebraTransition_of

@[simp]
theorem zcCompletedGroupAlgebraTransition_of
    (C : ProCGroups.FiniteGroupClass.{u})
    (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    {i j : ZCCompletedGroupAlgebraIndex C H} (hij : i ≤ j)
    (q : CompletedGroupAlgebraQuotientInClass H C j.2) :
    zcCompletedGroupAlgebraTransition C H hij
        (MonoidAlgebra.of (ModNCompletedCoeff j.1.modulus) _ q) =
      MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus) _
        ((OpenNormalSubgroupInClass.map
          (C := C) (G := H)
          (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q)

Evaluation of a pro-\(C\) transition on a group-like basis element.

Show Lean proof

Theorem FoxDifferential.zcCompletedGroupAlgebraTransition_single

@[simp]
theorem zcCompletedGroupAlgebraTransition_single
    (C : ProCGroups.FiniteGroupClass.{u})
    (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    {i j : ZCCompletedGroupAlgebraIndex C H} (hij : i ≤ j)
    (q : CompletedGroupAlgebraQuotientInClass H C j.2)
    (a : ModNCompletedCoeff j.1.modulus) :
    zcCompletedGroupAlgebraTransition C H hij (MonoidAlgebra.single q a) =
      MonoidAlgebra.single
        ((OpenNormalSubgroupInClass.map
          (C := C) (G := H)
          (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q)
        (modNCompletedCoeffMap (n := i.1.modulus) (m := j.1.modulus) hij.1 a)

The transition map \(R[G/V] \to R[G/U]\) sends a singleton supported at a class of \(G/V\) to the singleton supported at its image in \(G/U\), with the same coefficient.

Show Lean proof

Theorem FoxDifferential.zcCompletedGroupAlgebraTransition_id

@[simp]
theorem zcCompletedGroupAlgebraTransition_id
    (C : ProCGroups.FiniteGroupClass.{u})
    (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (i : ZCCompletedGroupAlgebraIndex C H) :
    zcCompletedGroupAlgebraTransition C H (le_rfl : i ≤ i) = RingHom.id _

The \(\mathbb{Z}_C\)-completed group-algebra transition for a reflexive refinement is the identity ring homomorphism.

Show Lean proof

Theorem FoxDifferential.zcCompletedGroupAlgebraTransition_comp

@[simp 900]
theorem zcCompletedGroupAlgebraTransition_comp
    (C : ProCGroups.FiniteGroupClass.{u})
    (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    {i j k : ZCCompletedGroupAlgebraIndex C H}
    (hij : i ≤ j) (hjk : j ≤ k) :
    (zcCompletedGroupAlgebraTransition C H hij).comp
        (zcCompletedGroupAlgebraTransition C H hjk) =
      zcCompletedGroupAlgebraTransition C H (hij.trans hjk)

\(\mathbb{Z}_C\)-completed group-algebra transitions compose along quotient refinements.

Show Lean proof

Definition FoxDifferential.zcCompletedGroupAlgebraSystem

def zcCompletedGroupAlgebraSystem
    (C : ProCGroups.FiniteGroupClass.{u})
    (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    InverseSystem (I := ZCCompletedGroupAlgebraIndex C H) where
  X := ZCCompletedGroupAlgebraStage C H
  topologicalSpace := fun _ => ⊥
  map := fun {i j} hij => zcCompletedGroupAlgebraTransition C H hij
  continuous_map := by
    intro i j hij
    letI : TopologicalSpace (ZCCompletedGroupAlgebraStage C H i) := ⊥
    letI : TopologicalSpace (ZCCompletedGroupAlgebraStage C H j) := ⊥
    letI : DiscreteTopology (ZCCompletedGroupAlgebraStage C H j) := ⟨rfl⟩
    exact continuous_of_discreteTopology
  map_id := by
    intro i
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (zcCompletedGroupAlgebraTransition_id C H i)) x
  map_comp := by
    intro i j k hij hjk
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (zcCompletedGroupAlgebraTransition_comp C H hij hjk)) x

The inverse system defining the pro-\(C\) completed group algebra.

Definition FoxDifferential.ZCCompletedGroupAlgebraCompatible

def ZCCompletedGroupAlgebraCompatible
    (C : ProCGroups.FiniteGroupClass.{u})
    (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (x : ∀ i : ZCCompletedGroupAlgebraIndex C H, ZCCompletedGroupAlgebraStage C H i) : Prop :=
  ∀ i j, ∀ hij : i ≤ j, zcCompletedGroupAlgebraTransition C H hij (x j) = x i

Compatibility for a family of finite \(\mathbb{Z}_C\llbracket H\rrbracket\) stage elements.

Abbreviation FoxDifferential.ZCCompletedGroupAlgebra

abbrev ZCCompletedGroupAlgebra
    (C : ProCGroups.FiniteGroupClass.{u})
    (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] : Type u :=
  {x : ∀ i : ZCCompletedGroupAlgebraIndex C H, ZCCompletedGroupAlgebraStage C H i //
    ZCCompletedGroupAlgebraCompatible C H x}

The completed group algebra \(\mathbb{Z}_C\llbracket H\rrbracket\).

Abbreviation FoxDifferential.zcCompletedGroupAlgebraProjection

abbrev zcCompletedGroupAlgebraProjection
    (C : ProCGroups.FiniteGroupClass.{u})
    (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (i : ZCCompletedGroupAlgebraIndex C H) :
    ZCCompletedGroupAlgebra C H → ZCCompletedGroupAlgebraStage C H i :=
  fun x => x.1 i

The projection from \(\mathbb{Z}_C\llbracket H\rrbracket\) to a finite \(C\)-coefficient and \(C\)-quotient stage.

Instance FoxDifferential.instZeroZCCompletedGroupAlgebra

instance instZeroZCCompletedGroupAlgebra : Zero (ZCCompletedGroupAlgebra C H) where
  zero := ⟨fun i => 0, by intro i j hij; exact map_zero _⟩

The zero element is defined coordinatewise as the compatible family of zero elements at all finite stages.

Instance FoxDifferential.instAddZCCompletedGroupAlgebra

instance instAddZCCompletedGroupAlgebra : Add (ZCCompletedGroupAlgebra C H) where
  add x y := ⟨fun i => x.1 i + y.1 i, by
    intro i j hij
    rw [map_add]
    exact congrArg₂ HAdd.hAdd (x.2 i j hij) (y.2 i j hij)⟩

Addition on \(\mathbb{Z}_C\llbracket H\rrbracket\) is defined coordinatewise through finite-stage group-algebra additions.

Instance FoxDifferential.instNegZCCompletedGroupAlgebra

instance instNegZCCompletedGroupAlgebra : Neg (ZCCompletedGroupAlgebra C H) where
  neg x := ⟨fun i => -x.1 i, by
    intro i j hij
    rw [map_neg]
    exact congrArg Neg.neg (x.2 i j hij)⟩

Negation on the \(\mathbb{Z}_C\)-completed group algebra is defined coordinatewise through finite-stage group-algebra negations.

Instance FoxDifferential.instSubZCCompletedGroupAlgebra

instance instSubZCCompletedGroupAlgebra : Sub (ZCCompletedGroupAlgebra C H) where
  sub x y := ⟨fun i => x.1 i - y.1 i, by
    intro i j hij
    rw [map_sub]
    exact congrArg₂ HSub.hSub (x.2 i j hij) (y.2 i j hij)⟩

Subtraction on the completed group algebra is defined coordinatewise through the finite-stage group-algebra subtractions.

Instance FoxDifferential.instSMulNatZCCompletedGroupAlgebra

instance instSMulNatZCCompletedGroupAlgebra : SMul ℕ (ZCCompletedGroupAlgebra C H) where
  smul n x := ⟨fun i => n • x.1 i, by
    intro i j hij
    rw [map_nsmul]
    exact congrArg (n • ·) (x.2 i j hij)⟩

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

Instance FoxDifferential.instSMulIntZCCompletedGroupAlgebra

instance instSMulIntZCCompletedGroupAlgebra : SMul ℤ (ZCCompletedGroupAlgebra C H) where
  smul n x := ⟨fun i => n • x.1 i, by
    intro i j hij
    rw [map_zsmul]
    exact congrArg (n • ·) (x.2 i j hij)⟩

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

Theorem FoxDifferential.coe_zero_zcCompletedGroupAlgebra

@[simp]
theorem coe_zero_zcCompletedGroupAlgebra :
    ((0 : ZCCompletedGroupAlgebra C H) :
      (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = 0

The zero element of \(\mathbb{Z}_C\llbracket H\rrbracket\) is represented by the compatible family of finite-stage zero elements.

Show Lean proof

Theorem FoxDifferential.coe_add_zcCompletedGroupAlgebra

@[simp]
theorem coe_add_zcCompletedGroupAlgebra (x y : ZCCompletedGroupAlgebra C H) :
    ((x + y : ZCCompletedGroupAlgebra C H) :
      (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = x + y

The underlying finite-stage family of a sum in \(\mathbb{Z}_C\llbracket H\rrbracket\) is the sum of the underlying finite-stage families.

Show Lean proof

Theorem FoxDifferential.coe_neg_zcCompletedGroupAlgebra

@[simp]
theorem coe_neg_zcCompletedGroupAlgebra (x : ZCCompletedGroupAlgebra C H) :
    ((-x : ZCCompletedGroupAlgebra C H) :
      (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = -x

The underlying finite-stage family of a negation in \(\mathbb{Z}_C\llbracket H\rrbracket\) is the negation of the underlying finite-stage family.

Show Lean proof

Theorem FoxDifferential.coe_sub_zcCompletedGroupAlgebra

@[simp]
theorem coe_sub_zcCompletedGroupAlgebra (x y : ZCCompletedGroupAlgebra C H) :
    ((x - y : ZCCompletedGroupAlgebra C H) :
      (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = x - y

The underlying finite-stage family of a difference in \(\mathbb{Z}_C\llbracket H\rrbracket\) is the difference of the underlying finite-stage families.

Show Lean proof

Theorem FoxDifferential.coe_nsmul_zcCompletedGroupAlgebra

@[simp]
theorem coe_nsmul_zcCompletedGroupAlgebra (n : ℕ) (x : ZCCompletedGroupAlgebra C H) :
    ((n • x : ZCCompletedGroupAlgebra C H) :
      (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = n • x

Natural-number scalar multiplication in \(\mathbb{Z}_C\llbracket H\rrbracket\) is computed coordinatewise at every finite stage.

Show Lean proof

Theorem FoxDifferential.coe_zsmul_zcCompletedGroupAlgebra

@[simp]
theorem coe_zsmul_zcCompletedGroupAlgebra (n : ℤ) (x : ZCCompletedGroupAlgebra C H) :
    ((n • x : ZCCompletedGroupAlgebra C H) :
      (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = n • x

Integer scalar multiplication in \(\mathbb{Z}_C\llbracket H\rrbracket\) is computed coordinatewise at every finite stage.

Show Lean proof

Instance FoxDifferential.instOneZCCompletedGroupAlgebra

instance instOneZCCompletedGroupAlgebra : One (ZCCompletedGroupAlgebra C H) where
  one := ⟨fun i => 1, by intro i j hij; exact map_one _⟩

The unit of \(\mathbb{Z}_C\llbracket H\rrbracket\) is the compatible family of finite-stage units.

Instance FoxDifferential.instMulZCCompletedGroupAlgebra

instance instMulZCCompletedGroupAlgebra : Mul (ZCCompletedGroupAlgebra C H) where
  mul x y := ⟨fun i => x.1 i * y.1 i, by
    intro i j hij
    rw [map_mul]
    exact congrArg₂ HMul.hMul (x.2 i j hij) (y.2 i j hij)⟩

Multiplication on the completed group algebra is defined coordinatewise through the finite-stage group-algebra products.

Instance FoxDifferential.instNatCastZCCompletedGroupAlgebra

instance instNatCastZCCompletedGroupAlgebra : NatCast (ZCCompletedGroupAlgebra C H) where
  natCast n := ⟨fun i => n, by intro i j hij; exact map_natCast _ _⟩

Natural number casts in \(\mathbb{Z}_C\llbracket H\rrbracket\) are computed coordinatewise from finite-stage natural number casts.

Instance FoxDifferential.instIntCastZCCompletedGroupAlgebra

instance instIntCastZCCompletedGroupAlgebra : IntCast (ZCCompletedGroupAlgebra C H) where
  intCast n := ⟨fun i => n, by intro i j hij; exact map_intCast _ _⟩

Integer casts in \(\mathbb{Z}_C\llbracket H\rrbracket\) are computed coordinatewise from finite-stage integer casts.

Instance FoxDifferential.instPowZCCompletedGroupAlgebra

instance instPowZCCompletedGroupAlgebra : Pow (ZCCompletedGroupAlgebra C H) ℕ where
  pow x n := ⟨fun i => x.1 i ^ n, by
    intro i j hij
    rw [map_pow]
    exact congrArg (fun z => z ^ n) (x.2 i j hij)⟩

The completed group algebra has powers computed at every finite-stage coordinate.

Theorem FoxDifferential.coe_one_zcCompletedGroupAlgebra

@[simp]
theorem coe_one_zcCompletedGroupAlgebra :
    ((1 : ZCCompletedGroupAlgebra C H) :
      (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = 1

The unit of \(\mathbb{Z}_C\llbracket H\rrbracket\) is represented by the compatible family of finite-stage units.

Show Lean proof

Theorem FoxDifferential.coe_mul_zcCompletedGroupAlgebra

@[simp]
theorem coe_mul_zcCompletedGroupAlgebra (x y : ZCCompletedGroupAlgebra C H) :
    ((x * y : ZCCompletedGroupAlgebra C H) :
      (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = x * y

The underlying finite-stage family of a product in \(\mathbb{Z}_C\llbracket H\rrbracket\) is the product of the underlying finite-stage families.

Show Lean proof

Theorem FoxDifferential.coe_natCast_zcCompletedGroupAlgebra

@[simp]
theorem coe_natCast_zcCompletedGroupAlgebra (n : ℕ) :
    ((n : ZCCompletedGroupAlgebra C H) :
      (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = n

Natural number casts in the completed group algebra are computed coefficientwise after projection to every completed finite quotient stage.

Show Lean proof

Theorem FoxDifferential.coe_intCast_zcCompletedGroupAlgebra

@[simp]
theorem coe_intCast_zcCompletedGroupAlgebra (n : ℤ) :
    ((n : ZCCompletedGroupAlgebra C H) :
      (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = n

Integer casts in the completed group algebra are computed coefficientwise after projection to every completed finite quotient stage.

Show Lean proof

Theorem FoxDifferential.coe_pow_zcCompletedGroupAlgebra

@[simp]
theorem coe_pow_zcCompletedGroupAlgebra (x : ZCCompletedGroupAlgebra C H) (n : ℕ) :
    ((x ^ n : ZCCompletedGroupAlgebra C H) :
      (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = x ^ n

Powers in \(\mathbb{Z}_C\llbracket H\rrbracket\) are computed coordinatewise at every finite stage.

Show Lean proof

Instance FoxDifferential.instRingZCCompletedGroupAlgebra

instance instRingZCCompletedGroupAlgebra : Ring (ZCCompletedGroupAlgebra C H) :=
  Function.Injective.ring
    (fun x : ZCCompletedGroupAlgebra C H =>
      (x : (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i))
    Subtype.val_injective
    (coe_zero_zcCompletedGroupAlgebra (C := C) (H := H))
    (coe_one_zcCompletedGroupAlgebra (C := C) (H := H))
    (coe_add_zcCompletedGroupAlgebra (C := C) (H := H))
    (coe_mul_zcCompletedGroupAlgebra (C := C) (H := H))
    (coe_neg_zcCompletedGroupAlgebra (C := C) (H := H))
    (coe_sub_zcCompletedGroupAlgebra (C := C) (H := H))
    (fun n x => coe_nsmul_zcCompletedGroupAlgebra (C := C) (H := H) n x)
    (fun n x => coe_zsmul_zcCompletedGroupAlgebra (C := C) (H := H) n x)
    (fun x n => coe_pow_zcCompletedGroupAlgebra (C := C) (H := H) x n)
    (by intro n; exact coe_natCast_zcCompletedGroupAlgebra (C := C) (H := H) n)
    (by intro z; exact coe_intCast_zcCompletedGroupAlgebra (C := C) (H := H) z)

The completed group algebra is a ring because all ring operations and ring axioms are inherited coordinatewise from the finite-stage group algebras.

Theorem FoxDifferential.zcCompletedGroupAlgebraProjection_one

@[simp]
theorem zcCompletedGroupAlgebraProjection_one
    (i : ZCCompletedGroupAlgebraIndex C H) :
    zcCompletedGroupAlgebraProjection C H i (1 : ZCCompletedGroupAlgebra C H) = 1

The finite-stage projection sends \(1\) to \(1\).

Show Lean proof

Theorem FoxDifferential.zcCompletedGroupAlgebraProjection_mul

@[simp]
theorem zcCompletedGroupAlgebraProjection_mul
    (i : ZCCompletedGroupAlgebraIndex C H) (x y : ZCCompletedGroupAlgebra C H) :
    zcCompletedGroupAlgebraProjection C H i (x * y) =
      zcCompletedGroupAlgebraProjection C H i x *
        zcCompletedGroupAlgebraProjection C H i y

The finite-stage projection preserves multiplication.

Show Lean proof

Theorem FoxDifferential.zcCompletedGroupAlgebraProjection_zero

@[simp]
theorem zcCompletedGroupAlgebraProjection_zero
    (i : ZCCompletedGroupAlgebraIndex C H) :
    zcCompletedGroupAlgebraProjection C H i (0 : ZCCompletedGroupAlgebra C H) = 0

The finite-stage projection sends \(0\) to \(0\).

Show Lean proof

Theorem FoxDifferential.zcCompletedGroupAlgebraProjection_add

@[simp]
theorem zcCompletedGroupAlgebraProjection_add
    (i : ZCCompletedGroupAlgebraIndex C H) (x y : ZCCompletedGroupAlgebra C H) :
    zcCompletedGroupAlgebraProjection C H i (x + y) =
      zcCompletedGroupAlgebraProjection C H i x +
        zcCompletedGroupAlgebraProjection C H i y

The finite-stage projection preserves addition.

Show Lean proof

Theorem FoxDifferential.zcCompletedGroupAlgebraProjection_neg

@[simp]
theorem zcCompletedGroupAlgebraProjection_neg
    (i : ZCCompletedGroupAlgebraIndex C H) (x : ZCCompletedGroupAlgebra C H) :
    zcCompletedGroupAlgebraProjection C H i (-x) =
      -zcCompletedGroupAlgebraProjection C H i x

The finite-stage projection preserves negation.

Show Lean proof

Theorem FoxDifferential.zcCompletedGroupAlgebraProjection_sub

@[simp]
theorem zcCompletedGroupAlgebraProjection_sub
    (i : ZCCompletedGroupAlgebraIndex C H) (x y : ZCCompletedGroupAlgebra C H) :
    zcCompletedGroupAlgebraProjection C H i (x - y) =
      zcCompletedGroupAlgebraProjection C H i x -
        zcCompletedGroupAlgebraProjection C H i y

The finite-stage projection preserves subtraction.

Show Lean proof

Definition FoxDifferential.zcCompletedGroupAlgebraProjectionRingHom

def zcCompletedGroupAlgebraProjectionRingHom
    (i : ZCCompletedGroupAlgebraIndex C H) :
    ZCCompletedGroupAlgebra C H →+* ZCCompletedGroupAlgebraStage C H i where
  toFun := zcCompletedGroupAlgebraProjection C H i
  map_zero' := zcCompletedGroupAlgebraProjection_zero C H i
  map_one' := zcCompletedGroupAlgebraProjection_one C H i
  map_add' := zcCompletedGroupAlgebraProjection_add C H i
  map_mul' := zcCompletedGroupAlgebraProjection_mul C H i

The projection from \(\mathbb{Z}_C\llbracket H\rrbracket\) to a finite stage is bundled as a ring homomorphism.

Theorem FoxDifferential.zcCompletedGroupAlgebraProjectionRingHom_apply

@[simp]
theorem zcCompletedGroupAlgebraProjectionRingHom_apply
    (i : ZCCompletedGroupAlgebraIndex C H) (x : ZCCompletedGroupAlgebra C H) :
    zcCompletedGroupAlgebraProjectionRingHom C H i x =
      zcCompletedGroupAlgebraProjection C H i x

The ring-homomorphism projection has the same underlying coordinate map as the finite-stage projection.

Show Lean proof

Instance FoxDifferential.instModuleZCCompletedGroupAlgebraStage

instance instModuleZCCompletedGroupAlgebraStage
    (i : ZCCompletedGroupAlgebraIndex C H) :
    Module (ZCCompletedGroupAlgebra C H) (ZCCompletedGroupAlgebraStage C H i) :=
  Module.compHom _ (zcCompletedGroupAlgebraProjectionRingHom C H i)

The \(\mathbb{Z}_C\)-completed group algebra stage is a module over its coefficient ring.

Theorem FoxDifferential.zcCompletedGroupAlgebraProjection_ext

theorem zcCompletedGroupAlgebraProjection_ext
    {x y : ZCCompletedGroupAlgebra C H}
    (h : ∀ i : ZCCompletedGroupAlgebraIndex C H,
      zcCompletedGroupAlgebraProjection C H i x =
        zcCompletedGroupAlgebraProjection C H i y) :
    x = y

Finite-stage projections separate points of \(\mathbb{Z}_C\llbracket H\rrbracket\).

Show Lean proof

Theorem FoxDifferential.zcCompletedGroupAlgebraTransition_projection

@[simp]
theorem zcCompletedGroupAlgebraTransition_projection
    {i j : ZCCompletedGroupAlgebraIndex C H} (hij : i ≤ j)
    (x : ZCCompletedGroupAlgebra C H) :
    zcCompletedGroupAlgebraTransition C H hij
        (zcCompletedGroupAlgebraProjection C H j x) =
      zcCompletedGroupAlgebraProjection C H i x

Finite projections from \(\mathbb{Z}_C\llbracket H\rrbracket\) commute with the finite transition maps.

Show Lean proof

Definition FoxDifferential.zcCompletedGroupAlgebraProjectionLinearMap

def zcCompletedGroupAlgebraProjectionLinearMap
    (i : ZCCompletedGroupAlgebraIndex C H) :
    ZCCompletedGroupAlgebra C H →ₗ[ZCCompletedGroupAlgebra C H]
      ZCCompletedGroupAlgebraStage C H i where
  toFun := zcCompletedGroupAlgebraProjection C H i
  map_add' x y := zcCompletedGroupAlgebraProjection_add C H i x y
  map_smul' r x := by
    change zcCompletedGroupAlgebraProjection C H i (r * x) =
      zcCompletedGroupAlgebraProjection C H i r *
        zcCompletedGroupAlgebraProjection C H i x
    exact zcCompletedGroupAlgebraProjection_mul C H i r x

A finite stage projection as a linear map over the completed group algebra.

Theorem FoxDifferential.zcCompletedGroupAlgebraProjectionLinearMap_apply

@[simp]
theorem zcCompletedGroupAlgebraProjectionLinearMap_apply
    (i : ZCCompletedGroupAlgebraIndex C H) (x : ZCCompletedGroupAlgebra C H) :
    zcCompletedGroupAlgebraProjectionLinearMap C H i x =
      zcCompletedGroupAlgebraProjection C H i x

The \(\mathbb{Z}_C\)-completed group-algebra projection, bundled as a linear map, acts by its defining finite-stage coordinate formula.

Show Lean proof

Theorem FoxDifferential.zcCompletedGroupAlgebraProjection_sum

theorem zcCompletedGroupAlgebraProjection_sum
    (C : ProCGroups.FiniteGroupClass.{u})
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    {I : Type v} [Fintype I]
    (j : ZCCompletedGroupAlgebraIndex C H)
    (f : I → ZCCompletedGroupAlgebra C H) :
    zcCompletedGroupAlgebraProjection C H j (∑ i : I, f i) =
      ∑ i : I, zcCompletedGroupAlgebraProjection C H j (f i)

The projection from \(\mathbb{Z}_C\llbracket H\rrbracket\) to a finite stage commutes with finite sums.

Show Lean proof

Definition FoxDifferential.zcCompletedGroupAlgebraCoeff

def zcCompletedGroupAlgebraCoeff
    (C : ProCGroups.FiniteGroupClass.{u})
    (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (a : ZCCoeff C) : ZCCompletedGroupAlgebra C H :=
  ⟨fun i =>
      MonoidAlgebra.single
        (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
        (proCIntegerProj (C := C) i.1 a), by
    intro i j hij
    letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
    letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
    rw [zcCompletedGroupAlgebraTransition, RingHom.comp_apply]
    change
      modNCompletedGroupAlgebraStageCoeffMapInClass
          (n := i.1.modulus) (m := j.1.modulus) (G := H) C i.2 hij.1
          (MonoidAlgebra.mapDomain
            (OpenNormalSubgroupInClass.map
              (C := C) (G := H)
              (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2)
            (MonoidAlgebra.single
              (1 : CompletedGroupAlgebraQuotientInClass H C j.2)
              (proCIntegerProj (C := C) j.1 a))) =
        MonoidAlgebra.single
          (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
          (proCIntegerProj (C := C) i.1 a)
    rw [MonoidAlgebra.mapDomain_single,
      modNCompletedGroupAlgebraStageCoeffMapInClass_single_apply]
    have ha : modNCompletedCoeffMap (n := i.1.modulus) (m := j.1.modulus) hij.1
        (proCIntegerProj (C := C) j.1 a) =
        proCIntegerProj (C := C) i.1 a :=
      proCIntegerProj_transition (C := C) hij.1 a
    have hmap :
        (OpenNormalSubgroupInClass.map
          (C := C) (G := H)
          (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2)
            (1 : CompletedGroupAlgebraQuotientInClass H C j.2) =
          (1 : CompletedGroupAlgebraQuotientInClass H C i.2) :=
      map_one _
    rw [hmap, ha]⟩

The coefficient element of \(\mathbb{Z}_C\llbracket H\rrbracket\) supported at the identity of \(H\).

Definition FoxDifferential.zcCompletedGroupAlgebraCoeffMap

def zcCompletedGroupAlgebraCoeffMap
    (C : ProCGroups.FiniteGroupClass.{u})
    (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    ZCCoeff C →+* ZCCompletedGroupAlgebra C H where
  toFun := zcCompletedGroupAlgebraCoeff C H
  map_zero' := by
    apply Subtype.ext
    funext i
    change
      MonoidAlgebra.single
          (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
          (proCIntegerProj (C := C) i.1 0) = 0
    rw [proCIntegerProj_zero, MonoidAlgebra.single_zero]
  map_one' := by
    apply Subtype.ext
    funext i
    letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
    change
      MonoidAlgebra.single
          (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
          (proCIntegerProj (C := C) i.1 1) = 1
    rw [proCIntegerProj_one, ← MonoidAlgebra.one_def]
  map_add' a b := by
    apply Subtype.ext
    funext i
    change
      MonoidAlgebra.single
          (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
          (proCIntegerProj (C := C) i.1 (a + b)) =
        MonoidAlgebra.single
            (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
            (proCIntegerProj (C := C) i.1 a) +
          MonoidAlgebra.single
            (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
            (proCIntegerProj (C := C) i.1 b)
    rw [proCIntegerProj_add, MonoidAlgebra.single_add]
  map_mul' a b := by
    apply Subtype.ext
    funext i
    letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
    change MonoidAlgebra.single
        (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
        (proCIntegerProj (C := C) i.1 (a * b)) =
      MonoidAlgebra.single
        (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
        (proCIntegerProj (C := C) i.1 a) *
      MonoidAlgebra.single
        (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
        (proCIntegerProj (C := C) i.1 b)
    simp only [proCIntegerProj_mul, MonoidAlgebra.single_mul_single, mul_one]

Coefficient change is performed stagewise: supports are unchanged and coefficients are transported by the given ring homomorphism.

Theorem FoxDifferential.zcCompletedGroupAlgebraProjection_coeffMap

@[simp]
theorem zcCompletedGroupAlgebraProjection_coeffMap
    (C : ProCGroups.FiniteGroupClass.{u})
    (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (i : ZCCompletedGroupAlgebraIndex C H) (a : ZCCoeff C) :
    zcCompletedGroupAlgebraProjection C H i
        (zcCompletedGroupAlgebraCoeffMap C H a) =
      MonoidAlgebra.single
        (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
        (proCIntegerProj (C := C) i.1 a)

The completed group-algebra projection commutes with the coefficient-change map at the corresponding finite stage.

Show Lean proof

Definition FoxDifferential.zcGroupLike

def zcGroupLike
    (C : ProCGroups.FiniteGroupClass.{u})
    (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    H →* ZCCompletedGroupAlgebra C H where
  toFun h := ⟨fun i =>
      MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
        (CompletedGroupAlgebraQuotientInClass H C i.2) (QuotientGroup.mk h), by
    intro i j hij
    change
      zcCompletedGroupAlgebraTransition C H hij
          (MonoidAlgebra.of (ModNCompletedCoeff j.1.modulus)
            (CompletedGroupAlgebraQuotientInClass H C j.2) (QuotientGroup.mk h)) =
        MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
          (CompletedGroupAlgebraQuotientInClass H C i.2) (QuotientGroup.mk h)
    rw [zcCompletedGroupAlgebraTransition_of C H hij]
    rfl⟩
  map_one' := by
    apply Subtype.ext
    funext i
    change
      MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
          (CompletedGroupAlgebraQuotientInClass H C i.2)
          (1 : CompletedGroupAlgebraQuotientInClass H C i.2) = 1
    exact map_one
      (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
        (CompletedGroupAlgebraQuotientInClass H C i.2))
  map_mul' h₁ h₂ := by
    apply Subtype.ext
    funext i
    change
      MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
          (CompletedGroupAlgebraQuotientInClass H C i.2) (QuotientGroup.mk (h₁ * h₂)) =
        MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
            (CompletedGroupAlgebraQuotientInClass H C i.2) (QuotientGroup.mk h₁) *
          MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
            (CompletedGroupAlgebraQuotientInClass H C i.2) (QuotientGroup.mk h₂)
    change
      MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
          (CompletedGroupAlgebraQuotientInClass H C i.2)
          ((QuotientGroup.mk h₁ :
            CompletedGroupAlgebraQuotientInClass H C i.2) *
            (QuotientGroup.mk h₂ :
              CompletedGroupAlgebraQuotientInClass H C i.2)) =
        MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
            (CompletedGroupAlgebraQuotientInClass H C i.2)
            (QuotientGroup.mk h₁) *
          MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
            (CompletedGroupAlgebraQuotientInClass H C i.2)
            (QuotientGroup.mk h₂)
    exact map_mul
      (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
        (CompletedGroupAlgebraQuotientInClass H C i.2)) _ _

The group-like map \(H \to \mathbb{Z}_C\llbracket H\rrbracket\).

Theorem FoxDifferential.zcCompletedGroupAlgebraProjection_groupLike

@[simp]
theorem zcCompletedGroupAlgebraProjection_groupLike
    (C : ProCGroups.FiniteGroupClass.{u})
    (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (i : ZCCompletedGroupAlgebraIndex C H) (h : H) :
    zcCompletedGroupAlgebraProjection C H i (zcGroupLike C H h) =
      MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
        (CompletedGroupAlgebraQuotientInClass H C i.2) (QuotientGroup.mk h)

Projecting a group-like element of \(\mathbb{Z}_C\llbracket H\rrbracket\) gives its finite-stage group-like image.

Show Lean proof

Theorem FoxDifferential.zcCompletedGroupAlgebraProjectionRingHom_groupLike

@[simp]
theorem zcCompletedGroupAlgebraProjectionRingHom_groupLike
    (C : ProCGroups.FiniteGroupClass.{u})
    (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (i : ZCCompletedGroupAlgebraIndex C H) (h : H) :
    zcCompletedGroupAlgebraProjectionRingHom C H i (zcGroupLike C H h) =
      MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
        (CompletedGroupAlgebraQuotientInClass H C i.2) (QuotientGroup.mk h)

The projection ring homomorphism sends a group-like element to its image in the corresponding finite group-algebra stage.

Show Lean proof

Theorem FoxDifferential.zcCompletedGroupAlgebra_projection_sub_one_mul_eq_zero

theorem zcCompletedGroupAlgebra_projection_sub_one_mul_eq_zero
    (C : ProCGroups.FiniteGroupClass.{u})
    (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (h : H) (y : ZCCompletedGroupAlgebra C H)
    (i : ZCCompletedGroupAlgebraIndex C H)
    (hrel : (zcGroupLike C H h - 1) * y = 0) :
    (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
        (CompletedGroupAlgebraQuotientInClass H C i.2)
        (QuotientGroup.mk h) - 1) *
      zcCompletedGroupAlgebraProjection C H i y = 0

A completed group-algebra relation \((h - 1)y = 0\) descends to every finite stage.

Show Lean proof

Theorem FoxDifferential.zcCompletedGroupAlgebra_projection_zpow_sub_one_mul_eq_zero

theorem zcCompletedGroupAlgebra_projection_zpow_sub_one_mul_eq_zero
    (C : ProCGroups.FiniteGroupClass.{u})
    (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (h : H) (n : ℤ) (y : ZCCompletedGroupAlgebra C H)
    (i : ZCCompletedGroupAlgebraIndex C H)
    (hrel : (zcGroupLike C H (h ^ n) - 1) * y = 0) :
    (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
        (CompletedGroupAlgebraQuotientInClass H C i.2)
        ((QuotientGroup.mk h : CompletedGroupAlgebraQuotientInClass H C i.2) ^ n) -
        1) *
      zcCompletedGroupAlgebraProjection C H i y = 0

Integer-power version of finite-stage descent for \((h^n - 1)y = 0\).

Show Lean proof

Theorem FoxDifferential.zcCompletedGroupAlgebraTransition_sameCoeff

theorem zcCompletedGroupAlgebraTransition_sameCoeff
    (C : ProCGroups.FiniteGroupClass.{u})
    (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (coeff : ProCIntegerIndex C)
    {U V : OpenNormalSubgroupInClass C H}
    (hUV : (V.1 : Subgroup H) ≤ (U.1 : Subgroup H)) :
    zcCompletedGroupAlgebraTransition C H
        (i := (coeff, OrderDual.toDual U))
        (j := (coeff, OrderDual.toDual V))
        (show (coeff, OrderDual.toDual U) ≤ (coeff, OrderDual.toDual V) from
          ⟨dvd_rfl, hUV⟩) =
      MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff coeff.modulus)
        (OpenNormalSubgroupInClass.map
          (C := C) (G := H) (U := U) (V := V) hUV)

A \(\mathbb{Z}_C\llbracket H\rrbracket\) transition with unchanged coefficient modulus is just the quotient map on the finite group-algebra domain.

Show Lean proof

Theorem FoxDifferential.zcCompletedGroupAlgebraProjection_coeffMap_mul_groupLike

@[simp]
theorem zcCompletedGroupAlgebraProjection_coeffMap_mul_groupLike
    (C : ProCGroups.FiniteGroupClass.{u})
    (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (i : ZCCompletedGroupAlgebraIndex C H) (a : ZCCoeff C) (h : H) :
    zcCompletedGroupAlgebraProjection C H i
        (zcCompletedGroupAlgebraCoeffMap C H a * zcGroupLike C H h) =
      MonoidAlgebra.single
        (QuotientGroup.mk h : CompletedGroupAlgebraQuotientInClass H C i.2)
        (proCIntegerProj (C := C) i.1 a)

After coefficient change, projection of multiplication by a group-like element is computed in the corresponding finite group-algebra stage.

Show Lean proof

Theorem FoxDifferential.zcCompletedGroupAlgebraProjection_surjective

theorem zcCompletedGroupAlgebraProjection_surjective
    (C : ProCGroups.FiniteGroupClass.{u})
    (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (i : ZCCompletedGroupAlgebraIndex C H) :
    Function.Surjective (zcCompletedGroupAlgebraProjection C H i)

Every finite-stage projection from the pro-\(C\) completed group algebra is surjective.

Show Lean proof

Definition FoxDifferential.zcCompletedGroupAlgebraScalar

def zcCompletedGroupAlgebraScalar (ψ : G →* H) :
    G →* ZCCompletedGroupAlgebra C H :=
  (zcGroupLike C H).comp ψ

The completed coefficient homomorphism \(G \to \mathbb{Z}_C\llbracket H\rrbracket\) induced by \(\psi: G \to H\).

Theorem FoxDifferential.zcCompletedGroupAlgebraScalar_apply

@[simp]
theorem zcCompletedGroupAlgebraScalar_apply (ψ : G →* H) (g : G) :
    zcCompletedGroupAlgebraScalar C ψ g = zcGroupLike C H (ψ g)

The completed group-algebra scalar associated to g is the group-like element determined by ψ g.

Show Lean proof

Theorem FoxDifferential.zcCompletedGroupAlgebraScalar_subtype_ker

@[simp]
theorem zcCompletedGroupAlgebraScalar_subtype_ker (ψ : G →* H) (g : ψ.ker) :
    zcCompletedGroupAlgebraScalar C ψ g = 1

If \(g\in\ker \psi\), then the completed coefficient homomorphism induced by \(\psi\) sends \(g\) to the unit element.

Show Lean proof

Abbreviation FoxDifferential.ZCCompletedDifferentialModule

abbrev ZCCompletedDifferentialModule (ψ : G →* H) : Type _ :=
  CrossedDifferentialModule (zcCompletedGroupAlgebraScalar C ψ)

The algebraic universal \(\mathbb{Z}_C\llbracket H\rrbracket\) differential module attached to \(\psi : G \to H\). It is the \(\mathbb{Z}_C\llbracket H\rrbracket\)-module generated by the symbols dg, subject to the Leibniz relations \(d(gh)=dg+\) \([\psi(g)]\) dh, i.e. the quotient by the raw crossed-differential relation submodule. The final profinite Crowell middle term is the separated finite-stage quotient \(\mathbb{Z}_C\)-separated completed differential module, not this algebraic quotient.

Definition FoxDifferential.zcUniversalDifferential

def zcUniversalDifferential (ψ : G →* H) :
    ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCCompletedDifferentialModule C ψ) :=
  universalCrossedHom (zcCompletedGroupAlgebraScalar C ψ)

The universal completed crossed differential, bundled with its Fox--Leibniz law.

Definition FoxDifferential.zcCompletedGroupAlgebraBoundary

def zcCompletedGroupAlgebraBoundary (ψ : G →* H) :
    ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCCompletedGroupAlgebra C H) where
  toFun g := zcGroupLike C H (ψ g) - 1
  map_mul' g h := by
    simp only [scalarCrossedAction_apply, map_mul, sub_eq_add_neg, add_comm,
      zcCompletedGroupAlgebraScalar_apply, smul_eq_mul, mul_add, mul_neg,
      mul_one, add_assoc, add_neg_cancel_comm_assoc]

The completed Fox boundary \(g \mapsto [\psi(g)] - 1\), bundled with its Fox--Leibniz law.

Theorem FoxDifferential.zcCompletedGroupAlgebraBoundary_eq_zero_of_mem_ker

@[simp]
theorem zcCompletedGroupAlgebraBoundary_eq_zero_of_mem_ker
    (ψ : G →* H) {g : G} (hg : ψ g = 1) :
    zcCompletedGroupAlgebraBoundary C ψ g = 0

The completed Fox boundary vanishes on elements in the kernel of the target map.

Show Lean proof

Theorem FoxDifferential.zcCompletedGroupAlgebraBoundary_subtype_ker

@[simp]
theorem zcCompletedGroupAlgebraBoundary_subtype_ker
    (ψ : G →* H) (g : ψ.ker) :
    zcCompletedGroupAlgebraBoundary C ψ g = 0

The completed Fox boundary restricted to the kernel subgroup is zero.

Show Lean proof

Definition FoxDifferential.zcToCompletedGroupAlgebra

def zcToCompletedGroupAlgebra (ψ : G →* H) :
    ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
      ZCCompletedGroupAlgebra C H :=
  crossedHomModuleLift (A := ZCCompletedGroupAlgebra C H)
    (zcCompletedGroupAlgebraScalar C ψ) (zcCompletedGroupAlgebraBoundary C ψ)

The universal \(\mathbb{Z}_C\llbracket H\rrbracket\)-linear map from the completed crossed-differential module to the completed group algebra is induced by the completed Fox boundary \(g\mapsto [\psi(g)]-1\).

Theorem FoxDifferential.zcToCompletedGroupAlgebra_universal

@[simp]
theorem zcToCompletedGroupAlgebra_universal (ψ : G →* H) (g : G) :
    zcToCompletedGroupAlgebra C ψ (zcUniversalDifferential C ψ g) =
      zcCompletedGroupAlgebraBoundary C ψ g

The universal map to the completed group algebra sends the universal differential of \(g\) to the completed Fox boundary \([\psi(g)]-1\).

Show Lean proof

Theorem FoxDifferential.existsUnique_zcToCompletedGroupAlgebra

theorem existsUnique_zcToCompletedGroupAlgebra (ψ : G →* H) :
    ∃! f :
        ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
          ZCCompletedGroupAlgebra C H,
      ∀ g, f (zcUniversalDifferential C ψ g) =
        zcCompletedGroupAlgebraBoundary C ψ g

There is a unique \(\mathbb{Z}_C\llbracket H\rrbracket\)-linear map from the completed crossed-differential module to the completed group algebra that sends every universal differential to the corresponding completed Fox boundary.

Show Lean proof

Definition FoxDifferential.zcCompletedDifferentialModuleSourceMap

def zcCompletedDifferentialModuleSourceMap
    (ψ' : G' →* H) (f : G →* G') :
    ZCCompletedDifferentialModule C (ψ'.comp f) →ₗ[ZCCompletedGroupAlgebra C H]
      ZCCompletedDifferentialModule C ψ' :=
  crossedHomModuleLift (A := ZCCompletedDifferentialModule C ψ')
    (zcCompletedGroupAlgebraScalar C (ψ'.comp f))
    { toFun := fun g => zcUniversalDifferential C ψ' (f g)
      map_mul' := by
        intro g h
        change zcUniversalDifferential C ψ' (f (g * h)) =
          zcUniversalDifferential C ψ' (f g) +
            zcCompletedGroupAlgebraScalar C (ψ'.comp f) g •
              zcUniversalDifferential C ψ' (f h)
        rw [map_mul, ScalarCrossedHom.map_mul (zcUniversalDifferential C ψ')]
        rfl }

Source functoriality for the completed universal differential module. For a homomorphism \(f:G \to G'\), the universal crossed differential attached to \(\psi'\circ f\) maps to the one attached to \(\psi'\) by sending \(dg\) to \(d(f(g))\).

Theorem FoxDifferential.zcCompletedDifferentialModuleSourceMap_universal

@[simp]
theorem zcCompletedDifferentialModuleSourceMap_universal
    (ψ' : G' →* H) (f : G →* G') (g : G) :
    zcCompletedDifferentialModuleSourceMap (C := C) ψ' f
        (zcUniversalDifferential C (ψ'.comp f) g) =
      zcUniversalDifferential C ψ' (f g)

The universal source map on the completed differential module is determined by the source quotient maps at finite stages.

Show Lean proof

Theorem FoxDifferential.zcUniversalDifferential_eq_zero_of_source

theorem zcUniversalDifferential_eq_zero_of_source
    (ψ' : G' →* H) (f : G →* G') {g : G}
    (hg : zcUniversalDifferential C (ψ'.comp f) g = 0) :
    zcUniversalDifferential C ψ' (f g) = 0

Completed universal zero descends along a source homomorphism.

Show Lean proof

Theorem FoxDifferential.crossedDifferential_eq_zero_of_zcUniversalDifferential_eq_zero

theorem crossedDifferential_eq_zero_of_zcUniversalDifferential_eq_zero
    (ψ : G →* H)
    (D : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
    {g : G} (hg : zcUniversalDifferential C ψ g = 0) :
    D g = 0

A zero universal differential is killed by every crossed differential represented by the completed universal module.

Show Lean proof

ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.Core

Declarations