ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System.Basic

7 Theorems | 3 Definitions | 3 Abbreviations | 1 Instance

The principal declarations in this module are:

ModNCompletedGroupAlgebraStage The mod-\(N\) completed group-algebra stage combines the finite group quotient with the coefficient quotient modulo \(N\). - modNCompletedGroupAlgebraTransition The mod-\(n\) group-algebra transition from a finer finite quotient stage to a coarser stage. - modNCompletedGroupAlgebraTransition_of The transition map sends a group-like basis element to the basis element supported at its image in the coarser quotient in the Fox differential construction. - modNCompletedGroupAlgebraTransition_id The transition map attached to the identity refinement is the identity homomorphism in the Fox differential construction.

imports

Imported by

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System.AddCommGroup

Abbreviation FoxDifferential.ModNCompletedGroupAlgebraStage

omit [Fact (0 < n)] in
abbrev ModNCompletedGroupAlgebraStage (U :
    _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) : Type _ :=
  ModNCompletedGroupRing n (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U)

The mod-\(N\) completed group-algebra stage combines the finite group quotient with the coefficient quotient modulo \(N\).

Instance FoxDifferential.instFiniteModNCompletedGroupAlgebraStage

instance instFiniteModNCompletedGroupAlgebraStage (U :
    _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
    Finite (ModNCompletedGroupAlgebraStage n G U) := by
  classical
  letI : Finite (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U) :=
      (OrderDual.ofDual U).2
  letI : Fintype (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U) :=
      Fintype.ofFinite _
  letI : DecidableEq (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U) :=
      Classical.decEq _
  letI : NeZero n := ⟨Nat.ne_of_gt (show 0 < n from Fact.out)⟩
  letI : Fintype (ModNCompletedCoeff n) := Fintype.ofEquiv (Fin n) (ZMod.finEquiv n)
  letI : Finite (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U →
      ModNCompletedCoeff n) := by
    letI : Fintype (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U →
        ModNCompletedCoeff n) := inferInstance
    exact Finite.of_fintype _
  let f :
      ModNCompletedGroupAlgebraStage n G U →
        _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U →
          ModNCompletedCoeff n := fun x q => x.coeff q
  refine Finite.of_injective f ?_
  intro x y hxy
  ext q
  exact congrFun hxy q

Each mod-\(n\) completed group-algebra stage is finite.

Definition FoxDifferential.modNCompletedGroupAlgebraTransition

omit [Fact (0 < n)] in
def modNCompletedGroupAlgebraTransition
    {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
    ModNCompletedGroupAlgebraStage n G V →+* ModNCompletedGroupAlgebraStage n G U :=
  MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n)
    (OpenNormalSubgroupInClass.map
      (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
      (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)

The mod-\(n\) group-algebra transition from a finer finite quotient stage to a coarser stage.

Theorem FoxDifferential.modNCompletedGroupAlgebraTransition_of

omit [Fact (0 < n)] in
@[simp]
theorem modNCompletedGroupAlgebraTransition_of
    {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V)
    (g : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G V) :
    modNCompletedGroupAlgebraTransition n G hUV (MonoidAlgebra.of (ModNCompletedCoeff n) _ g) =
      MonoidAlgebra.single ((OpenNormalSubgroupInClass.map
        (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
        (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) g) 1

The transition map sends a group-like basis element to the basis element supported at its image in the coarser quotient in the Fox differential construction.

Show Lean proof

Theorem FoxDifferential.modNCompletedGroupAlgebraTransition_id

omit [Fact (0 < n)] in
@[simp]
theorem modNCompletedGroupAlgebraTransition_id (U :
    _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
    modNCompletedGroupAlgebraTransition n G (le_rfl : U ≤ U) = RingHom.id _

The transition map attached to the identity refinement is the identity homomorphism in the Fox differential construction.

Show Lean proof

Theorem FoxDifferential.modNCompletedGroupAlgebraTransition_comp

omit [Fact (0 < n)] in
@[simp]
theorem modNCompletedGroupAlgebraTransition_comp
    {U V W : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) (hVW : V ≤
        W) :
    (modNCompletedGroupAlgebraTransition n G hUV).comp
        (modNCompletedGroupAlgebraTransition n G hVW) =
      modNCompletedGroupAlgebraTransition n G (hUV.trans hVW)

Mod-\(n\) completed group-algebra transitions compose along quotient refinements.

Show Lean proof

Theorem FoxDifferential.modNCompletedGroupAlgebraTransition_single_apply

omit [Fact (0 < n)] in
theorem modNCompletedGroupAlgebraTransition_single_apply
    {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V)
    (q : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G V)
    (a : ModNCompletedCoeff n) :
    modNCompletedGroupAlgebraTransition n G hUV (MonoidAlgebra.single q a) =
      MonoidAlgebra.single
        ((OpenNormalSubgroupInClass.map
          (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
          (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q) a

The \(n\)-modular completed group-algebra transition sends a singleton to the singleton supported at the induced quotient class with the same coefficient.

Show Lean proof

Theorem FoxDifferential.modNCompletedGroupAlgebraTransition_surjective

omit [Fact (0 < n)] in
theorem modNCompletedGroupAlgebraTransition_surjective
    {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
    Function.Surjective (modNCompletedGroupAlgebraTransition n G hUV)

The finite-stage transition map is surjective, with preimages obtained by lifting quotient representatives.

Show Lean proof

Definition FoxDifferential.modNCompletedGroupAlgebraStageMap

omit [Fact (0 < n)] in
def modNCompletedGroupAlgebraStageMap (U :
    _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
    ModNCompletedGroupRing n G →+* ModNCompletedGroupAlgebraStage n G U :=
  MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n)
    (openNormalSubgroupInClassProj
      (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U)

The quotient map \((\mathbb{Z}/n\mathbb{Z})[G] \to (\mathbb{Z}/n\mathbb{Z})[G/U]\).

Theorem FoxDifferential.modNCompletedGroupAlgebraStageMap_of

omit [Fact (0 < n)] in
@[simp]
theorem modNCompletedGroupAlgebraStageMap_of
    (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (g : G) :
    modNCompletedGroupAlgebraStageMap n G U (MonoidAlgebra.of (ModNCompletedCoeff n) _ g) =
      MonoidAlgebra.single (openNormalSubgroupInClassProj
        (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) 1

The finite-stage group-like map sends a group element to the corresponding singleton basis element in the quotient group algebra in the Fox differential construction.

Show Lean proof

Theorem FoxDifferential.modNCompletedGroupAlgebraStageMap_compatible

omit [Fact (0 < n)] in
@[simp]
theorem modNCompletedGroupAlgebraStageMap_compatible
    {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
    (modNCompletedGroupAlgebraTransition n G hUV).comp
        (modNCompletedGroupAlgebraStageMap n G V) =
      modNCompletedGroupAlgebraStageMap n G U

The mod-\(n\) completed group-algebra stage maps are compatible with quotient refinement.

Show Lean proof

Definition FoxDifferential.modNCompletedGroupAlgebraSystem

omit [Fact (0 < n)] in
def modNCompletedGroupAlgebraSystem :
    InverseSystem (I := _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) where
  X := ModNCompletedGroupAlgebraStage n G
  topologicalSpace := fun _ => ⊥
  map := fun {U V} hUV => modNCompletedGroupAlgebraTransition n G hUV
  continuous_map := by
    intro U V hUV
    letI : TopologicalSpace (ModNCompletedGroupAlgebraStage n G U) := ⊥
    letI : TopologicalSpace (ModNCompletedGroupAlgebraStage n G V) := ⊥
    letI : DiscreteTopology (ModNCompletedGroupAlgebraStage n G V) := ⟨rfl⟩
    exact continuous_of_discreteTopology
  map_id := by
    intro U
    funext x
    exact congrFun
      (congrArg DFunLike.coe (modNCompletedGroupAlgebraTransition_id (n := n) (G := G) U)) x
  map_comp := by
    intro U V W hUV hVW
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (modNCompletedGroupAlgebraTransition_comp (n := n) (G := G) hUV hVW)) x

The inverse system \(U \mapsto (\mathbb{Z}/n\mathbb{Z})[G/U]\).

Abbreviation FoxDifferential.ModNCompletedGroupAlgebra

omit [Fact (0 < n)] in
abbrev ModNCompletedGroupAlgebra :=
  (modNCompletedGroupAlgebraSystem n G).inverseLimit

The inverse-limit object of the residue-coefficient stage tower.

Abbreviation FoxDifferential.modNCompletedGroupAlgebraProjection

omit [Fact (0 < n)] in
abbrev modNCompletedGroupAlgebraProjection (U :
    _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
    ModNCompletedGroupAlgebra n G → ModNCompletedGroupAlgebraStage n G U :=
  (modNCompletedGroupAlgebraSystem n G).projection U

The projection from the residue-coefficient inverse limit to one finite stage.

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System.Basic

Declarations