Module

SourceProjection.lean

Nyll.ProCGroups.FoxDifferential.Completed.Comparison.SourceProjection

5 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — comparison — source projection

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.

Imports2

Imported by1

Nyll.ProCGroups.FoxDifferential.Completed.Comparison.All

theorem

freeProCZCCompletedFoxBoundary_finiteStageProjection

L41 ↗

FoxDifferential.freeProCZCCompletedFoxBoundary_finiteStageProjection

Documentation

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

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section SourceBoundaryProjection
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {X H : Type u} [Fintype X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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)

theorem

freeProCZCCompletedFoxBoundary_finiteStageProjection_stage

L58 ↗

FoxDifferential.freeProCZCCompletedFoxBoundary_finiteStageProjection_stage

Documentation

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

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section SourceBoundaryProjection
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {X H : Type u} [Fintype X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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)

theorem

zcFreeFoxCoordinatesMap_finiteStageProjection

L84 ↗

FoxDifferential.zcFreeFoxCoordinatesMap_finiteStageProjection

Documentation

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

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section TargetProjectionNaturality
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
variable {X H K : Type u} [Fintype X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
omit [Fintype X] in

Lean source · statement

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

theorem

freeProCZCCompletedFoxBoundary_mapTarget_finiteStageProjection_stage

L97 ↗

FoxDifferential.freeProCZCCompletedFoxBoundary_mapTarget_finiteStageProjection_stage

Documentation

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

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section TargetProjectionNaturality
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
variable {X H K : Type u} [Fintype X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [Group K] [TopologicalSpace K] [IsTopologicalGroup K]

Lean source · statement

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)

theorem

finite_completedGroupAlgebraStage

L128 ↗

FoxDifferential.ZCFiniteStageQuotientBundle.finite_completedGroupAlgebraStage

Documentation

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.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section GenuineFiniteQuotientStage
variable {X : Type u} [DecidableEq X]
variable {N : Subgroup (FreeGroup X)} [N.Normal]
omit [DecidableEq X] in

Lean source · full declaration

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) := by
  let : TopologicalSpace B.Target := B.targetTopology
  let : IsTopologicalGroup B.Target := B.targetIsTopologicalGroup
  let : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
  exact
    finite_modNCompletedGroupAlgebraStageInClass
      (n := j.1.modulus) (G := B.Target) C j.2

Module documentation

Fox differential: completed — comparison — source projection

Declarations

freeProCZCCompletedFoxBoundary_finiteStageProjection

freeProCZCCompletedFoxBoundary_finiteStageProjection_stage

zcFreeFoxCoordinatesMap_finiteStageProjection

freeProCZCCompletedFoxBoundary_mapTarget_finiteStageProjection_stage

finite_completedGroupAlgebraStage