ProCGroups.FoxDifferential.Completed.FreeProC.ProCIntegerStageCoeffProjection

10 Theorems | 2 Definitions

The principal declarations in this module are:

zcCompletedGroupAlgebraStageToFoxAlgebraicStage A finite stage of \(\mathbb{Z}_C\llbracket H\rrbracket\) maps to a finite Fox target group algebra once its coefficient modulus dominates \(n\) and its finite quotient maps to \(F/N\). - zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap The resulting completed-to-finite coefficient map. - zcCompletedGroupAlgebraStageToFoxAlgebraicStage_of Evaluation on a completed group-algebra stage basis element. - zcCompletedGroupAlgebraStageToFoxAlgebraicStage_single Evaluation on a single coefficient at a stage quotient element.

imports

Imported by

Definition FoxDifferential.zcCompletedGroupAlgebraStageToFoxAlgebraicStage

def zcCompletedGroupAlgebraStageToFoxAlgebraicStage
    (hmod : n ∣ i.1.modulus)
    (qmap : CompletedGroupAlgebraQuotientInClass H C i.2 →*
      foxAlgebraicStageTargetQuotient (X := X) N) :
    ZCCompletedGroupAlgebraStage C H i →+*
      foxAlgebraicStageTargetGroupAlgebra (X := X) N n := by
  letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
  letI : Algebra (ModNCompletedCoeff i.1.modulus) (ModNCompletedCoeff n) :=
    ZMod.algebra' (R := ModNCompletedCoeff n) (m := n) (n := i.1.modulus) hmod
  letI : Algebra (ModNCompletedCoeff i.1.modulus)
      (foxAlgebraicStageTargetGroupAlgebra (X := X) N n) := inferInstance
  exact
    (MonoidAlgebra.lift (ModNCompletedCoeff i.1.modulus)
      (foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
      (CompletedGroupAlgebraQuotientInClass H C i.2)
      ((MonoidAlgebra.of (ModNCompletedCoeff n)
        (foxAlgebraicStageTargetQuotient (X := X) N)).comp qmap)).toRingHom

A finite stage of \(\mathbb{Z}_C\llbracket H\rrbracket\) maps to a finite Fox target group algebra once its coefficient modulus dominates \(n\) and its finite quotient maps to \(F/N\).

Theorem FoxDifferential.zcCompletedGroupAlgebraStageToFoxAlgebraicStage_of

omit [DecidableEq X] [Fact (0 < n)] in
@[simp]
theorem zcCompletedGroupAlgebraStageToFoxAlgebraicStage_of
    (hmod : n ∣ i.1.modulus)
    (qmap : CompletedGroupAlgebraQuotientInClass H C i.2 →*
      foxAlgebraicStageTargetQuotient (X := X) N)
    (q : CompletedGroupAlgebraQuotientInClass H C i.2) :
    zcCompletedGroupAlgebraStageToFoxAlgebraicStage
        (C := C) (X := X) (H := H) N n i hmod qmap
        (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
          (CompletedGroupAlgebraQuotientInClass H C i.2) q) =
      MonoidAlgebra.of (ModNCompletedCoeff n)
        (foxAlgebraicStageTargetQuotient (X := X) N) (qmap q)

Evaluation on a completed group-algebra stage basis element.

Show Lean proof

Theorem FoxDifferential.zcCompletedGroupAlgebraStageToFoxAlgebraicStage_single

omit [DecidableEq X] [Fact (0 < n)] in
theorem zcCompletedGroupAlgebraStageToFoxAlgebraicStage_single
    (hmod : n ∣ i.1.modulus)
    (qmap : CompletedGroupAlgebraQuotientInClass H C i.2 →*
      foxAlgebraicStageTargetQuotient (X := X) N)
    (q : CompletedGroupAlgebraQuotientInClass H C i.2)
    (a : ModNCompletedCoeff i.1.modulus) :
    zcCompletedGroupAlgebraStageToFoxAlgebraicStage
        (C := C) (X := X) (H := H) N n i hmod qmap
        (MonoidAlgebra.single q a) =
      MonoidAlgebra.single (qmap q)
        (modNCompletedCoeffMap (n := n) (m := i.1.modulus) hmod a)

Evaluation on a single coefficient at a stage quotient element.

Show Lean proof

Theorem FoxDifferential.zcCompletedGroupAlgebraStageToFoxAlgebraicStage_self_injective

omit [DecidableEq X] in
theorem zcCompletedGroupAlgebraStageToFoxAlgebraicStage_self_injective
    (qmap : CompletedGroupAlgebraQuotientInClass H C i.2 →*
      foxAlgebraicStageTargetQuotient (X := X) N)
    (hqmap : Function.Injective qmap) :
    Function.Injective
      (zcCompletedGroupAlgebraStageToFoxAlgebraicStage
        (C := C) (X := X) (H := H) N i.1.modulus i dvd_rfl qmap)

If no coefficient reduction is taken and the target quotient comparison is injective, then the finite-stage map from the completed group-algebra stage to the finite Fox target group algebra is injective.

Show Lean proof

Definition FoxDifferential.zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap

def zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap
    (hmod : n ∣ i.1.modulus)
    (qmap : CompletedGroupAlgebraQuotientInClass H C i.2 →*
      foxAlgebraicStageTargetQuotient (X := X) N) :
    ZCCompletedGroupAlgebra C H →+*
      foxAlgebraicStageTargetGroupAlgebra (X := X) N n :=
  (zcCompletedGroupAlgebraStageToFoxAlgebraicStage
    (C := C) (X := X) (H := H) N n i hmod qmap).comp
    (zcCompletedGroupAlgebraProjectionRingHom C H i)

The resulting completed-to-finite coefficient map.

Theorem FoxDifferential.zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap_apply

omit [DecidableEq X] [Fact (0 < n)] in
@[simp]
theorem zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap_apply
    (hmod : n ∣ i.1.modulus)
    (qmap : CompletedGroupAlgebraQuotientInClass H C i.2 →*
      foxAlgebraicStageTargetQuotient (X := X) N)
    (a : ZCCompletedGroupAlgebra C H) :
    zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap
        (C := C) (X := X) (H := H) N n i hmod qmap a =
      zcCompletedGroupAlgebraStageToFoxAlgebraicStage
        (C := C) (X := X) (H := H) N n i hmod qmap
        (zcCompletedGroupAlgebraProjection C H i a)

The Fox algebraic stage coefficient map evaluates a completed element by stage projection followed by the prescribed target quotient and coefficient maps.

Show Lean proof

Theorem FoxDifferential.zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap_groupLike

omit [DecidableEq X] [Fact (0 < n)] in
theorem zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap_groupLike
    (hmod : n ∣ i.1.modulus)
    (qmap : CompletedGroupAlgebraQuotientInClass H C i.2 →*
      foxAlgebraicStageTargetQuotient (X := X) N)
    (h : H) :
    zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap
        (C := C) (X := X) (H := H) N n i hmod qmap
        (zcGroupLike C H h) =
      MonoidAlgebra.of (ModNCompletedCoeff n)
        (foxAlgebraicStageTargetQuotient (X := X) N)
        (qmap (QuotientGroup.mk h))

Group-like formula for the completed-to-finite coefficient map.

Show Lean proof

Theorem FoxDifferential.zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap_groupLike_eq_stageRight

omit [DecidableEq X] [Fact (0 < n)] in
theorem zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap_groupLike_eq_stageRight
    (hmod : n ∣ i.1.modulus)
    (qmap : CompletedGroupAlgebraQuotientInClass H C i.2 →*
      foxAlgebraicStageTargetQuotient (X := X) N)
    (stageRight : H →* foxAlgebraicStageTargetQuotient (X := X) N)
    (hqmap : ∀ h : H, qmap (QuotientGroup.mk h) = stageRight h)
    (h : H) :
    zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap
        (C := C) (X := X) (H := H) N n i hmod qmap
        (zcGroupLike C H h) =
      MonoidAlgebra.of (ModNCompletedCoeff n)
        (foxAlgebraicStageTargetQuotient (X := X) N) (stageRight h)

Group-like formula rewritten through a named finite right quotient map.

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageTargetGroupAlgebraMap_single_apply

omit [DecidableEq X] [Fact (0 < n)] in
theorem foxAlgebraicStageTargetGroupAlgebraMap_single_apply
    (q : foxAlgebraicStageTargetQuotient (X := X) N)
    (a : ModNCompletedCoeff n) :
    foxAlgebraicStageTargetGroupAlgebraMap (X := X) hNM n
        (MonoidAlgebra.single q a) =
      MonoidAlgebra.single (foxAlgebraicStageTargetQuotientMap (X := X) hNM q) a

Target quotient maps send a single group-algebra coefficient to the mapped basis element.

Show Lean proof

Theorem FoxDifferential.foxAlgebraicStageBifilteredTargetGroupAlgebraMap_single_apply

omit [DecidableEq X] [Fact (0 < n)] [Fact (0 < m)] in
theorem foxAlgebraicStageBifilteredTargetGroupAlgebraMap_single_apply
    (q : foxAlgebraicStageTargetQuotient (X := X) N)
    (a : ModNCompletedCoeff m) :
    foxAlgebraicStageBifilteredTargetGroupAlgebraMap (X := X) hNM hnm
        (MonoidAlgebra.single q a) =
      MonoidAlgebra.single (foxAlgebraicStageTargetQuotientMap (X := X) hNM q)
        (modNCompletedCoeffMap (n := n) (m := m) hnm a)

The bifiltered target transition on a single group-algebra coefficient.

Show Lean proof

Theorem FoxDifferential.zcCompletedGroupAlgebraStageToFoxAlgebraicStage_transition

omit [DecidableEq X] [Fact (0 < n)] [Fact (0 < m)] in
theorem zcCompletedGroupAlgebraStageToFoxAlgebraicStage_transition
    (hmod_i : n ∣ i.1.modulus)
    (hmod_j : m ∣ j.1.modulus)
    (hcoeff : ∀ a : ModNCompletedCoeff j.1.modulus,
      modNCompletedCoeffMap (n := n) (m := i.1.modulus) hmod_i
          (modNCompletedCoeffMap (n := i.1.modulus) (m := j.1.modulus) hij.1 a) =
        modNCompletedCoeffMap (n := n) (m := m) hnm
          (modNCompletedCoeffMap (n := m) (m := j.1.modulus) hmod_j a))
    (qmap_i : CompletedGroupAlgebraQuotientInClass H C i.2 →*
      foxAlgebraicStageTargetQuotient (X := X) M)
    (qmap_j : CompletedGroupAlgebraQuotientInClass H C j.2 →*
      foxAlgebraicStageTargetQuotient (X := X) N)
    (hqmap : ∀ q : CompletedGroupAlgebraQuotientInClass H C j.2,
      qmap_i
          ((OpenNormalSubgroupInClass.map
            (C := C) (G := H)
            (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q) =
        foxAlgebraicStageTargetQuotientMap (X := X) hNM (qmap_j q))
    (x : ZCCompletedGroupAlgebraStage C H j) :
    foxAlgebraicStageBifilteredTargetGroupAlgebraMap (X := X) hNM hnm
        (zcCompletedGroupAlgebraStageToFoxAlgebraicStage
          (C := C) (X := X) (H := H) N m j hmod_j qmap_j x) =
      zcCompletedGroupAlgebraStageToFoxAlgebraicStage
        (C := C) (X := X) (H := H) M n i hmod_i qmap_i
        (zcCompletedGroupAlgebraTransition C H hij x)

Stage-to-finite maps commute with completed-group-algebra transitions when the coefficient reductions and quotient maps commute.

Show Lean proof

Theorem FoxDifferential.zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap_transition

omit [DecidableEq X] [Fact (0 < n)] [Fact (0 < m)] in
theorem zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap_transition
    (hmod_i : n ∣ i.1.modulus)
    (hmod_j : m ∣ j.1.modulus)
    (hcoeff : ∀ a : ModNCompletedCoeff j.1.modulus,
      modNCompletedCoeffMap (n := n) (m := i.1.modulus) hmod_i
          (modNCompletedCoeffMap (n := i.1.modulus) (m := j.1.modulus) hij.1 a) =
        modNCompletedCoeffMap (n := n) (m := m) hnm
          (modNCompletedCoeffMap (n := m) (m := j.1.modulus) hmod_j a))
    (qmap_i : CompletedGroupAlgebraQuotientInClass H C i.2 →*
      foxAlgebraicStageTargetQuotient (X := X) M)
    (qmap_j : CompletedGroupAlgebraQuotientInClass H C j.2 →*
      foxAlgebraicStageTargetQuotient (X := X) N)
    (hqmap : ∀ q : CompletedGroupAlgebraQuotientInClass H C j.2,
      qmap_i
          ((OpenNormalSubgroupInClass.map
            (C := C) (G := H)
            (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q) =
        foxAlgebraicStageTargetQuotientMap (X := X) hNM (qmap_j q))
    (a : ZCCompletedGroupAlgebra C H) :
    foxAlgebraicStageBifilteredTargetGroupAlgebraMap (X := X) hNM hnm
        (zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap
          (C := C) (X := X) (H := H) N m j hmod_j qmap_j a) =
      zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap
        (C := C) (X := X) (H := H) M n i hmod_i qmap_i a

The completed coefficient maps built from stage projections are compatible on completed points once the underlying finite-stage maps commute with transitions.

Show Lean proof

ProCGroups.FoxDifferential.Completed.FreeProC.ProCIntegerStageCoeffProjection

Declarations