ProCGroups.FoxDifferential.Completed.Continuous.Universal.Basic

16 Theorems | 11 Definitions | 3 Instances

The principal declarations in this module are:

zcUniversalDifferentialFinalTopology The final topology on the completed universal differential module generated by the universal crossed differential \(G \to d_{\mathbb{Z}_C\llbracket H\rrbracket}G\). Unlike the finite-rank free-coordinate topology, this topology is available for an arbitrary source group and states the genuine topological universal property: a map out is continuous exactly when its composite with the universal differential is continuous. - zcCompletedDifferentialModuleLiftUniversalContinuousLinearMap The representing universal lift as a continuous linear map for the final universal topology, from a continuous crossed differential. - continuous_zcUniversalDifferential_universalTopology The universal crossed differential is continuous for the final universal topology. - continuous_zcCompletedDifferentialModuleLift_universalTopology_iff The completed differential-module criterion is equivalent to the corresponding finite-stage coordinate condition.

imports

Imported by

Definition FoxDifferential.zcUniversalDifferentialFinalTopology

@[reducible] def zcUniversalDifferentialFinalTopology (ψ : G →* H) :
    TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
  TopologicalSpace.coinduced (zcUniversalDifferential C ψ) inferInstance

The final topology on the completed universal differential module generated by the universal crossed differential \(G \to d_{\mathbb{Z}_C\llbracket H\rrbracket}G\). Unlike the finite-rank free-coordinate topology, this topology is available for an arbitrary source group and states the genuine topological universal property: a map out is continuous exactly when its composite with the universal differential is continuous.

Theorem FoxDifferential.continuous_zcUniversalDifferential_universalTopology

theorem continuous_zcUniversalDifferential_universalTopology
    (ψ : G →* H) :
    @Continuous G (ZCCompletedDifferentialModule C ψ) inferInstance
      (zcUniversalDifferentialFinalTopology C ψ)
      (zcUniversalDifferential C ψ)

The universal crossed differential is continuous for the final universal topology.

Show Lean proof

Theorem FoxDifferential.continuous_zcCompletedDifferentialModuleLift_universalTopology_iff

theorem continuous_zcCompletedDifferentialModuleLift_universalTopology_iff
    {ψ : G →* H}
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A) :
    @Continuous (ZCCompletedDifferentialModule C ψ) A
        (zcUniversalDifferentialFinalTopology C ψ) inferInstance
        (crossedHomModuleLift (A := A)
          (zcCompletedGroupAlgebraScalar C ψ) delta) ↔
      Continuous delta

The completed differential-module criterion is equivalent to the corresponding finite-stage coordinate condition.

Show Lean proof

Instance FoxDifferential.zcCompletedDifferentialModuleUniversalTopologyInst

instance zcCompletedDifferentialModuleUniversalTopologyInst :
    TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
  zcUniversalDifferentialFinalTopology C ψ

The completed differential module carries the universal finite-stage topology.

Definition FoxDifferential.zcCompletedDifferentialModuleLiftUniversalContinuousLinearMap

def zcCompletedDifferentialModuleLiftUniversalContinuousLinearMap
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
    (hcont : Continuous delta) :
    ZCCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H] A where
  toLinearMap :=
    crossedHomModuleLift (A := A) (zcCompletedGroupAlgebraScalar C ψ) delta
  cont :=
    (continuous_zcCompletedDifferentialModuleLift_universalTopology_iff
      (C := C) (G := G) (H := H) (A := A) (ψ := ψ) delta).2 hcont

The representing universal lift as a continuous linear map for the final universal topology, from a continuous crossed differential.

Theorem FoxDifferential.zcCompletedDifferentialModuleLiftUniversalContinuousLinearMap_apply

@[simp]
theorem zcCompletedDifferentialModuleLiftUniversalContinuousLinearMap_apply
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
    (hcont : Continuous delta)
    (m : ZCCompletedDifferentialModule C ψ) :
    zcCompletedDifferentialModuleLiftUniversalContinuousLinearMap
        (C := C) (G := G) (H := H) (A := A) ψ delta hcont m =
      crossedHomModuleLift (A := A)
        (zcCompletedGroupAlgebraScalar C ψ) delta m

Evaluation of the universal-topology continuous lift.

Show Lean proof

Definition FoxDifferential.zcCompletedContinuousCrossedDifferentialEquivContinuousLinearMap

def zcCompletedContinuousCrossedDifferentialEquivContinuousLinearMap :
    {delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A //
        Continuous delta} ≃
      (ZCCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H] A) where
  toFun delta :=
    zcCompletedDifferentialModuleLiftUniversalContinuousLinearMap
      (C := C) (G := G) (H := H) (A := A) ψ delta.1 delta.2
  invFun f :=
    ⟨{ toFun := fun g => f (zcUniversalDifferential C ψ g)
       map_mul' := by
        intro g h
        change f (zcUniversalDifferential C ψ (g * h)) =
          f (zcUniversalDifferential C ψ g) +
            zcCompletedGroupAlgebraScalar C ψ g •
              f (zcUniversalDifferential C ψ h)
        rw [ScalarCrossedHom.map_mul (zcUniversalDifferential C ψ)]
        simp only [zcCompletedGroupAlgebraScalar_apply, map_add, map_smul] },
      f.cont.comp (continuous_zcUniversalDifferential_universalTopology C ψ)⟩
  left_inv delta := by
    apply Subtype.ext
    apply CrossedHom.ext
    intro g
    exact crossedHomModuleLift_universal
      (A := A) (zcCompletedGroupAlgebraScalar C ψ) delta.1 g
  right_inv f := by
    apply ContinuousLinearMap.ext
    intro m
    let delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A :=
      { toFun := fun g => f (zcUniversalDifferential C ψ g)
        map_mul' := by
          intro g h
          change f (zcUniversalDifferential C ψ (g * h)) =
            f (zcUniversalDifferential C ψ g) +
              zcCompletedGroupAlgebraScalar C ψ g •
                f (zcUniversalDifferential C ψ h)
          rw [ScalarCrossedHom.map_mul (zcUniversalDifferential C ψ)]
          simp only [zcCompletedGroupAlgebraScalar_apply, map_add, map_smul] }
    have hlin :
        f.toLinearMap =
          crossedHomModuleLift (A := A)
            (zcCompletedGroupAlgebraScalar C ψ) delta := by
      apply crossedHomModuleLift_unique
        (A := A) (zcCompletedGroupAlgebraScalar C ψ) delta
      intro g
      rfl
    exact congrFun (congrArg DFunLike.coe hlin.symm) m

Topological universal representation theorem for completed crossed differentials. With the final universal topology on the completed differential module, continuous crossed differentials \(G \to A\) are equivalent to continuous \(\mathbb{Z}_C\llbracket H\rrbracket\)-linear maps out of the completed universal differential module.

Theorem FoxDifferential.continuous_zcToCompletedGroupAlgebra_universalTopology

theorem continuous_zcToCompletedGroupAlgebra_universalTopology
    (ψ : G →* H) (hψ : Continuous ψ) :
    @Continuous (ZCCompletedDifferentialModule C ψ) (ZCCompletedGroupAlgebra C H)
      (zcUniversalDifferentialFinalTopology C ψ) inferInstance
      (zcToCompletedGroupAlgebra C ψ)

The universal boundary map from the completed differential module to Z_C[[H]] is continuous for the final universal topology whenever the target homomorphism is continuous.

Show Lean proof

Definition FoxDifferential.zcCompletedDifferentialModuleFreeTopology

@[reducible] def zcCompletedDifferentialModuleFreeTopology (ψ : FreeGroup X →* H) :
    TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
  TopologicalSpace.induced (zcDifferentialToFreeFoxCoordinates C ψ) inferInstance

The finite-rank topology on the completed universal module, induced by completed Fox coordinates. This is intentionally a named topology, not a global instance.

Theorem FoxDifferential.continuous_zcDifferentialToFreeFoxCoordinates_freeTopology

omit [Fintype X] in
theorem continuous_zcDifferentialToFreeFoxCoordinates_freeTopology
    (ψ : FreeGroup X →* H) :
    @Continuous (ZCCompletedDifferentialModule C ψ)
      (ZCFreeFoxCoordinates C (X := X) (H := H))
      (zcCompletedDifferentialModuleFreeTopology C ψ) inferInstance
      (zcDifferentialToFreeFoxCoordinates C ψ)

The coordinate map out of the completed universal module is continuous for the finite-rank coordinate-induced topology.

Show Lean proof

Theorem FoxDifferential.continuous_zcFreeFoxCoordinatesLinearMap_freeTopology

theorem continuous_zcFreeFoxCoordinatesLinearMap_freeTopology
    (ψ : FreeGroup X →* H) :
    @Continuous (ZCFreeFoxCoordinates C (X := X) (H := H))
      (ZCCompletedDifferentialModule C ψ) inferInstance
      (zcCompletedDifferentialModuleFreeTopology C ψ)
      (zcFreeFoxCoordinatesLinearMap C ψ)

The coordinate-to-universal-module map is continuous for the finite-rank coordinate-induced topology.

Show Lean proof

Instance FoxDifferential.instContinuousSMulZCFreeFoxCoordinates

instance instContinuousSMulZCFreeFoxCoordinates :
    ContinuousSMul (ZCCompletedGroupAlgebra C H)
      (ZCFreeFoxCoordinates C (X := X) (H := H)) :=
  inferInstance

The coordinate module Z_C[[H]]^X has continuous scalar multiplication.

Instance FoxDifferential.instContinuousSMulZCCompletedDifferentialModuleFreeTopology

instance instContinuousSMulZCCompletedDifferentialModuleFreeTopology
    (ψ : FreeGroup X →* H) :
    @ContinuousSMul (ZCCompletedGroupAlgebra C H)
      (ZCCompletedDifferentialModule C ψ)
      inferInstance inferInstance (zcCompletedDifferentialModuleFreeTopology C ψ) :=
  ContinuousSMul.induced (zcDifferentialToFreeFoxCoordinates C ψ)

The finite-rank completed universal module has continuous scalar multiplication for the coordinate-induced topology.

Definition FoxDifferential.zcFreeCrossedDifferentialCoordinateLift

def zcFreeCrossedDifferentialCoordinateLift
    {ψ : FreeGroup X →* H}
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A) :
    ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra C H] A where
  toFun v := ∑ x : X, v x • delta (FreeGroup.of x)
  map_add' v w := by
    simp only [Pi.add_apply, add_smul, Finset.sum_add_distrib]
  map_smul' r v := by
    simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply, Finset.smul_sum, smul_smul]

The finite coordinate linear map attached to the generator values of a completed crossed differential.

Theorem FoxDifferential.zcFreeCrossedDifferentialCoordinateLift_apply

omit [DecidableEq X] in
theorem zcFreeCrossedDifferentialCoordinateLift_apply
    {ψ : FreeGroup X →* H}
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
    (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
    zcFreeCrossedDifferentialCoordinateLift (H := H) C delta v =
      ∑ x : X, v x • delta (FreeGroup.of x)

Evaluation formula for the coordinate lift attached to generator values.

Show Lean proof

Theorem FoxDifferential.zcFreeCrossedDifferentialCoordinateLift_derivativeVector

theorem zcFreeCrossedDifferentialCoordinateLift_derivativeVector
    (ψ : FreeGroup X →* H)
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
    (w : FreeGroup X) :
    zcFreeCrossedDifferentialCoordinateLift (H := H) C delta
        (zcFreeGroupFoxDerivativeVector C ψ w) =
      delta w

The coordinate lift applied to the completed free derivative vector recovers the crossed differential it represents.

Show Lean proof

Theorem FoxDifferential.zcFreeCrossedDifferentialCoordinateLift_eq_completedLift_comp_coordinates

omit [DecidableEq X] in
theorem zcFreeCrossedDifferentialCoordinateLift_eq_completedLift_comp_coordinates
    (ψ : FreeGroup X →* H)
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A) :
    zcFreeCrossedDifferentialCoordinateLift (H := H) C delta =
      (crossedHomModuleLift (A := A)
        (zcCompletedGroupAlgebraScalar C ψ) delta).comp
        (zcFreeFoxCoordinatesLinearMap C ψ)

The coordinate lift is the representing universal-module lift composed with the coordinate-to-module map.

Show Lean proof

Theorem FoxDifferential.zcCompletedDifferentialModuleLift_eq_coordinateLift_comp

theorem zcCompletedDifferentialModuleLift_eq_coordinateLift_comp
    (ψ : FreeGroup X →* H)
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A) :
    crossedHomModuleLift (A := A)
      (zcCompletedGroupAlgebraScalar C ψ) delta =
      (zcFreeCrossedDifferentialCoordinateLift (H := H) C delta).comp
        (zcDifferentialToFreeFoxCoordinates C ψ)

The representing universal-module lift factors through completed Fox coordinates.

Show Lean proof

Theorem FoxDifferential.continuous_zcCompletedDifferentialModuleLift_freeTopology_iff

theorem continuous_zcCompletedDifferentialModuleLift_freeTopology_iff
    {ψ : FreeGroup X →* H}
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A) :
    @Continuous (ZCCompletedDifferentialModule C ψ) A
        (zcCompletedDifferentialModuleFreeTopology C ψ) inferInstance
        (crossedHomModuleLift (A := A)
          (zcCompletedGroupAlgebraScalar C ψ) delta) ↔
      Continuous (zcFreeCrossedDifferentialCoordinateLift (H := H) C delta)

Continuous representation theorem for finite-rank completed universal modules.

With the coordinate-induced topology on ZCCompletedDifferentialModule, the universal linear map representing a completed crossed differential is continuous exactly when the finite coordinate linear map determined by its generator values is continuous.

Show Lean proof

Definition FoxDifferential.zcCompletedDifferentialModuleFreeTopologyInst

@[reducible] def zcCompletedDifferentialModuleFreeTopologyInst :
    TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
  zcCompletedDifferentialModuleFreeTopology C ψ

The free completed differential pre-module carries the finite-stage topology used before quotienting by crossed-differential relations.

Definition FoxDifferential.zcDifferentialToFreeFoxCoordinatesContinuousLinearMap

def zcDifferentialToFreeFoxCoordinatesContinuousLinearMap :
    ZCCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H]
      ZCFreeFoxCoordinates C (X := X) (H := H) where
  toLinearMap := zcDifferentialToFreeFoxCoordinates C ψ
  cont := continuous_zcDifferentialToFreeFoxCoordinates_freeTopology (X := X) (H := H) C ψ

The completed coordinate map as a continuous linear map for the coordinate-induced topology.

Theorem FoxDifferential.zcDifferentialToFreeFoxCoordinatesContinuousLinearMap_apply

omit [Fintype X] in
@[simp]
theorem zcDifferentialToFreeFoxCoordinatesContinuousLinearMap_apply
    (m : ZCCompletedDifferentialModule C ψ) :
    zcDifferentialToFreeFoxCoordinatesContinuousLinearMap (X := X) (H := H) C ψ m =
      zcDifferentialToFreeFoxCoordinates C ψ m

Evaluation of the continuous completed coordinate map.

Show Lean proof

Definition FoxDifferential.zcFreeFoxCoordinatesContinuousLinearMap

def zcFreeFoxCoordinatesContinuousLinearMap :
    ZCFreeFoxCoordinates C (X := X) (H := H) →L[ZCCompletedGroupAlgebra C H]
      ZCCompletedDifferentialModule C ψ where
  toLinearMap := zcFreeFoxCoordinatesLinearMap C ψ
  cont := continuous_zcFreeFoxCoordinatesLinearMap_freeTopology (X := X) (H := H) C ψ

The coordinate-to-universal map as a continuous linear map for the coordinate-induced topology.

Theorem FoxDifferential.zcFreeFoxCoordinatesContinuousLinearMap_apply

@[simp]
theorem zcFreeFoxCoordinatesContinuousLinearMap_apply
    (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
    zcFreeFoxCoordinatesContinuousLinearMap (X := X) (H := H) C ψ v =
      zcFreeFoxCoordinatesLinearMap C ψ v

Evaluation of the continuous coordinate-to-universal map.

Show Lean proof

Definition FoxDifferential.zcFreeCrossedDifferentialCoordinateContinuousLinearMap

def zcFreeCrossedDifferentialCoordinateContinuousLinearMap
    {ψ : FreeGroup X →* H}
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
    (hcont : Continuous (zcFreeCrossedDifferentialCoordinateLift (H := H) C delta)) :
    ZCFreeFoxCoordinates C (X := X) (H := H) →L[ZCCompletedGroupAlgebra C H] A where
  toLinearMap := zcFreeCrossedDifferentialCoordinateLift (H := H) C delta
  cont := hcont

A finite coordinate lift bundled as a continuous linear map, once its continuity is known.

Theorem FoxDifferential.zcFreeCrossedDifferentialCoordinateContinuousLinearMap_apply

omit [DecidableEq X] in
@[simp]
theorem zcFreeCrossedDifferentialCoordinateContinuousLinearMap_apply
    {ψ : FreeGroup X →* H}
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
    (hcont : Continuous (zcFreeCrossedDifferentialCoordinateLift (H := H) C delta))
    (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
    zcFreeCrossedDifferentialCoordinateContinuousLinearMap
        (X := X) (H := H) (A := A) C delta hcont v =
      ∑ x : X, v x • delta (FreeGroup.of x)

Evaluation of the continuous coordinate lift attached to generator values.

Show Lean proof

Definition FoxDifferential.zcCompletedDifferentialModuleLiftContinuousLinearMap

def zcCompletedDifferentialModuleLiftContinuousLinearMap
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
    (hcont : Continuous (crossedHomModuleLift (A := A)
      (zcCompletedGroupAlgebraScalar C ψ) delta)) :
    ZCCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H] A where
  toLinearMap :=
    crossedHomModuleLift (A := A) (zcCompletedGroupAlgebraScalar C ψ) delta
  cont := hcont

The representing universal lift bundled as a continuous linear map, once its continuity for the coordinate-induced topology is known.

Theorem FoxDifferential.zcCompletedDifferentialModuleLiftContinuousLinearMap_apply

omit [Fintype X] in
@[simp]
theorem zcCompletedDifferentialModuleLiftContinuousLinearMap_apply
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
    (hcont : Continuous (crossedHomModuleLift (A := A)
      (zcCompletedGroupAlgebraScalar C ψ) delta))
    (m : ZCCompletedDifferentialModule C ψ) :
    zcCompletedDifferentialModuleLiftContinuousLinearMap
        (X := X) (H := H) (A := A) C ψ delta hcont m =
      crossedHomModuleLift (A := A)
        (zcCompletedGroupAlgebraScalar C ψ) delta m

Evaluation of the continuous representing universal lift.

Show Lean proof

Definition FoxDifferential.zcCompletedDifferentialModuleLiftContinuousLinearMapOfCoordinate

def zcCompletedDifferentialModuleLiftContinuousLinearMapOfCoordinate
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
    (hcoord : Continuous (zcFreeCrossedDifferentialCoordinateLift (H := H) C delta)) :
    ZCCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H] A :=
  zcCompletedDifferentialModuleLiftContinuousLinearMap
    (X := X) (H := H) (A := A) C ψ delta
    ((continuous_zcCompletedDifferentialModuleLift_freeTopology_iff
      (X := X) (H := H) (A := A) (ψ := ψ) delta).2 hcoord)

Continuous representation theorem packaged as a continuous linear map under continuity of the finite coordinate lift.

Theorem FoxDifferential.zcCompletedDifferentialModuleLiftContinuousLinearMapOfCoordinate_apply

@[simp]
theorem zcCompletedDifferentialModuleLiftContinuousLinearMapOfCoordinate_apply
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
    (hcoord : Continuous (zcFreeCrossedDifferentialCoordinateLift (H := H) C delta))
    (m : ZCCompletedDifferentialModule C ψ) :
    zcCompletedDifferentialModuleLiftContinuousLinearMapOfCoordinate
        (X := X) (H := H) (A := A) C ψ delta hcoord m =
      crossedHomModuleLift (A := A)
        (zcCompletedGroupAlgebraScalar C ψ) delta m

Evaluation of the continuous universal lift obtained from a continuous finite coordinate lift.

Show Lean proof

ProCGroups.FoxDifferential.Completed.Continuous.Universal.Basic

Declarations