FoxDifferential.Completed.FiniteStage.Stage.Semidirect
This module sets up the finite-stage and inverse-limit description of the construction. It records the stage maps, projections, and comparison lemmas used to pass back to the completed object.
abbrev finiteFoxStageTargetQuotient : Type u :=
FreeGroup X ⧸ NThe finite-stage target quotient \(F/N\).
abbrev finiteFoxStageTargetGroupAlgebra : Type u :=
MonoidAlgebra (ModNCompletedCoeff n) (finiteFoxStageTargetQuotient (X := X) N)The finite-stage target group algebra \((\mathbb{Z}/n\mathbb{Z})[F/N]\).
abbrev finiteFoxStageSourceGroupAlgebra : Type u :=
MonoidAlgebra (ModNCompletedCoeff n)
(FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n)The finite-stage source group algebra \((\mathbb{Z}/n\mathbb{Z})[F/[N,N]N^n]\).
def finiteFoxStageGroupAlgebraMapKernelIdeal :
Ideal (finiteFoxStageSourceGroupAlgebra (X := X) N n) :=
RingHom.ker (finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n)The finite-stage kernel \(K_j\) of \((\mathbb{Z}/n\mathbb{Z})[F/[N,N]N^n] \to (\mathbb{Z}/n\mathbb{Z})[F/N]\).
theorem mem_finiteFoxStageGroupAlgebraMapKernelIdeal
{N : Subgroup (FreeGroup X)} [N.Normal] {n : ℕ}
{x : finiteFoxStageSourceGroupAlgebra (X := X) N n} :
x ∈ finiteFoxStageGroupAlgebraMapKernelIdeal (X := X) N n ↔
finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n x = 0Membership test for the finite-stage group-algebra map kernel ideal.
Show proof
by
rflProof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□def finiteFoxStageSourceAugmentationIdeal :
Ideal (finiteFoxStageSourceGroupAlgebra (X := X) N n) :=
RingHom.ker
(finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation
(F := FreeGroup X) N n).toRingHomThe finite-stage source augmentation ideal is the kernel of the corresponding finite-stage augmentation map.
theorem mem_finiteFoxStageSourceAugmentationIdeal
{N : Subgroup (FreeGroup X)} {n : ℕ}
{x : finiteFoxStageSourceGroupAlgebra (X := X) N n} :
x ∈ finiteFoxStageSourceAugmentationIdeal (X := X) N n ↔
finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation
(F := FreeGroup X) N n x = 0Membership in the finite-stage source augmentation ideal is equivalent to vanishing under the finite-stage source augmentation map.
Show proof
by
rflProof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□def finiteFoxStageGroupAlgebraMapKernelMulAugmentationIdeal :
Ideal (finiteFoxStageSourceGroupAlgebra (X := X) N n) :=
finiteFoxStageGroupAlgebraMapKernelIdeal (X := X) N n *
finiteFoxStageSourceAugmentationIdeal (X := X) N nThe finite-stage product ideal \(K_j I_j\) governing the Fox kernel criterion.
abbrev finiteFoxStageCoordinateVector : Type u :=
X → finiteFoxStageTargetGroupAlgebra (X := X) N nCoordinate vectors for finite-stage Fox derivatives.
structure FiniteFoxStageSemidirect where
left : finiteFoxStageCoordinateVector (X := X) N n
right : finiteFoxStageTargetQuotient (X := X) NFinite-stage Fox semidirect target \(A^X \rtimes F/N\), whose left component stores the derivative vector and whose right component stores the quotient word.
theorem ext
{a b : FiniteFoxStageSemidirect (X := X) N n}
(hleft : a.left = b.left) (hright : a.right = b.right) : a = bExtensionality for finite-stage semidirect elements.
Show proof
by
cases a
cases b
simp_allProof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□instance instOneFiniteFoxStageSemidirect : One (FiniteFoxStageSemidirect (X := X) N n) where
one := ⟨0, 1⟩The identity element of the finite-stage Fox semidirect product is \((0,1)\).
instance instMulFiniteFoxStageSemidirect : Mul (FiniteFoxStageSemidirect (X := X) N n) where
mul a b :=
⟨a.left +
(MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) N) a.right) • b.left,
a.right * b.right⟩instance instInvFiniteFoxStageSemidirect : Inv (FiniteFoxStageSemidirect (X := X) N n) where
inv a :=
⟨-((MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) N) a.right⁻¹) • a.left),
a.right⁻¹⟩Inversion in the finite-stage Fox semidirect product.
theorem one_left :
(1 : FiniteFoxStageSemidirect (X := X) N n).left = 0The left component of the finite-stage semidirect identity is zero.
Show proof
rflProof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□theorem one_right :
(1 : FiniteFoxStageSemidirect (X := X) N n).right = 1The right component of the finite-stage semidirect identity is the group identity.
Show proof
rflProof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□theorem mul_left
(a b : FiniteFoxStageSemidirect (X := X) N n) :
(a * b).left =
a.left +
(MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) N) a.right) • b.leftLeft-component formula for multiplication in the finite-stage semidirect product.
Show proof
rflProof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□theorem mul_right
(a b : FiniteFoxStageSemidirect (X := X) N n) :
(a * b).right = a.right * b.rightRight-component formula for multiplication in the finite-stage semidirect product.
Show proof
rflProof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□theorem inv_left
(a : FiniteFoxStageSemidirect (X := X) N n) :
a⁻¹.left =
-((MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) N) a.right⁻¹) • a.left)Left-component formula for inversion in the finite-stage semidirect product.
Show proof
rflProof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□theorem inv_right
(a : FiniteFoxStageSemidirect (X := X) N n) :
a⁻¹.right = a.right⁻¹Right-component formula for inversion in the finite-stage semidirect product.
Show proof
rflProof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□instance instGroupFiniteFoxStageSemidirect : Group (FiniteFoxStageSemidirect (X := X) N n) where
one := 1
mul := (· * ·)
inv := Inv.inv
mul_assoc a b c := by
apply ext
· funext i
simp only [mul_left, MonoidAlgebra.of_apply, mul_right, Pi.add_apply, Pi.smul_apply, smul_eq_mul, add_assoc,
smul_add, smul_smul, MonoidAlgebra.single_mul_single, mul_one]
· simp only [mul_right, mul_assoc]
one_mul a := by
apply ext
· funext i
simp only [mul_left, one_left, one_right, Pi.smul_apply, zero_add]
have hone :
(MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) N) 1 :
finiteFoxStageTargetGroupAlgebra (X := X) N n) = 1 := by
simp only [MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.one_def]
rw [hone, one_smul]
· simp only [mul_right, one_right, one_mul]
mul_one a := by
apply ext
· funext i
simp only [mul_left, MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk, OneHom.coe_mk, one_left,
smul_zero, Pi.add_apply, Pi.zero_apply, add_zero]
· simp only [mul_right, one_right, mul_one]
inv_mul_cancel a := by
apply ext
· funext i
simp only [mul_left, inv_left, MonoidAlgebra.of_apply, inv_right, Pi.add_apply, Pi.neg_apply, Pi.smul_apply,
smul_eq_mul, neg_add_cancel, one_left, Pi.zero_apply]
· simp only [mul_right, inv_right, inv_mul_cancel, one_right]Group structure on the finite-stage Fox semidirect product.