Module

Automorphism.lean

Nyll.ProCGroups.FoxDifferential.Completed.Continuous.Automorphism

13 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — continuous — automorphism

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.

Imports2

Imported by1

Nyll.ProCGroups.FoxDifferential.Completed.Continuous.All

def

allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse

L44 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse

Documentation

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

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section AllFiniteAutomorphismJacobian
variable {X F H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]

Lean source · statement

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)

def

allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse

L59 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse

Documentation

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

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section AllFiniteAutomorphismJacobian
variable {X F H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]

Lean source · statement

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)

def

allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverseStage

L75 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverseStage

Documentation

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

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section AllFiniteAutomorphismJacobian
variable {X F H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]

Lean source · statement

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)

theorem

allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverseStage_apply

L93 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverseStage_apply

Documentation

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

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section AllFiniteAutomorphismJacobian
variable {X F H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
omit [Fintype X] in

Lean source · statement

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)

theorem

allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse_eq_vecMul

L107 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse_eq_vecMul

Documentation

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

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section AllFiniteAutomorphismJacobian
variable {X F H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]

Lean source · statement

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 φ)

theorem

allFinite_freeProCZCCompletedFoxAutomorphism_pullback_symm

L129 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxAutomorphism_pullback_symm

Documentation

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

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section AllFiniteAutomorphismJacobian
variable {X F H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
omit [Fintype X] in

Lean source · statement

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 φ ι)
        ι =
      φ

theorem

allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMap_comp_inverse

L194 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMap_comp_inverse

Documentation

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

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section AllFiniteAutomorphismJacobian
variable {X F H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]

Lean source · statement

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

theorem

allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMap_inverse_comp

L228 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearMap_inverse_comp

Documentation

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

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section AllFiniteAutomorphismJacobian
variable {X F H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]

Lean source · statement

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

theorem

allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse_mul

L274 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse_mul

Documentation

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

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section AllFiniteAutomorphismJacobian
variable {X F H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]

Lean source · statement

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))

theorem

allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrix_mul_inverse

L299 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrix_mul_inverse

Documentation

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

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section AllFiniteAutomorphismJacobian
variable {X F H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]

Lean source · statement

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))

theorem

allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixStageInverse_mul

L325 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixStageInverse_mul

Documentation

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

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section AllFiniteAutomorphismJacobian
variable {X F H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]

Lean source · statement

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))

theorem

allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixStage_mul_inverse

L369 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxAutomorphismJacobianMatrixStage_mul_inverse

Documentation

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

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section AllFiniteAutomorphismJacobian
variable {X F H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]

Lean source · statement

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))

def

allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearEquiv

L410 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxAutomorphismJacobianLinearEquiv

Documentation

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

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section AllFiniteAutomorphismJacobian
variable {X F H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]

Lean source · statement

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)

Module documentation

Fox differential: completed — continuous — automorphism

Declarations