ProCGroups.FoxDifferential.Completed.Continuous.Automorphism

9 Theorems | 4 Definitions

The principal declarations in this module are:

allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse The named inverse linear map for the completed Fox-Jacobian of a continuous automorphism. - allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse The named inverse matrix for the completed Fox-Jacobian of a continuous automorphism. - allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverseStage_apply Evaluation of the finite-stage inverse matrix for a completed Fox-Jacobian of a continuous automorphism. - allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse_eq_vecMul The named inverse linear map is row-vector multiplication by the named inverse matrix.

import

ProCGroups.FoxDifferential.Completed.Continuous.ChainRule.Iterated

Imported by

ProCGroups.FoxDifferential.Completed.Continuous

Definition FoxDifferential.allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse

def allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) ι)
    (e : F ≃* F) (φ : X → H) :
    ZCFreeFoxCoordinates ProCGroups.FiniteGroupClass.allFinite (X := X) (H := H)
        →ₗ[ZCCompletedGroupAlgebra ProCGroups.FiniteGroupClass.allFinite H]
      ZCFreeFoxCoordinates ProCGroups.FiniteGroupClass.allFinite (X := X) (H := H) :=
  allFinite_freeProCZCCompletedFoxJacobianLinearMap
    (X := X) (Y := X) (F := F) (F' := F) hι e.symm.toMonoidHom
    (allFinite_freeProCZCCompletedFoxPullbackGenerator
      (X := X) (F := F) hι e.toMonoidHom φ ι)
    ι

The named inverse linear map for the completed Fox-Jacobian of a continuous automorphism.

Definition FoxDifferential.allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse

def allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) ι)
    (e : F ≃* F) (φ : X → H) :
    Matrix X X (ZCCompletedGroupAlgebra ProCGroups.FiniteGroupClass.allFinite H) :=
  allFinite_freeProCZCCompletedFoxJacobianMatrix
    (X := X) (Y := X) (F := F) (F' := F) hι e.symm.toMonoidHom
    (allFinite_freeProCZCCompletedFoxPullbackGenerator
      (X := X) (F := F) hι e.toMonoidHom φ ι)
    ι

The named inverse matrix for the completed Fox-Jacobian of a continuous automorphism.

Definition FoxDifferential.allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverseStage

def allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverseStage
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) ι)
    (e : F ≃* F) (φ : X → H)
    (j : ZCCompletedGroupAlgebraIndex ProCGroups.FiniteGroupClass.allFinite H) :
    Matrix X X (ZCCompletedGroupAlgebraStage ProCGroups.FiniteGroupClass.allFinite H j) :=
  fun x y =>
    zcCompletedGroupAlgebraProjection ProCGroups.FiniteGroupClass.allFinite H j
      (allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse
        (X := X) (F := F) (H := H) hι e φ x y)

A finite-stage projection of the named inverse matrix for a completed Fox-Jacobian of a continuous automorphism.

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverseStage_apply

omit [Fintype X] in
@[simp]
theorem allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverseStage_apply
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) ι)
    (e : F ≃* F) (φ : X → H)
    (j : ZCCompletedGroupAlgebraIndex ProCGroups.FiniteGroupClass.allFinite H) (x y : X) :
    allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverseStage
        (X := X) (F := F) (H := H) hι e φ j x y =
      zcCompletedGroupAlgebraProjection ProCGroups.FiniteGroupClass.allFinite H j
        (allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse
          (X := X) (F := F) (H := H) hι e φ x y)

Evaluation of the finite-stage inverse matrix for a completed Fox-Jacobian of a continuous automorphism.

Show Lean proof

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse_eq_vecMul

theorem allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse_eq_vecMul
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) ι)
    (e : F ≃* F) (φ : X → H)
    (v : ZCFreeFoxCoordinates ProCGroups.FiniteGroupClass.allFinite (X := X) (H := H)) :
    allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse
        (X := X) (F := F) (H := H) hι e φ v =
      Matrix.vecMul v
        (allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse
          (X := X) (F := F) (H := H) hι e φ)

The named inverse linear map is row-vector multiplication by the named inverse matrix.

Show Lean proof

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxAutomorphism_pullback_symm

omit [Fintype X] in
theorem allFinite_freeProCZCCompletedFoxAutomorphism_pullback_symm
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) ι)
    (e : F ≃* F) (he_continuous : Continuous e) (φ : X → H) :
    allFinite_freeProCZCCompletedFoxPullbackGenerator
        (X := X) (F := F) hι e.symm.toMonoidHom
        (allFinite_freeProCZCCompletedFoxPullbackGenerator
          (X := X) (F := F) hι e.toMonoidHom φ ι)
        ι =
      φ

Pulling the target generator map first along an automorphism and then along its inverse recovers the original generator map.

Show Lean proof

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMap_comp_inverse

theorem allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMap_comp_inverse
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) ι)
    (e : F ≃* F) (he_continuous : Continuous e) (φ : X → H) :
    (allFinite_freeProCZCCompletedFoxJacobianLinearMap
        (X := X) (Y := X) (F := F) (F' := F) hι e.toMonoidHom φ ι).comp
      (allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse
        (X := X) (F := F) (H := H) hι e φ) =
      LinearMap.id

Composing the completed Fox-Jacobian linear map of a continuous automorphism with its named inverse gives the identity.

Show Lean proof

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMap_inverse_comp

theorem allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMap_inverse_comp
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) ι)
    (e : F ≃* F) (he_continuous : Continuous e) (he_symm_continuous : Continuous e.symm)
    (φ : X → H) :
    (allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse
        (X := X) (F := F) (H := H) hι e φ).comp
      (allFinite_freeProCZCCompletedFoxJacobianLinearMap
        (X := X) (Y := X) (F := F) (F' := F) hι e.toMonoidHom φ ι) =
      LinearMap.id

Composing the named inverse for the completed Fox-Jacobian linear map of a continuous automorphism with the Jacobian gives the identity.

Show Lean proof

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse_mul

theorem allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse_mul
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) ι)
    (e : F ≃* F) (he_continuous : Continuous e) (φ : X → H) :
    allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse
        (X := X) (F := F) (H := H) hι e φ *
      allFinite_freeProCZCCompletedFoxJacobianMatrix
        (X := X) (Y := X) (F := F) (F' := F) hι e.toMonoidHom φ ι =
      (1 : Matrix X X (ZCCompletedGroupAlgebra ProCGroups.FiniteGroupClass.allFinite H))

The named inverse matrix is a left inverse for the completed Fox-Jacobian matrix of a continuous automorphism.

Show Lean proof

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrix_mul_inverse

theorem allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrix_mul_inverse
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) ι)
    (e : F ≃* F) (he_continuous : Continuous e) (he_symm_continuous : Continuous e.symm)
    (φ : X → H) :
    allFinite_freeProCZCCompletedFoxJacobianMatrix
        (X := X) (Y := X) (F := F) (F' := F) hι e.toMonoidHom φ ι *
      allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse
        (X := X) (F := F) (H := H) hι e φ =
      (1 : Matrix X X (ZCCompletedGroupAlgebra ProCGroups.FiniteGroupClass.allFinite H))

The named inverse matrix is a right inverse for the completed Fox-Jacobian matrix of a continuous automorphism.

Show Lean proof

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixStageInverse_mul

theorem allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixStageInverse_mul
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) ι)
    (e : F ≃* F) (he_continuous : Continuous e) (φ : X → H)
    (j : ZCCompletedGroupAlgebraIndex ProCGroups.FiniteGroupClass.allFinite H) :
    allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverseStage
        (X := X) (F := F) (H := H) hι e φ j *
      allFinite_freeProCZCCompletedFoxJacobianMatrixStage
        (X := X) (Y := X) (F := F) (F' := F) hι e.toMonoidHom φ ι j =
      (1 : Matrix X X (ZCCompletedGroupAlgebraStage ProCGroups.FiniteGroupClass.allFinite H j))

The finite-stage inverse matrix is a left inverse for the finite-stage completed Fox-Jacobian matrix of a continuous automorphism.

Show Lean proof

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixStage_mul_inverse

theorem allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixStage_mul_inverse
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) ι)
    (e : F ≃* F) (he_continuous : Continuous e) (he_symm_continuous : Continuous e.symm)
    (φ : X → H) (j : ZCCompletedGroupAlgebraIndex ProCGroups.FiniteGroupClass.allFinite H) :
    allFinite_freeProCZCCompletedFoxJacobianMatrixStage
        (X := X) (Y := X) (F := F) (F' := F) hι e.toMonoidHom φ ι j *
      allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverseStage
        (X := X) (F := F) (H := H) hι e φ j =
      (1 : Matrix X X (ZCCompletedGroupAlgebraStage ProCGroups.FiniteGroupClass.allFinite H j))

The finite-stage inverse matrix is a right inverse for the finite-stage completed Fox-Jacobian matrix of a continuous automorphism.

Show Lean proof

Definition FoxDifferential.allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearEquiv

def allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearEquiv
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) ι)
    (e : F ≃* F) (he_continuous : Continuous e) (he_symm_continuous : Continuous e.symm)
    (φ : X → H) :
    ZCFreeFoxCoordinates ProCGroups.FiniteGroupClass.allFinite (X := X) (H := H)
        ≃ₗ[ZCCompletedGroupAlgebra ProCGroups.FiniteGroupClass.allFinite H]
      ZCFreeFoxCoordinates ProCGroups.FiniteGroupClass.allFinite (X := X) (H := H) := by
  refine LinearEquiv.ofLinear
    (allFinite_freeProCZCCompletedFoxJacobianLinearMap
      (X := X) (Y := X) (F := F) (F' := F) hι e.toMonoidHom φ ι)
    (allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse
      (X := X) (F := F) (H := H) hι e φ)
    ?_ ?_
  · exact allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMap_comp_inverse
      (X := X) (F := F) (H := H) hι e he_continuous φ
  · exact allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMap_inverse_comp
      (X := X) (F := F) (H := H) hι e he_continuous he_symm_continuous φ

The completed Fox-Jacobian of a continuous automorphism is bundled into a linear equivalence.

ProCGroups.FoxDifferential.Completed.Continuous.Automorphism

Declarations