NYLL
Module

Basic.lean

Nyll.ProCGroups.FoxDifferential.Completed.Continuous.Universal.Basic
30 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — continuous — universal — basic

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.

Imports3
Imported by2

Declarations

def

zcUniversalDifferentialFinalTopology

L53 ↗
FoxDifferential.zcUniversalDifferentialFinalTopology
Documentation

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.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section UniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
def zcUniversalDifferentialFinalTopology (ψ : G →* H) :
    TopologicalSpace (ZCCompletedDifferentialModule C ψ)
theorem

continuous_zcUniversalDifferential_universalTopology

L58 ↗
FoxDifferential.continuous_zcUniversalDifferential_universalTopology
Documentation

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

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section UniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem continuous_zcUniversalDifferential_universalTopology
    (ψ : G →* H) :
    @Continuous G (ZCCompletedDifferentialModule C ψ) inferInstance
      (zcUniversalDifferentialFinalTopology C ψ)
      (zcUniversalDifferential C ψ)
theorem

continuous_zcCompletedDifferentialModuleLift_universalTopology_iff

L72 ↗
FoxDifferential.continuous_zcCompletedDifferentialModuleLift_universalTopology_iff
Documentation

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

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section UniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
variable [TopologicalSpace A]
Lean source · statement
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
instance

zcCompletedDifferentialModuleUniversalTopologyInst

L100 ↗
FoxDifferential.zcCompletedDifferentialModuleUniversalTopologyInst
Documentation

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

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section UniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
variable [TopologicalSpace A]
section ContinuousLinearMapPackaging
variable (ψ : G →* H)
Lean source · statement
instance zcCompletedDifferentialModuleUniversalTopologyInst :
    TopologicalSpace (ZCCompletedDifferentialModule C ψ)
def

zcCompletedDifferentialModuleLiftUniversalContinuousLinearMap

L108 ↗
FoxDifferential.zcCompletedDifferentialModuleLiftUniversalContinuousLinearMap
Documentation

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

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section UniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
variable [TopologicalSpace A]
section ContinuousLinearMapPackaging
variable (ψ : G →* H)
Lean source · full declaration
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
theorem

zcCompletedDifferentialModuleLiftUniversalContinuousLinearMap_apply

L120 ↗
FoxDifferential.zcCompletedDifferentialModuleLiftUniversalContinuousLinearMap_apply
Documentation

Evaluation of the universal-topology continuous lift.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section UniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
variable [TopologicalSpace A]
section ContinuousLinearMapPackaging
variable (ψ : G →* H)
Lean source · statement
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
def

zcCompletedContinuousCrossedDifferentialEquivContinuousLinearMap

L136 ↗
FoxDifferential.zcCompletedContinuousCrossedDifferentialEquivContinuousLinearMap
Documentation

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.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section UniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
variable [TopologicalSpace A]
section ContinuousLinearMapPackaging
variable (ψ : G →* H)
Lean source · full declaration
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
theorem

continuous_zcToCompletedGroupAlgebra_universalTopology

L187 ↗
FoxDifferential.continuous_zcToCompletedGroupAlgebra_universalTopology
Documentation

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.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section UniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
variable [TopologicalSpace A]
Lean source · statement
theorem continuous_zcToCompletedGroupAlgebra_universalTopology
    (ψ : G →* H) (hψ : Continuous ψ) :
    @Continuous (ZCCompletedDifferentialModule C ψ) (ZCCompletedGroupAlgebra C H)
      (zcUniversalDifferentialFinalTopology C ψ) inferInstance
      (zcToCompletedGroupAlgebra C ψ)
def

zcCompletedDifferentialModuleFreeTopology

L210 ↗
FoxDifferential.zcCompletedDifferentialModuleFreeTopology
Documentation

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

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section FreeGroupUniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [Fintype X] [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
def zcCompletedDifferentialModuleFreeTopology (ψ : FreeGroup X →* H) :
    TopologicalSpace (ZCCompletedDifferentialModule C ψ)
theorem

continuous_zcDifferentialToFreeFoxCoordinates_freeTopology

L219 ↗
FoxDifferential.continuous_zcDifferentialToFreeFoxCoordinates_freeTopology
Documentation

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

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section FreeGroupUniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [Fintype X] [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [Fintype X] in
Lean source · statement
theorem continuous_zcDifferentialToFreeFoxCoordinates_freeTopology
    (ψ : FreeGroup X →* H) :
    @Continuous (ZCCompletedDifferentialModule C ψ)
      (ZCFreeFoxCoordinates C (X := X) (H := H))
      (zcCompletedDifferentialModuleFreeTopology C ψ) inferInstance
      (zcDifferentialToFreeFoxCoordinates C ψ)
theorem

continuous_zcFreeFoxCoordinatesLinearMap_freeTopology

L231 ↗
FoxDifferential.continuous_zcFreeFoxCoordinatesLinearMap_freeTopology
Documentation

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

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section FreeGroupUniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [Fintype X] [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem continuous_zcFreeFoxCoordinatesLinearMap_freeTopology
    (ψ : FreeGroup X →* H) :
    @Continuous (ZCFreeFoxCoordinates C (X := X) (H := H))
      (ZCCompletedDifferentialModule C ψ) inferInstance
      (zcCompletedDifferentialModuleFreeTopology C ψ)
      (zcFreeFoxCoordinatesLinearMap C ψ)
instance

instContinuousSMulZCFreeFoxCoordinates

L253 ↗
FoxDifferential.instContinuousSMulZCFreeFoxCoordinates
Documentation

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

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section FreeGroupUniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [Fintype X] [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
instance instContinuousSMulZCFreeFoxCoordinates :
    ContinuousSMul (ZCCompletedGroupAlgebra C H)
      (ZCFreeFoxCoordinates C (X := X) (H := H))
instance

instContinuousSMulZCCompletedDifferentialModuleFreeTopology

L260 ↗
FoxDifferential.instContinuousSMulZCCompletedDifferentialModuleFreeTopology
Documentation

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

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section FreeGroupUniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [Fintype X] [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
instance instContinuousSMulZCCompletedDifferentialModuleFreeTopology
    (ψ : FreeGroup X →* H) :
    @ContinuousSMul (ZCCompletedGroupAlgebra C H)
      (ZCCompletedDifferentialModule C ψ)
      inferInstance inferInstance (zcCompletedDifferentialModuleFreeTopology C ψ)
def

zcFreeCrossedDifferentialCoordinateLift

L273 ↗
FoxDifferential.zcFreeCrossedDifferentialCoordinateLift
Documentation

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

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section FreeGroupUniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [Fintype X] [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
Lean source · full declaration
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]
theorem

zcFreeCrossedDifferentialCoordinateLift_apply

L285 ↗
FoxDifferential.zcFreeCrossedDifferentialCoordinateLift_apply
Documentation

Evaluation formula for the coordinate lift attached to generator values.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section FreeGroupUniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [Fintype X] [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
omit [DecidableEq X] in
Lean source · statement
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)
theorem

zcFreeCrossedDifferentialCoordinateLift_derivativeVector

L297 ↗
FoxDifferential.zcFreeCrossedDifferentialCoordinateLift_derivativeVector
Documentation

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

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section FreeGroupUniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [Fintype X] [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
Lean source · statement
theorem zcFreeCrossedDifferentialCoordinateLift_derivativeVector
    (ψ : FreeGroup X →* H)
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
    (w : FreeGroup X) :
    zcFreeCrossedDifferentialCoordinateLift (H := H) C delta
        (zcFreeGroupFoxDerivativeVector C ψ w) =
      delta w
theorem

zcFreeCrossedDifferentialCoordinateLift_eq_completedLift_comp_coordinates

L338 ↗
FoxDifferential.zcFreeCrossedDifferentialCoordinateLift_eq_completedLift_comp_coordinates
Documentation

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

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section FreeGroupUniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [Fintype X] [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
omit [DecidableEq X] in
Lean source · statement
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 ψ)
theorem

zcCompletedDifferentialModuleLift_eq_coordinateLift_comp

L362 ↗
FoxDifferential.zcCompletedDifferentialModuleLift_eq_coordinateLift_comp
Documentation

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

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section FreeGroupUniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [Fintype X] [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
Lean source · statement
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 ψ)
theorem

continuous_zcCompletedDifferentialModuleLift_freeTopology_iff

L397 ↗
FoxDifferential.continuous_zcCompletedDifferentialModuleLift_freeTopology_iff
Documentation

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.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section FreeGroupUniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [Fintype X] [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
variable [TopologicalSpace A]
variable {C} in
Lean source · statement
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)
def

zcCompletedDifferentialModuleFreeTopologyInst

L435 ↗
FoxDifferential.zcCompletedDifferentialModuleFreeTopologyInst
Documentation

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

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section FreeGroupUniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [Fintype X] [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
variable [TopologicalSpace A]
variable {C} in
section ContinuousLinearMapPackaging
variable (ψ : FreeGroup X →* H)
Lean source · statement
def zcCompletedDifferentialModuleFreeTopologyInst :
    TopologicalSpace (ZCCompletedDifferentialModule C ψ)
def

zcDifferentialToFreeFoxCoordinatesContinuousLinearMap

L442 ↗
FoxDifferential.zcDifferentialToFreeFoxCoordinatesContinuousLinearMap
Documentation

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

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section FreeGroupUniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [Fintype X] [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
variable [TopologicalSpace A]
variable {C} in
section ContinuousLinearMapPackaging
variable (ψ : FreeGroup X →* H)
attribute [local instance] zcCompletedDifferentialModuleFreeTopologyInst
Lean source · full declaration
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 ψ
theorem

zcDifferentialToFreeFoxCoordinatesContinuousLinearMap_apply

L451 ↗
FoxDifferential.zcDifferentialToFreeFoxCoordinatesContinuousLinearMap_apply
Documentation

Evaluation of the continuous completed coordinate map.

Source context 15 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section FreeGroupUniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [Fintype X] [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
variable [TopologicalSpace A]
variable {C} in
section ContinuousLinearMapPackaging
variable (ψ : FreeGroup X →* H)
attribute [local instance] zcCompletedDifferentialModuleFreeTopologyInst
omit [Fintype X] in
Lean source · statement
theorem zcDifferentialToFreeFoxCoordinatesContinuousLinearMap_apply
    (m : ZCCompletedDifferentialModule C ψ) :
    zcDifferentialToFreeFoxCoordinatesContinuousLinearMap (X := X) (H := H) C ψ m =
      zcDifferentialToFreeFoxCoordinates C ψ m
def

zcFreeFoxCoordinatesContinuousLinearMap

L460 ↗
FoxDifferential.zcFreeFoxCoordinatesContinuousLinearMap
Documentation

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

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section FreeGroupUniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [Fintype X] [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
variable [TopologicalSpace A]
variable {C} in
section ContinuousLinearMapPackaging
variable (ψ : FreeGroup X →* H)
attribute [local instance] zcCompletedDifferentialModuleFreeTopologyInst
Lean source · full declaration
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 ψ
theorem

zcFreeFoxCoordinatesContinuousLinearMap_apply

L468 ↗
FoxDifferential.zcFreeFoxCoordinatesContinuousLinearMap_apply
Documentation

Evaluation of the continuous coordinate-to-universal map.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section FreeGroupUniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [Fintype X] [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
variable [TopologicalSpace A]
variable {C} in
section ContinuousLinearMapPackaging
variable (ψ : FreeGroup X →* H)
attribute [local instance] zcCompletedDifferentialModuleFreeTopologyInst
Lean source · statement
theorem zcFreeFoxCoordinatesContinuousLinearMap_apply
    (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
    zcFreeFoxCoordinatesContinuousLinearMap (X := X) (H := H) C ψ v =
      zcFreeFoxCoordinatesLinearMap C ψ v
def

zcFreeCrossedDifferentialCoordinateContinuousLinearMap

L475 ↗
FoxDifferential.zcFreeCrossedDifferentialCoordinateContinuousLinearMap
Documentation

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

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section FreeGroupUniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [Fintype X] [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
variable [TopologicalSpace A]
variable {C} in
section ContinuousLinearMapPackaging
variable (ψ : FreeGroup X →* H)
attribute [local instance] zcCompletedDifferentialModuleFreeTopologyInst
Lean source · full declaration
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
theorem

zcFreeCrossedDifferentialCoordinateContinuousLinearMap_apply

L486 ↗
FoxDifferential.zcFreeCrossedDifferentialCoordinateContinuousLinearMap_apply
Documentation

Evaluation of the continuous coordinate lift attached to generator values.

Source context 15 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section FreeGroupUniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [Fintype X] [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
variable [TopologicalSpace A]
variable {C} in
section ContinuousLinearMapPackaging
variable (ψ : FreeGroup X →* H)
attribute [local instance] zcCompletedDifferentialModuleFreeTopologyInst
omit [DecidableEq X] in
Lean source · statement
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)
def

zcCompletedDifferentialModuleLiftContinuousLinearMap

L498 ↗
FoxDifferential.zcCompletedDifferentialModuleLiftContinuousLinearMap
Documentation

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

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section FreeGroupUniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [Fintype X] [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
variable [TopologicalSpace A]
variable {C} in
section ContinuousLinearMapPackaging
variable (ψ : FreeGroup X →* H)
attribute [local instance] zcCompletedDifferentialModuleFreeTopologyInst
Lean source · full declaration
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
theorem

zcCompletedDifferentialModuleLiftContinuousLinearMap_apply

L510 ↗
FoxDifferential.zcCompletedDifferentialModuleLiftContinuousLinearMap_apply
Documentation

Evaluation of the continuous representing universal lift.

Source context 15 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section FreeGroupUniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [Fintype X] [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
variable [TopologicalSpace A]
variable {C} in
section ContinuousLinearMapPackaging
variable (ψ : FreeGroup X →* H)
attribute [local instance] zcCompletedDifferentialModuleFreeTopologyInst
omit [Fintype X] in
Lean source · statement
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
def

zcCompletedDifferentialModuleLiftContinuousLinearMapOfCoordinate

L523 ↗
FoxDifferential.zcCompletedDifferentialModuleLiftContinuousLinearMapOfCoordinate
Documentation

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

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section FreeGroupUniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [Fintype X] [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
variable [TopologicalSpace A]
variable {C} in
section ContinuousLinearMapPackaging
variable (ψ : FreeGroup X →* H)
attribute [local instance] zcCompletedDifferentialModuleFreeTopologyInst
Lean source · statement
def zcCompletedDifferentialModuleLiftContinuousLinearMapOfCoordinate
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
    (hcoord : Continuous (zcFreeCrossedDifferentialCoordinateLift (H := H) C delta)) :
    ZCCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H] A
theorem

zcCompletedDifferentialModuleLiftContinuousLinearMapOfCoordinate_apply

L536 ↗
FoxDifferential.zcCompletedDifferentialModuleLiftContinuousLinearMapOfCoordinate_apply
Documentation

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

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section FreeGroupUniversalTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable {X : Type u} [Fintype X] [DecidableEq X]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
variable [TopologicalSpace A]
variable {C} in
section ContinuousLinearMapPackaging
variable (ψ : FreeGroup X →* H)
attribute [local instance] zcCompletedDifferentialModuleFreeTopologyInst
Lean source · statement
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

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.