ProCGroups.FoxDifferential.Completed.Continuous.ChainRule.Iterated

10 Theorems | 2 Abbreviations

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.

import

ProCGroups.FoxDifferential.Completed.Continuous.ChainRule.Basic

Imported by

Abbreviation FoxDifferential.allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator

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

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

Abbreviation FoxDifferential.allFinite_freeProCZCCompletedFoxFirstPullbackGenerator

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 :=
  allFinite_freeProCZCCompletedFoxPullbackGenerator
    (X := X) (Y := Y) (F := F) (F' := F') hκ η
    (allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator
      (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)
    ι

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

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxJacobianLinearMap_comp_comp

omit [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
    [TopologicalSpace F] [IsTopologicalGroup F] in
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 θ φ κ)
          ι)

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

Show Lean proof

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxJacobianMatrix_comp_comp

omit [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
    [TopologicalSpace F] [IsTopologicalGroup F] in
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 θ φ κ

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

Show Lean proof

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxDerivativeVector_comp_comp

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

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

Show Lean proof

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxDerivativeVector_comp_comp_matrix

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

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

Show Lean proof

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxDerivativeVector_comp_comp_apply

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

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

Show Lean proof

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxJacobianLinearMap_comp_comp_continuousMonoidHom

omit [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
    [IsTopologicalGroup F] [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F] in
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 φ κ)
          ι)

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

Show Lean proof

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxJacobianMatrix_comp_comp_continuousMonoidHom

omit [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
    [IsTopologicalGroup F] [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F] in
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 φ κ

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

Show Lean proof

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxDerivativeVector_comp_comp_continuousMonoidHom

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

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

Show Lean proof

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxDerivativeVector_comp_comp_matrix_continuousMonoidHom

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

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

Show Lean proof

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxDerivativeVector_comp_comp_apply_continuousMonoidHom

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

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

Show Lean proof

ProCGroups.FoxDifferential.Completed.Continuous.ChainRule.Iterated

Declarations