Nyll.ProCGroups.FoxDifferential.Completed.DifferentialModule.Map.Limit

def

primePowerCompletedGroupAlgebraMap

FoxDifferential.primePowerCompletedGroupAlgebraMap

Documentation

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

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ)
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · full declaration

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

theorem

primePowerCompletedGroupAlgebraProjection_map

L133 ↗

FoxDifferential.primePowerCompletedGroupAlgebraProjection_map

Documentation

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

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ)
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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)

theorem

continuous_primePowerCompletedGroupAlgebraMap

L147 ↗

FoxDifferential.continuous_primePowerCompletedGroupAlgebraMap

Documentation

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

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ)
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem continuous_primePowerCompletedGroupAlgebraMap
    (ψ : ContinuousMonoidHom G H) :
    Continuous (primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ)

Limit.lean

Module documentation

Fox differential: completed — differential module — map — limit

primePowerCompletedGroupAlgebraMap

primePowerCompletedGroupAlgebraProjection_map

continuous_primePowerCompletedGroupAlgebraMap

Module documentation

Fox differential: completed — differential module — map — limit

Declarations

primePowerCompletedGroupAlgebraMap

primePowerCompletedGroupAlgebraProjection_map

continuous_primePowerCompletedGroupAlgebraMap