Module

Basic.lean

Nyll.ProCGroups.FoxDifferential.Completed.Continuous.ChainRule.Basic

17 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — continuous — chain rule — basic

The principal declarations in this module are:

allFinite_freeProCZCCompletedFoxPullbackGenerator

The target generator map pulled back along a continuous homomorphism of free pro-\(C\) sources.

allFinite_freeProCZCCompletedFoxJacobian

The completed Fox-Jacobian family of a continuous homomorphism between free pro-\(C\) sources.

allFinite_freeProCZCCompletedFoxJacobianMatrix_apply

The matrix evaluation is componentwise the completed Fox-Jacobian family.

allFinite_freeProCZCCompletedFoxJacobianMatrixStage_apply

Evaluation of the finite-stage completed Fox-Jacobian matrix.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.Continuous.Free.Rules

Imported by2

def

allFinite_freeProCZCCompletedFoxPullbackGenerator

L47 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxPullbackGenerator

Documentation

The target generator map pulled back along a continuous homomorphism of free pro-\(C\) sources.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section AllFiniteChainRule
variable {X Y F F' H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [DecidableEq Y] [TopologicalSpace Y] [DiscreteTopology Y]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace 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_freeProCZCCompletedFoxPullbackGenerator
    {κ : Y → F'}
    (hκ : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) κ)
    (η : F →* F') (φ : Y → H) (ι : X → F) : X → H

def

allFinite_freeProCZCCompletedFoxJacobian

L63 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxJacobian

Documentation

The completed Fox-Jacobian family of a continuous homomorphism between free pro-\(C\) sources.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section AllFiniteChainRule
variable {X Y F F' H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [DecidableEq Y] [TopologicalSpace Y] [DiscreteTopology Y]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace 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_freeProCZCCompletedFoxJacobian
    {κ : Y → F'}
    (hκ : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) κ)
    (η : F →* F') (φ : Y → H) (ι : X → F) :
    X → ZCFreeFoxCoordinates ProCGroups.FiniteGroupClass.allFinite (X := Y) (H := H)

def

allFinite_freeProCZCCompletedFoxJacobianLinearMap

L81 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxJacobianLinearMap

Documentation

The completed Fox-Jacobian family is bundled into a finite linear map on completed coordinate vectors.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section AllFiniteChainRule
variable {X Y F F' H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [DecidableEq Y] [TopologicalSpace Y] [DiscreteTopology Y]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace 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_freeProCZCCompletedFoxJacobianLinearMap
    {κ : Y → F'}
    (hκ : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) κ)
    (η : F →* F') (φ : Y → H) (ι : X → F) :
    ZCFreeFoxCoordinates
        ProCGroups.FiniteGroupClass.allFinite (X := X) (H := H) →ₗ[
          ZCCompletedGroupAlgebra ProCGroups.FiniteGroupClass.allFinite H]
      ZCFreeFoxCoordinates ProCGroups.FiniteGroupClass.allFinite (X := Y) (H := H)

def

allFinite_freeProCZCCompletedFoxJacobianMatrix

L94 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxJacobianMatrix

Documentation

The completed Fox-Jacobian is packaged as a matrix.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section AllFiniteChainRule
variable {X Y F F' H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [DecidableEq Y] [TopologicalSpace Y] [DiscreteTopology Y]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace 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_freeProCZCCompletedFoxJacobianMatrix
    {κ : Y → F'}
    (hκ : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) κ)
    (η : F →* F') (φ : Y → H) (ι : X → F) :
    Matrix X Y (ZCCompletedGroupAlgebra ProCGroups.FiniteGroupClass.allFinite H)

def

allFinite_freeProCZCCompletedFoxJacobianMatrixStage

L104 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxJacobianMatrixStage

Documentation

A finite-stage projection of the completed Fox-Jacobian matrix.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section AllFiniteChainRule
variable {X Y F F' H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [DecidableEq Y] [TopologicalSpace Y] [DiscreteTopology Y]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace 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_freeProCZCCompletedFoxJacobianMatrixStage
    {κ : Y → F'}
    (hκ : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) κ)
    (η : F →* F') (φ : Y → H) (ι : X → F)
    (j : ZCCompletedGroupAlgebraIndex ProCGroups.FiniteGroupClass.allFinite H) :
    Matrix X Y (ZCCompletedGroupAlgebraStage ProCGroups.FiniteGroupClass.allFinite H j)

theorem

allFinite_freeProCZCCompletedFoxJacobianMatrix_apply

L120 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxJacobianMatrix_apply

Documentation

The matrix evaluation is componentwise the completed Fox-Jacobian family.

Source context 15 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section AllFiniteChainRule
variable {X Y F F' H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [DecidableEq Y] [TopologicalSpace Y] [DiscreteTopology Y]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace 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] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
    [TopologicalSpace F] [IsTopologicalGroup F] in

Lean source · statement

theorem allFinite_freeProCZCCompletedFoxJacobianMatrix_apply
    {κ : Y → F'}
    (hκ : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) κ)
    (η : F →* F') (φ : Y → H) (ι : X → F)
    (x : X) (y : Y) :
    allFinite_freeProCZCCompletedFoxJacobianMatrix
        (X := X) (F := F) hκ η φ ι x y =
      allFinite_freeProCZCCompletedFoxJacobian
        (X := X) (F := F) hκ η φ ι x y

theorem

allFinite_freeProCZCCompletedFoxJacobianMatrixStage_apply

L136 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxJacobianMatrixStage_apply

Documentation

Evaluation of the finite-stage completed Fox-Jacobian matrix.

Source context 15 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section AllFiniteChainRule
variable {X Y F F' H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [DecidableEq Y] [TopologicalSpace Y] [DiscreteTopology Y]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace 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] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
    [TopologicalSpace F] [IsTopologicalGroup F] in

Lean source · statement

theorem allFinite_freeProCZCCompletedFoxJacobianMatrixStage_apply
    {κ : Y → F'}
    (hκ : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) κ)
    (η : F →* F') (φ : Y → H) (ι : X → F)
    (j : ZCCompletedGroupAlgebraIndex ProCGroups.FiniteGroupClass.allFinite H) (x : X) (y : Y) :
    allFinite_freeProCZCCompletedFoxJacobianMatrixStage
        (X := X) (F := F) hκ η φ ι j x y =
      zcCompletedGroupAlgebraProjection ProCGroups.FiniteGroupClass.allFinite H j
        (allFinite_freeProCZCCompletedFoxJacobianMatrix
          (X := X) (F := F) hκ η φ ι x y)

theorem

allFinite_freeProCZCCompletedFoxJacobianLinearMap_apply

L156 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxJacobianLinearMap_apply

Documentation

The all-finite pro-\(C\) completed Fox-Jacobian linear map is evaluated coordinatewise at each finite quotient stage.

Source context 15 commands

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

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

Lean source · statement

theorem allFinite_freeProCZCCompletedFoxJacobianLinearMap_apply
    {κ : Y → F'}
    (hκ : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) κ)
    (η : F →* F') (φ : Y → H) (ι : X → F)
    (v : ZCFreeFoxCoordinates ProCGroups.FiniteGroupClass.allFinite (X := X) (H := H)) (y : Y) :
    allFinite_freeProCZCCompletedFoxJacobianLinearMap
        (X := X) (F := F) hκ η φ ι v y =
      ∑ x : X,
        v x * allFinite_freeProCZCCompletedFoxJacobian
          (X := X) (F := F) hκ η φ ι x y

theorem

allFinite_freeProCZCCompletedFoxJacobianLinearMap_eq_vecMul

L172 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxJacobianLinearMap_eq_vecMul

Documentation

The completed Fox-Jacobian linear map is row-vector multiplication by its matrix.

Source context 15 commands

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

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

Lean source · statement

theorem allFinite_freeProCZCCompletedFoxJacobianLinearMap_eq_vecMul
    {κ : Y → F'}
    (hκ : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) κ)
    (η : F →* F') (φ : Y → H) (ι : X → F)
    (v : ZCFreeFoxCoordinates ProCGroups.FiniteGroupClass.allFinite (X := X) (H := H)) :
    allFinite_freeProCZCCompletedFoxJacobianLinearMap
        (X := X) (F := F) hκ η φ ι v =
      Matrix.vecMul v
        (allFinite_freeProCZCCompletedFoxJacobianMatrix
          (X := X) (F := F) hκ η φ ι)

theorem

allFinite_freeProCZCCompletedFoxRightHom_comp

L191 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxRightHom_comp

Documentation

The canonical right homomorphism for the pulled-back generator map is the composite of the target right homomorphism with the source homomorphism.

Source context 15 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section AllFiniteChainRule
variable {X Y F F' H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [DecidableEq Y] [TopologicalSpace Y] [DiscreteTopology Y]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace 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_freeProCZCCompletedFoxRightHom_comp
    {ι : X → F} {κ : Y → F'}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) ι)
    (hκ : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) κ)
    (η : F →* F') (hη_continuous : Continuous η) (φ : Y → H) :
    freeProCZCCompletedFoxRightHom
        (C := ProCGroups.FiniteGroupClass.allFinite) hι
        (ProCGrp.allFinite_property (ProfiniteGrp.of _))
        (allFinite_freeProCZCCompletedFoxPullbackGenerator
          (X := X) (F := F) hκ η φ ι)
        (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
            ProCGroups.FiniteGroupClass.allFinite) X H
          (allFinite_freeProCZCCompletedFoxPullbackGenerator
            (X := X) (F := F) hκ η φ ι)) =
      (freeProCZCCompletedFoxRightHom
        (C := ProCGroups.FiniteGroupClass.allFinite) hκ
        (ProCGrp.allFinite_property (ProfiniteGrp.of _)) φ
        (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
            ProCGroups.FiniteGroupClass.allFinite) Y H φ)).comp η

theorem

allFinite_freeProCZCCompletedFoxDerivativeVector_comp

L249 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxDerivativeVector_comp

Documentation

Completed pro-\(C\) Fox chain rule in vector form.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section AllFiniteChainRule
variable {X Y F F' H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [DecidableEq Y] [TopologicalSpace Y] [DiscreteTopology Y]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace 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_freeProCZCCompletedFoxDerivativeVector_comp
    {ι : X → F} {κ : Y → F'}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) ι)
    (hκ : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) κ)
    (η : F →* F') (hη_continuous : Continuous η) (φ : Y → H) (g : F) :
    freeProCZCCompletedFoxDerivativeVector
        (C := ProCGroups.FiniteGroupClass.allFinite) hκ
        (ProCGrp.allFinite_property (ProfiniteGrp.of _)) φ
        (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
            ProCGroups.FiniteGroupClass.allFinite) Y H φ) (η g) =
      allFinite_freeProCZCCompletedFoxJacobianLinearMap
        (X := X) (F := F) hκ η φ ι
        (freeProCZCCompletedFoxDerivativeVector
          (C := ProCGroups.FiniteGroupClass.allFinite) hι
          (ProCGrp.allFinite_property (ProfiniteGrp.of _))
          (allFinite_freeProCZCCompletedFoxPullbackGenerator
            (X := X) (F := F) hκ η φ ι)
          (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
              ProCGroups.FiniteGroupClass.allFinite) X H
            (allFinite_freeProCZCCompletedFoxPullbackGenerator
              (X := X) (F := F) hκ η φ ι)) g)

theorem

allFinite_freeProCZCCompletedFoxDerivativeVector_comp_apply

L393 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxDerivativeVector_comp_apply

Documentation

Completed pro-\(C\) Fox chain rule in component form.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section AllFiniteChainRule
variable {X Y F F' H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [DecidableEq Y] [TopologicalSpace Y] [DiscreteTopology Y]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace 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_freeProCZCCompletedFoxDerivativeVector_comp_apply
    {ι : X → F} {κ : Y → F'}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) ι)
    (hκ : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) κ)
    (η : F →* F') (hη_continuous : Continuous η) (φ : Y → H) (g : F) (y : Y) :
    freeProCZCCompletedFoxDerivativeVector
        (C := ProCGroups.FiniteGroupClass.allFinite) hκ
        (ProCGrp.allFinite_property (ProfiniteGrp.of _)) φ
        (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
            ProCGroups.FiniteGroupClass.allFinite) Y H φ) (η g) y =
      ∑ x : X,
        freeProCZCCompletedFoxDerivativeVector
            (C := ProCGroups.FiniteGroupClass.allFinite) hι
            (ProCGrp.allFinite_property (ProfiniteGrp.of _))
            (allFinite_freeProCZCCompletedFoxPullbackGenerator
              (X := X) (F := F) hκ η φ ι)
            (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
                ProCGroups.FiniteGroupClass.allFinite) X H
              (allFinite_freeProCZCCompletedFoxPullbackGenerator
                (X := X) (F := F) hκ η φ ι)) g x *
          allFinite_freeProCZCCompletedFoxJacobian
            (X := X) (F := F) hκ η φ ι x y

theorem

allFinite_freeProCZCCompletedFoxDerivativeVector_comp_matrix

L424 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxDerivativeVector_comp_matrix

Documentation

The completed pro-\(C\) Fox chain rule in matrix form.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section AllFiniteChainRule
variable {X Y F F' H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [DecidableEq Y] [TopologicalSpace Y] [DiscreteTopology Y]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace 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_freeProCZCCompletedFoxDerivativeVector_comp_matrix
    {ι : X → F} {κ : Y → F'}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) ι)
    (hκ : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) κ)
    (η : F →* F') (hη_continuous : Continuous η) (φ : Y → H) (g : F) :
    freeProCZCCompletedFoxDerivativeVector
        (C := ProCGroups.FiniteGroupClass.allFinite) hκ
        (ProCGrp.allFinite_property (ProfiniteGrp.of _)) φ
        (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
            ProCGroups.FiniteGroupClass.allFinite) Y H φ) (η g) =
      Matrix.vecMul
        (freeProCZCCompletedFoxDerivativeVector
          (C := ProCGroups.FiniteGroupClass.allFinite) hι
          (ProCGrp.allFinite_property (ProfiniteGrp.of _))
          (allFinite_freeProCZCCompletedFoxPullbackGenerator
            (X := X) (F := F) hκ η φ ι)
          (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
              ProCGroups.FiniteGroupClass.allFinite) X H
            (allFinite_freeProCZCCompletedFoxPullbackGenerator
              (X := X) (F := F) hκ η φ ι)) g)
        (allFinite_freeProCZCCompletedFoxJacobianMatrix
          (X := X) (F := F) hκ η φ ι)

theorem

allFinite_freeProCZCCompletedFoxRightHom_comp_continuousMonoidHom

L465 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxRightHom_comp_continuousMonoidHom

Documentation

Continuous-homomorphism form of the right-homomorphism chain rule.

Source context 15 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section AllFiniteChainRule
variable {X Y F F' H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [DecidableEq Y] [TopologicalSpace Y] [DiscreteTopology Y]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace 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_freeProCZCCompletedFoxRightHom_comp_continuousMonoidHom
    {ι : X → F} {κ : Y → F'}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) ι)
    (hκ : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) κ)
    (η : F →ₜ* F') (φ : Y → H) :
    freeProCZCCompletedFoxRightHom
        (C := ProCGroups.FiniteGroupClass.allFinite) hι
        (ProCGrp.allFinite_property (ProfiniteGrp.of _))
        (allFinite_freeProCZCCompletedFoxPullbackGenerator
          (X := X) (F := F) hκ η.toMonoidHom φ ι)
        (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
            ProCGroups.FiniteGroupClass.allFinite) X H
          (allFinite_freeProCZCCompletedFoxPullbackGenerator
            (X := X) (F := F) hκ η.toMonoidHom φ ι)) =
      (freeProCZCCompletedFoxRightHom
        (C := ProCGroups.FiniteGroupClass.allFinite) hκ
        (ProCGrp.allFinite_property (ProfiniteGrp.of _)) φ
        (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
            ProCGroups.FiniteGroupClass.allFinite) Y H φ)).comp η.toMonoidHom

theorem

allFinite_freeProCZCCompletedFoxDerivativeVector_comp_continuousMonoidHom

L491 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxDerivativeVector_comp_continuousMonoidHom

Documentation

Continuous-homomorphism form of the completed pro-\(C\) Fox chain rule in vector form.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section AllFiniteChainRule
variable {X Y F F' H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [DecidableEq Y] [TopologicalSpace Y] [DiscreteTopology Y]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace 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_freeProCZCCompletedFoxDerivativeVector_comp_continuousMonoidHom
    {ι : X → F} {κ : Y → F'}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) ι)
    (hκ : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) κ)
    (η : F →ₜ* F') (φ : Y → H) (g : F) :
    freeProCZCCompletedFoxDerivativeVector
        (C := ProCGroups.FiniteGroupClass.allFinite) hκ
        (ProCGrp.allFinite_property (ProfiniteGrp.of _)) φ
        (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
            ProCGroups.FiniteGroupClass.allFinite) Y H φ) (η g) =
      allFinite_freeProCZCCompletedFoxJacobianLinearMap
        (X := X) (F := F) hκ η.toMonoidHom φ ι
        (freeProCZCCompletedFoxDerivativeVector
          (C := ProCGroups.FiniteGroupClass.allFinite) hι
          (ProCGrp.allFinite_property (ProfiniteGrp.of _))
          (allFinite_freeProCZCCompletedFoxPullbackGenerator
            (X := X) (F := F) hκ η.toMonoidHom φ ι)
          (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
              ProCGroups.FiniteGroupClass.allFinite) X H
            (allFinite_freeProCZCCompletedFoxPullbackGenerator
              (X := X) (F := F) hκ η.toMonoidHom φ ι)) g)

theorem

allFinite_freeProCZCCompletedFoxDerivativeVector_comp_apply_continuousMonoidHom

L519 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxDerivativeVector_comp_apply_continuousMonoidHom

Documentation

Continuous-homomorphism form of the completed pro-\(C\) Fox chain rule in component form.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section AllFiniteChainRule
variable {X Y F F' H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [DecidableEq Y] [TopologicalSpace Y] [DiscreteTopology Y]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace 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_freeProCZCCompletedFoxDerivativeVector_comp_apply_continuousMonoidHom
    {ι : X → F} {κ : Y → F'}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) ι)
    (hκ : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) κ)
    (η : F →ₜ* F') (φ : Y → H) (g : F) (y : Y) :
    freeProCZCCompletedFoxDerivativeVector
        (C := ProCGroups.FiniteGroupClass.allFinite) hκ
        (ProCGrp.allFinite_property (ProfiniteGrp.of _)) φ
        (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
            ProCGroups.FiniteGroupClass.allFinite) Y H φ) (η g) y =
      ∑ x : X,
        freeProCZCCompletedFoxDerivativeVector
            (C := ProCGroups.FiniteGroupClass.allFinite) hι
            (ProCGrp.allFinite_property (ProfiniteGrp.of _))
            (allFinite_freeProCZCCompletedFoxPullbackGenerator
              (X := X) (F := F) hκ η.toMonoidHom φ ι)
            (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
                ProCGroups.FiniteGroupClass.allFinite) X H
              (allFinite_freeProCZCCompletedFoxPullbackGenerator
                (X := X) (F := F) hκ η.toMonoidHom φ ι)) g x *
          allFinite_freeProCZCCompletedFoxJacobian
            (X := X) (F := F) hκ η.toMonoidHom φ ι x y

theorem

allFinite_freeProCZCCompletedFoxDerivativeVector_comp_matrix_continuousMonoidHom

L548 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxDerivativeVector_comp_matrix_continuousMonoidHom

Documentation

The continuous-homomorphism form of the completed pro-\(C\) Fox chain rule in matrix form.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section AllFiniteChainRule
variable {X Y F F' H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [DecidableEq Y] [TopologicalSpace Y] [DiscreteTopology Y]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace 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_freeProCZCCompletedFoxDerivativeVector_comp_matrix_continuousMonoidHom
    {ι : X → F} {κ : Y → F'}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) ι)
    (hκ : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) κ)
    (η : F →ₜ* F') (φ : Y → H) (g : F) :
    freeProCZCCompletedFoxDerivativeVector
        (C := ProCGroups.FiniteGroupClass.allFinite) hκ
        (ProCGrp.allFinite_property (ProfiniteGrp.of _)) φ
        (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
            ProCGroups.FiniteGroupClass.allFinite) Y H φ) (η g) =
      Matrix.vecMul
        (freeProCZCCompletedFoxDerivativeVector
          (C := ProCGroups.FiniteGroupClass.allFinite) hι
          (ProCGrp.allFinite_property (ProfiniteGrp.of _))
          (allFinite_freeProCZCCompletedFoxPullbackGenerator
            (X := X) (F := F) hκ η.toMonoidHom φ ι)
          (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
              ProCGroups.FiniteGroupClass.allFinite) X H
            (allFinite_freeProCZCCompletedFoxPullbackGenerator
              (X := X) (F := F) hκ η.toMonoidHom φ ι)) g)
        (allFinite_freeProCZCCompletedFoxJacobianMatrix
          (X := X) (F := F) hκ η.toMonoidHom φ ι)

Module documentation

Fox differential: completed — continuous — chain rule — basic

Declarations