NYLL
Module

Automorphism.lean

Nyll.ProCGroups.FoxDifferential.Discrete.Jacobian.Automorphism
7 declarations indexed from sourceView source ↗

Module documentation

Fox differential: discrete — jacobian — automorphism

The principal declarations in this module are:

  • freeGroupAutomorphismFoxJacobianMatrixInverse

The named inverse matrix for the Fox Jacobian of a free-group automorphism. For \(J_{\psi}(e)\), the inverse is the Jacobian of the inverse automorphism \(e^{-1}\), with coefficients pushed forward by the composite of \(\psi\) and the monoid homomorphism underlying \(e\).

  • freeGroupAutomorphismFoxJacobian_left_inverse_apply

The Fox Jacobian of a free-group automorphism, multiplied on the left by the Jacobian of its inverse, has Kronecker-delta entries.

  • freeGroupAutomorphismFoxJacobian_right_inverse_apply

The Fox Jacobian of a free-group automorphism, multiplied on the right by the Jacobian of its inverse, has Kronecker-delta entries.

  • freeGroupAutomorphismFoxJacobianMatrix_left_inverse

The Jacobian matrix of a free-group automorphism has the expected left inverse.

Imports1
Imported by1

Declarations

theorem

freeGroupAutomorphismFoxJacobian_left_inverse_apply

L44 ↗
FoxDifferential.FoxCalculus.freeGroupAutomorphismFoxJacobian_left_inverse_apply
Documentation

The Fox Jacobian of a free-group automorphism, multiplied on the left by the Jacobian of its inverse, has Kronecker-delta entries.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v w z t
variable {H : Type w} [Group H]
variable {X : Type u} {Y : Type v}
Lean source · statement
theorem freeGroupAutomorphismFoxJacobian_left_inverse_apply
    [DecidableEq X] [Fintype X]
    (ψ : FreeGroup X →* H) (e : FreeGroup X ≃* FreeGroup X)
    (x z : X) :
    (∑ y : X,
        freeGroupHomFoxJacobian (H := H) (ψ.comp e.toMonoidHom)
          e.symm.toMonoidHom x y *
          freeGroupHomFoxJacobian (H := H) ψ e.toMonoidHom y z) =
      (Pi.single x (1 : GroupRing H) : X → GroupRing H) z
theorem

freeGroupAutomorphismFoxJacobian_right_inverse_apply

L68 ↗
FoxDifferential.FoxCalculus.freeGroupAutomorphismFoxJacobian_right_inverse_apply
Documentation

The Fox Jacobian of a free-group automorphism, multiplied on the right by the Jacobian of its inverse, has Kronecker-delta entries.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v w z t
variable {H : Type w} [Group H]
variable {X : Type u} {Y : Type v}
Lean source · statement
theorem freeGroupAutomorphismFoxJacobian_right_inverse_apply
    [DecidableEq X] [Fintype X]
    (ψ : FreeGroup X →* H) (e : FreeGroup X ≃* FreeGroup X)
    (x z : X) :
    (∑ y : X,
        freeGroupHomFoxJacobian (H := H) (ψ.comp e.symm.toMonoidHom)
          e.toMonoidHom x y *
          freeGroupHomFoxJacobian (H := H) ψ e.symm.toMonoidHom y z) =
      (Pi.single x (1 : GroupRing H) : X → GroupRing H) z
theorem

freeGroupAutomorphismFoxJacobianMatrix_left_inverse

L89 ↗
FoxDifferential.FoxCalculus.freeGroupAutomorphismFoxJacobianMatrix_left_inverse
Documentation

The Jacobian matrix of a free-group automorphism has the expected left inverse.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v w z t
variable {H : Type w} [Group H]
variable {X : Type u} {Y : Type v}
Lean source · statement
theorem freeGroupAutomorphismFoxJacobianMatrix_left_inverse
    [DecidableEq X] [Fintype X]
    (ψ : FreeGroup X →* H) (e : FreeGroup X ≃* FreeGroup X) :
    freeGroupHomFoxJacobianMatrix (H := H) (ψ.comp e.toMonoidHom)
        e.symm.toMonoidHom *
      freeGroupHomFoxJacobianMatrix (H := H) ψ e.toMonoidHom =
      (1 : Matrix X X (GroupRing H))
theorem

freeGroupAutomorphismFoxJacobianMatrix_right_inverse

L117 ↗
FoxDifferential.FoxCalculus.freeGroupAutomorphismFoxJacobianMatrix_right_inverse
Documentation

The Jacobian matrix of a free-group automorphism has the expected right inverse.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v w z t
variable {H : Type w} [Group H]
variable {X : Type u} {Y : Type v}
Lean source · statement
theorem freeGroupAutomorphismFoxJacobianMatrix_right_inverse
    [DecidableEq X] [Fintype X]
    (ψ : FreeGroup X →* H) (e : FreeGroup X ≃* FreeGroup X) :
    freeGroupHomFoxJacobianMatrix (H := H) (ψ.comp e.symm.toMonoidHom)
        e.toMonoidHom *
      freeGroupHomFoxJacobianMatrix (H := H) ψ e.symm.toMonoidHom =
      (1 : Matrix X X (GroupRing H))
def

freeGroupAutomorphismFoxJacobianMatrixInverse

L149 ↗
FoxDifferential.FoxCalculus.freeGroupAutomorphismFoxJacobianMatrixInverse
Documentation

The named inverse matrix for the Fox Jacobian of a free-group automorphism. For \(J_{\psi}(e)\), the inverse is the Jacobian of the inverse automorphism \(e^{-1}\), with coefficients pushed forward by the composite of \(\psi\) and the monoid homomorphism underlying \(e\).

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v w z t
variable {H : Type w} [Group H]
variable {X : Type u} {Y : Type v}
Lean source · statement
def freeGroupAutomorphismFoxJacobianMatrixInverse
    [DecidableEq X]
    (ψ : FreeGroup X →* H) (e : FreeGroup X ≃* FreeGroup X) :
    Matrix X X (GroupRing H)
theorem

freeGroupAutomorphismFoxJacobianMatrixInverse_mul

L156 ↗
FoxDifferential.FoxCalculus.freeGroupAutomorphismFoxJacobianMatrixInverse_mul
Documentation

The named inverse matrix is a left inverse for the Fox Jacobian of a free-group automorphism.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v w z t
variable {H : Type w} [Group H]
variable {X : Type u} {Y : Type v}
Lean source · statement
theorem freeGroupAutomorphismFoxJacobianMatrixInverse_mul
    [DecidableEq X] [Fintype X]
    (ψ : FreeGroup X →* H) (e : FreeGroup X ≃* FreeGroup X) :
    freeGroupAutomorphismFoxJacobianMatrixInverse (H := H) ψ e *
        freeGroupHomFoxJacobianMatrix (H := H) ψ e.toMonoidHom =
      (1 : Matrix X X (GroupRing H))
theorem

freeGroupAutomorphismFoxJacobianMatrix_mul_inverse

L168 ↗
FoxDifferential.FoxCalculus.freeGroupAutomorphismFoxJacobianMatrix_mul_inverse
Documentation

The named inverse matrix is a right inverse for the Fox Jacobian of a free-group automorphism.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
namespace FoxCalculus
open scoped BigOperators
universe u v w z t
variable {H : Type w} [Group H]
variable {X : Type u} {Y : Type v}
Lean source · statement
theorem freeGroupAutomorphismFoxJacobianMatrix_mul_inverse
    [DecidableEq X] [Fintype X]
    (ψ : FreeGroup X →* H) (e : FreeGroup X ≃* FreeGroup X) :
    freeGroupHomFoxJacobianMatrix (H := H) ψ e.toMonoidHom *
        freeGroupAutomorphismFoxJacobianMatrixInverse (H := H) ψ e =
      (1 : Matrix X X (GroupRing H))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.