ProCGroups.FoxDifferential.Completed.FreeProC.PrimePowerStageProjection

9 Theorems | 2 Definitions

The principal declarations in this module are:

freeProCZCCompletedFoxSemidirectPrimePowerStageMap A completed Fox semidirect projection to the \(\ell^a\) finite stage. - freeProCZCCompletedFoxSemidirectPrimePowerLimitMap Assemble compatible prime-power stage maps into a map to the inverse limit of finite semidirect stages. - freeProCZCCompletedFoxSemidirectPrimePowerStageMap_left The left component of the prime-power finite-stage semidirect map is the prescribed coordinate map applied to the source component. - freeProCZCCompletedFoxSemidirectPrimePowerStageMap_right The right coordinate of the prime-power completed Fox semidirect stage map is the selected target quotient map.

imports

Imported by

ProCGroups.FoxDifferential.Completed.FreeProC

Definition FoxDifferential.freeProCZCCompletedFoxSemidirectPrimePowerStageMap

def freeProCZCCompletedFoxSemidirectPrimePowerStageMap
    (a : ℕ)
    (stageLeft :
      ZCFreeFoxCoordinates C (X := X) (H := H) →+
        foxAlgebraicStageCoordinateVector (X := X) N (ℓ ^ a))
    (stageRight : H →* foxAlgebraicStageTargetQuotient (X := X) N)
    (hscalar :
      ∀ (h : H) (v : ZCFreeFoxCoordinates C (X := X) (H := H)),
        stageLeft (zcGroupLike C H h • v) =
          (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
            (foxAlgebraicStageTargetQuotient (X := X) N) (stageRight h)) •
            stageLeft v) :
    ZCCompletedFoxSemidirect C X H →*
      FoxAlgebraicStageSemidirect (X := X) N (ℓ ^ a) :=
  freeProCZCCompletedFoxSemidirectStageMap
    (C := C) (X := X) (H := H) N (ℓ ^ a) stageLeft stageRight hscalar

A completed Fox semidirect projection to the \(\ell^a\) finite stage.

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectPrimePowerStageMap_left

omit [Fact (0 < ℓ)] [DecidableEq X] [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
    [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
@[simp]
theorem freeProCZCCompletedFoxSemidirectPrimePowerStageMap_left
    (a : ℕ)
    (stageLeft :
      ZCFreeFoxCoordinates C (X := X) (H := H) →+
        foxAlgebraicStageCoordinateVector (X := X) N (ℓ ^ a))
    (stageRight : H →* foxAlgebraicStageTargetQuotient (X := X) N)
    (hscalar :
      ∀ (h : H) (v : ZCFreeFoxCoordinates C (X := X) (H := H)),
        stageLeft (zcGroupLike C H h • v) =
          (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
            (foxAlgebraicStageTargetQuotient (X := X) N) (stageRight h)) •
            stageLeft v)
    (y : ZCCompletedFoxSemidirect C X H) :
    (freeProCZCCompletedFoxSemidirectPrimePowerStageMap
      (C := C) (X := X) (H := H) ℓ N a stageLeft stageRight hscalar y).left =
      stageLeft y.left

The left component of the prime-power finite-stage semidirect map is the prescribed coordinate map applied to the source component.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectPrimePowerStageMap_right

omit [Fact (0 < ℓ)] [DecidableEq X] [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
    [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
@[simp]
theorem freeProCZCCompletedFoxSemidirectPrimePowerStageMap_right
    (a : ℕ)
    (stageLeft :
      ZCFreeFoxCoordinates C (X := X) (H := H) →+
        foxAlgebraicStageCoordinateVector (X := X) N (ℓ ^ a))
    (stageRight : H →* foxAlgebraicStageTargetQuotient (X := X) N)
    (hscalar :
      ∀ (h : H) (v : ZCFreeFoxCoordinates C (X := X) (H := H)),
        stageLeft (zcGroupLike C H h • v) =
          (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
            (foxAlgebraicStageTargetQuotient (X := X) N) (stageRight h)) •
            stageLeft v)
    (y : ZCCompletedFoxSemidirect C X H) :
    (freeProCZCCompletedFoxSemidirectPrimePowerStageMap
      (C := C) (X := X) (H := H) ℓ N a stageLeft stageRight hscalar y).right =
      stageRight y.right

The right coordinate of the prime-power completed Fox semidirect stage map is the selected target quotient map.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectPrimePowerStageMap_mem_finiteBoundaryCycleSet

omit [Fact (0 < ℓ)] [TopologicalSpace (ZCCompletedFoxSemidirect C X H)] [IsTopologicalGroup
    (ZCCompletedFoxSemidirect C X H)] in
omit [DecidableEq X] in
theorem freeProCZCCompletedFoxSemidirectPrimePowerStageMap_mem_finiteBoundaryCycleSet
    [Fintype X]
    (φ : X → H) (a : ℕ)
    (stageLeft :
      ZCFreeFoxCoordinates C (X := X) (H := H) →+
        foxAlgebraicStageCoordinateVector (X := X) N (ℓ ^ a))
    (stageRight : H →* foxAlgebraicStageTargetQuotient (X := X) N)
    (hscalar :
      ∀ (h : H) (v : ZCFreeFoxCoordinates C (X := X) (H := H)),
        stageLeft (zcGroupLike C H h • v) =
          (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
            (foxAlgebraicStageTargetQuotient (X := X) N) (stageRight h)) •
            stageLeft v)
    (stageBoundary :
      ZCCompletedGroupAlgebra C H →+
        foxAlgebraicStageTargetGroupAlgebra (X := X) N (ℓ ^ a))
    (hboundary :
      ∀ v : ZCFreeFoxCoordinates C (X := X) (H := H),
        foxAlgebraicStageFoxBoundary (X := X) N (ℓ ^ a) (stageLeft v) =
          stageBoundary
            (zcFreeGroupFoxBoundary C (FreeGroup.lift φ) v))
    {y : ZCCompletedFoxSemidirect C X H}
    (hy : y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ) :
    freeProCZCCompletedFoxSemidirectPrimePowerStageMap
        (C := C) (X := X) (H := H) ℓ N a stageLeft stageRight hscalar y ∈
      foxAlgebraicStageSemidirectBoundaryCycleSet (X := X) N (ℓ ^ a)

Boundary-cycle preservation for a prime-power completed-to-finite stage map.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectPrimePowerStageMap_kernelWordPoint

omit [Fact (0 < ℓ)] [TopologicalSpace (ZCCompletedFoxSemidirect C X H)] [IsTopologicalGroup
    (ZCCompletedFoxSemidirect C X H)] in
theorem freeProCZCCompletedFoxSemidirectPrimePowerStageMap_kernelWordPoint
    (φ : X → H) (a : ℕ)
    (stageLeft :
      ZCFreeFoxCoordinates C (X := X) (H := H) →+
        foxAlgebraicStageCoordinateVector (X := X) N (ℓ ^ a))
    (stageRight : H →* foxAlgebraicStageTargetQuotient (X := X) N)
    (hscalar :
      ∀ (h : H) (v : ZCFreeFoxCoordinates C (X := X) (H := H)),
        stageLeft (zcGroupLike C H h • v) =
          (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
            (foxAlgebraicStageTargetQuotient (X := X) N) (stageRight h)) •
            stageLeft v)
    (hderivative :
      ∀ w : FreeGroup X,
        stageLeft
          (zcFreeGroupFoxDerivativeVector C
            (FreeGroup.lift φ) w) =
          foxAlgebraicStageDerivativeVector (X := X) N (ℓ ^ a) w)
    (w : FreeGroup X) :
    freeProCZCCompletedFoxSemidirectPrimePowerStageMap
        (C := C) (X := X) (H := H) ℓ N a stageLeft stageRight hscalar
        (freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w) =
      foxAlgebraicStageSemidirectKernelWordPoint (X := X) N (ℓ ^ a) w

Kernel-word points project to kernel-word points at prime-power finite stages.

Show Lean proof

Definition FoxDifferential.freeProCZCCompletedFoxSemidirectPrimePowerLimitMap

def freeProCZCCompletedFoxSemidirectPrimePowerLimitMap
    (π : ∀ a : ℕ,
      ZCCompletedFoxSemidirect C X H →*
        FoxAlgebraicStageSemidirect (X := X) N (ℓ ^ a))
    (hπ : ∀ {a b : ℕ} (hab : a ≤ b),
      (foxAlgebraicStagePrimePowerSemidirectTransition (ℓ := ℓ) (X := X) N hab).comp (π b) =
        π a) :
    ZCCompletedFoxSemidirect C X H →*
      FoxAlgebraicStagePrimePowerSemidirectLimit (ℓ := ℓ) (X := X) N where
  toFun y :=
    ⟨fun a => π a y, by
      intro a b hab
      exact congrArg (fun f => f y) (hπ hab)⟩
  map_one' := by
    apply Subtype.ext
    funext a
    exact map_one (π a)
  map_mul' y z := by
    apply Subtype.ext
    funext a
    exact map_mul (π a) y z

Assemble compatible prime-power stage maps into a map to the inverse limit of finite semidirect stages.

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectPrimePowerLimitMap_projection

omit [Fact (0 < ℓ)] [DecidableEq X] [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
    [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
@[simp]
theorem freeProCZCCompletedFoxSemidirectPrimePowerLimitMap_projection
    (π : ∀ a : ℕ,
      ZCCompletedFoxSemidirect C X H →*
        FoxAlgebraicStageSemidirect (X := X) N (ℓ ^ a))
    (hπ : ∀ {a b : ℕ} (hab : a ≤ b),
      (foxAlgebraicStagePrimePowerSemidirectTransition (ℓ := ℓ) (X := X) N hab).comp (π b) =
        π a)
    (a : ℕ) (y : ZCCompletedFoxSemidirect C X H) :
    foxAlgebraicStagePrimePowerSemidirectLimitProjection (ℓ := ℓ) (X := X) N a
        (freeProCZCCompletedFoxSemidirectPrimePowerLimitMap
          (C := C) (X := X) (H := H) ℓ N π hπ y) =
      π a y

Projection after the free pro-\(C\) \(\mathbb{Z}_C\)-completed Fox semidirect prime-power limit map is computed by the finite-stage coordinate map.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectPrimePowerLimitMap_mem_boundaryCycleSet

omit [Fact (0 < ℓ)] [DecidableEq X] [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
    [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
theorem freeProCZCCompletedFoxSemidirectPrimePowerLimitMap_mem_boundaryCycleSet
    [Fintype X] (φ : X → H)
    (π : ∀ a : ℕ,
      ZCCompletedFoxSemidirect C X H →*
        FoxAlgebraicStageSemidirect (X := X) N (ℓ ^ a))
    (hπ : ∀ {a b : ℕ} (hab : a ≤ b),
      (foxAlgebraicStagePrimePowerSemidirectTransition (ℓ := ℓ) (X := X) N hab).comp (π b) =
        π a)
    (hboundary_stage :
      ∀ y : ZCCompletedFoxSemidirect C X H,
        y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ →
          ∀ a : ℕ, π a y ∈ foxAlgebraicStageSemidirectBoundaryCycleSet (X := X) N (ℓ ^ a))
    {y : ZCCompletedFoxSemidirect C X H}
    (hy : y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ) :
    freeProCZCCompletedFoxSemidirectPrimePowerLimitMap
        (C := C) (X := X) (H := H) ℓ N π hπ y ∈
      foxAlgebraicStagePrimePowerSemidirectLimitBoundaryCycleSet (ℓ := ℓ) (X := X) N

A completed boundary-cycle point maps to a stagewise boundary-cycle point in the prime-power inverse limit.

Show Lean proof

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectPrimePowerLimitMap_kernelWordPoint

omit [Fact (0 < ℓ)] [TopologicalSpace (ZCCompletedFoxSemidirect C X H)] [IsTopologicalGroup
    (ZCCompletedFoxSemidirect C X H)] in
theorem freeProCZCCompletedFoxSemidirectPrimePowerLimitMap_kernelWordPoint
    (φ : X → H)
    (π : ∀ a : ℕ,
      ZCCompletedFoxSemidirect C X H →*
        FoxAlgebraicStageSemidirect (X := X) N (ℓ ^ a))
    (hπ : ∀ {a b : ℕ} (hab : a ≤ b),
      (foxAlgebraicStagePrimePowerSemidirectTransition (ℓ := ℓ) (X := X) N hab).comp (π b) =
        π a)
    (hkernel_word_projection :
      ∀ a : ℕ, ∀ w : FreeGroup X,
        π a (freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w) =
          foxAlgebraicStageSemidirectKernelWordPoint (X := X) N (ℓ ^ a) w)
    (w : FreeGroup X) :
    freeProCZCCompletedFoxSemidirectPrimePowerLimitMap
        (C := C) (X := X) (H := H) ℓ N π hπ
        (freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w) =
      foxAlgebraicStagePrimePowerSemidirectKernelWordPointLimit (ℓ := ℓ) (X := X) N w

Kernel-word points commute with the prime-power inverse-limit map.

Show Lean proof

Theorem FoxDifferential.boundaryCycles_subset_kernelClosure_of_ppStageMaps

omit [Fact (0 < ℓ)] in
theorem boundaryCycles_subset_kernelClosure_of_ppStageMaps
    [Fintype X] (φ : X → H)
    (stageLeft : ∀ a : ℕ,
      ZCFreeFoxCoordinates C (X := X) (H := H) →+
        foxAlgebraicStageCoordinateVector (X := X) N (ℓ ^ a))
    (stageRight : ∀ _a : ℕ,
      H →* foxAlgebraicStageTargetQuotient (X := X) N)
    (hscalar :
      ∀ a : ℕ, ∀ (h : H)
        (v : ZCFreeFoxCoordinates C (X := X) (H := H)),
        stageLeft a (zcGroupLike C H h • v) =
          (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
            (foxAlgebraicStageTargetQuotient (X := X) N) (stageRight a h)) •
            stageLeft a v)
    (hidentity_basis :
      HasIdentityQuotientKernelNeighbourhoodBasis
        (Y := ZCCompletedFoxSemidirect C X H)
        (fun a : ℕ =>
          freeProCZCCompletedFoxSemidirectPrimePowerStageMap
            (C := C) (X := X) (H := H) ℓ N a
            (stageLeft a) (stageRight a) (hscalar a)))
    (stageBoundary : ∀ a : ℕ,
      ZCCompletedGroupAlgebra C H →+
        foxAlgebraicStageTargetGroupAlgebra (X := X) N (ℓ ^ a))
    (hboundary :
      ∀ a : ℕ,
        ∀ v : ZCFreeFoxCoordinates C (X := X) (H := H),
          foxAlgebraicStageFoxBoundary (X := X) N (ℓ ^ a) (stageLeft a v) =
            stageBoundary a
              (zcFreeGroupFoxBoundary C (FreeGroup.lift φ) v))
    (hN_kernel : ∀ {w : FreeGroup X}, w ∈ N → FreeGroup.lift φ w = 1)
    (hderivative :
      ∀ a : ℕ, ∀ w : FreeGroup X,
        stageLeft a
          (zcFreeGroupFoxDerivativeVector C
            (FreeGroup.lift φ) w) =
          foxAlgebraicStageDerivativeVector (X := X) N (ℓ ^ a) w) :
    freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
      closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ)

Completed Fox density from prime-power stage maps and the finite relation-ideal derivative theorem.

Show Lean proof

Theorem FoxDifferential.boundaryCycles_subset_closedGenTarget_of_ppStageMaps

omit [Fact (0 < ℓ)] in
theorem boundaryCycles_subset_closedGenTarget_of_ppStageMaps
    [Fintype X] (φ : X → H)
    (stageLeft : ∀ a : ℕ,
      ZCFreeFoxCoordinates C (X := X) (H := H) →+
        foxAlgebraicStageCoordinateVector (X := X) N (ℓ ^ a))
    (stageRight : ∀ _a : ℕ,
      H →* foxAlgebraicStageTargetQuotient (X := X) N)
    (hscalar :
      ∀ a : ℕ, ∀ (h : H)
        (v : ZCFreeFoxCoordinates C (X := X) (H := H)),
        stageLeft a (zcGroupLike C H h • v) =
          (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
            (foxAlgebraicStageTargetQuotient (X := X) N) (stageRight a h)) •
            stageLeft a v)
    (hidentity_basis :
      HasIdentityQuotientKernelNeighbourhoodBasis
        (Y := ZCCompletedFoxSemidirect C X H)
        (fun a : ℕ =>
          freeProCZCCompletedFoxSemidirectPrimePowerStageMap
            (C := C) (X := X) (H := H) ℓ N a
            (stageLeft a) (stageRight a) (hscalar a)))
    (stageBoundary : ∀ a : ℕ,
      ZCCompletedGroupAlgebra C H →+
        foxAlgebraicStageTargetGroupAlgebra (X := X) N (ℓ ^ a))
    (hboundary :
      ∀ a : ℕ,
        ∀ v : ZCFreeFoxCoordinates C (X := X) (H := H),
          foxAlgebraicStageFoxBoundary (X := X) N (ℓ ^ a) (stageLeft a v) =
            stageBoundary a
              (zcFreeGroupFoxBoundary C (FreeGroup.lift φ) v))
    (hN_kernel : ∀ {w : FreeGroup X}, w ∈ N → FreeGroup.lift φ w = 1)
    (hderivative :
      ∀ a : ℕ, ∀ w : FreeGroup X,
        stageLeft a
          (zcFreeGroupFoxDerivativeVector C
            (FreeGroup.lift φ) w) =
          foxAlgebraicStageDerivativeVector (X := X) N (ℓ ^ a) w) :
    freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
      ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H)) : Set
          (ZCCompletedFoxSemidirect C X H))

Closed-generated-target version of the prime-power stage-map density theorem.

Show Lean proof

ProCGroups.FoxDifferential.Completed.FreeProC.PrimePowerStageProjection

Declarations