Module

Iterated.lean

Nyll.ProCGroups.FoxDifferential.Completed.Continuous.ChainRule.Iterated

12 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — continuous — chain rule — iterated

The principal declarations in this module are:

allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator

The pulled-back target generator on the middle free source in a two-step source chain.

allFinite_freeProCZCCompletedFoxFirstPullbackGenerator

The pulled-back target generator on the first free source in a two-step source chain.

allFinite_freeProCZCCompletedFoxJacobianLinearMap_comp_comp

Completed Fox-Jacobian functoriality for two composable continuous free pro-\(C\) source maps, as a composition of finite linear maps.

allFinite_freeProCZCCompletedFoxJacobianMatrix_comp_comp

Completed Fox-Jacobian functoriality for two composable continuous free pro-\(C\) source maps, as a matrix product.

Imports1

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

Imported by2

abbrev

allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator

L50 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator

Documentation

The pulled-back target generator on the middle free source in a two-step source chain.

Source context 17 commands

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

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

Lean source · statement

abbrev allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator
    {mu : Z → F''}
    (hmu : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) mu)
    (θ : F' →* F'') (φ : Z → H) (κ : Y → F') : Y → H

abbrev

allFinite_freeProCZCCompletedFoxFirstPullbackGenerator

L59 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxFirstPullbackGenerator

Documentation

The pulled-back target generator on the first free source in a two-step source chain.

Source context 17 commands

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

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

Lean source · statement

abbrev allFinite_freeProCZCCompletedFoxFirstPullbackGenerator
    {κ : Y → F'} {mu : Z → F''}
    (hκ : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) κ)
    (hmu : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) mu)
    (η : F →* F') (θ : F' →* F'') (φ : Z → H) (ι : X → F) : X → H

theorem

allFinite_freeProCZCCompletedFoxJacobianLinearMap_comp_comp

L78 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxJacobianLinearMap_comp_comp

Documentation

Completed Fox-Jacobian functoriality for two composable continuous free pro-\(C\) source maps, as a composition of finite linear maps.

Source context 18 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section AllFiniteIteratedChainRule
variable {X Y Z F F' F'' H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [Fintype Y] [DecidableEq Y] [TopologicalSpace Y] [DiscreteTopology Y]
variable [DecidableEq Z] [TopologicalSpace Z] [DiscreteTopology Z]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
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 [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_comp_comp
    {ι : X → F} {κ : Y → F'} {mu : Z → F''}
    (hκ : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) κ)
    (hmu : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) mu)
    (η : F →* F') (θ : F' →* F'') (hθ_continuous : Continuous θ) (φ : Z → H) :
    allFinite_freeProCZCCompletedFoxJacobianLinearMap
        (X := X) (Y := Z) (F := F) (F' := F'') hmu (θ.comp η) φ ι =
      (allFinite_freeProCZCCompletedFoxJacobianLinearMap
        (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ φ κ).comp
        (allFinite_freeProCZCCompletedFoxJacobianLinearMap
          (X := X) (Y := Y) (F := F) (F' := F') hκ η
          (allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator
            (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)
          ι)

theorem

allFinite_freeProCZCCompletedFoxJacobianMatrix_comp_comp

L111 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxJacobianMatrix_comp_comp

Documentation

Completed Fox-Jacobian functoriality for two composable continuous free pro-\(C\) source maps, as a matrix product.

Source context 18 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section AllFiniteIteratedChainRule
variable {X Y Z F F' F'' H : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [Fintype Y] [DecidableEq Y] [TopologicalSpace Y] [DiscreteTopology Y]
variable [DecidableEq Z] [TopologicalSpace Z] [DiscreteTopology Z]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
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 [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_comp_comp
    {ι : X → F} {κ : Y → F'} {mu : Z → F''}
    (hκ : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) κ)
    (hmu : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) mu)
    (η : F →* F') (θ : F' →* F'') (hθ_continuous : Continuous θ) (φ : Z → H) :
    allFinite_freeProCZCCompletedFoxJacobianMatrix
        (X := X) (Y := Z) (F := F) (F' := F'') hmu (θ.comp η) φ ι =
      allFinite_freeProCZCCompletedFoxJacobianMatrix
          (X := X) (Y := Y) (F := F) (F' := F') hκ η
          (allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator
            (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)
          ι *
        allFinite_freeProCZCCompletedFoxJacobianMatrix
          (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ φ κ

theorem

allFinite_freeProCZCCompletedFoxDerivativeVector_comp_comp

L139 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxDerivativeVector_comp_comp

Documentation

Three-term completed pro-\(C\) Fox chain rule in vector form.

Source context 17 commands

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

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

theorem

allFinite_freeProCZCCompletedFoxDerivativeVector_comp_comp_matrix

L221 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxDerivativeVector_comp_comp_matrix

Documentation

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

Source context 17 commands

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

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

theorem

allFinite_freeProCZCCompletedFoxDerivativeVector_comp_comp_apply

L263 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxDerivativeVector_comp_comp_apply

Documentation

Three-term completed pro-\(C\) Fox chain rule in component form.

Source context 17 commands

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

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

theorem

allFinite_freeProCZCCompletedFoxJacobianLinearMap_comp_comp_continuousMonoidHom

L311 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxJacobianLinearMap_comp_comp_continuousMonoidHom

Documentation

Continuous-homomorphism form of completed Fox-Jacobian functoriality, as a composition of finite linear maps.

Source context 18 commands

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

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

Lean source · statement

theorem allFinite_freeProCZCCompletedFoxJacobianLinearMap_comp_comp_continuousMonoidHom
    {ι : X → F} {κ : Y → F'} {mu : Z → F''}
    (hκ : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) κ)
    (hmu : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) mu)
    (η : F →ₜ* F') (θ : F' →ₜ* F'') (φ : Z → H) :
    allFinite_freeProCZCCompletedFoxJacobianLinearMap
        (X := X) (Y := Z) (F := F) (F' := F'') hmu
        (θ.toMonoidHom.comp η.toMonoidHom) φ ι =
      (allFinite_freeProCZCCompletedFoxJacobianLinearMap
        (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ.toMonoidHom φ κ).comp
        (allFinite_freeProCZCCompletedFoxJacobianLinearMap
          (X := X) (Y := Y) (F := F) (F' := F') hκ η.toMonoidHom
          (allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator
            (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ.toMonoidHom φ κ)
          ι)

theorem

allFinite_freeProCZCCompletedFoxJacobianMatrix_comp_comp_continuousMonoidHom

L335 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxJacobianMatrix_comp_comp_continuousMonoidHom

Documentation

Continuous-homomorphism form of completed Fox-Jacobian functoriality, as a matrix product.

Source context 18 commands

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

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

Lean source · statement

theorem allFinite_freeProCZCCompletedFoxJacobianMatrix_comp_comp_continuousMonoidHom
    {ι : X → F} {κ : Y → F'} {mu : Z → F''}
    (hκ : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) κ)
    (hmu : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) mu)
    (η : F →ₜ* F') (θ : F' →ₜ* F'') (φ : Z → H) :
    allFinite_freeProCZCCompletedFoxJacobianMatrix
        (X := X) (Y := Z) (F := F) (F' := F'') hmu
        (θ.toMonoidHom.comp η.toMonoidHom) φ ι =
      allFinite_freeProCZCCompletedFoxJacobianMatrix
          (X := X) (Y := Y) (F := F) (F' := F') hκ η.toMonoidHom
          (allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator
            (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ.toMonoidHom φ κ)
          ι *
        allFinite_freeProCZCCompletedFoxJacobianMatrix
          (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ.toMonoidHom φ κ

theorem

allFinite_freeProCZCCompletedFoxDerivativeVector_comp_comp_continuousMonoidHom

L357 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxDerivativeVector_comp_comp_continuousMonoidHom

Documentation

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

Source context 17 commands

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

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

theorem

allFinite_freeProCZCCompletedFoxDerivativeVector_comp_comp_matrix_continuousMonoidHom

L397 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxDerivativeVector_comp_comp_matrix_continuousMonoidHom

Documentation

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

Source context 17 commands

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

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

theorem

allFinite_freeProCZCCompletedFoxDerivativeVector_comp_comp_apply_continuousMonoidHom

L439 ↗

FoxDifferential.allFinite_freeProCZCCompletedFoxDerivativeVector_comp_comp_apply_continuousMonoidHom

Documentation

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

Source context 17 commands

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

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

Module documentation

Fox differential: completed — continuous — chain rule — iterated

Declarations