Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.DifferentialModule.Map.Limit
ProCGroups/FoxDifferential/Completed/DifferentialModule/Map/Limit

ProCGroups.FoxDifferential.Completed.DifferentialModule.Map.Limit

2 Theorems | 1 Definition

The principal declarations in this module are:

  • primePowerCompletedGroupAlgebraMap The ring homomorphism on prime-power completed group algebras induced stagewise by a continuous group homomorphism. - primePowerCompletedGroupAlgebraProjection_map The finite-stage Fox-differential projection is computed by the prime-power completed group-algebra projection formula. - continuous_primePowerCompletedGroupAlgebraMap The completed group-algebra map induced by a continuous homomorphism is continuous for the inverse-limit topologies.
import
Imported by

Declarations

Definition FoxDifferential.primePowerCompletedGroupAlgebraMap 
def primePowerCompletedGroupAlgebraMap
    (ψ : ContinuousMonoidHom G H) :
    PrimePowerCompletedGroupAlgebra ℓ G →+* PrimePowerCompletedGroupAlgebra ℓ H where
  toFun x := ⟨fun i =>
      primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i
        (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
          (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) x), by
    intro i j hij
    let hsource :
        (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) ≤
          (j.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ j.2) :=
      ⟨hij.1, completedGroupAlgebraComapIndex_mono (G := G) (H := H) ψ hij.2⟩
    have hx := x.2
      (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2)
      (j.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ j.2)
      hsource
    change
      primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hsource
          (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
            (j.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ j.2) x) =
        primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
          (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) x at hx
    have hcompat := congrFun
      (congrArg DFunLike.coe
        (primePowerCompletedGroupAlgebraMapStage_compatible
          (ℓ := ℓ) (G := G) (H := H) ψ hij))
      (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
        (j.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ j.2) x)
    rw [RingHom.comp_apply, RingHom.comp_apply] at hcompat
    rw [hx] at hcompat
    simpa [primePowerCompletedGroupAlgebraSystem] using hcompat⟩
  map_one' := by
    apply (primePowerCompletedGroupAlgebraSystem ℓ H).ext
    intro i
    change
      primePowerCompletedGroupAlgebraMapStage
          (ℓ := ℓ) (G := G) (H := H) ψ i 1 = 1
    exact map_one _
  map_mul' := by
    intro x y
    apply (primePowerCompletedGroupAlgebraSystem ℓ H).ext
    intro i
    change
      primePowerCompletedGroupAlgebraMapStage
          (ℓ := ℓ) (G := G) (H := H) ψ i
          (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
            (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) x *
           primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
            (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) y) =
        primePowerCompletedGroupAlgebraMapStage
            (ℓ := ℓ) (G := G) (H := H) ψ i
            (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
              (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) x) *
          primePowerCompletedGroupAlgebraMapStage
            (ℓ := ℓ) (G := G) (H := H) ψ i
            (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
              (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) y)
    exact map_mul _ _ _
  map_zero' := by
    apply (primePowerCompletedGroupAlgebraSystem ℓ H).ext
    intro i
    change
      primePowerCompletedGroupAlgebraMapStage
          (ℓ := ℓ) (G := G) (H := H) ψ i 0 = 0
    exact map_zero _
  map_add' := by
    intro x y
    apply (primePowerCompletedGroupAlgebraSystem ℓ H).ext
    intro i
    change
      primePowerCompletedGroupAlgebraMapStage
          (ℓ := ℓ) (G := G) (H := H) ψ i
          (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
            (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) x +
           primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
            (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) y) =
        primePowerCompletedGroupAlgebraMapStage
            (ℓ := ℓ) (G := G) (H := H) ψ i
            (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
              (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) x) +
          primePowerCompletedGroupAlgebraMapStage
            (ℓ := ℓ) (G := G) (H := H) ψ i
            (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
              (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) y)
    exact map_add _ _ _

The ring homomorphism on prime-power completed group algebras induced stagewise by a continuous group homomorphism.

Theorem FoxDifferential.primePowerCompletedGroupAlgebraProjection_map 
@[simp]
theorem primePowerCompletedGroupAlgebraProjection_map
    (ψ : ContinuousMonoidHom G H) (i : PrimePowerCompletedGroupAlgebraIndex H)
    (x : PrimePowerCompletedGroupAlgebra ℓ G) :
    primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := H) i
        (primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ x) =
      primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i
        (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
          (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) x)

The finite-stage Fox-differential projection is computed by the prime-power completed group-algebra projection formula.

Show Lean proof
Theorem FoxDifferential.continuous_primePowerCompletedGroupAlgebraMap 
theorem continuous_primePowerCompletedGroupAlgebraMap
    (ψ : ContinuousMonoidHom G H) :
    Continuous (primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ)

The completed group-algebra map induced by a continuous homomorphism is continuous for the inverse-limit topologies.

Show Lean proof