Module

Semidirect.lean

Nyll.ProCGroups.FoxDifferential.RightDerivative.Semidirect

14 declarations indexed from sourceView source ↗

Module documentation

Fox differential: right derivative — semidirect

The principal declarations in this module are:

RightFoxSemidirect

The right Fox semidirect product records a group element together with its right-derivative coordinate.

rightHom

The right Fox semidirect construction defines a homomorphism from a right derivation.

ext

The Fox semidirect construction has the stated component formula.

one_left

The additive component of the identity semidirect element is zero.

Imports1

Nyll.ProCGroups.FoxDifferential.Discrete.GroupRing

Imported by1

Nyll.ProCGroups.FoxDifferential.RightDerivative.All

structure

RightFoxSemidirect

L33 ↗

FoxDifferential.RightFoxSemidirect

Documentation

The right Fox semidirect product records a group element together with its right-derivative coordinate.

Source context 2 commands

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

namespace FoxDifferential
noncomputable section

Lean source · full declaration

structure RightFoxSemidirect (G : Type*) [Group G] where
  /-- The group-ring coordinate, representing the right Fox derivative. -/
  left : FoxDifferential.GroupRing G
  /-- The underlying group element. -/
  right : G

theorem

ext

L45 ↗

FoxDifferential.RightFoxSemidirect.ext

Documentation

The Fox semidirect construction has the stated component formula.

Source context 4 commands

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

namespace FoxDifferential
noncomputable section
namespace RightFoxSemidirect
variable {G : Type*} [Group G]

Lean source · statement

theorem ext {x y : RightFoxSemidirect G}
    (hleft : x.left = y.left) (hright : x.right = y.right) : x = y

instance

instOneRightFoxSemidirect

L52 ↗

FoxDifferential.RightFoxSemidirect.instOneRightFoxSemidirect

Documentation

The unit of the right Fox semidirect product is the pair of identity components.

Source context 4 commands

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

namespace FoxDifferential
noncomputable section
namespace RightFoxSemidirect
variable {G : Type*} [Group G]

Lean source · full declaration

instance instOneRightFoxSemidirect : One (RightFoxSemidirect G) where
  one := ⟨0, 1⟩

instance

instMulRightFoxSemidirect

L59 ↗

FoxDifferential.RightFoxSemidirect.instMulRightFoxSemidirect

Documentation

Multiplication in the right Fox semidirect product is given by the right action and group multiplication.

Source context 4 commands

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

namespace FoxDifferential
noncomputable section
namespace RightFoxSemidirect
variable {G : Type*} [Group G]

Lean source · full declaration

instance instMulRightFoxSemidirect : Mul (RightFoxSemidirect G) where
  mul x y :=
    ⟨x.left * MonoidAlgebra.of ℤ G y.right + y.left, x.right * y.right⟩

instance

instInvRightFoxSemidirect

L67 ↗

FoxDifferential.RightFoxSemidirect.instInvRightFoxSemidirect

Documentation

Inversion in the right Fox semidirect product is computed from the right action and the inverse in the base group.

Source context 4 commands

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

namespace FoxDifferential
noncomputable section
namespace RightFoxSemidirect
variable {G : Type*} [Group G]

Lean source · full declaration

instance instInvRightFoxSemidirect : Inv (RightFoxSemidirect G) where
  inv x :=
    ⟨-x.left * MonoidAlgebra.of ℤ G x.right⁻¹, x.right⁻¹⟩

theorem

one_left

L73 ↗

FoxDifferential.RightFoxSemidirect.one_left

Documentation

The additive component of the identity semidirect element is zero.

Source context 4 commands

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

namespace FoxDifferential
noncomputable section
namespace RightFoxSemidirect
variable {G : Type*} [Group G]

Lean source · statement

theorem one_left : (1 : RightFoxSemidirect G).left = 0

theorem

one_right

L78 ↗

FoxDifferential.RightFoxSemidirect.one_right

Documentation

The free-group component of the identity semidirect element is the identity word.

Source context 4 commands

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

namespace FoxDifferential
noncomputable section
namespace RightFoxSemidirect
variable {G : Type*} [Group G]

Lean source · statement

theorem one_right : (1 : RightFoxSemidirect G).right = 1

theorem

mul_left

L83 ↗

FoxDifferential.RightFoxSemidirect.mul_left

Documentation

The left component of semidirect multiplication is computed by the Fox product rule.

Source context 4 commands

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

namespace FoxDifferential
noncomputable section
namespace RightFoxSemidirect
variable {G : Type*} [Group G]

Lean source · statement

theorem mul_left (x y : RightFoxSemidirect G) :
    (x * y).left = x.left * MonoidAlgebra.of ℤ G y.right + y.left

theorem

mul_right

L89 ↗

FoxDifferential.RightFoxSemidirect.mul_right

Documentation

The right component of semidirect multiplication is the product of right components.

Source context 4 commands

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

namespace FoxDifferential
noncomputable section
namespace RightFoxSemidirect
variable {G : Type*} [Group G]

Lean source · statement

theorem mul_right (x y : RightFoxSemidirect G) :
    (x * y).right = x.right * y.right

theorem

inv_left

L95 ↗

FoxDifferential.RightFoxSemidirect.inv_left

Documentation

The left component of the semidirect inverse is computed by the Fox inverse formula.

Source context 4 commands

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

namespace FoxDifferential
noncomputable section
namespace RightFoxSemidirect
variable {G : Type*} [Group G]

Lean source · statement

theorem inv_left (x : RightFoxSemidirect G) :
    x⁻¹.left = -x.left * MonoidAlgebra.of ℤ G x.right⁻¹

theorem

inv_right

L101 ↗

FoxDifferential.RightFoxSemidirect.inv_right

Documentation

The right component of the semidirect inverse is the inverse of the right component.

Source context 4 commands

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

namespace FoxDifferential
noncomputable section
namespace RightFoxSemidirect
variable {G : Type*} [Group G]

Lean source · statement

theorem inv_right (x : RightFoxSemidirect G) :
    x⁻¹.right = x.right⁻¹

instance

instGroupRightFoxSemidirect

L106 ↗

FoxDifferential.RightFoxSemidirect.instGroupRightFoxSemidirect

Documentation

The right Fox semidirect product carries the group structure induced by its right action.

Source context 4 commands

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

namespace FoxDifferential
noncomputable section
namespace RightFoxSemidirect
variable {G : Type*} [Group G]

Lean source · full declaration

instance instGroupRightFoxSemidirect : Group (RightFoxSemidirect G) where
  one := 1
  mul := (· * ·)
  inv := Inv.inv
  mul_assoc x y z := by
    apply RightFoxSemidirect.ext
    · simp only [mul_left, mul_right, map_mul, add_mul, mul_assoc, add_assoc]
    · simp only [mul_right, mul_assoc]
  one_mul x := by
    apply RightFoxSemidirect.ext
    · simp only [mul_left, one_left, MonoidAlgebra.of_apply, zero_mul, zero_add]
    · simp only [mul_right, one_right, one_mul]
  mul_one x := by
    apply RightFoxSemidirect.ext
    · simp only [mul_left, one_right, map_one, one_left, add_zero, mul_one]
    · simp only [mul_right, one_right, mul_one]
  inv_mul_cancel x := by
    apply RightFoxSemidirect.ext
    · simp only [mul_left, inv_left]
      rw [mul_assoc, ← map_mul, inv_mul_cancel, map_one, mul_one,
        neg_add_cancel, one_left]
    · simp only [mul_right, inv_right, inv_mul_cancel, one_right]

def

rightHom

L130 ↗

FoxDifferential.RightFoxSemidirect.rightHom

Documentation

The right Fox semidirect construction defines a homomorphism from a right derivation.

Source context 4 commands

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

namespace FoxDifferential
noncomputable section
namespace RightFoxSemidirect
variable {G : Type*} [Group G]

Lean source · full declaration

def rightHom : RightFoxSemidirect G →* G where
  toFun x := x.right
  map_one' := rfl
  map_mul' _ _ := rfl

theorem

rightHom_apply

L137 ↗

FoxDifferential.RightFoxSemidirect.rightHom_apply

Documentation

The right projection homomorphism of a Fox semidirect product returns its right coordinate.

Source context 4 commands

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

namespace FoxDifferential
noncomputable section
namespace RightFoxSemidirect
variable {G : Type*} [Group G]

Lean source · statement

theorem rightHom_apply (x : RightFoxSemidirect G) :
    rightHom x = x.right

Module documentation

Fox differential: right derivative — semidirect

Declarations