ProCGroups.FoxDifferential.Completed.Continuous.Naturality

18 Theorems | 2 Definitions

The principal declarations in this module are:

zcCompletedFoxSemidirectMapTarget Target functoriality for completed Fox semidirect products. - zcCompletedFoxSemidirectMapTargetHom Target functoriality for completed Fox semidirect products as a continuous homomorphism. - continuous_zcCompletedGroupAlgebraMap The completed group-algebra map induced by a continuous target homomorphism is continuous. - zcCompletedGroupAlgebraMap_surjective_of_surjective A surjective target homomorphism induces a surjective completed group-algebra map.

import

ProCGroups.FoxDifferential.Completed.Continuous.Free.Rules

Imported by

Theorem FoxDifferential.continuous_zcCompletedGroupAlgebraMap

theorem continuous_zcCompletedGroupAlgebraMap (η : H →ₜ* K) :
    Continuous (zcCompletedGroupAlgebraMap C hC η)

The completed group-algebra map induced by a continuous target homomorphism is continuous.

Show Lean proof

Theorem FoxDifferential.zcCompletedGroupAlgebraMap_surjective_of_surjective

theorem zcCompletedGroupAlgebraMap_surjective_of_surjective
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (η : H →ₜ* K) (hη : Function.Surjective η) :
    Function.Surjective (zcCompletedGroupAlgebraMap C hC η)

A surjective target homomorphism induces a surjective completed group-algebra map.

Show Lean proof

Theorem FoxDifferential.isQuotientMap_zcCompletedGroupAlgebraMap_of_surjective

theorem isQuotientMap_zcCompletedGroupAlgebraMap_of_surjective
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (η : H →ₜ* K) (hη : Function.Surjective η) :
    Topology.IsQuotientMap (zcCompletedGroupAlgebraMap C hC η)

A surjective completed group-algebra map is a quotient map.

Show Lean proof

Theorem FoxDifferential.isOpenQuotientMap_zcCompletedGroupAlgebraMap_of_surjective

theorem isOpenQuotientMap_zcCompletedGroupAlgebraMap_of_surjective
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (η : H →ₜ* K) (hη : Function.Surjective η) :
    IsOpenQuotientMap (zcCompletedGroupAlgebraMap C hC η)

A surjective completed group-algebra map is an open quotient map as an additive-group homomorphism.

Show Lean proof

Theorem FoxDifferential.continuous_zcFreeFoxCoordinatesMap

theorem continuous_zcFreeFoxCoordinatesMap (η : H →ₜ* K) :
    Continuous (zcFreeFoxCoordinatesMap (X := X) C hC η)

The coordinatewise target map on completed Fox-coordinate vectors is continuous.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxBoundary_mapTarget

theorem freeProCZCCompletedFoxBoundary_mapTarget
    (η : H →ₜ* K) (φ : X → H)
    (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
    zcCompletedGroupAlgebraMap C hC η (freeProCZCCompletedFoxBoundary C φ v) =
      freeProCZCCompletedFoxBoundary C (fun x : X => η (φ x))
        (zcFreeFoxCoordinatesMap (X := X) C hC η v)

Source-shaped completed Fox boundary maps are natural in the target group.

Show Lean proof

Definition FoxDifferential.zcCompletedFoxSemidirectMapTarget

def zcCompletedFoxSemidirectMapTarget (η : H →ₜ* K) :
    ZCCompletedFoxSemidirect C X H →* ZCCompletedFoxSemidirect C X K where
  toFun a :=
    { left := zcFreeFoxCoordinatesMap (X := X) C hC η a.left
      right := η a.right }
  map_one' := by
    ext x
    · simp only [ZCCompletedFoxSemidirect.one_left, zcFreeFoxCoordinatesMap_apply,
        Pi.zero_apply, map_zero, zcCompletedGroupAlgebraProjection_zero]
    · simp only [ZCCompletedFoxSemidirect.one_right, map_one]
  map_mul' a b := by
    ext x
    · simp only [ZCCompletedFoxSemidirect.mul_left, zcFreeFoxCoordinatesMap_apply,
        Pi.add_apply, Pi.smul_apply, smul_eq_mul, map_add, map_mul,
        zcCompletedGroupAlgebraMap_groupLike, zcCompletedGroupAlgebraProjection_add,
        zcCompletedGroupAlgebraProjection_map, zcCompletedGroupAlgebraProjection_mul,
        zcCompletedGroupAlgebraProjection_groupLike, MonoidAlgebra.of_apply,
        MonoidAlgebra.coeff_add]
    · simp only [ZCCompletedFoxSemidirect.mul_right, map_mul]

Target functoriality for completed Fox semidirect products.

Theorem FoxDifferential.zcCompletedFoxSemidirectMapTarget_left

omit [DecidableEq X] in
@[simp]
theorem zcCompletedFoxSemidirectMapTarget_left
    (η : H →ₜ* K) (a : ZCCompletedFoxSemidirect C X H) :
    (zcCompletedFoxSemidirectMapTarget (X := X) C hC η a).left =
      zcFreeFoxCoordinatesMap (X := X) C hC η a.left

This declaration identifies the left component of the target map on completed Fox semidirect products.

Show Lean proof

Theorem FoxDifferential.zcCompletedFoxSemidirectMapTarget_right

omit [DecidableEq X] in
@[simp]
theorem zcCompletedFoxSemidirectMapTarget_right
    (η : H →ₜ* K) (a : ZCCompletedFoxSemidirect C X H) :
    (zcCompletedFoxSemidirectMapTarget (X := X) C hC η a).right = η a.right

This declaration identifies the right component of the target map on completed Fox semidirect products.

Show Lean proof

Theorem FoxDifferential.continuous_zcCompletedFoxSemidirectMapTarget

omit [DecidableEq X] in
theorem continuous_zcCompletedFoxSemidirectMapTarget
    (η : H →ₜ* K) :
    Continuous (zcCompletedFoxSemidirectMapTarget (X := X) C hC η)

The target map on completed Fox semidirect products is continuous.

Show Lean proof

Definition FoxDifferential.zcCompletedFoxSemidirectMapTargetHom

def zcCompletedFoxSemidirectMapTargetHom (η : H →ₜ* K) :
    ZCCompletedFoxSemidirect C X H →ₜ* ZCCompletedFoxSemidirect C X K where
  toMonoidHom := zcCompletedFoxSemidirectMapTarget (X := X) C hC η
  continuous_toFun := continuous_zcCompletedFoxSemidirectMapTarget (X := X) C hC η

Target functoriality for completed Fox semidirect products as a continuous homomorphism.

Theorem FoxDifferential.zcCompletedFoxSemidirectMapTargetHom_toMonoidHom

omit [DecidableEq X] in
@[simp]
theorem zcCompletedFoxSemidirectMapTargetHom_toMonoidHom
    (η : H →ₜ* K) :
    (zcCompletedFoxSemidirectMapTargetHom (X := X) C hC η).toMonoidHom =
      zcCompletedFoxSemidirectMapTarget (X := X) C hC η

The continuous target map has the expected underlying homomorphism.

Show Lean proof

Theorem FoxDifferential.zcCompletedFoxSemidirectMapTargetHom_left

omit [DecidableEq X] in
@[simp]
theorem zcCompletedFoxSemidirectMapTargetHom_left
    (η : H →ₜ* K) (a : ZCCompletedFoxSemidirect C X H) :
    (zcCompletedFoxSemidirectMapTargetHom (X := X) C hC η a).left =
      zcFreeFoxCoordinatesMap (X := X) C hC η a.left

This declaration identifies the left component of the continuous target map on completed Fox semidirect products.

Show Lean proof

Theorem FoxDifferential.zcCompletedFoxSemidirectMapTargetHom_right

omit [DecidableEq X] in
@[simp]
theorem zcCompletedFoxSemidirectMapTargetHom_right
    (η : H →ₜ* K) (a : ZCCompletedFoxSemidirect C X H) :
    (zcCompletedFoxSemidirectMapTargetHom (X := X) C hC η a).right = η a.right

This declaration identifies the right component of the continuous target map on completed Fox semidirect products.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectLift_mapTarget

omit [Fintype X] in
theorem freeProCZCCompletedFoxSemidirectLift_mapTarget
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (htargetH :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (htargetK :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X K))
    (η : H →ₜ* K) (φ : X → H) (g : F) :
    zcCompletedFoxSemidirectMapTarget (X := X) C hC η
        (freeProCZCCompletedFoxSemidirectLift
          (C := C) hι htargetH φ
          (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ) g) =
      freeProCZCCompletedFoxSemidirectLift
        (C := C) hι htargetK (fun x : X => η (φ x))
        (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X K (fun x :
            X => η (φ x))) g

Target naturality of the canonical completed Fox semidirect lift.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectLiftHom_mapTarget

omit [Fintype X] in
theorem freeProCZCCompletedFoxSemidirectLiftHom_mapTarget
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (htargetH :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (htargetK :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X K))
    (η : H →ₜ* K) (φ : X → H) :
    (zcCompletedFoxSemidirectMapTargetHom (X := X) C hC η).comp
        (freeProCZCCompletedFoxSemidirectLiftHom
          (C := C) hι htargetH φ
          (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ)) =
      freeProCZCCompletedFoxSemidirectLiftHom
        (C := C) hι htargetK (fun x : X => η (φ x))
        (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X K (fun x :
            X => η (φ x)))

Continuous-hom form of target naturality for the canonical completed Fox semidirect lift.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxRightHom_mapTarget

omit [Fintype X] in
theorem freeProCZCCompletedFoxRightHom_mapTarget
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (htargetH :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (htargetK :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X K))
    (η : H →ₜ* K) (φ : X → H) :
    freeProCZCCompletedFoxRightHom
        (C := C) hι htargetK (fun x : X => η (φ x))
        (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X K (fun x :
            X => η (φ x))) =
      η.toMonoidHom.comp
        (freeProCZCCompletedFoxRightHom
          (C := C) hι htargetH φ
          (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ))

Target naturality of the right homomorphism of the canonical completed Fox lift.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxDerivativeVector_mapTarget

omit [Fintype X] in
theorem freeProCZCCompletedFoxDerivativeVector_mapTarget
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (htargetH :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (htargetK :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X K))
    (η : H →ₜ* K) (φ : X → H) (g : F) :
    freeProCZCCompletedFoxDerivativeVector
        (C := C) hι htargetK (fun x : X => η (φ x))
        (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X K (fun x :
            X => η (φ x))) g =
      zcFreeFoxCoordinatesMap (X := X) C hC η
        (freeProCZCCompletedFoxDerivativeVector
          (C := C) hι htargetH φ
          (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ) g)

Target naturality of the derivative vector of the canonical completed Fox lift.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxDerivativeVector_mapTarget_apply

omit [Fintype X] in
theorem freeProCZCCompletedFoxDerivativeVector_mapTarget_apply
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (htargetH :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (htargetK :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X K))
    (η : H →ₜ* K) (φ : X → H) (g : F) (x : X) :
    freeProCZCCompletedFoxDerivativeVector
        (C := C) hι htargetK (fun x : X => η (φ x))
        (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X K (fun x :
            X => η (φ x))) g x =
      zcCompletedGroupAlgebraMap C hC η
        (freeProCZCCompletedFoxDerivativeVector
          (C := C) hι htargetH φ
          (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ) g x)

Target naturality for the canonical completed Fox derivative holds componentwise.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxBoundary_mapTarget_of_derivativeVector

theorem freeProCZCCompletedFoxBoundary_mapTarget_of_derivativeVector
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (htargetH :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (htargetK :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X K))
    (η : H →ₜ* K) (φ : X → H) (g : F) :
    zcCompletedGroupAlgebraMap C hC η
        (freeProCZCCompletedFoxBoundary C φ
          (freeProCZCCompletedFoxDerivativeVector
            (C := C) hι htargetH φ
            (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ) g)) =
      freeProCZCCompletedFoxBoundary C (fun x : X => η (φ x))
        (freeProCZCCompletedFoxDerivativeVector
          (C := C) hι htargetK (fun x : X => η (φ x))
          (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X K (fun x
              : X => η (φ x))) g)

Target naturality for the source-shaped boundary applied to the canonical completed Fox derivative vector.

Show Lean proof

ProCGroups.FoxDifferential.Completed.Continuous.Naturality

Declarations