ProCGroups.FoxDifferential.Completed.Continuous.ChainRule.Basic

12 Theorems | 5 Definitions

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.

import

ProCGroups.FoxDifferential.Completed.Continuous.Free.Rules

Imported by

Definition FoxDifferential.allFinite_freeProCZCCompletedFoxPullbackGenerator

def allFinite_freeProCZCCompletedFoxPullbackGenerator
    {κ : Y → F'}
    (hκ : ProCGroups.FreeProC.IsFreeProCGroup
      (C := ProCGroups.FiniteGroupClass.allFinite) κ)
    (η : F →* F') (φ : Y → H) (ι : X → F) : X → H :=
  fun x =>
    freeProCZCCompletedFoxRightHom
      (C := ProCGroups.FiniteGroupClass.allFinite) hκ
      (ProCGrp.allFinite_property (ProfiniteGrp.of _)) φ
      (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
          ProCGroups.FiniteGroupClass.allFinite) Y H φ)
      (η (ι x))

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

Definition FoxDifferential.allFinite_freeProCZCCompletedFoxJacobian

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) :=
  fun x =>
    freeProCZCCompletedFoxDerivativeVector
      (C := ProCGroups.FiniteGroupClass.allFinite) hκ
      (ProCGrp.allFinite_property (ProfiniteGrp.of _)) φ
      (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
          ProCGroups.FiniteGroupClass.allFinite) Y H φ)
      (η (ι x))

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

Definition FoxDifferential.allFinite_freeProCZCCompletedFoxJacobianLinearMap

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) :=
  foxJacobianLinearMap
    (allFinite_freeProCZCCompletedFoxJacobian (X := X) (F := F) hκ η φ ι)

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

Definition FoxDifferential.allFinite_freeProCZCCompletedFoxJacobianMatrix

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) :=
  foxJacobianMatrix
    (allFinite_freeProCZCCompletedFoxJacobian (X := X) (F := F) hκ η φ ι)

The completed Fox-Jacobian is packaged as a matrix.

Definition FoxDifferential.allFinite_freeProCZCCompletedFoxJacobianMatrixStage

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) :=
  fun x y =>
    zcCompletedGroupAlgebraProjection ProCGroups.FiniteGroupClass.allFinite H j
      (allFinite_freeProCZCCompletedFoxJacobianMatrix
        (X := X) (F := F) hκ η φ ι x y)

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

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxJacobianMatrix_apply

omit [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
    [TopologicalSpace F] [IsTopologicalGroup F] in
@[simp]
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

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

Show Lean proof

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxJacobianMatrixStage_apply

omit [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
    [TopologicalSpace F] [IsTopologicalGroup F] in
@[simp]
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)

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

Show Lean proof

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxJacobianLinearMap_apply

omit [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
    [TopologicalSpace F] [IsTopologicalGroup F] in
@[simp]
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

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

Show Lean proof

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxJacobianLinearMap_eq_vecMul

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

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

Show Lean proof

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxRightHom_comp

omit [Fintype X] in
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 η

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

Show Lean proof

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxDerivativeVector_comp

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)

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

Show Lean proof

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxDerivativeVector_comp_apply

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

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

Show Lean proof

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxDerivativeVector_comp_matrix

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

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

Show Lean proof

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxRightHom_comp_continuousMonoidHom

omit [Fintype X] in
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

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

Show Lean proof

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxDerivativeVector_comp_continuousMonoidHom

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)

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

Show Lean proof

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxDerivativeVector_comp_apply_continuousMonoidHom

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

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

Show Lean proof

Theorem FoxDifferential.allFinite_freeProCZCCompletedFoxDerivativeVector_comp_matrix_continuousMonoidHom

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

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

Show Lean proof

ProCGroups.FoxDifferential.Completed.Continuous.ChainRule.Basic

Declarations