Module

Semidirect.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.Stage.Semidirect

21 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — finite stage — stage — semidirect

The principal declarations in this module are:

foxAlgebraicStageTargetQuotient

The finite-stage target quotient \(F/N\).

foxAlgebraicStageTargetGroupAlgebra

The finite-stage target group algebra \((\mathbb{Z}/n\mathbb{Z})[F/N]\).

mem_foxAlgebraicStageGroupAlgebraMapKernelIdeal

Membership test for the finite-stage group-algebra map kernel ideal.

mem_foxAlgebraicStageSourceAugmentationIdeal

Membership in the finite-stage source augmentation ideal is equivalent to vanishing under the finite-stage source augmentation map.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.Basic

Imported by2

abbrev

foxAlgebraicStageTargetQuotient

L43 ↗

FoxDifferential.foxAlgebraicStageTargetQuotient

Documentation

The finite-stage target quotient \(F/N\).

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

abbrev foxAlgebraicStageTargetQuotient : Type u

abbrev

foxAlgebraicStageTargetGroupAlgebra

L47 ↗

FoxDifferential.foxAlgebraicStageTargetGroupAlgebra

Documentation

The finite-stage target group algebra \((\mathbb{Z}/n\mathbb{Z})[F/N]\).

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

abbrev foxAlgebraicStageTargetGroupAlgebra : Type u

abbrev

foxAlgebraicStageSourceGroupAlgebra

L51 ↗

FoxDifferential.foxAlgebraicStageSourceGroupAlgebra

Documentation

The finite-stage source group algebra \((\mathbb{Z}/n\mathbb{Z})[F/[N,N]N^n]\).

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

abbrev foxAlgebraicStageSourceGroupAlgebra : Type u

def

foxAlgebraicStageGroupAlgebraMapKernelIdeal

L59 ↗

FoxDifferential.foxAlgebraicStageGroupAlgebraMapKernelIdeal

Documentation

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

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

def foxAlgebraicStageGroupAlgebraMapKernelIdeal :
    Ideal (foxAlgebraicStageSourceGroupAlgebra (X := X) N n)

theorem

mem_foxAlgebraicStageGroupAlgebraMapKernelIdeal

L66 ↗

FoxDifferential.mem_foxAlgebraicStageGroupAlgebraMapKernelIdeal

Documentation

Membership test for the finite-stage group-algebra map kernel ideal.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [DecidableEq X] in

Lean source · statement

theorem mem_foxAlgebraicStageGroupAlgebraMapKernelIdeal
    {N : Subgroup (FreeGroup X)} [N.Normal] {n : ℕ}
    {x : foxAlgebraicStageSourceGroupAlgebra (X := X) N n} :
    x ∈ foxAlgebraicStageGroupAlgebraMapKernelIdeal (X := X) N n ↔
      foxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n x = 0

def

foxAlgebraicStageSourceAugmentationIdeal

L77 ↗

FoxDifferential.foxAlgebraicStageSourceAugmentationIdeal

Documentation

The finite-stage source augmentation ideal is the kernel of the corresponding finite-stage augmentation map.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

def foxAlgebraicStageSourceAugmentationIdeal :
    Ideal (foxAlgebraicStageSourceGroupAlgebra (X := X) N n)

theorem

mem_foxAlgebraicStageSourceAugmentationIdeal

L89 ↗

FoxDifferential.mem_foxAlgebraicStageSourceAugmentationIdeal

Documentation

Membership in the finite-stage source augmentation ideal is equivalent to vanishing under the finite-stage source augmentation map.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [DecidableEq X] in

Lean source · statement

theorem mem_foxAlgebraicStageSourceAugmentationIdeal
    {N : Subgroup (FreeGroup X)} {n : ℕ}
    {x : foxAlgebraicStageSourceGroupAlgebra (X := X) N n} :
    x ∈ foxAlgebraicStageSourceAugmentationIdeal (X := X) N n ↔
      foxCommutatorPowerSourceGroupAlgebraAugmentation
        (F := FreeGroup X) N n x = 0

def

foxAlgebraicStageGroupAlgebraMapKernelMulAugmentationIdeal

L98 ↗

FoxDifferential.foxAlgebraicStageGroupAlgebraMapKernelMulAugmentationIdeal

Documentation

The finite-stage product ideal \(K_j I_j\) governing the Fox kernel criterion.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

def foxAlgebraicStageGroupAlgebraMapKernelMulAugmentationIdeal :
    Ideal (foxAlgebraicStageSourceGroupAlgebra (X := X) N n)

abbrev

foxAlgebraicStageCoordinateVector

L104 ↗

FoxDifferential.foxAlgebraicStageCoordinateVector

Documentation

Coordinate vectors for finite-stage Fox derivatives.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

abbrev foxAlgebraicStageCoordinateVector : Type u

structure

FoxAlgebraicStageSemidirect

L111 ↗

FoxDifferential.FoxAlgebraicStageSemidirect

Documentation

Finite-stage Fox semidirect target \(A^X \rtimes F/N\), whose left component stores the derivative vector and whose right component stores the quotient word.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · full declaration

structure FoxAlgebraicStageSemidirect where
  /-- The vector of finite-stage Fox-derivative coordinates. -/
  left : foxAlgebraicStageCoordinateVector (X := X) N n
  /-- The element of the finite-stage target quotient. -/
  right : foxAlgebraicStageTargetQuotient (X := X) N

theorem

ext

L122 ↗

FoxDifferential.FoxAlgebraicStageSemidirect.ext

Documentation

Extensionality for algebraic-stage semidirect elements.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
namespace FoxAlgebraicStageSemidirect
omit [DecidableEq X] [N.Normal] in

Lean source · statement

theorem ext
    {a b : FoxAlgebraicStageSemidirect (X := X) N n}
    (hleft : a.left = b.left) (hright : a.right = b.right) : a = b

instance

instOneFoxAlgebraicStageSemidirect

L130 ↗

FoxDifferential.FoxAlgebraicStageSemidirect.instOneFoxAlgebraicStageSemidirect

Documentation

The identity element of the finite-stage Fox semidirect product is \((0,1)\).

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
namespace FoxAlgebraicStageSemidirect

Lean source · full declaration

instance instOneFoxAlgebraicStageSemidirect : One (FoxAlgebraicStageSemidirect (X := X) N n) where
  one := ⟨0, 1⟩

instance

instMulFoxAlgebraicStageSemidirect

L137 ↗

FoxDifferential.FoxAlgebraicStageSemidirect.instMulFoxAlgebraicStageSemidirect

Documentation

Multiplication in a finite Fox-stage semidirect product is defined by the finite-stage coefficient action and quotient-group multiplication.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
namespace FoxAlgebraicStageSemidirect

Lean source · full declaration

instance instMulFoxAlgebraicStageSemidirect : Mul (FoxAlgebraicStageSemidirect (X := X) N n) where
  mul a b :=
    ⟨a.left +
        (MonoidAlgebra.of (ModNCompletedCoeff n)
          (foxAlgebraicStageTargetQuotient (X := X) N) a.right) • b.left,
      a.right * b.right⟩

instance

instInvFoxAlgebraicStageSemidirect

L145 ↗

FoxDifferential.FoxAlgebraicStageSemidirect.instInvFoxAlgebraicStageSemidirect

Documentation

Inversion in the finite-stage Fox semidirect product.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
namespace FoxAlgebraicStageSemidirect

Lean source · full declaration

instance instInvFoxAlgebraicStageSemidirect : Inv (FoxAlgebraicStageSemidirect (X := X) N n) where
  inv a :=
    ⟨-((MonoidAlgebra.of (ModNCompletedCoeff n)
        (foxAlgebraicStageTargetQuotient (X := X) N) a.right⁻¹) • a.left),
      a.right⁻¹⟩

theorem

one_left

L154 ↗

FoxDifferential.FoxAlgebraicStageSemidirect.one_left

Documentation

The left component of the algebraic-stage semidirect identity is zero.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
namespace FoxAlgebraicStageSemidirect
omit [DecidableEq X] in

Lean source · statement

theorem one_left :
    (1 : FoxAlgebraicStageSemidirect (X := X) N n).left = 0

theorem

one_right

L160 ↗

FoxDifferential.FoxAlgebraicStageSemidirect.one_right

Documentation

The right component of the algebraic-stage semidirect identity is the group identity.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
namespace FoxAlgebraicStageSemidirect
omit [DecidableEq X] in

Lean source · statement

theorem one_right :
    (1 : FoxAlgebraicStageSemidirect (X := X) N n).right = 1

theorem

mul_left

L166 ↗

FoxDifferential.FoxAlgebraicStageSemidirect.mul_left

Documentation

Left-component formula for multiplication in the algebraic-stage semidirect product.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
namespace FoxAlgebraicStageSemidirect
omit [DecidableEq X] in

Lean source · statement

theorem mul_left
    (a b : FoxAlgebraicStageSemidirect (X := X) N n) :
    (a * b).left =
      a.left +
        (MonoidAlgebra.of (ModNCompletedCoeff n)
          (foxAlgebraicStageTargetQuotient (X := X) N) a.right) • b.left

theorem

mul_right

L176 ↗

FoxDifferential.FoxAlgebraicStageSemidirect.mul_right

Documentation

Right-component formula for multiplication in the algebraic-stage semidirect product.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
namespace FoxAlgebraicStageSemidirect
omit [DecidableEq X] in

Lean source · statement

theorem mul_right
    (a b : FoxAlgebraicStageSemidirect (X := X) N n) :
    (a * b).right = a.right * b.right

theorem

inv_left

L183 ↗

FoxDifferential.FoxAlgebraicStageSemidirect.inv_left

Documentation

Left-component formula for inversion in the algebraic-stage semidirect product.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
namespace FoxAlgebraicStageSemidirect
omit [DecidableEq X] in

Lean source · statement

theorem inv_left
    (a : FoxAlgebraicStageSemidirect (X := X) N n) :
    a⁻¹.left =
      -((MonoidAlgebra.of (ModNCompletedCoeff n)
        (foxAlgebraicStageTargetQuotient (X := X) N) a.right⁻¹) • a.left)

theorem

inv_right

L192 ↗

FoxDifferential.FoxAlgebraicStageSemidirect.inv_right

Documentation

Right-component formula for inversion in the algebraic-stage semidirect product.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
namespace FoxAlgebraicStageSemidirect
omit [DecidableEq X] in

Lean source · statement

theorem inv_right
    (a : FoxAlgebraicStageSemidirect (X := X) N n) :
    a⁻¹.right = a.right⁻¹

instance

instGroupFoxAlgebraicStageSemidirect

L197 ↗

FoxDifferential.FoxAlgebraicStageSemidirect.instGroupFoxAlgebraicStageSemidirect

Documentation

Group structure on the finite-stage Fox semidirect product.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
namespace FoxAlgebraicStageSemidirect

Lean source · full declaration

instance instGroupFoxAlgebraicStageSemidirect : Group (FoxAlgebraicStageSemidirect (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)
            (foxAlgebraicStageTargetQuotient (X := X) N) 1 :
              foxAlgebraicStageTargetGroupAlgebra (X := X) N n) = 1 := by
        exact map_one
          (MonoidAlgebra.of (ModNCompletedCoeff n)
            (foxAlgebraicStageTargetQuotient (X := X) N))
      rw [hone, one_smul]
    · simp only [mul_right, one_right, one_mul]
  mul_one a := by
    apply ext
    · funext i
      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
    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]

Module documentation

Fox differential: completed — finite stage — stage — semidirect

Declarations