ProCGroups.FoxDifferential.Completed.FiniteStage.Basic

10 Theorems | 6 Definitions | 1 Instance

The principal declarations in this module are:

foxCommutatorPowerRelatorSet Relators defining the finite Fox source quotient: commutators in \(N\) and \(n\)-th powers in \(N\). - foxCommutatorPowerSubgroup Normal subgroup generated by commutators in \(N\) and \(n\)-th powers in \(N\). - modNCompletedGroupAlgebraStageMap_algebraMap The finite-stage completed group-algebra projection preserves coefficient algebra maps. - foxCommutatorPowerRelatorSet_subset The finite Fox commutator-power relator set is contained in N.

import

ProCGroups.FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.SubtypeLinear

Imported by

Theorem FoxDifferential.modNCompletedGroupAlgebraStageMap_algebraMap

omit [Fact (0 < n)] in
@[simp]
theorem modNCompletedGroupAlgebraStageMap_algebraMap
    (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (c : ModNCompletedCoeff n) :
    modNCompletedGroupAlgebraStageMap n G U
        (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) c) =
      algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupAlgebraStage n G U) c

The finite-stage completed group-algebra projection preserves coefficient algebra maps.

Show Lean proof

Definition FoxDifferential.foxCommutatorPowerRelatorSet

def foxCommutatorPowerRelatorSet (N : Subgroup F) (n : ℕ) : Set F :=
  {g | (∃ a ∈ N, ∃ b ∈ N, ⁅a, b⁆ = g) ∨ ∃ a ∈ N, a ^ n = g}

Relators defining the finite Fox source quotient: commutators in \(N\) and \(n\)-th powers in \(N\).

Definition FoxDifferential.foxCommutatorPowerSubgroup

def foxCommutatorPowerSubgroup (N : Subgroup F) (n : ℕ) : Subgroup F :=
  Subgroup.normalClosure (foxCommutatorPowerRelatorSet (F := F) N n)

Normal subgroup generated by commutators in \(N\) and \(n\)-th powers in \(N\).

Instance FoxDifferential.foxCommutatorPowerSubgroup_normal

instance foxCommutatorPowerSubgroup_normal
    (N : Subgroup F) (n : ℕ) :
    (foxCommutatorPowerSubgroup (F := F) N n).Normal := by
  dsimp [foxCommutatorPowerSubgroup]
  infer_instance

The finite Fox commutator-power subgroup is normal by construction.

Theorem FoxDifferential.foxCommutatorPowerRelatorSet_subset

theorem foxCommutatorPowerRelatorSet_subset
    (N : Subgroup F) (n : ℕ) :
    foxCommutatorPowerRelatorSet (F := F) N n ⊆ N

The finite Fox commutator-power relator set is contained in N.

Show Lean proof

Theorem FoxDifferential.foxCommutatorPowerSubgroup_le_normal

theorem foxCommutatorPowerSubgroup_le_normal
    (N : Subgroup F) [N.Normal] (n : ℕ) :
    foxCommutatorPowerSubgroup (F := F) N n ≤ N

The finite Fox commutator-power subgroup is contained in \(N\) when \(N\) is normal.

Show Lean proof

Definition FoxDifferential.foxCommutatorPowerQuotientMapToNormalQuotient

def foxCommutatorPowerQuotientMapToNormalQuotient
    (N : Subgroup F) [N.Normal] (n : ℕ) :
    F ⧸ foxCommutatorPowerSubgroup (F := F) N n →* F ⧸ N :=
  QuotientGroup.map _ _ (MonoidHom.id F)
    (foxCommutatorPowerSubgroup_le_normal (F := F) N n)

Natural quotient map \(F/[N,N]N^n \to F/N\).

Theorem FoxDifferential.foxCommutatorPowerQuotientMapToNormalQuotient_mk

@[simp]
theorem foxCommutatorPowerQuotientMapToNormalQuotient_mk
    (N : Subgroup F) [N.Normal] (n : ℕ) (g : F) :
    foxCommutatorPowerQuotientMapToNormalQuotient (F := F) N n
        (QuotientGroup.mk'
          (foxCommutatorPowerSubgroup (F := F) N n) g) =
      QuotientGroup.mk' N g

Evaluation of the natural quotient map \(F/[N,N]N^n \to F/N\) on a representative.

Show Lean proof

Theorem FoxDifferential.foxCommutatorPowerQuotientMapToNormalQuotient_surjective

theorem foxCommutatorPowerQuotientMapToNormalQuotient_surjective
    (N : Subgroup F) [N.Normal] (n : ℕ) :
    Function.Surjective
      (foxCommutatorPowerQuotientMapToNormalQuotient (F := F) N n)

The natural quotient map \(F/[N,N]N^n \to F/N\) is surjective.

Show Lean proof

Definition FoxDifferential.foxCommutatorPowerGroupAlgebraMap

def foxCommutatorPowerGroupAlgebraMap
    (N : Subgroup F) [N.Normal] (n : ℕ) :
    MonoidAlgebra (ModNCompletedCoeff n)
        (F ⧸ foxCommutatorPowerSubgroup (F := F) N n) →+*
      MonoidAlgebra (ModNCompletedCoeff n) (F ⧸ N) :=
  MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n)
    (foxCommutatorPowerQuotientMapToNormalQuotient (F := F) N n)

Group-algebra map induced by the natural quotient \(F/[N,N]N^n \to F/N\).

Definition FoxDifferential.foxCommutatorPowerGroupAlgebraAlgHom

def foxCommutatorPowerGroupAlgebraAlgHom
    (N : Subgroup F) [N.Normal] (n : ℕ) :
    MonoidAlgebra (ModNCompletedCoeff n)
        (F ⧸ foxCommutatorPowerSubgroup (F := F) N n) →ₐ[
      ModNCompletedCoeff n]
      MonoidAlgebra (ModNCompletedCoeff n) (F ⧸ N) :=
  MonoidAlgebra.mapDomainAlgHom (ModNCompletedCoeff n) (ModNCompletedCoeff n)
    (foxCommutatorPowerQuotientMapToNormalQuotient (F := F) N n)

Algebra-hom version of the group-algebra map induced by \(F/[N,N]N^n \to F/N\).

Theorem FoxDifferential.foxCommutatorPowerGroupAlgebraAlgHom_apply

@[simp]
theorem foxCommutatorPowerGroupAlgebraAlgHom_apply
    (N : Subgroup F) [N.Normal] (n : ℕ)
    (x : MonoidAlgebra (ModNCompletedCoeff n)
        (F ⧸ foxCommutatorPowerSubgroup (F := F) N n)) :
    foxCommutatorPowerGroupAlgebraAlgHom (F := F) N n x =
      foxCommutatorPowerGroupAlgebraMap (F := F) N n x

The algebra-hom and ring-hom versions of the finite Fox quotient map agree on values.

Show Lean proof

Definition FoxDifferential.foxCommutatorPowerSourceGroupAlgebraAugmentation

def foxCommutatorPowerSourceGroupAlgebraAugmentation
    (N : Subgroup F) (n : ℕ) :
    MonoidAlgebra (ModNCompletedCoeff n)
        (F ⧸ foxCommutatorPowerSubgroup (F := F) N n) →ₐ[
      ModNCompletedCoeff n] ModNCompletedCoeff n :=
  MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n)
    (F ⧸ foxCommutatorPowerSubgroup (F := F) N n)
    (1 : (F ⧸ foxCommutatorPowerSubgroup (F := F) N n) →*
      ModNCompletedCoeff n)

Augmentation map on the finite Fox source group algebra.

Theorem FoxDifferential.foxCommutatorPowerSourceGroupAlgebraAugmentation_of_quotient

@[simp]
theorem foxCommutatorPowerSourceGroupAlgebraAugmentation_of_quotient
    (N : Subgroup F) (n : ℕ)
    (q : F ⧸ foxCommutatorPowerSubgroup (F := F) N n) :
    foxCommutatorPowerSourceGroupAlgebraAugmentation (F := F) N n
        (MonoidAlgebra.of (ModNCompletedCoeff n)
          (F ⧸ foxCommutatorPowerSubgroup (F := F) N n) q) =
      1

The source augmentation sends every quotient group basis element to \(1\).

Show Lean proof

Theorem FoxDifferential.foxCommutatorPowerGroupAlgebraMap_of

@[simp]
theorem foxCommutatorPowerGroupAlgebraMap_of
    (N : Subgroup F) [N.Normal] (n : ℕ) (g : F) :
    foxCommutatorPowerGroupAlgebraMap (F := F) N n
        (MonoidAlgebra.of (ModNCompletedCoeff n)
          (F ⧸ foxCommutatorPowerSubgroup (F := F) N n)
          (QuotientGroup.mk'
            (foxCommutatorPowerSubgroup (F := F) N n) g)) =
      MonoidAlgebra.of (ModNCompletedCoeff n) (F ⧸ N) (QuotientGroup.mk' N g)

The finite Fox source-to-target group-algebra map evaluated on a represented word.

Show Lean proof

Theorem FoxDifferential.foxCommutatorPowerGroupAlgebraMap_of_quotient

@[simp]
theorem foxCommutatorPowerGroupAlgebraMap_of_quotient
    (N : Subgroup F) [N.Normal] (n : ℕ)
    (q : F ⧸ foxCommutatorPowerSubgroup (F := F) N n) :
    foxCommutatorPowerGroupAlgebraMap (F := F) N n
        (MonoidAlgebra.of (ModNCompletedCoeff n)
          (F ⧸ foxCommutatorPowerSubgroup (F := F) N n) q) =
      MonoidAlgebra.of (ModNCompletedCoeff n) (F ⧸ N)
        (foxCommutatorPowerQuotientMapToNormalQuotient (F := F) N n q)

The finite Fox source-to-target group-algebra map evaluated on a quotient basis element.

Show Lean proof

Theorem FoxDifferential.foxCommutatorPowerGroupAlgebraMap_single_apply

omit [Fact (0 < ℓ)] in
@[simp]
theorem foxCommutatorPowerGroupAlgebraMap_single_apply
    (N : Subgroup F) [N.Normal] (n : ℕ)
    (q : F ⧸ foxCommutatorPowerSubgroup (F := F) N n)
    (a : ModNCompletedCoeff n) :
    foxCommutatorPowerGroupAlgebraMap (F := F) N n
        (MonoidAlgebra.single q a) =
      MonoidAlgebra.single
        (foxCommutatorPowerQuotientMapToNormalQuotient (F := F) N n q) a

The finite Fox source-to-target group-algebra map evaluated on a single coefficient basis term.

Show Lean proof

ProCGroups.FoxDifferential.Completed.FiniteStage.Basic

Declarations