NYLL
Module

Stage.lean

Nyll.ProCGroups.FoxDifferential.Completed.DifferentialModule.Map.Stage
6 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — differential module — map — stage

The principal declarations in this module are:

  • primePowerCompletedGroupAlgebraMapStage

The finite-stage prime-power group-algebra map induced by the quotient map associated to ψ and i.

  • primePowerCompletedGroupAlgebraMapStage_of

The finite-stage prime-power map sends a group-like basis element to the basis element supported at its quotient image.

  • primePowerCompletedGroupAlgebraMapStage_single

The finite-stage component of the completed group-algebra map sends arbitrary group-ring basis coefficients by the pulled-back quotient map.

  • primePowerCompletedGroupAlgebraMapStage_surjective

If \(\psi : G \to H\) is surjective, then every finite-stage group-algebra component of the completed map is surjective.

Imports1
Imported by2

Declarations

def

primePowerCompletedGroupAlgebraMapStage

L45 ↗
FoxDifferential.primePowerCompletedGroupAlgebraMapStage
Documentation

The finite-stage prime-power group-algebra map induced by the quotient map associated to ψ and i.

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
def primePowerCompletedGroupAlgebraMapStage
    (ψ : ContinuousMonoidHom G H) (i : PrimePowerCompletedGroupAlgebraIndex H) :
    PrimePowerCompletedGroupAlgebraStage ℓ G
        (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) →+*
      PrimePowerCompletedGroupAlgebraStage ℓ H i
theorem

primePowerCompletedGroupAlgebraMapStage_of

L58 ↗
FoxDifferential.primePowerCompletedGroupAlgebraMapStage_of
Documentation

The finite-stage prime-power map sends a group-like basis element to the basis element supported at its quotient image.

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 primePowerCompletedGroupAlgebraMapStage_of
    (ψ : ContinuousMonoidHom G H) (i : PrimePowerCompletedGroupAlgebraIndex H)
    (q : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G
      (completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2)) :
    primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i
        (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1)) _ q) =
      MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1)) _
        (completedGroupAlgebraComapQuotientMap (G := G) (H := H) ψ i.2 q)
theorem

primePowerCompletedGroupAlgebraMapStage_single

L79 ↗
FoxDifferential.primePowerCompletedGroupAlgebraMapStage_single
Documentation

The finite-stage component of the completed group-algebra map sends arbitrary group-ring basis coefficients by the pulled-back quotient map.

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 primePowerCompletedGroupAlgebraMapStage_single
    (ψ : ContinuousMonoidHom G H) (i : PrimePowerCompletedGroupAlgebraIndex H)
    (q : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G
      (completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2))
    (a : ModNCompletedCoeff (ℓ ^ i.1)) :
    primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i
        (MonoidAlgebra.single q a) =
      MonoidAlgebra.single
        (completedGroupAlgebraComapQuotientMap (G := G) (H := H) ψ i.2 q) a
theorem

primePowerCompletedGroupAlgebraMapStage_surjective

L100 ↗
FoxDifferential.primePowerCompletedGroupAlgebraMapStage_surjective
Documentation

If \(\psi : G \to H\) is surjective, then every finite-stage group-algebra component of the completed map is surjective.

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 primePowerCompletedGroupAlgebraMapStage_surjective
    (ψ : ContinuousMonoidHom G H) (hψ : Function.Surjective ψ)
    (i : PrimePowerCompletedGroupAlgebraIndex H) :
    Function.Surjective
      (primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i)
theorem

primePowerCompletedGroupAlgebraMapStage_augmentation

L123 ↗
FoxDifferential.primePowerCompletedGroupAlgebraMapStage_augmentation
Documentation

The finite-stage component of a completed group-algebra map preserves augmentation.

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 primePowerCompletedGroupAlgebraMapStage_augmentation
    (ψ : ContinuousMonoidHom G H) (i : PrimePowerCompletedGroupAlgebraIndex H)
    (x : PrimePowerCompletedGroupAlgebraStage ℓ G
      (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2)) :
    modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) H i.2
        (primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i x) =
      modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G
        (completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) x
theorem

primePowerCompletedGroupAlgebraMapStage_compatible

L186 ↗
FoxDifferential.primePowerCompletedGroupAlgebraMapStage_compatible
Documentation

The finite-stage prime-power maps commute with transition maps between refined target indices.

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
theorem primePowerCompletedGroupAlgebraMapStage_compatible
    (ψ : ContinuousMonoidHom G H) {i j : PrimePowerCompletedGroupAlgebraIndex H} (hij : i ≤ j) :
    (primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := H) hij).comp
        (primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ j) =
      (primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i).comp
        (primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G)
          (show
            (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) ≤
              (j.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ j.2) from
            ⟨hij.1, completedGroupAlgebraComapIndex_mono (G := G) (H := H) ψ hij.2⟩)) := by
  apply RingHom.ext
  intro x
  refine MonoidAlgebra.induction_on
    (motive := fun x =>
      ((primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := H) hij).comp
          (primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ j)) x =
        ((primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i).comp
          (primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G)
            (show
              (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) ≤
                (j.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ j.2) from
              ⟨hij.1,
                completedGroupAlgebraComapIndex_mono (G := G) (H := H) ψ hij.2⟩))) x)
    x ?_ ?_ ?_
  · intro q
    rw [RingHom.comp_apply, RingHom.comp_apply,
      primePowerCompletedGroupAlgebraMapStage_of,
      primePowerCompletedGroupAlgebraTransition_of,
      primePowerCompletedGroupAlgebraTransition_of]
    change
      MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1))
          (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient H i.2)
          ((OpenNormalSubgroupInClass.map
            (C := ProCGroups.FiniteGroupClass.allFinite) (G := H)
            (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2)
            (completedGroupAlgebraComapQuotientMap (G := G) (H := H) ψ j.2 q)) =
        primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i
          (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1))
            (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G
              (completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2))
            ((OpenNormalSubgroupInClass.map
              (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
              (U := OrderDual.ofDual
                (completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2))
              (V := OrderDual.ofDual
                (completedGroupAlgebraComapIndex (G := G) (H := H) ψ j.2))
              (completedGroupAlgebraComapIndex_mono (G := G) (H := H) ψ hij.2)) q))
    erw [primePowerCompletedGroupAlgebraMapStage_of]
    exact congrArg (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1))
      (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient H i.2))
      (congrFun
        (congrArg DFunLike.coe
          (completedGroupAlgebraComapQuotientMap_compatible
            (G := G) (H := H) ψ hij.2)) q)
  · intro x y hx hy
    rw [map_add, map_add, hx, hy]
  · intro a x hx
    rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
    rw [Algebra.smul_def, RingHom.map_mul, RingHom.map_mul, hx]
    simp only [primePowerCompletedGroupAlgebraTransition, modNCompletedGroupAlgebraStageCoeffMap,
  modNCompletedGroupRingCoeffMap, AlgHom.toRingHom_eq_coe,
      primePowerCompletedGroupAlgebraMapStage, map_intCast,
  RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, MonoidAlgebra.mapDomainRingHom_apply]

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.