ProCGroups.FoxDifferential.Completed.Semidirect

18 Theorems | 4 Definitions | 1 Structure | 4 Instances

The principal declarations in this module are:

ZCCompletedFoxSemidirect The completed Fox semidirect target Z_C[[H]]^X ⋊ H. - rightMonoidHom The right projection from the completed Fox semidirect product to the target group. - ext Extensionality for completed Fox semidirect elements. - one_left The left component of the identity semidirect element is zero.

imports

Imported by

Structure FoxDifferential.ZCCompletedFoxSemidirect

omit [DecidableEq X] in
structure ZCCompletedFoxSemidirect where
  /-- The completed Fox-coordinate component. -/
  left : ZCFreeFoxCoordinates C (X := X) (H := H)
  /-- The target group component. -/
  right : H

The completed Fox semidirect target Z_C[[H]]^X ⋊ H.

Theorem FoxDifferential.ZCCompletedFoxSemidirect.ext

omit [DecidableEq X] in
@[ext]
theorem ext {a b : ZCCompletedFoxSemidirect C X H}
    (hleft : a.left = b.left) (hright : a.right = b.right) : a = b

Extensionality for completed Fox semidirect elements.

Show Lean proof

Instance FoxDifferential.ZCCompletedFoxSemidirect.instOneZCCompletedFoxSemidirect

instance instOneZCCompletedFoxSemidirect : One (ZCCompletedFoxSemidirect C X H) where
  one := ⟨0, 1⟩

Identity element of the completed Fox semidirect product.

Instance FoxDifferential.ZCCompletedFoxSemidirect.instMulZCCompletedFoxSemidirect

instance instMulZCCompletedFoxSemidirect : Mul (ZCCompletedFoxSemidirect C X H) where
  mul a b :=
    ⟨a.left + zcGroupLike C H a.right • b.left, a.right * b.right⟩

Multiplication in the completed Fox semidirect product.

Instance FoxDifferential.ZCCompletedFoxSemidirect.instInvZCCompletedFoxSemidirect

instance instInvZCCompletedFoxSemidirect : Inv (ZCCompletedFoxSemidirect C X H) where
  inv a :=
    ⟨-(zcGroupLike C H a.right⁻¹ • a.left), a.right⁻¹⟩

Inversion in the completed Fox semidirect product.

Theorem FoxDifferential.ZCCompletedFoxSemidirect.one_left

omit [DecidableEq X] in
@[simp]
theorem one_left :
    (1 : ZCCompletedFoxSemidirect C X H).left = 0

The left component of the identity semidirect element is zero.

Show Lean proof

Theorem FoxDifferential.ZCCompletedFoxSemidirect.one_right

omit [DecidableEq X] in
@[simp]
theorem one_right :
    (1 : ZCCompletedFoxSemidirect C X H).right = 1

The right component of the identity semidirect element is the group identity.

Show Lean proof

Theorem FoxDifferential.ZCCompletedFoxSemidirect.mul_left

omit [DecidableEq X] in
@[simp]
theorem mul_left (a b : ZCCompletedFoxSemidirect C X H) :
    (a * b).left = a.left + zcGroupLike C H a.right • b.left

The left component of semidirect multiplication.

Show Lean proof

Theorem FoxDifferential.ZCCompletedFoxSemidirect.mul_right

omit [DecidableEq X] in
@[simp]
theorem mul_right (a b : ZCCompletedFoxSemidirect C X H) :
    (a * b).right = a.right * b.right

The right component of semidirect multiplication.

Show Lean proof

Theorem FoxDifferential.ZCCompletedFoxSemidirect.inv_left

omit [DecidableEq X] in
@[simp]
theorem inv_left (a : ZCCompletedFoxSemidirect C X H) :
    a⁻¹.left = -(zcGroupLike C H a.right⁻¹ • a.left)

The left component of semidirect inversion.

Show Lean proof

Theorem FoxDifferential.ZCCompletedFoxSemidirect.inv_right

omit [DecidableEq X] in
@[simp]
theorem inv_right (a : ZCCompletedFoxSemidirect C X H) :
    a⁻¹.right = a.right⁻¹

The right component of semidirect inversion.

Show Lean proof

Instance FoxDifferential.ZCCompletedFoxSemidirect.instGroupZCCompletedFoxSemidirect

instance instGroupZCCompletedFoxSemidirect : Group (ZCCompletedFoxSemidirect C X H) where
  one := 1
  mul := (· * ·)
  inv := Inv.inv
  mul_assoc a b c := by
    ext
    · simp only [mul_left, mul_right, map_mul, Pi.add_apply, Pi.smul_apply, smul_eq_mul, add_assoc,
  zcCompletedGroupAlgebraProjection_add, zcCompletedGroupAlgebraProjection_mul,
  zcCompletedGroupAlgebraProjection_groupLike, MonoidAlgebra.of_apply,
  MonoidAlgebra.single_mul_single, mul_one, MonoidAlgebra.coeff_add, smul_add, smul_smul]
    · simp only [mul_right, mul_assoc]
  one_mul a := by
    ext
    · simp only [mul_left, one_left, one_right, map_one, one_smul, Pi.add_apply, Pi.zero_apply,
        zero_add]
    · simp only [mul_right, one_right, one_mul]
  mul_one a := by
    ext
    · simp only [mul_left, 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
    ext
    · simp only [mul_left, inv_left, inv_right, Pi.add_apply, Pi.neg_apply, Pi.smul_apply,
        smul_eq_mul,
  neg_add_cancel, zcCompletedGroupAlgebraProjection_zero, Pi.zero_apply, one_left]
    · simp only [mul_right, inv_right, inv_mul_cancel, one_right]

Group structure on the completed Fox semidirect product.

Definition FoxDifferential.ZCCompletedFoxSemidirect.rightMonoidHom

omit [DecidableEq X] in
def rightMonoidHom : ZCCompletedFoxSemidirect C X H →* H where
  toFun a := a.right
  map_one' := rfl
  map_mul' _ _ := rfl

The right projection from the completed Fox semidirect product to the target group.

Theorem FoxDifferential.ZCCompletedFoxSemidirect.rightMonoidHom_apply

omit [DecidableEq X] in
@[simp]
theorem rightMonoidHom_apply (a : ZCCompletedFoxSemidirect C X H) :
    rightMonoidHom C X H a = a.right

Projection to the right factor of the completed Fox semidirect product returns its stored group element.

Show Lean proof

Definition FoxDifferential.zcCompletedFoxSemidirectLift

def zcCompletedFoxSemidirectLift (ψ : FreeGroup X →* H) :
    FreeGroup X →* ZCCompletedFoxSemidirect C X H :=
  FreeGroup.lift fun x =>
    { left := Pi.single x (1 : ZCCompletedGroupAlgebra C H)
      right := ψ (FreeGroup.of x) }

The completed Fox semidirect lift of a free group homomorphism.

Theorem FoxDifferential.zcCompletedFoxSemidirectLift_right

@[simp]
theorem zcCompletedFoxSemidirectLift_right
    (ψ : FreeGroup X →* H) (w : FreeGroup X) :
    (zcCompletedFoxSemidirectLift C ψ w).right = ψ w

The right component of the completed Fox semidirect lift is ψ.

Show Lean proof

Definition FoxDifferential.zcCompletedFoxSemidirectDerivativeVector

def zcCompletedFoxSemidirectDerivativeVector
    (ψ : FreeGroup X →* H) :
    ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCFreeFoxCoordinates C (X := X) (H := H)) where
  toFun w := (zcCompletedFoxSemidirectLift C ψ w).left
  map_mul' u v := by
    simp only [scalarCrossedAction_apply, map_mul, ZCCompletedFoxSemidirect.mul_left,
      zcCompletedFoxSemidirectLift_right,
      zcCompletedGroupAlgebraScalar_apply]

The left component of the completed Fox semidirect lift.

Theorem FoxDifferential.zcCompletedFoxSemidirectDerivativeVector_of

@[simp]
theorem zcCompletedFoxSemidirectDerivativeVector_of
    (ψ : FreeGroup X →* H) (x : X) :
    zcCompletedFoxSemidirectDerivativeVector C ψ (FreeGroup.of x) =
      Pi.single x (1 : ZCCompletedGroupAlgebra C H)

The completed semidirect derivative vector sends a free generator to the coordinate basis vector.

Show Lean proof

Theorem FoxDifferential.zcCompletedFoxSemidirectDerivativeVector_eq

theorem zcCompletedFoxSemidirectDerivativeVector_eq
    (ψ : FreeGroup X →* H) :
    zcCompletedFoxSemidirectDerivativeVector C ψ =
      zcFreeGroupFoxDerivativeVector C ψ

The completed semidirect derivative vector is the completed free-group Fox derivative vector.

Show Lean proof

Theorem FoxDifferential.zcCompletedFoxSemidirectLift_eq

theorem zcCompletedFoxSemidirectLift_eq
    (ψ : FreeGroup X →* H) (w : FreeGroup X) :
    zcCompletedFoxSemidirectLift C ψ w =
      { left := zcFreeGroupFoxDerivativeVector C ψ w
        right := ψ w }

The completed semidirect lift stores the completed Fox derivative vector and the target homomorphism.

Show Lean proof

Definition FoxDifferential.zcCompletedFoxSemidirectLiftLeftCrossedHom

omit [DecidableEq X] in
def zcCompletedFoxSemidirectLiftLeftCrossedHom
    (ψ : FreeGroup X →* H)
    (φ : FreeGroup X →* ZCCompletedFoxSemidirect C X H)
    (hright : ∀ w : FreeGroup X, (φ w).right = ψ w) :
    ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCFreeFoxCoordinates C (X := X) (H := H)) where
  toFun w := (φ w).left
  map_mul' u v := by
    have h := congrArg ZCCompletedFoxSemidirect.left (map_mul φ u v)
    change (φ (u * v)).left =
      (φ u).left + zcCompletedGroupAlgebraScalar C ψ u • (φ v).left
    rw [h]
    simp only [ZCCompletedFoxSemidirect.mul_left, hright u,
      zcCompletedGroupAlgebraScalar_apply]

The left component of a semidirect homomorphism with prescribed right component, bundled as a completed crossed homomorphism.

Theorem FoxDifferential.zcCompletedFoxSemidirectLift_unique

theorem zcCompletedFoxSemidirectLift_unique
    (ψ : FreeGroup X →* H)
    (φ : FreeGroup X →* ZCCompletedFoxSemidirect C X H)
    (hright : ∀ w : FreeGroup X, (φ w).right = ψ w)
    (hbasis :
      ∀ x : X, (φ (FreeGroup.of x)).left =
        Pi.single x (1 : ZCCompletedGroupAlgebra C H)) :
    φ = zcCompletedFoxSemidirectLift C ψ

Uniqueness of the completed semidirect lift with prescribed right component and generator coordinate values.

Show Lean proof

Theorem FoxDifferential.existsUnique_zcCompletedFoxSemidirectLift

theorem existsUnique_zcCompletedFoxSemidirectLift
    (ψ : FreeGroup X →* H) :
    ∃! φ : FreeGroup X →* ZCCompletedFoxSemidirect C X H,
      (∀ w : FreeGroup X, (φ w).right = ψ w) ∧
        ∀ x : X, (φ (FreeGroup.of x)).left =
          Pi.single x (1 : ZCCompletedGroupAlgebra C H)

Existence and uniqueness theorem for the completed semidirect lift.

Show Lean proof

Theorem FoxDifferential.zcCompletedFoxSemidirectDerivativeVector_foxBoundary

theorem zcCompletedFoxSemidirectDerivativeVector_foxBoundary
    (ψ : FreeGroup X →* H) (w : FreeGroup X) :
    zcFreeGroupFoxBoundary C ψ (zcCompletedFoxSemidirectDerivativeVector C ψ w) =
      zcCompletedGroupAlgebraBoundary C ψ w

Boundary-map form of the completed Fox fundamental formula for the semidirect derivative vector.

Show Lean proof

Theorem FoxDifferential.zcCompletedFoxSemidirectLift_euler_formula

theorem zcCompletedFoxSemidirectLift_euler_formula
    (ψ : FreeGroup X →* H) (w : FreeGroup X) :
    zcGroupLike C H (ψ w) - 1 =
      ∑ i : X,
        (zcCompletedFoxSemidirectLift C ψ w).left i *
          (zcGroupLike C H (ψ (FreeGroup.of i)) - 1)

Completed Fox-Euler formula using the left component of the semidirect lift: [ψ(w)] - 1 = ∑ i, φ(w)_i * ([ψ(x_i)] - 1).

Show Lean proof

Theorem FoxDifferential.zcCompletedFoxSemidirectLift_foxBoundary_of_generatorValues

theorem zcCompletedFoxSemidirectLift_foxBoundary_of_generatorValues
    (ψ : FreeGroup X →* H)
    (φ : FreeGroup X →* ZCCompletedFoxSemidirect C X H)
    (hright : ∀ w : FreeGroup X, (φ w).right = ψ w)
    (hbasis :
      ∀ x : X, (φ (FreeGroup.of x)).left =
        Pi.single x (1 : ZCCompletedGroupAlgebra C H))
    (w : FreeGroup X) :
    zcFreeGroupFoxBoundary C ψ (φ w).left =
      zcCompletedGroupAlgebraBoundary C ψ w

Conditional semidirect Fox boundary formula. Any semidirect lift with right component ψ and standard generator coordinates satisfies the completed Fox boundary formula.

Show Lean proof

Theorem FoxDifferential.zcCompletedFoxSemidirectLift_euler_formula_of_generatorValues

theorem zcCompletedFoxSemidirectLift_euler_formula_of_generatorValues
    (ψ : FreeGroup X →* H)
    (φ : FreeGroup X →* ZCCompletedFoxSemidirect C X H)
    (hright : ∀ w : FreeGroup X, (φ w).right = ψ w)
    (hbasis :
      ∀ x : X, (φ (FreeGroup.of x)).left =
        Pi.single x (1 : ZCCompletedGroupAlgebra C H))
    (w : FreeGroup X) :
    zcGroupLike C H (ψ w) - 1 =
      ∑ i : X,
        (φ w).left i * (zcGroupLike C H (ψ (FreeGroup.of i)) - 1)

Conditional semidirect Fox-Euler formula. The left component of any semidirect lift with right component ψ and standard generator coordinates gives the completed Fox-Euler sum.

Show Lean proof

ProCGroups.FoxDifferential.Completed.Semidirect

Declarations