ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebra

11 Theorems | 7 Definitions | 4 Abbreviations

The principal declarations in this module are:

CompletedGroupAlgebraIndexInClass The index set for a completed group algebra over finite quotients belonging to a class C. - CompletedGroupAlgebraQuotientInClass The finite quotient of G attached to one class-restricted completed-group-algebra stage. - completedGroupAlgebraTransitionInClass_id Identity case for completedGroupAlgebraTransitionInClass_id. - completedGroupAlgebraTransitionInClass_comp Composition lemma completedGroupAlgebraTransitionInClass_comp.

imports

Mathlib.Algebra.MonoidAlgebra.MapDomain
ProCGroups.ProC.OpenNormalSubgroups.ProCGroup

Imported by

Abbreviation FoxDifferential.CompletedGroupAlgebraIndexInClass

abbrev CompletedGroupAlgebraIndexInClass (C : ProCGroups.FiniteGroupClass.{u}) :=
  OrderDual (OpenNormalSubgroupInClass C G)

The index set for a completed group algebra over finite quotients belonging to a class C.

Abbreviation FoxDifferential.CompletedGroupAlgebraQuotientInClass

abbrev CompletedGroupAlgebraQuotientInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) : Type _ :=
  (openNormalSubgroupInClassSystem C G).X U

The finite quotient of G attached to one class-restricted completed-group-algebra stage.

Abbreviation FoxDifferential.CompletedGroupAlgebraStageInClass

abbrev CompletedGroupAlgebraStageInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) : Type _ :=
  MonoidAlgebra ℤ (CompletedGroupAlgebraQuotientInClass G C U)

The discrete group ring over one class-restricted finite quotient of G.

Definition FoxDifferential.completedGroupAlgebraTransitionInClass

def completedGroupAlgebraTransitionInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
    CompletedGroupAlgebraStageInClass G C V →+*
      CompletedGroupAlgebraStageInClass G C U :=
  MonoidAlgebra.mapDomainRingHom ℤ
    (OpenNormalSubgroupInClass.map
      (C := C) (G := G)
      (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)

The transition map between two class-restricted completed-group-algebra stages.

Theorem FoxDifferential.completedGroupAlgebraTransitionInClass_id

@[simp]
theorem completedGroupAlgebraTransitionInClass_id
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
    completedGroupAlgebraTransitionInClass G C (le_rfl : U ≤ U) = RingHom.id _

Identity case for completedGroupAlgebraTransitionInClass_id.

Show Lean proof

Theorem FoxDifferential.completedGroupAlgebraTransitionInClass_comp

@[simp]
theorem completedGroupAlgebraTransitionInClass_comp
    (C : ProCGroups.FiniteGroupClass.{u})
    {U V W : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) (hVW : V ≤ W) :
    (completedGroupAlgebraTransitionInClass G C hUV).comp
        (completedGroupAlgebraTransitionInClass G C hVW) =
      completedGroupAlgebraTransitionInClass G C (hUV.trans hVW)

Composition lemma completedGroupAlgebraTransitionInClass_comp.

Show Lean proof

Definition FoxDifferential.completedGroupAlgebraSystemInClass

def completedGroupAlgebraSystemInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    InverseSystem (I := CompletedGroupAlgebraIndexInClass G C) where
  X := CompletedGroupAlgebraStageInClass G C
  topologicalSpace := fun _ => ⊥
  map := fun {U V} hUV => completedGroupAlgebraTransitionInClass G C hUV
  continuous_map := by
    intro U V hUV
    letI : TopologicalSpace (CompletedGroupAlgebraStageInClass G C U) := ⊥
    letI : TopologicalSpace (CompletedGroupAlgebraStageInClass G C V) := ⊥
    letI : DiscreteTopology (CompletedGroupAlgebraStageInClass G C V) := ⟨rfl⟩
    exact continuous_of_discreteTopology
  map_id := by
    intro U
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (completedGroupAlgebraTransitionInClass_id G C U)) x
  map_comp := by
    intro U V W hUV hVW
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (completedGroupAlgebraTransitionInClass_comp G C hUV hVW)) x

The class-restricted inverse system of finite-stage integral group rings.

Definition FoxDifferential.completedGroupAlgebraStageMapInClass

def completedGroupAlgebraStageMapInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
    MonoidAlgebra ℤ G →+* CompletedGroupAlgebraStageInClass G C U :=
  MonoidAlgebra.mapDomainRingHom ℤ
    (openNormalSubgroupInClassProj (C := C) (G := G) U)

The quotient ring map from ℤ[G] to one class-restricted finite stage.

Theorem FoxDifferential.completedGroupAlgebraStageMapInClass_of

@[simp]
theorem completedGroupAlgebraStageMapInClass_of
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) (g : G) :
    completedGroupAlgebraStageMapInClass G C U (MonoidAlgebra.of ℤ _ g) =
      MonoidAlgebra.single (openNormalSubgroupInClassProj (C := C) (G := G) U g) 1

Evaluation formula for completedGroupAlgebraStageMapInClass_of.

Show Lean proof

Theorem FoxDifferential.completedGroupAlgebraStageMapInClass_compatible

@[simp]
theorem completedGroupAlgebraStageMapInClass_compatible
    (C : ProCGroups.FiniteGroupClass.{u})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
    (completedGroupAlgebraTransitionInClass G C hUV).comp
        (completedGroupAlgebraStageMapInClass G C V) =
      completedGroupAlgebraStageMapInClass G C U

Compatibility lemma completedGroupAlgebraStageMapInClass_compatible.

Show Lean proof

Definition FoxDifferential.CompletedGroupAlgebraCompatibleInClass

def CompletedGroupAlgebraCompatibleInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (x : ∀ U : CompletedGroupAlgebraIndexInClass G C,
      CompletedGroupAlgebraStageInClass G C U) : Prop :=
  (completedGroupAlgebraSystemInClass G C).Compatible x

Compatibility for a class-restricted completed group algebra family.

Abbreviation FoxDifferential.CompletedGroupAlgebraInClass

abbrev CompletedGroupAlgebraInClass (C : ProCGroups.FiniteGroupClass.{u}) : Type _ :=
  {x : ∀ U : CompletedGroupAlgebraIndexInClass G C,
      CompletedGroupAlgebraStageInClass G C U //
    CompletedGroupAlgebraCompatibleInClass G C x}

The class-restricted completed group algebra as an inverse-limit subtype.

Definition FoxDifferential.completedGroupAlgebraProjectionInClass

def completedGroupAlgebraProjectionInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
    CompletedGroupAlgebraInClass G C → CompletedGroupAlgebraStageInClass G C U :=
  (completedGroupAlgebraSystemInClass G C).projection U

Projection from the class-restricted completed group algebra to one finite stage.

Definition FoxDifferential.completedGroupAlgebraComapIndexInClass

def completedGroupAlgebraComapIndexInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (ψ : ContinuousMonoidHom G H) (U : CompletedGroupAlgebraIndexInClass H C) :
    CompletedGroupAlgebraIndexInClass G C := by
  let V : OpenNormalSubgroup H := (OrderDual.ofDual U).1
  let W : OpenNormalSubgroup G := OpenNormalSubgroup.comap ψ.toMonoidHom ψ.continuous_toFun V
  refine OrderDual.toDual ⟨W, ?_⟩
  let f : G ⧸ (W : Subgroup G) →* H ⧸ (V : Subgroup H) :=
    QuotientGroup.map _ _ ψ.toMonoidHom (by
      intro g hg
      simpa [W] using hg)
  have hf : Function.Injective f := by
    intro x y hxy
    rcases QuotientGroup.mk'_surjective (W : Subgroup G) x with ⟨a, rfl⟩
    rcases QuotientGroup.mk'_surjective (W : Subgroup G) y with ⟨b, rfl⟩
    apply QuotientGroup.eq.2
    change ψ (a⁻¹ * b) ∈ (V : Subgroup H)
    have hv : (ψ a)⁻¹ * ψ b ∈ (V : Subgroup H) := QuotientGroup.eq.1 hxy
    simpa using hv
  exact hC.of_injective (OrderDual.ofDual U).2 f hf

Pull back a class-restricted finite quotient along a continuous homomorphism.

The hereditary hypothesis is the precise extra closure property needed: the pulled-back quotient embeds into the target quotient, so membership in C follows from closure under subgroups.

Definition FoxDifferential.completedGroupAlgebraComapQuotientMapInClass

def completedGroupAlgebraComapQuotientMapInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (ψ : ContinuousMonoidHom G H) (U : CompletedGroupAlgebraIndexInClass H C) :
    CompletedGroupAlgebraQuotientInClass G C
        (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ U) →*
      CompletedGroupAlgebraQuotientInClass H C U := by
  let V : OpenNormalSubgroup H := (OrderDual.ofDual U).1
  let W : OpenNormalSubgroup G := OpenNormalSubgroup.comap ψ.toMonoidHom ψ.continuous_toFun V
  exact QuotientGroup.map _ _ ψ.toMonoidHom (by
    intro g hg
    simpa [W, completedGroupAlgebraComapIndexInClass] using hg)

The finite quotient map induced by a continuous homomorphism after pulling back the stage.

Theorem FoxDifferential.completedGroupAlgebraComapQuotientMapInClass_mk

@[simp]
theorem completedGroupAlgebraComapQuotientMapInClass_mk
    (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (ψ : ContinuousMonoidHom G H) (U : CompletedGroupAlgebraIndexInClass H C) (g : G) :
    completedGroupAlgebraComapQuotientMapInClass
        (G := G) (H := H) C hC ψ U
        (QuotientGroup.mk'
          ((((OrderDual.ofDual
            (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ U)).1 :
              OpenNormalSubgroup G) : Subgroup G)) g) =
      QuotientGroup.mk' ((((OrderDual.ofDual U).1 : OpenNormalSubgroup H) : Subgroup H))
        (ψ g)

Evaluation formula for completedGroupAlgebraComapQuotientMapInClass_mk.

Show Lean proof

Theorem FoxDifferential.completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective

theorem completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
    (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (ψ : ContinuousMonoidHom G H) (hψ : Function.Surjective ψ)
    (U : CompletedGroupAlgebraIndexInClass H C) :
    Function.Surjective
      (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hC ψ U)

Surjectivity lemma completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective.

Show Lean proof

Theorem FoxDifferential.completedGroupAlgebraComapIndexInClass_mono

omit [IsTopologicalGroup G] in
theorem completedGroupAlgebraComapIndexInClass_mono
    (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (ψ : ContinuousMonoidHom G H) {U V : CompletedGroupAlgebraIndexInClass H C}
    (hUV : U ≤ V) :
    completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ U ≤
      completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ V

有限群クラスを固定した標準写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。

Show Lean proof

Theorem FoxDifferential.completedGroupAlgebraComapQuotientMapInClass_compatible

@[simp]
theorem completedGroupAlgebraComapQuotientMapInClass_compatible
    (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (ψ : ContinuousMonoidHom G H) {U V : CompletedGroupAlgebraIndexInClass H C}
    (hUV : U ≤ V) :
    (OpenNormalSubgroupInClass.map
        (C := C) (G := H)
        (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV).comp
        (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hC ψ V) =
      (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hC ψ U).comp
        (OpenNormalSubgroupInClass.map
          (C := C) (G := G)
          (U := OrderDual.ofDual
            (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ U))
          (V := OrderDual.ofDual
            (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ V))
          (completedGroupAlgebraComapIndexInClass_mono (G := G) (H := H) C hC ψ hUV))

Compatibility lemma completedGroupAlgebraComapQuotientMapInClass_compatible.

Show Lean proof

Theorem FoxDifferential.completedGroupAlgebraComapIndexInClass_id

@[simp]
theorem completedGroupAlgebraComapIndexInClass_id
    (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (U : CompletedGroupAlgebraIndexInClass G C) :
    completedGroupAlgebraComapIndexInClass (G := G) (H := G) C hC
        (ContinuousMonoidHom.id G) U = U

Pulling a finite quotient back along the identity continuous homomorphism gives the same class-restricted index. This is intentionally an equality theorem, since dependent inverse-limit indices are often not definitionally equal after target naturality rewrites.

Show Lean proof

Theorem FoxDifferential.completedGroupAlgebraComapIndexInClass_comp

omit [IsTopologicalGroup G] in
@[simp]
theorem completedGroupAlgebraComapIndexInClass_comp
    (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
    (φ : G →ₜ* H) (ψ : H →ₜ* K) (U : CompletedGroupAlgebraIndexInClass K C) :
    completedGroupAlgebraComapIndexInClass (G := G) (H := K) C hC (ψ.comp φ) U =
      completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC φ
        (completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC ψ U)

Pullback of class-restricted finite quotients is functorial for continuous target maps.

This is the index-level rewrite needed when the two inverse-limit stage indices produced by a composite target map are propositionally, but not definitionally, the same.

Show Lean proof

Theorem FoxDifferential.completedGroupAlgebraComapIndexInClass_top

omit [IsTopologicalGroup G] in
@[simp]
theorem completedGroupAlgebraComapIndexInClass_top
    (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (ψ : G →ₜ* H) :
    completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ
        (OrderDual.toDual (OpenNormalSubgroupInClass.top (C := C) (G := H))) =
      OrderDual.toDual (OpenNormalSubgroupInClass.top (C := C) (G := G))

Pulling back the canonical trivial quotient gives the canonical trivial quotient.

Show Lean proof

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebra

Declarations