Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.Comparison.SourceProjection
ProCGroups/FoxDifferential/Completed/Comparison/SourceProjection

ProCGroups.FoxDifferential.Completed.Comparison.SourceProjection

5 Theorems

The principal declarations in this module are:

  • freeProCZCCompletedFoxBoundary_finiteStageProjection Finite-stage projection of the source-shaped completed Fox boundary map. - freeProCZCCompletedFoxBoundary_finiteStageProjection_stage Finite-stage projection of the source-shaped completed Fox boundary map, with generator boundaries written in the selected finite pro-C quotient. - zcFreeFoxCoordinatesMap_finiteStageProjection Componentwise finite-stage projection formula for target maps on completed Fox coordinates. - freeProCZCCompletedFoxBoundary_mapTarget_finiteStageProjection_stage Finite-stage projection of target naturality for source-shaped completed Fox boundary maps.
imports
Imported by

Declarations

Theorem FoxDifferential.freeProCZCCompletedFoxBoundary_finiteStageProjection 
theorem freeProCZCCompletedFoxBoundary_finiteStageProjection
    (φ : X → H) (v : ZCFreeFoxCoordinates C (X := X) (H := H))
    (j : ZCCompletedGroupAlgebraIndex C H) :
    zcCompletedGroupAlgebraProjection C H j
        (freeProCZCCompletedFoxBoundary C φ v) =
      ∑ x : X,
        zcCompletedGroupAlgebraProjection C H j (v x) *
          zcCompletedGroupAlgebraProjection C H j (zcGroupLike C H (φ x) - 1)

Finite-stage projection of the source-shaped completed Fox boundary map.

Show Lean proof
Theorem FoxDifferential.freeProCZCCompletedFoxBoundary_finiteStageProjection_stage 
theorem freeProCZCCompletedFoxBoundary_finiteStageProjection_stage
    (φ : X → H) (v : ZCFreeFoxCoordinates C (X := X) (H := H))
    (j : ZCCompletedGroupAlgebraIndex C H) :
    zcCompletedGroupAlgebraProjection C H j
        (freeProCZCCompletedFoxBoundary C φ v) =
      ∑ x : X,
        zcCompletedGroupAlgebraProjection C H j (v x) *
          (MonoidAlgebra.of (ModNCompletedCoeff j.1.modulus)
            (CompletedGroupAlgebraQuotientInClass H C j.2)
            (QuotientGroup.mk (φ x)) - 1)

Finite-stage projection of the source-shaped completed Fox boundary map, with generator boundaries written in the selected finite pro-C quotient.

Show Lean proof
Theorem FoxDifferential.zcFreeFoxCoordinatesMap_finiteStageProjection 
omit [Fintype X] in
theorem zcFreeFoxCoordinatesMap_finiteStageProjection
    (η : H →ₜ* K)
    (v : ZCFreeFoxCoordinates C (X := X) (H := H))
    (j : ZCCompletedGroupAlgebraIndex C K) (x : X) :
    zcCompletedGroupAlgebraProjection C K j
        (zcFreeFoxCoordinatesMap (X := X) C hC η v x) =
      zcCompletedGroupAlgebraMapStage C hC η j
        (zcCompletedGroupAlgebraProjection C H
          (j.1, completedGroupAlgebraComapIndexInClass
            (G := H) (H := K) C hC η j.2) (v x))

Componentwise finite-stage projection formula for target maps on completed Fox coordinates.

Show Lean proof
Theorem FoxDifferential.freeProCZCCompletedFoxBoundary_mapTarget_finiteStageProjection_stage 
theorem freeProCZCCompletedFoxBoundary_mapTarget_finiteStageProjection_stage
    (η : H →ₜ* K) (φ : X → H)
    (v : ZCFreeFoxCoordinates C (X := X) (H := H))
    (j : ZCCompletedGroupAlgebraIndex C K) :
    zcCompletedGroupAlgebraProjection C K j
        (zcCompletedGroupAlgebraMap C hC η (freeProCZCCompletedFoxBoundary C φ v)) =
      ∑ x : X,
        zcCompletedGroupAlgebraMapStage C hC η j
          (zcCompletedGroupAlgebraProjection C H
            (j.1, completedGroupAlgebraComapIndexInClass
              (G := H) (H := K) C hC η j.2) (v x)) *
          (MonoidAlgebra.of (ModNCompletedCoeff j.1.modulus)
            (CompletedGroupAlgebraQuotientInClass K C j.2)
            (QuotientGroup.mk (η (φ x))) - 1)

Finite-stage projection of target naturality for source-shaped completed Fox boundary maps.

Show Lean proof
Theorem FoxDifferential.ZCFiniteStageQuotientBundle.finite_completedGroupAlgebraStage 
omit [DecidableEq X] in
theorem ZCFiniteStageQuotientBundle.finite_completedGroupAlgebraStage
    (C : ProCGroups.FiniteGroupClass.{u})
    (B : ZCFiniteStageQuotientBundle N)
    (j : B.Index C) :
    letI : TopologicalSpace B.Target := B.targetTopology
    letI : IsTopologicalGroup B.Target := B.targetIsTopologicalGroup
    Finite (ZCCompletedGroupAlgebraStage C B.Target j)

A quotient bundle certifies that every associated pro-C completed group-algebra stage is actually finite. This is the canonical finite-stage consumer of ZCFiniteStageQuotientBundle; the unbundled comparison lemmas remain purely algebraic.

Show Lean proof