Module

Semidirect.lean

Nyll.ProCGroups.FoxDifferential.Completed.Semidirect

27 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — semidirect

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.

Imports2

Imported by2

structure

ZCCompletedFoxSemidirect

L39 ↗

FoxDifferential.ZCCompletedFoxSemidirect

Documentation

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

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [DecidableEq X] in

Lean source · full declaration

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

theorem

ext

L50 ↗

FoxDifferential.ZCCompletedFoxSemidirect.ext

Documentation

Extensionality for completed Fox semidirect elements.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
namespace ZCCompletedFoxSemidirect
omit [DecidableEq X] in

Lean source · statement

theorem ext {a b : ZCCompletedFoxSemidirect C X H}
    (hleft : a.left = b.left) (hright : a.right = b.right) : a = b

instance

instOneZCCompletedFoxSemidirect

L57 ↗

FoxDifferential.ZCCompletedFoxSemidirect.instOneZCCompletedFoxSemidirect

Documentation

Identity element of the completed Fox semidirect product.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
namespace ZCCompletedFoxSemidirect

Lean source · full declaration

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

instance

instMulZCCompletedFoxSemidirect

L61 ↗

FoxDifferential.ZCCompletedFoxSemidirect.instMulZCCompletedFoxSemidirect

Documentation

Multiplication in the completed Fox semidirect product.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
namespace ZCCompletedFoxSemidirect

Lean source · full declaration

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

instance

instInvZCCompletedFoxSemidirect

L66 ↗

FoxDifferential.ZCCompletedFoxSemidirect.instInvZCCompletedFoxSemidirect

Documentation

Inversion in the completed Fox semidirect product.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
namespace ZCCompletedFoxSemidirect

Lean source · full declaration

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

theorem

one_left

L73 ↗

FoxDifferential.ZCCompletedFoxSemidirect.one_left

Documentation

The left component of the identity semidirect element is zero.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
namespace ZCCompletedFoxSemidirect
omit [DecidableEq X] in

Lean source · statement

theorem one_left :
    (1 : ZCCompletedFoxSemidirect C X H).left = 0

theorem

one_right

L80 ↗

FoxDifferential.ZCCompletedFoxSemidirect.one_right

Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
namespace ZCCompletedFoxSemidirect
omit [DecidableEq X] in

Lean source · statement

theorem one_right :
    (1 : ZCCompletedFoxSemidirect C X H).right = 1

theorem

mul_left

L87 ↗

FoxDifferential.ZCCompletedFoxSemidirect.mul_left

Documentation

The left component of semidirect multiplication.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
namespace ZCCompletedFoxSemidirect
omit [DecidableEq X] in

Lean source · statement

theorem mul_left (a b : ZCCompletedFoxSemidirect C X H) :
    (a * b).left = a.left + zcGroupLike C H a.right • b.left

theorem

mul_right

L94 ↗

FoxDifferential.ZCCompletedFoxSemidirect.mul_right

Documentation

The right component of semidirect multiplication.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
namespace ZCCompletedFoxSemidirect
omit [DecidableEq X] in

Lean source · statement

theorem mul_right (a b : ZCCompletedFoxSemidirect C X H) :
    (a * b).right = a.right * b.right

theorem

inv_left

L101 ↗

FoxDifferential.ZCCompletedFoxSemidirect.inv_left

Documentation

The left component of semidirect inversion.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
namespace ZCCompletedFoxSemidirect
omit [DecidableEq X] in

Lean source · statement

theorem inv_left (a : ZCCompletedFoxSemidirect C X H) :
    a⁻¹.left = -(zcGroupLike C H a.right⁻¹ • a.left)

theorem

inv_right

L108 ↗

FoxDifferential.ZCCompletedFoxSemidirect.inv_right

Documentation

The right component of semidirect inversion.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
namespace ZCCompletedFoxSemidirect
omit [DecidableEq X] in

Lean source · statement

theorem inv_right (a : ZCCompletedFoxSemidirect C X H) :
    a⁻¹.right = a.right⁻¹

instance

instGroupZCCompletedFoxSemidirect

L113 ↗

FoxDifferential.ZCCompletedFoxSemidirect.instGroupZCCompletedFoxSemidirect

Documentation

Group structure on the completed Fox semidirect product.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
namespace ZCCompletedFoxSemidirect

Lean source · full declaration

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.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]

def

rightMonoidHom

L141 ↗

FoxDifferential.ZCCompletedFoxSemidirect.rightMonoidHom

Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
namespace ZCCompletedFoxSemidirect
omit [DecidableEq X] in

Lean source · full declaration

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

theorem

rightMonoidHom_apply

L150 ↗

FoxDifferential.ZCCompletedFoxSemidirect.rightMonoidHom_apply

Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
namespace ZCCompletedFoxSemidirect
omit [DecidableEq X] in

Lean source · statement

theorem rightMonoidHom_apply (a : ZCCompletedFoxSemidirect C X H) :
    rightMonoidHom C X H a = a.right

def

zcCompletedFoxSemidirectLift

L161 ↗

FoxDifferential.zcCompletedFoxSemidirectLift

Documentation

The completed Fox semidirect lift of a free group homomorphism.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section Lift
variable {X H}

Lean source · statement

def zcCompletedFoxSemidirectLift (ψ : FreeGroup X →* H) :
    FreeGroup X →* ZCCompletedFoxSemidirect C X H

theorem

zcCompletedFoxSemidirectLift_right

L169 ↗

FoxDifferential.zcCompletedFoxSemidirectLift_right

Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section Lift
variable {X H}

Lean source · statement

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

def

zcCompletedFoxSemidirectDerivativeVector

L183 ↗

FoxDifferential.zcCompletedFoxSemidirectDerivativeVector

Documentation

The left component of the completed Fox semidirect lift.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section Lift
variable {X H}

Lean source · full declaration

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]

theorem

zcCompletedFoxSemidirectDerivativeVector_of

L196 ↗

FoxDifferential.zcCompletedFoxSemidirectDerivativeVector_of

Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section Lift
variable {X H}

Lean source · statement

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

theorem

zcCompletedFoxSemidirectDerivativeVector_eq

L206 ↗

FoxDifferential.zcCompletedFoxSemidirectDerivativeVector_eq

Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section Lift
variable {X H}

Lean source · statement

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

theorem

zcCompletedFoxSemidirectLift_eq

L216 ↗

FoxDifferential.zcCompletedFoxSemidirectLift_eq

Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section Lift
variable {X H}

Lean source · statement

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

def

zcCompletedFoxSemidirectLiftLeftCrossedHom

L229 ↗

FoxDifferential.zcCompletedFoxSemidirectLiftLeftCrossedHom

Documentation

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

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section Lift
variable {X H}
omit [DecidableEq X] in

Lean source · full declaration

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]

theorem

zcCompletedFoxSemidirectLift_unique

L246 ↗

FoxDifferential.zcCompletedFoxSemidirectLift_unique

Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section Lift
variable {X H}

Lean source · statement

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 ψ

theorem

existsUnique_zcCompletedFoxSemidirectLift

L266 ↗

FoxDifferential.existsUnique_zcCompletedFoxSemidirectLift

Documentation

Existence and uniqueness theorem for the completed semidirect lift.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section Lift
variable {X H}

Lean source · statement

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)

theorem

zcCompletedFoxSemidirectDerivativeVector_foxBoundary

L284 ↗

FoxDifferential.zcCompletedFoxSemidirectDerivativeVector_foxBoundary

Documentation

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

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section Lift
variable {X H}
section FiniteBasis
variable [Fintype X]

Lean source · statement

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

theorem

zcCompletedFoxSemidirectLift_euler_formula

L294 ↗

FoxDifferential.zcCompletedFoxSemidirectLift_euler_formula

Documentation

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

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section Lift
variable {X H}
section FiniteBasis
variable [Fintype X]

Lean source · statement

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)

theorem

zcCompletedFoxSemidirectLift_foxBoundary_of_generatorValues

L306 ↗

FoxDifferential.zcCompletedFoxSemidirectLift_foxBoundary_of_generatorValues

Documentation

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

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section Lift
variable {X H}
section FiniteBasis
variable [Fintype X]

Lean source · statement

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

theorem

zcCompletedFoxSemidirectLift_euler_formula_of_generatorValues

L322 ↗

FoxDifferential.zcCompletedFoxSemidirectLift_euler_formula_of_generatorValues

Documentation

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.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section Lift
variable {X H}
section FiniteBasis
variable [Fintype X]

Lean source · statement

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)

Module documentation

Fox differential: completed — semidirect

Declarations