ProCGroups.FoxDifferential.Completed.Continuous.Universal.AugmentationQuotient

150 Theorems | 49 Definitions | 4 Abbreviations

The principal declarations in this module are:

  • zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard The algebraic product \(I(\ker \psi)I(G)\) inside the algebraic standard source augmentation ideal. - zcCompletedGroupAlgebraStandardAugmentationIdealProjection Projection of the algebraic standard augmentation ideal to a finite augmentation stage. - zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard_generator_mem A generator \((n-1)s\) lies in the algebraic product \(I(\ker \psi)I(G)\). - zcCompletedGroupAlgebraStandardAugmentationIdealProjection_val The value of the augmentation-ideal projection is the value of the corresponding finite-stage projection.
imports
Imported by

Declarations

def zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard
    (psi : ContinuousMonoidHom G H) :
    Submodule (ZCCompletedGroupAlgebra C G)
      (zcCompletedGroupAlgebraStandardAugmentationIdeal C G) :=
  Submodule.span (ZCCompletedGroupAlgebra C G)
    (Set.range fun p :
      ProfiniteKernelSubgroup psi × zcCompletedGroupAlgebraStandardAugmentationIdeal C G =>
        (zcGroupLike C G p.1.1 - 1) • p.2)

The algebraic product \(I(\ker \psi)I(G)\) inside the algebraic standard source augmentation ideal.

omit [IsTopologicalGroup H] in
theorem zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard_generator_mem
    (psi : ContinuousMonoidHom G H) (n : ProfiniteKernelSubgroup psi)
    (s : zcCompletedGroupAlgebraStandardAugmentationIdeal C G) :
    (zcGroupLike C G n.1 - 1) • s ∈
      zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi

A generator \((n-1)s\) lies in the algebraic product \(I(\ker \psi)I(G)\).

Show Lean proof
def zcCompletedGroupAlgebraStandardAugmentationIdealProjection
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (i : ZCCompletedGroupAlgebraIndex C G) :
    zcCompletedGroupAlgebraStandardAugmentationIdeal C G →
      zcCompletedGroupAlgebraStageAugmentationIdeal C G i := by
  intro x
  let xAug : ZCCompletedGroupAlgebraAugmentationIdeal C G :=
    ⟨x, zcCompletedGroupAlgebraStandardAugmentationIdeal_le_augmentationIdeal C G x.2⟩
  exact zcCompletedGroupAlgebraAugmentationIdealProjection C G i xAug

Projection of the algebraic standard augmentation ideal to a finite augmentation stage.

@[simp]
theorem zcCompletedGroupAlgebraStandardAugmentationIdealProjection_val
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (i : ZCCompletedGroupAlgebraIndex C G)
    (x : zcCompletedGroupAlgebraStandardAugmentationIdeal C G) :
    ((zcCompletedGroupAlgebraStandardAugmentationIdealProjection C i x :
      ZCCompletedGroupAlgebraStage C G i)) =
      zcCompletedGroupAlgebraProjection C G i x

The value of the augmentation-ideal projection is the value of the corresponding finite-stage projection.

Show Lean proof
theorem continuous_zcCompletedGroupAlgebraStandardAugmentationIdealProjection
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (i : ZCCompletedGroupAlgebraIndex C G) :
    Continuous (zcCompletedGroupAlgebraStandardAugmentationIdealProjection C i)

The standard augmentation-ideal projection is continuous.

Show Lean proof
theorem zcCompletedGAStageAugmentationIdeal_identityBoundary_monoidAlgebraToIdentity
    (i : ZCCompletedGroupAlgebraIndex C G)
    (x : zcCompletedGroupAlgebraStageAugmentationIdeal C G i) :
    identityCrossedDifferentialBoundary
        (monoidAlgebraToIdentityCrossedDifferentialModule
          (S := ModNCompletedCoeff i.1.modulus)
          (G := CompletedGroupAlgebraQuotientInClass G C i.2)
          (x : ZCCompletedGroupAlgebraStage C G i)) =
      (x : ZCCompletedGroupAlgebraStage C G i)

On a finite coefficient stage, the identity crossed-differential boundary is a left inverse to the additive lift from the finite augmentation ideal.

Show Lean proof
@[simp]
theorem zcCompletedGroupAlgebraStandardAugmentationIdealProjection_zero
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (i : ZCCompletedGroupAlgebraIndex C G) :
    zcCompletedGroupAlgebraStandardAugmentationIdealProjection C i
        (0 : zcCompletedGroupAlgebraStandardAugmentationIdeal C G) = 0

The finite-stage augmentation-ideal projection is compatible with zero.

Show Lean proof
@[simp]
theorem zcCompletedGroupAlgebraStandardAugmentationIdealProjection_add
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (i : ZCCompletedGroupAlgebraIndex C G)
    (x y : zcCompletedGroupAlgebraStandardAugmentationIdeal C G) :
    zcCompletedGroupAlgebraStandardAugmentationIdealProjection C i (x + y) =
      zcCompletedGroupAlgebraStandardAugmentationIdealProjection C i x +
        zcCompletedGroupAlgebraStandardAugmentationIdealProjection C i y

The finite-stage augmentation-ideal projection is compatible with addition.

Show Lean proof
@[simp]
theorem zcCompletedGroupAlgebraStandardAugmentationIdealProjection_smul
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (i : ZCCompletedGroupAlgebraIndex C G)
    (a : ZCCompletedGroupAlgebra C G)
    (x : zcCompletedGroupAlgebraStandardAugmentationIdeal C G) :
    zcCompletedGroupAlgebraStandardAugmentationIdealProjection C i (a • x) =
      zcCompletedGroupAlgebraProjection C G i a •
        zcCompletedGroupAlgebraStandardAugmentationIdealProjection C i x

The finite-stage augmentation-ideal projection is compatible with scalar multiplication.

Show Lean proof
def zcCompletedGroupAlgebraStandardAugmentationIdealProjectionLinear
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (i : ZCCompletedGroupAlgebraIndex C G) :
    zcCompletedGroupAlgebraStandardAugmentationIdeal C G →ₛₗ[
      zcCompletedGroupAlgebraProjectionRingHom C G i]
      zcCompletedGroupAlgebraStageAugmentationIdeal C G i where
  toFun := zcCompletedGroupAlgebraStandardAugmentationIdealProjection C i
  map_add' := by
    intro x y
    exact zcCompletedGroupAlgebraStandardAugmentationIdealProjection_add C i x y
  map_smul' := by
    intro a x
    exact zcCompletedGroupAlgebraStandardAugmentationIdealProjection_smul C i a x

The finite-stage projection of the standard augmentation ideal, as a semilinear map over the completed group-algebra projection.

@[simp]
theorem zcCompletedGroupAlgebraStandardAugmentationIdealProjectionLinear_apply
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (i : ZCCompletedGroupAlgebraIndex C G)
    (x : zcCompletedGroupAlgebraStandardAugmentationIdeal C G) :
    zcCompletedGroupAlgebraStandardAugmentationIdealProjectionLinear C i x =
      zcCompletedGroupAlgebraStandardAugmentationIdealProjection C i x

The linear finite-stage projection of the standard completed augmentation ideal has the same value as its underlying projection.

Show Lean proof
@[simp]
theorem zcCompletedGroupAlgebraStandardAugmentationIdealProjection_sub
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (i : ZCCompletedGroupAlgebraIndex C G)
    (x y : zcCompletedGroupAlgebraStandardAugmentationIdeal C G) :
    zcCompletedGroupAlgebraStandardAugmentationIdealProjection C i (x - y) =
      zcCompletedGroupAlgebraStandardAugmentationIdealProjection C i x -
        zcCompletedGroupAlgebraStandardAugmentationIdealProjection C i y

The finite-stage augmentation-ideal projection is compatible with subtraction.

Show Lean proof
def zcCompletedGroupAlgebraStandardAugmentationIdealProjectionProduct
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
    zcCompletedGroupAlgebraStandardAugmentationIdeal C G →
      ∀ i : ZCCompletedGroupAlgebraIndex C G,
        zcCompletedGroupAlgebraStageAugmentationIdeal C G i :=
  fun x i => zcCompletedGroupAlgebraStandardAugmentationIdealProjection C i x

The product of all finite-stage projections of the standard completed augmentation ideal.

@[simp]
theorem zcCompletedGroupAlgebraStandardAugmentationIdealProjectionProduct_apply
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (x : zcCompletedGroupAlgebraStandardAugmentationIdeal C G)
    (i : ZCCompletedGroupAlgebraIndex C G) :
    zcCompletedGroupAlgebraStandardAugmentationIdealProjectionProduct C x i =
      zcCompletedGroupAlgebraStandardAugmentationIdealProjection C i x

Evaluating the product of standard augmentation-ideal projections at i returns the projection at i.

Show Lean proof
theorem zcCompletedGroupAlgebraStandardAugmentationIdealProjectionProduct_injective
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
    Function.Injective
      (zcCompletedGroupAlgebraStandardAugmentationIdealProjectionProduct C (G := G))

Finite-stage projections separate points of the standard completed augmentation ideal.

Show Lean proof
theorem zcCompletedGroupAlgebraStandardAugmentationIdealProjection_ext
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    {x y : zcCompletedGroupAlgebraStandardAugmentationIdeal C G}
    (h : ∀ i : ZCCompletedGroupAlgebraIndex C G,
      zcCompletedGroupAlgebraStandardAugmentationIdealProjection C i x =
      zcCompletedGroupAlgebraStandardAugmentationIdealProjection C i y) :
    x = y

Extensionality for standard completed augmentation ideal elements by finite-stage projections.

Show Lean proof
theorem zcCompletedGroupAlgebraStandardAugmentationIdealProjection_surjective
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (i : ZCCompletedGroupAlgebraIndex C G) :
    Function.Surjective
      (zcCompletedGroupAlgebraStandardAugmentationIdealProjection C i)

Every finite standard augmentation stage is hit by the completed standard augmentation ideal projection.

Show Lean proof
def zcCompletedGroupAlgebraOpenImageKernelAugmentationIdealMulStageStandard
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G) :
    Submodule (ZCCompletedGroupAlgebraStage C G i)
      (zcCompletedGroupAlgebraStageAugmentationIdeal C G i) :=
  Submodule.span (ZCCompletedGroupAlgebraStage C G i)
    (Set.range fun p :
      (zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i).ker ×
        zcCompletedGroupAlgebraStageAugmentationIdeal C G i =>
        (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
            (CompletedGroupAlgebraQuotientInClass G C i.2) p.1.1 - 1) • p.2)

The finite-stage product \(I(\ker)\,I(G/U)\) attached to the open-image quotient at a source stage.

theorem zcCompletedGAOpenImageKernelAugmentationIdealMulStageStandard_generator_mem
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G)
    (q : (zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i).ker)
    (s : zcCompletedGroupAlgebraStageAugmentationIdeal C G i) :
    (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
        (CompletedGroupAlgebraQuotientInClass G C i.2) q.1 - 1) • s ∈
      zcCompletedGroupAlgebraOpenImageKernelAugmentationIdealMulStageStandard
        C hC hForm psi hpsi hfopen i

A finite-stage product generator belongs to the finite-stage product submodule.

Show Lean proof
def zcCompletedGroupAlgebraOpenImageKernelClass
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G)
    (n : ProfiniteKernelSubgroup psi) :
    (zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i).ker := by
  refine ⟨QuotientGroup.mk'
      ((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup G) : Subgroup G)) n.1, ?_⟩
  rw [MonoidHom.mem_ker]
  rw [zcCompletedGroupAlgebraOpenImageQuotientMap_mk]
  change QuotientGroup.mk'
      ((((OrderDual.ofDual
        (zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)).1 :
          OpenNormalSubgroup H) : Subgroup H)) (psi n.1) = 1
  rw [show psi n.1 = 1 from n.2]
  simp only [QuotientGroup.mk'_apply, QuotientGroup.mk_one]

An actual kernel element determines a class in the finite-stage open-image kernel.

@[simp]
theorem zcCompletedGroupAlgebraOpenImageKernelClass_val
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G)
    (n : ProfiniteKernelSubgroup psi) :
    (zcCompletedGroupAlgebraOpenImageKernelClass C hC hForm psi hpsi hfopen i n).1 =
      QuotientGroup.mk'
        ((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup G) : Subgroup G)) n.1

The open-image kernel class has the expected underlying subgroup, characterized by finite-stage Fox coordinate formulas.

Show Lean proof
@[simp 900]
theorem zcCompletedGroupAlgebraStandardAugmentationIdealProjection_kernel_generator_smul
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G)
    (n : ProfiniteKernelSubgroup psi)
    (s : zcCompletedGroupAlgebraStandardAugmentationIdeal C G) :
    zcCompletedGroupAlgebraStandardAugmentationIdealProjection C i
        ((zcGroupLike C G n.1 - 1) • s) =
      (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
          (CompletedGroupAlgebraQuotientInClass G C i.2)
          (zcCompletedGroupAlgebraOpenImageKernelClass
            C hC hForm psi hpsi hfopen i n).1 - 1) •
        zcCompletedGroupAlgebraStandardAugmentationIdealProjection C i s

The finite-stage augmentation-ideal projection is compatible with scalar multiplication.

Show Lean proof
theorem zcCompletedGAKernelAugmentationIdealMulStandard_proj_mem_openImageStage
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G)
    {x : zcCompletedGroupAlgebraStandardAugmentationIdeal C G}
    (hx : x ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi) :
    zcCompletedGroupAlgebraStandardAugmentationIdealProjection C i x ∈
      zcCompletedGroupAlgebraOpenImageKernelAugmentationIdealMulStageStandard
        C hC hForm psi hpsi hfopen i

Projecting an element of \(I(\ker\psi)I(G)\) to an open-image finite stage lands in the corresponding finite-stage kernel-augmentation product.

Show Lean proof
theorem zcCompletedGAOpenImageKernelAugmentationIdealMulStageStandard_mem_proj
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G)
    (x : zcCompletedGroupAlgebraStageAugmentationIdeal C G i)
    (hx :
      x ∈ zcCompletedGroupAlgebraOpenImageKernelAugmentationIdealMulStageStandard
        C hC hForm psi hpsi hfopen i) :
    ∃ y ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi,
      zcCompletedGroupAlgebraStandardAugmentationIdealProjection C i y = x

Every element of the finite-stage open-image kernel-augmentation product is the projection of an element of the algebraic product \(I(\ker\psi)I(G)\).

Show Lean proof
def zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    Submodule (ZCCompletedGroupAlgebra C G)
      (zcCompletedGroupAlgebraStandardAugmentationIdeal C G) where
  carrier := {x | ∀ i : ZCCompletedGroupAlgebraIndex C G,
    zcCompletedGroupAlgebraStandardAugmentationIdealProjection C i x ∈
      zcCompletedGroupAlgebraOpenImageKernelAugmentationIdealMulStageStandard
        C hC hForm psi hpsi hfopen i}
  zero_mem' := by
    intro i
    simp only [zcCompletedGroupAlgebraStandardAugmentationIdealProjection_zero, zero_mem]
  add_mem' := by
    intro x y hx hy i
    simpa using
      (zcCompletedGroupAlgebraOpenImageKernelAugmentationIdealMulStageStandard
        C hC hForm psi hpsi hfopen i).add_mem (hx i) (hy i)
  smul_mem' := by
    intro a x hx i
    rw [zcCompletedGroupAlgebraStandardAugmentationIdealProjection_smul]
    exact
      (zcCompletedGroupAlgebraOpenImageKernelAugmentationIdealMulStageStandard
        C hC hForm psi hpsi hfopen i).smul_mem
        (zcCompletedGroupAlgebraProjection C G i a) (hx i)

The closed finite-stage hull of \(I(\ker \psi)I(G)\) inside the standard source augmentation ideal: an element belongs exactly when every finite projection belongs to the finite-stage open-image kernel product.

theorem zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard_le_closed
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi ≤
      zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
        C hC hForm psi hpsi hfopen

The algebraic product is contained in its finite-stage closed hull.

Show Lean proof
theorem isClosed_zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    IsClosed
      ((zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
        C hC hForm psi hpsi hfopen :
          Set (zcCompletedGroupAlgebraStandardAugmentationIdeal C G)))

The finite-stage hull is closed in the standard source augmentation ideal.

Show Lean proof
theorem closure_zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard_le_closed
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    closure
        ((zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi :
          Set (zcCompletedGroupAlgebraStandardAugmentationIdeal C G))) ⊆
      (zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
        C hC hForm psi hpsi hfopen :
          Set (zcCompletedGroupAlgebraStandardAugmentationIdeal C G))

The closure of the algebraic product is contained in the finite-stage closed hull.

Show Lean proof
theorem zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed_le_closure
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    (zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
        C hC hForm psi hpsi hfopen :
          Set (zcCompletedGroupAlgebraStandardAugmentationIdeal C G)) ⊆
      closure
        ((zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi :
          Set (zcCompletedGroupAlgebraStandardAugmentationIdeal C G)))

The finite-stage closed hull is contained in the closure of the algebraic product.

Show Lean proof
theorem closure_zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard_eq_closed
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    closure
        ((zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi :
          Set (zcCompletedGroupAlgebraStandardAugmentationIdeal C G))) =
      (zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
        C hC hForm psi hpsi hfopen :
          Set (zcCompletedGroupAlgebraStandardAugmentationIdeal C G))

The closure of \(I(\ker \psi)I(G)\) is exactly the finite-stage kernel-product condition.

Show Lean proof
theorem isClosed_zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard_iff_eq_closed
    {C : ProCGroups.FiniteGroupClass.{u}}
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    {psi : ContinuousMonoidHom G H} (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    IsClosed
        ((zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi :
          Set (zcCompletedGroupAlgebraStandardAugmentationIdeal C G))) ↔
      (zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi :
          Set (zcCompletedGroupAlgebraStandardAugmentationIdeal C G)) =
        (zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
          C hC hForm psi hpsi hfopen :
            Set (zcCompletedGroupAlgebraStandardAugmentationIdeal C G))

The algebraic product is closed exactly when it already equals the finite-stage closed hull. This is the precise non-circular closedness frontier.

Show Lean proof
abbrev KernelAugmentationIdealQuotient
    (psi : ContinuousMonoidHom G H) : Type u :=
  zcCompletedGroupAlgebraStandardAugmentationIdeal C G ⧸
    zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi

The source-side augmentation quotient \(I\mathbb{Z}_C\llbracket G\rrbracket / I(\ker \psi) I\mathbb{Z}_C\llbracket G\rrbracket\), before descending scalars to \(\mathbb{Z}_C\llbracket H\rrbracket\).

abbrev KernelAugmentationIdealClosedQuotient
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) : Type u :=
  zcCompletedGroupAlgebraStandardAugmentationIdeal C G ⧸
    zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
      C hC hForm psi hpsi hfopen

The closed source-side augmentation quotient, using the finite-stage closed hull of \(I(\ker \psi)I(G)\) as denominator.

theorem isQuotientMap_kernelAugmentationIdealClosedQuotient_mkQ
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    Topology.IsQuotientMap
      (zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
        C hC hForm psi hpsi hfopen).mkQ

The quotient map to the closed source augmentation quotient is a quotient map.

Show Lean proof
theorem continuous_kernelAugmentationIdealClosedQuotient_iff_comp_mkQ
    {C : ProCGroups.FiniteGroupClass.{u}}
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    {hC : ProCGroups.FiniteGroupClass.Hereditary C}
    {hForm : ProCGroups.FiniteGroupClass.Formation C}
    {psi : ContinuousMonoidHom G H} {hpsi : Function.Surjective psi}
    {hfopen : IsOpenMap psi}
    {A : Type u} [TopologicalSpace A]
    {f : KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen → A} :
    Continuous f ↔
      Continuous (fun x : zcCompletedGroupAlgebraStandardAugmentationIdeal C G =>
        f ((zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
          C hC hForm psi hpsi hfopen).mkQ x))

Continuity out of the closed source augmentation quotient can be tested after precomposing with the quotient map from the standard augmentation ideal.

Show Lean proof
theorem t1Space_kernelAugmentationIdealClosedQuotient
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    T1Space (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)

The closed source augmentation quotient is \(T_1\) for the quotient topology.

Show Lean proof
theorem isClosed_zero_kernelAugmentationIdealClosedQuotient
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    IsClosed
      ({0} : Set
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen))

The zero class is closed in the closed source augmentation quotient.

Show Lean proof
abbrev KernelAugmentationIdealClosedStageQuotient
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G) : Type u :=
  zcCompletedGroupAlgebraStageAugmentationIdeal C G i ⧸
    zcCompletedGroupAlgebraOpenImageKernelAugmentationIdealMulStageStandard
      C hC hForm psi hpsi hfopen i

The finite-stage quotient of the source augmentation ideal by the open-image kernel product.

def kernelAugmentationIdealClosedQuotientStageProjection
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G) :
    KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen →ₛₗ[
      zcCompletedGroupAlgebraProjectionRingHom C G i]
      KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i :=
  (zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
    C hC hForm psi hpsi hfopen).mapQ
    (zcCompletedGroupAlgebraOpenImageKernelAugmentationIdealMulStageStandard
      C hC hForm psi hpsi hfopen i)
    (zcCompletedGroupAlgebraStandardAugmentationIdealProjectionLinear C i)
    (by
      intro x hx
      exact hx i)

The finite-stage coordinate of the closed source augmentation quotient.

@[simp 900]
theorem kernelAugmentationIdealClosedQuotientStageProjection_mk
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G)
    (x : zcCompletedGroupAlgebraStandardAugmentationIdeal C G) :
    kernelAugmentationIdealClosedQuotientStageProjection
        C hC hForm psi hpsi hfopen i
        ((zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
          C hC hForm psi hpsi hfopen).mkQ x) =
      ((zcCompletedGroupAlgebraOpenImageKernelAugmentationIdealMulStageStandard
          C hC hForm psi hpsi hfopen i).mkQ
        (zcCompletedGroupAlgebraStandardAugmentationIdealProjection C i x) :
        KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i)

The stage projection of a closed kernel-augmentation quotient class is represented by the corresponding finite-stage projection.

Show Lean proof
theorem continuous_kernelAugmentationIdealClosedQuotientStageProjection
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G) :
    Continuous
      (kernelAugmentationIdealClosedQuotientStageProjection
        C hC hForm psi hpsi hfopen i)

Each finite-stage coordinate of the closed source augmentation quotient is continuous.

Show Lean proof
def kernelAugmentationIdealClosedQuotientStageProjectionProduct
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen →
      ∀ i : ZCCompletedGroupAlgebraIndex C G,
        KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i :=
  fun x i => kernelAugmentationIdealClosedQuotientStageProjection
    C hC hForm psi hpsi hfopen i x

The product of all finite-stage coordinates of the closed source augmentation quotient.

@[simp]
theorem kernelAugmentationIdealClosedQuotientStageProjectionProduct_apply
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (x : KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
    (i : ZCCompletedGroupAlgebraIndex C G) :
    kernelAugmentationIdealClosedQuotientStageProjectionProduct
        C hC hForm psi hpsi hfopen x i =
      kernelAugmentationIdealClosedQuotientStageProjection
        C hC hForm psi hpsi hfopen i x

Evaluating the product projection of the closed kernel-augmentation quotient at i returns its stage projection at i.

Show Lean proof
theorem continuous_kernelAugmentationIdealClosedQuotientStageProjectionProduct
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    Continuous
      (kernelAugmentationIdealClosedQuotientStageProjectionProduct
        C hC hForm psi hpsi hfopen)

The finite-stage coordinate product of the closed source augmentation quotient is continuous.

Show Lean proof
theorem kernelAugmentationIdealClosedQuotientStageProjectionProduct_injective
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    Function.Injective
      (kernelAugmentationIdealClosedQuotientStageProjectionProduct
        C hC hForm psi hpsi hfopen)

Finite-stage coordinates separate points in the closed source augmentation quotient.

Show Lean proof
theorem kernelAugmentationIdealClosedQuotientStageProjection_ext
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    {x y : KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen}
    (h : ∀ i : ZCCompletedGroupAlgebraIndex C G,
      kernelAugmentationIdealClosedQuotientStageProjection
        C hC hForm psi hpsi hfopen i x =
      kernelAugmentationIdealClosedQuotientStageProjection
        C hC hForm psi hpsi hfopen i y) :
    x = y

Extensionality for the closed source augmentation quotient by finite-stage coordinates.

Show Lean proof
theorem kernelAugmentationIdealClosedQuotient_topology_eq_induced_stageProjProduct
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    (inferInstance :
      TopologicalSpace
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)) =
      TopologicalSpace.induced
        (kernelAugmentationIdealClosedQuotientStageProjectionProduct
          C hC hForm psi hpsi hfopen) inferInstance

The quotient topology on the closed source augmentation quotient is exactly the topology induced by all finite closed-quotient coordinates.

Show Lean proof
def zcCompletedGroupAlgebraOpenImageStageRingHom
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G) :
    ZCCompletedGroupAlgebraStage C G i →+*
      ZCCompletedGroupAlgebraStage C H
        (zcCompletedGroupAlgebraOpenImageTargetIndex C hForm psi hpsi hfopen i) :=
  MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff i.1.modulus)
    (zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i)

The finite-stage source-to-open-image group-algebra map used to descend the source-stage action on the closed finite augmentation quotient to the matching target stage.

@[simp]
theorem zcCompletedGroupAlgebraOpenImageStageRingHom_of
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G)
    (q : CompletedGroupAlgebraQuotientInClass G C i.2) :
    zcCompletedGroupAlgebraOpenImageStageRingHom C hC hForm psi hpsi hfopen i
        (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
          (CompletedGroupAlgebraQuotientInClass G C i.2) q) =
      MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
        (CompletedGroupAlgebraQuotientInClass H C
          (zcCompletedGroupAlgebraOpenImageTargetIndex C hForm psi hpsi hfopen i).2)
        (zcCompletedGroupAlgebraOpenImageQuotientMap
          C hC hForm psi hpsi hfopen i q)

The open-image stage ring homomorphism sends generators according to the finite-stage Fox coordinate formula.

Show Lean proof
theorem zcCompletedGroupAlgebraOpenImageStageRingHom_surjective
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G) :
    Function.Surjective
      (zcCompletedGroupAlgebraOpenImageStageRingHom
        C hC hForm psi hpsi hfopen i)

The finite-stage source-to-open-image group-algebra map is surjective.

Show Lean proof
theorem zcCompletedGroupAlgebraOpenImageStageRingHom_ker_smul_mem
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G)
    (k : ZCCompletedGroupAlgebraStage C G i)
    (hk : k ∈ RingHom.ker
      (zcCompletedGroupAlgebraOpenImageStageRingHom
        C hC hForm psi hpsi hfopen i))
    (s : zcCompletedGroupAlgebraStageAugmentationIdeal C G i) :
    k • s ∈
      zcCompletedGroupAlgebraOpenImageKernelAugmentationIdealMulStageStandard
        C hC hForm psi hpsi hfopen i

Source-stage elements in the kernel of the open-image stage map multiply the finite augmentation stage into the finite kernel-product denominator.

Show Lean proof
theorem kernelAugmentationIdealClosedStageQuotient_openImageStageRingHom_ker_smul_eq_zero
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G)
    (k : ZCCompletedGroupAlgebraStage C G i)
    (hk : k ∈ RingHom.ker
      (zcCompletedGroupAlgebraOpenImageStageRingHom
        C hC hForm psi hpsi hfopen i))
    (x : KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i) :
    k • x = 0

Source-stage kernels act trivially on the closed finite augmentation quotient.

Show Lean proof
@[implicit_reducible]
def kernelAugmentationIdealClosedStageQuotientTargetStageModule
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G) :
    Module
      (ZCCompletedGroupAlgebraStage C H
        (zcCompletedGroupAlgebraOpenImageTargetIndex C hForm psi hpsi hfopen i))
      (KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i) := by
  let φ := zcCompletedGroupAlgebraOpenImageStageRingHom
    C hC hForm psi hpsi hfopen i
  let hφ := zcCompletedGroupAlgebraOpenImageStageRingHom_surjective
    C hC hForm psi hpsi hfopen i
  letI : SMul
      (ZCCompletedGroupAlgebraStage C H
        (zcCompletedGroupAlgebraOpenImageTargetIndex C hForm psi hpsi hfopen i))
      (KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i) :=
    ⟨fun a x => Function.surjInv hφ a • x⟩
  refine hφ.moduleLeft φ ?_
  intro a x
  change Function.surjInv hφ (φ a) • x = a • x
  have hdiff : Function.surjInv hφ (φ a) - a ∈ RingHom.ker φ := by
    rw [RingHom.mem_ker, map_sub, Function.surjInv_eq hφ, sub_self]
  have hzero :=
    kernelAugmentationIdealClosedStageQuotient_openImageStageRingHom_ker_smul_eq_zero
      C hC hForm psi hpsi hfopen i
      (Function.surjInv hφ (φ a) - a) hdiff x
  rw [sub_smul] at hzero
  exact sub_eq_zero.mp hzero

The finite closed augmentation quotient as a module over the matching open-image target group-algebra stage.

theorem kernelAugmentationIdealClosedStageQuotientTargetStageModule_map_smul
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G)
    (a : ZCCompletedGroupAlgebraStage C G i)
    (x : KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i) :
    letI : Module
        (ZCCompletedGroupAlgebraStage C H
          (zcCompletedGroupAlgebraOpenImageTargetIndex C hForm psi hpsi hfopen i))
        (KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i) :=
      kernelAugmentationIdealClosedStageQuotientTargetStageModule
        C hC hForm psi hpsi hfopen i
    zcCompletedGroupAlgebraOpenImageStageRingHom C hC hForm psi hpsi hfopen i a • x =
      a • x

The stage quotient target module map is compatible with scalar multiplication.

Show Lean proof
@[implicit_reducible]
def zcCompletedDifferentialModuleOpenImageIndex
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G) :
    ZCCompletedDifferentialModuleIndex C psi.toMonoidHom where
  source := OrderDual.ofDual i.2
  target := zcCompletedGroupAlgebraOpenImageTargetIndex C hForm psi hpsi hfopen i
  compatible := by
    intro g hg
    change psi g ∈
      ((((OrderDual.ofDual
        (zcCompletedGroupAlgebraOpenImageTargetIndex C hForm psi hpsi hfopen i).2).1 :
          OpenNormalSubgroup H) : Subgroup H))
    exact ⟨g, hg, rfl

The finite source quotient paired with the open-image target stage for a source group-algebra coordinate.

@[simp 900]
theorem zcCompletedDifferentialModuleOpenImageIndex_stageScalar
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G)
    (q : zcCompletedDifferentialModuleStageSource C psi.toMonoidHom
      (zcCompletedDifferentialModuleOpenImageIndex C hForm psi hpsi hfopen i)) :
    zcCompletedDifferentialModuleStageScalar C psi.toMonoidHom
        (zcCompletedDifferentialModuleOpenImageIndex C hForm psi hpsi hfopen i) q =
      zcCompletedGroupAlgebraOpenImageStageRingHom C hC hForm psi hpsi hfopen i
        (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
          (CompletedGroupAlgebraQuotientInClass G C i.2) q)

The open-image stage condition for the \(\mathbb{Z}_C\)-completed differential module is equivalent to the finite-stage coordinate condition.

Show Lean proof
def kernelAugmentationIdealClosedStageQuotientBoundary
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G) :
    let j := zcCompletedDifferentialModuleOpenImageIndex C hForm psi hpsi hfopen i
    letI : Module (zcCompletedDifferentialModuleStageRing C psi.toMonoidHom j)
        (KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i) :=
      kernelAugmentationIdealClosedStageQuotientTargetStageModule
        C hC hForm psi hpsi hfopen i
    ScalarCrossedHom
      (zcCompletedDifferentialModuleStageScalar C psi.toMonoidHom j)
      (KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i) := by
  let j := zcCompletedDifferentialModuleOpenImageIndex C hForm psi hpsi hfopen i
  let T :=
    zcCompletedGroupAlgebraOpenImageKernelAugmentationIdealMulStageStandard
      C hC hForm psi hpsi hfopen i
  letI : Module (zcCompletedDifferentialModuleStageRing C psi.toMonoidHom j)
      (KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i) :=
    kernelAugmentationIdealClosedStageQuotientTargetStageModule
      C hC hForm psi hpsi hfopen i
  refine
    { toFun := fun q =>
        Submodule.Quotient.mk
          (p := zcCompletedGroupAlgebraOpenImageKernelAugmentationIdealMulStageStandard
            C hC hForm psi hpsi hfopen i)
          (zcCompletedGroupAlgebraStageAugmentationGeneratorSubtype C G i q)
      map_mul' := ?_ }
  intro q r
  rw [scalarCrossedAction_apply]
  rw [zcCompletedDifferentialModuleOpenImageIndex_stageScalar
    (C := C) (hC := hC) (hForm := hForm) (psi := psi)
    (hpsi := hpsi) (hfopen := hfopen) (i := i)]
  rw [kernelAugmentationIdealClosedStageQuotientTargetStageModule_map_smul
    (C := C) (hC := hC) (hForm := hForm) (psi := psi)
    (hpsi := hpsi) (hfopen := hfopen) (i := i)
    (a := MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
      (CompletedGroupAlgebraQuotientInClass G C i.2) q)
    (x := Submodule.Quotient.mk
      (p := zcCompletedGroupAlgebraOpenImageKernelAugmentationIdealMulStageStandard
        C hC hForm psi hpsi hfopen i)
      (zcCompletedGroupAlgebraStageAugmentationGeneratorSubtype C G i r))]
  change
    Submodule.Quotient.mk (p := T)
        (zcCompletedGroupAlgebraStageAugmentationGeneratorSubtype C G i (q * r)) =
      Submodule.Quotient.mk (p := T)
          (zcCompletedGroupAlgebraStageAugmentationGeneratorSubtype C G i q) +
        MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
            (CompletedGroupAlgebraQuotientInClass G C i.2) q •
          Submodule.Quotient.mk (p := T)
            (zcCompletedGroupAlgebraStageAugmentationGeneratorSubtype C G i r)
  rw [← Submodule.Quotient.mk_smul, ← Submodule.Quotient.mk_add]
  apply congrArg (fun s : zcCompletedGroupAlgebraStageAugmentationIdeal C G i =>
    Submodule.Quotient.mk (p := T) s)
  apply Subtype.ext
  change
    MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
        (CompletedGroupAlgebraQuotientInClass G C i.2) (q * r) - 1 =
      (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
          (CompletedGroupAlgebraQuotientInClass G C i.2) q - 1) +
        MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
          (CompletedGroupAlgebraQuotientInClass G C i.2) q *
          (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
            (CompletedGroupAlgebraQuotientInClass G C i.2) r - 1)
  change CompletedGroupAlgebraQuotientInClass G C i.2 at q r
  change
    MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
        (CompletedGroupAlgebraQuotientInClass G C i.2) (q * r) - 1 =
      (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
          (CompletedGroupAlgebraQuotientInClass G C i.2) q - 1) +
        MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
          (CompletedGroupAlgebraQuotientInClass G C i.2) q *
          (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
            (CompletedGroupAlgebraQuotientInClass G C i.2) r - 1)
  rw [map_mul, mul_sub, mul_one]
  abel

The finite source-boundary coordinate over the matching open-image target stage.

def kernelAugmentationIdealClosedStageQuotientBoundaryLift
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G) :
    let j := zcCompletedDifferentialModuleOpenImageIndex C hForm psi hpsi hfopen i
    letI : Module (zcCompletedDifferentialModuleStageRing C psi.toMonoidHom j)
        (KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i) :=
      kernelAugmentationIdealClosedStageQuotientTargetStageModule
        C hC hForm psi hpsi hfopen i
    CrossedDifferentialPreModule
        (zcCompletedDifferentialModuleStageRing C psi.toMonoidHom j)
        (zcCompletedDifferentialModuleStageSource C psi.toMonoidHom j) →ₗ[
      zcCompletedDifferentialModuleStageRing C psi.toMonoidHom j]
      KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i := by
  let j := zcCompletedDifferentialModuleOpenImageIndex C hForm psi hpsi hfopen i
  letI : Module (zcCompletedDifferentialModuleStageRing C psi.toMonoidHom j)
      (KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i) :=
    kernelAugmentationIdealClosedStageQuotientTargetStageModule
      C hC hForm psi hpsi hfopen i
  exact
    crossedDifferentialModuleLiftLinear
      (R := zcCompletedDifferentialModuleStageRing C psi.toMonoidHom j)
      (kernelAugmentationIdealClosedStageQuotientBoundary
        C hC hForm psi hpsi hfopen i)

The finite-stage lift induced by the finite closed source-boundary coordinate.

@[simp 900]
theorem kernelAugmentationIdealClosedStageQuotientBoundaryLift_single
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G)
    (q : zcCompletedDifferentialModuleStageSource C psi.toMonoidHom
      (zcCompletedDifferentialModuleOpenImageIndex C hForm psi hpsi hfopen i))
    (a : zcCompletedDifferentialModuleStageRing C psi.toMonoidHom
      (zcCompletedDifferentialModuleOpenImageIndex C hForm psi hpsi hfopen i)) :
    let j := zcCompletedDifferentialModuleOpenImageIndex C hForm psi hpsi hfopen i
    letI : Module (zcCompletedDifferentialModuleStageRing C psi.toMonoidHom j)
        (KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i) :=
      kernelAugmentationIdealClosedStageQuotientTargetStageModule
        C hC hForm psi hpsi hfopen i
    kernelAugmentationIdealClosedStageQuotientBoundaryLift
        C hC hForm psi hpsi hfopen i (Finsupp.single q a) =
      a • kernelAugmentationIdealClosedStageQuotientBoundary
        C hC hForm psi hpsi hfopen i q

The boundary lift lands in the finite-stage closed augmentation quotient by the Fox-differential kernel condition.

Show Lean proof
def zcCompletedGroupAlgebraKernelAugmentationQuotientToClosedQuotient
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    KernelAugmentationIdealQuotient C psi →ₗ[ZCCompletedGroupAlgebra C G]
      KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen :=
  (zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi).mapQ
    (zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
      C hC hForm psi hpsi hfopen)
    LinearMap.id
    (by
      intro x hx
      simpa using
        zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard_le_closed
          C hC hForm psi hpsi hfopen hx)

The canonical quotient map from the algebraic kernel-product quotient to its closed finite-stage quotient.

@[simp]
theorem zcCompletedGroupAlgebraKernelAugmentationQuotientToClosedQuotient_mk
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (x : zcCompletedGroupAlgebraStandardAugmentationIdeal C G) :
    zcCompletedGroupAlgebraKernelAugmentationQuotientToClosedQuotient
        C hC hForm psi hpsi hfopen (Submodule.Quotient.mk x) =
      Submodule.Quotient.mk x

The map from the algebraic kernel-product quotient to the closed quotient sends a representative to its closed quotient class.

Show Lean proof
theorem zcCompletedGAKerAugQuotToClosedQuotient_inj_iff_eq_closed
    {C : ProCGroups.FiniteGroupClass.{u}}
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    {hC : ProCGroups.FiniteGroupClass.Hereditary C}
    {hForm : ProCGroups.FiniteGroupClass.Formation C}
    {psi : ContinuousMonoidHom G H} {hpsi : Function.Surjective psi}
    {hfopen : IsOpenMap psi} :
    Function.Injective
        (zcCompletedGroupAlgebraKernelAugmentationQuotientToClosedQuotient
          C hC hForm psi hpsi hfopen) ↔
      (zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi :
          Set (zcCompletedGroupAlgebraStandardAugmentationIdeal C G)) =
        (zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
          C hC hForm psi hpsi hfopen :
            Set (zcCompletedGroupAlgebraStandardAugmentationIdeal C G))

The canonical map from the algebraic quotient \(I(G) / I(\ker \psi)I(G)\) to the closed finite-stage quotient is injective exactly when the algebraic product already equals its finite-stage closed hull.

Show Lean proof
theorem isClosed_zcCompletedGAKernelAugmentationIdealMulStandard_iff_toClosedQuotient_inj
    {C : ProCGroups.FiniteGroupClass.{u}}
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    {psi : ContinuousMonoidHom G H} (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    IsClosed
        ((zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi :
          Set (zcCompletedGroupAlgebraStandardAugmentationIdeal C G))) ↔
      Function.Injective
        (zcCompletedGroupAlgebraKernelAugmentationQuotientToClosedQuotient
          C hC hForm psi hpsi hfopen)

Closedness of \(I(\ker \psi)I(G)\) is equivalently the injectivity of the canonical map from the algebraic source augmentation quotient to the closed finite-stage quotient.

Show Lean proof
def zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationQuotient
    (psi : ContinuousMonoidHom G H) :
    ScalarCrossedHom
      (zcCompletedGroupAlgebraScalar C (MonoidHom.id G))
      (KernelAugmentationIdealQuotient C psi) :=
  (zcCompletedGroupAlgebraBoundaryToStandardAugmentationIdeal
      C G (MonoidHom.id G)).mapLinear
    (Submodule.mkQ
      (zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi))

The source Fox boundary, valued in the source augmentation quotient.

def zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    ScalarCrossedHom
      (zcCompletedGroupAlgebraScalar C (MonoidHom.id G))
      (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
  (zcCompletedGroupAlgebraBoundaryToStandardAugmentationIdeal
      C G (MonoidHom.id G)).mapLinear
    (Submodule.mkQ
      (zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
        C hC hForm psi hpsi hfopen))

The source Fox boundary, valued in the closed source augmentation quotient.

@[simp]
theorem zcCompletedGroupAlgebraKernelAugmentationQuotientToClosedQuotient_sourceBoundary
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) (g : G) :
    zcCompletedGroupAlgebraKernelAugmentationQuotientToClosedQuotient
        C hC hForm psi hpsi hfopen
        (zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationQuotient C psi g) =
      zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
        C hC hForm psi hpsi hfopen g

The map from the algebraic source augmentation quotient to the closed quotient sends source boundary classes to the corresponding closed source boundary classes.

Show Lean proof
theorem continuous_zcCompletedGASourceBoundaryToKerAugClosedQuot
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    Continuous
      (zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
        C hC hForm psi hpsi hfopen)

The source Fox boundary into the closed source augmentation quotient is continuous.

Show Lean proof
omit [IsTopologicalGroup H] in
@[simp]
theorem zcCompletedGroupAlgebraKernelAugmentationIdealQuotient_mk_generator_smul
    (psi : ContinuousMonoidHom G H) (n : ProfiniteKernelSubgroup psi)
    (s : zcCompletedGroupAlgebraStandardAugmentationIdeal C G) :
    Submodule.Quotient.mk
        (p := zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi)
        ((zcGroupLike C G n.1 - 1) • s) = 0

Products \((n-1)s\) vanish in the source augmentation quotient.

Show Lean proof
omit [IsTopologicalGroup H] in
theorem zcCompletedGroupAlgebraKernelAugmentationQuotient_groupLike_smul_eq_of_map_eq
    (psi : ContinuousMonoidHom G H) {g₁ g₂ : G} (h : psi g₁ = psi g₂)
    (x : KernelAugmentationIdealQuotient C psi) :
    zcGroupLike C G g₁ • x = zcGroupLike C G g₂ • x

Source group-like actions with the same image under psi agree on the source augmentation quotient. This is the algebraic descent statement needed before a completed target scalar action can be installed.

Show Lean proof
omit [IsTopologicalGroup H] in
def zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupLikeEndOfSurjective
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) (h : H) :
    AddMonoid.End (KernelAugmentationIdealQuotient C psi) where
  toFun x := zcGroupLike C G (Function.surjInv hpsi h) • x
  map_zero' := smul_zero _
  map_add' := by
    intro x y
    rw [smul_add]

The additive endomorphism of the source augmentation quotient induced by any chosen lift of a target element.

omit [IsTopologicalGroup H] in
@[simp]
theorem zcCompletedGAKerAugQuotTargetGroupLikeEndOfSurjective_apply
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) (h : H)
    (x : KernelAugmentationIdealQuotient C psi) :
    zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupLikeEndOfSurjective
        C psi hpsi h x =
      zcGroupLike C G (Function.surjInv hpsi h) • x

The chosen-lift target group-like endomorphism acts by scalar multiplication with the completed group-like element of the selected source lift.

Show Lean proof
omit [IsTopologicalGroup H] in
theorem zcCompletedGAKerAugQuotTargetGroupLikeEndOfSurjective_eq_smul_of_map_eq
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) {h : H} {g : G}
    (hg : psi g = h) (x : KernelAugmentationIdealQuotient C psi) :
    zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupLikeEndOfSurjective
        C psi hpsi h x =
      zcGroupLike C G g • x

The chosen-lift target action agrees with scalar multiplication by any source lift of the same target element.

Show Lean proof
omit [IsTopologicalGroup H] in
@[simp]
theorem zcCompletedGAKerAugQuotTargetGroupLikeEndOfSurjective_one_apply
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (x : KernelAugmentationIdealQuotient C psi) :
    zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupLikeEndOfSurjective
        C psi hpsi (1 : H) x = x

The chosen-lift target group-like endomorphism for the identity target element acts as the identity.

Show Lean proof
omit [IsTopologicalGroup H] in
theorem zcCompletedGAKerAugQuotTargetGroupLikeEndOfSurjective_mul_apply
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) (h₁ h₂ : H)
    (x : KernelAugmentationIdealQuotient C psi) :
    zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupLikeEndOfSurjective
        C psi hpsi (h₁ * h₂) x =
      zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupLikeEndOfSurjective
        C psi hpsi h₁
        (zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupLikeEndOfSurjective
          C psi hpsi h₂ x)

The chosen-lift target group-like endomorphisms multiply pointwise on the quotient.

Show Lean proof
omit [IsTopologicalGroup H] in
def zcCompletedGAKerAugQuotTargetGroupLikeActionOfSurjective
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) :
    H →* AddMonoid.End (KernelAugmentationIdealQuotient C psi) where
  toFun h :=
    zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupLikeEndOfSurjective
      C psi hpsi h
  map_one' := by
    refine AddMonoidHom.ext ?_
    intro x
    exact
      zcCompletedGAKerAugQuotTargetGroupLikeEndOfSurjective_one_apply
        C psi hpsi x
  map_mul' h₁ h₂ := by
    refine AddMonoidHom.ext ?_
    intro x
    change
      zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupLikeEndOfSurjective
          C psi hpsi (h₁ * h₂) x =
        zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupLikeEndOfSurjective
          C psi hpsi h₁
          (zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupLikeEndOfSurjective
            C psi hpsi h₂ x)
    exact
      zcCompletedGAKerAugQuotTargetGroupLikeEndOfSurjective_mul_apply
        C psi hpsi h₁ h₂ x

The descended group-like target action on the source augmentation quotient, for a surjective \(\psi\).

omit [IsTopologicalGroup H] in
@[simp]
theorem zcCompletedGAKerAugQuotTargetGroupLikeActionOfSurjective_apply
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) (h : H)
    (x : KernelAugmentationIdealQuotient C psi) :
    zcCompletedGAKerAugQuotTargetGroupLikeActionOfSurjective
        C psi hpsi h x =
      zcGroupLike C G (Function.surjInv hpsi h) • x

The descended target group-like action for a surjective map acts through the selected source lift.

Show Lean proof
omit [IsTopologicalGroup H] in
def zcCompletedGroupAlgebraKernelAugmentationQuotientTargetCoeffEnd
    (psi : ContinuousMonoidHom G H) (a : ZCCoeff C) :
    AddMonoid.End (KernelAugmentationIdealQuotient C psi) where
  toFun x := zcCompletedGroupAlgebraCoeffMap C G a • x
  map_zero' := smul_zero _
  map_add' := by
    intro x y
    rw [smul_add]

Coefficients from \(\mathbb{Z}_C\) act on the source augmentation quotient through the source completed group algebra.

omit [IsTopologicalGroup H] in
@[simp]
theorem zcCompletedGroupAlgebraKernelAugmentationQuotientTargetCoeffEnd_apply
    (psi : ContinuousMonoidHom G H) (a : ZCCoeff C)
    (x : KernelAugmentationIdealQuotient C psi) :
    zcCompletedGroupAlgebraKernelAugmentationQuotientTargetCoeffEnd C psi a x =
      zcCompletedGroupAlgebraCoeffMap C G a • x

The target coefficient endomorphism acts on the kernel-augmentation quotient by multiplication with the coefficient-map image of a.

Show Lean proof
omit [IsTopologicalGroup H] in
def zcCompletedGroupAlgebraKernelAugmentationQuotientTargetCoeffAction
    (psi : ContinuousMonoidHom G H) :
    ZCCoeff C →+* AddMonoid.End (KernelAugmentationIdealQuotient C psi) where
  toFun a := zcCompletedGroupAlgebraKernelAugmentationQuotientTargetCoeffEnd C psi a
  map_zero' := by
    refine AddMonoidHom.ext ?_
    intro x
    change zcCompletedGroupAlgebraCoeffMap C G (0 : ZCCoeff C) • x = 0
    rw [map_zero, zero_smul]
  map_one' := by
    refine AddMonoidHom.ext ?_
    intro x
    change zcCompletedGroupAlgebraCoeffMap C G (1 : ZCCoeff C) • x = x
    rw [map_one, one_smul]
  map_add' a b := by
    refine AddMonoidHom.ext ?_
    intro x
    change zcCompletedGroupAlgebraCoeffMap C G (a + b) • x =
      zcCompletedGroupAlgebraCoeffMap C G a • x +
        zcCompletedGroupAlgebraCoeffMap C G b • x
    rw [map_add, add_smul]
  map_mul' a b := by
    refine AddMonoidHom.ext ?_
    intro x
    change zcCompletedGroupAlgebraCoeffMap C G (a * b) • x =
      zcCompletedGroupAlgebraCoeffMap C G a •
        (zcCompletedGroupAlgebraCoeffMap C G b • x)
    rw [map_mul, mul_smul]

The coefficient action of \(\mathbb{Z}_C\) on the source augmentation quotient.

omit [IsTopologicalGroup H] in
theorem zcCompletedGroupAlgebraCoeffMap_mul_groupLike_eq_groupLike_mul_coeffMap
    (a : ZCCoeff C) (g : G) :
    zcCompletedGroupAlgebraCoeffMap C G a * zcGroupLike C G g =
      zcGroupLike C G g * zcCompletedGroupAlgebraCoeffMap C G a

Coefficient elements are central with respect to group-like elements in \(\mathbb{Z}_C\llbracket G\rrbracket\).

Show Lean proof
omit [IsTopologicalGroup H] in
def kerAugQuotTargetGAActionOfSurj
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) :
    MonoidAlgebra (ZCCoeff C) H →+*
      AddMonoid.End (KernelAugmentationIdealQuotient C psi) :=
  MonoidAlgebra.liftNCRingHom
    (zcCompletedGroupAlgebraKernelAugmentationQuotientTargetCoeffAction C psi)
    (zcCompletedGAKerAugQuotTargetGroupLikeActionOfSurjective
      C psi hpsi)
    (by
      intro a h
      rw [Commute]
      apply AddMonoidHom.ext
      intro x
      change
        zcCompletedGroupAlgebraCoeffMap C G a •
            (zcGroupLike C G (Function.surjInv hpsi h) • x) =
          zcGroupLike C G (Function.surjInv hpsi h) •
            (zcCompletedGroupAlgebraCoeffMap C G a • x)
      rw [← mul_smul, ← mul_smul,
        zcCompletedGroupAlgebraCoeffMap_mul_groupLike_eq_groupLike_mul_coeffMap])

The algebraic target group algebra \(\mathbb{Z}_C[H]\) acts on the source augmentation quotient. This is the dense algebraic part of the eventual completed \(\mathbb{Z}_C\llbracket H\rrbracket\) scalar action.

omit [IsTopologicalGroup H] in
@[simp]
theorem kerAugQuotTargetGAActionOfSurj_of
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) (h : H) :
    kerAugQuotTargetGAActionOfSurj
        C psi hpsi (MonoidAlgebra.of (ZCCoeff C) H h) =
      zcCompletedGAKerAugQuotTargetGroupLikeActionOfSurjective
        C psi hpsi h

The induced target group-algebra action evaluates on group-like elements by lifting through the chosen surjection.

Show Lean proof
omit [IsTopologicalGroup H] in
noncomputable abbrev
    zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupAlgebraModuleOfSurjective
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) :
    Module (MonoidAlgebra (ZCCoeff C) H) (KernelAugmentationIdealQuotient C psi) :=
  Module.compHom (KernelAugmentationIdealQuotient C psi)
    (kerAugQuotTargetGAActionOfSurj
      C psi hpsi)

The descended algebraic Z_C[H]-module structure on the source augmentation quotient.

omit [IsTopologicalGroup H] in
@[simp]
theorem kerAugQuotTargetGAModuleOfSurj_smul
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (a : MonoidAlgebra (ZCCoeff C) H) (x : KernelAugmentationIdealQuotient C psi) :
    letI : Module (MonoidAlgebra (ZCCoeff C) H) (KernelAugmentationIdealQuotient C psi) :=
      zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupAlgebraModuleOfSurjective
        C psi hpsi
    a • x =
      kerAugQuotTargetGAActionOfSurj
        C psi hpsi a x

The target group-algebra module structure acts by the induced quotient action.

Show Lean proof
omit [IsTopologicalGroup H] in
@[simp]
theorem kerAugQuotTargetGAModuleOfSurj_of_smul
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) (h : H)
    (x : KernelAugmentationIdealQuotient C psi) :
    letI : Module (MonoidAlgebra (ZCCoeff C) H) (KernelAugmentationIdealQuotient C psi) :=
      zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupAlgebraModuleOfSurjective
        C psi hpsi
    MonoidAlgebra.of (ZCCoeff C) H h • x =
      zcGroupLike C G (Function.surjInv hpsi h) • x

A group-like basis element acts on the target quotient module by the induced quotient action.

Show Lean proof
omit [IsTopologicalGroup H] in
theorem kerAugQuotTargetGAModuleOfSurj_of_smul_eq_source_groupLike_smul
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) {h : H} {g : G}
    (hg : psi g = h) (x : KernelAugmentationIdealQuotient C psi) :
    letI : Module (MonoidAlgebra (ZCCoeff C) H) (KernelAugmentationIdealQuotient C psi) :=
      zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupAlgebraModuleOfSurjective
        C psi hpsi
    MonoidAlgebra.of (ZCCoeff C) H h • x = zcGroupLike C G g • x

The algebraic target group-algebra action by \([h]\) agrees with source multiplication by any lift of \(h\).

Show Lean proof
omit [IsTopologicalGroup H] in
def zcCompletedGASourceBoundaryToKerAugQuotTargetGACrossedHomOfSurjective
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) :
    letI : Module (MonoidAlgebra (ZCCoeff C) H) (KernelAugmentationIdealQuotient C psi) :=
      zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupAlgebraModuleOfSurjective
        C psi hpsi
    ScalarCrossedHom
      ((MonoidAlgebra.of (ZCCoeff C) H).comp psi.toMonoidHom)
      (KernelAugmentationIdealQuotient C psi) := by
  letI : Module (MonoidAlgebra (ZCCoeff C) H) (KernelAugmentationIdealQuotient C psi) :=
    zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupAlgebraModuleOfSurjective
      C psi hpsi
  exact
    { toFun := zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationQuotient C psi
      map_mul' := by
        intro g h
        rw [(zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationQuotient
          C psi).map_mul]
        congr 1
        exact
          (kerAugQuotTargetGAModuleOfSurj_of_smul_eq_source_groupLike_smul
            C psi hpsi (h := psi g) (g := g) rfl
            (zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationQuotient
              C psi h)).symm }

The source boundary is a crossed differential for the descended algebraic target group-algebra coefficients.

omit [IsTopologicalGroup H] in
def zcAlgebraicDifferentialModuleToKernelAugmentationQuotientOfSurjective
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) :
    letI : Module (MonoidAlgebra (ZCCoeff C) H) (KernelAugmentationIdealQuotient C psi) :=
      zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupAlgebraModuleOfSurjective
        C psi hpsi
    CrossedDifferentialModule ((MonoidAlgebra.of (ZCCoeff C) H).comp psi.toMonoidHom) →ₗ[
      MonoidAlgebra (ZCCoeff C) H] KernelAugmentationIdealQuotient C psi := by
  letI : Module (MonoidAlgebra (ZCCoeff C) H) (KernelAugmentationIdealQuotient C psi) :=
    zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupAlgebraModuleOfSurjective
      C psi hpsi
  exact
    crossedHomModuleLift
      (A := KernelAugmentationIdealQuotient C psi)
      ((MonoidAlgebra.of (ZCCoeff C) H).comp psi.toMonoidHom)
      (zcCompletedGASourceBoundaryToKerAugQuotTargetGACrossedHomOfSurjective
        C psi hpsi)

The algebraic target-coefficient universal differential module maps to the source augmentation quotient by \(dg \mapsto\) \([g]-1\).

omit [IsTopologicalGroup H] in
@[simp]
theorem zcAlgebraicDifferentialModuleToKernelAugmentationQuotientOfSurjective_universal
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) (g : G) :
    letI : Module (MonoidAlgebra (ZCCoeff C) H) (KernelAugmentationIdealQuotient C psi) :=
      zcCompletedGroupAlgebraKernelAugmentationQuotientTargetGroupAlgebraModuleOfSurjective
        C psi hpsi
    zcAlgebraicDifferentialModuleToKernelAugmentationQuotientOfSurjective C psi hpsi
        (universalCrossedDifferential
          ((MonoidAlgebra.of (ZCCoeff C) H).comp psi.toMonoidHom) g) =
      zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationQuotient C psi g

The algebraic differential module maps universally to the kernel-augmentation quotient in the surjective case.

Show Lean proof
omit [IsTopologicalGroup H] in
theorem mulStandard_mul_mem_of_mem_kernelAugIdealMul
    (psi : ContinuousMonoidHom G H)
    {k : ZCCompletedGroupAlgebra C G}
    (hk : k ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi)
    (y : zcCompletedGroupAlgebraStandardAugmentationIdeal C G) :
    (⟨k * (y : ZCCompletedGroupAlgebra C G),
      (zcCompletedGroupAlgebraStandardAugmentationIdeal C G).mul_mem_left k y.2⟩ :
        zcCompletedGroupAlgebraStandardAugmentationIdeal C G) ∈
      zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi

Multiplying an algebraic kernel-augmentation element by a standard augmentation element lands in the algebraic product \(I(\ker \psi)I(G)\). The remaining completed-target descent problem is exactly replacing the first hypothesis by membership in the completed map kernel.

Show Lean proof
theorem zcCompletedGAKernelAugmentationIdealMulStandard_mul_mem_closure_of_mem_ker_map
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    {k : ZCCompletedGroupAlgebra C G}
    (hk : k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi))
    (y : zcCompletedGroupAlgebraStandardAugmentationIdeal C G) :
    (⟨k * (y : ZCCompletedGroupAlgebra C G),
      (zcCompletedGroupAlgebraStandardAugmentationIdeal C G).mul_mem_left k y.2⟩ :
        zcCompletedGroupAlgebraStandardAugmentationIdeal C G) ∈
      closure
        ((zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi :
          Set (zcCompletedGroupAlgebraStandardAugmentationIdeal C G)))

Under the finite-stage open-map kernel theorem, a completed-kernel scalar times a standard augmentation element lies in the closure of the algebraic product; no closedness hypothesis is assumed.

Show Lean proof
theorem zcCompletedGAKernelAugmentationIdealMulStandard_mul_mem_closed_of_mem_ker_map
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    {k : ZCCompletedGroupAlgebra C G}
    (hk : k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi))
    (y : zcCompletedGroupAlgebraStandardAugmentationIdeal C G) :
    (⟨k * (y : ZCCompletedGroupAlgebra C G),
      (zcCompletedGroupAlgebraStandardAugmentationIdeal C G).mul_mem_left k y.2⟩ :
        zcCompletedGroupAlgebraStandardAugmentationIdeal C G) ∈
      zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
        C hC hForm psi hpsi hfopen

If \(k\) lies in the kernel of the completed group-algebra map, then \(k y\) lies in the finite-stage closed hull of \(I(\ker\psi)I(G)\) for every standard augmentation element \(y\).

Show Lean proof
theorem zcCompletedGAKernelAugmentationIdealMulStandard_kernelMulStandard_le_closed
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    ∀ k : ZCCompletedGroupAlgebra C G,
      k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) →
      ∀ y : zcCompletedGroupAlgebraStandardAugmentationIdeal C G,
        (⟨k * (y : ZCCompletedGroupAlgebra C G),
          (zcCompletedGroupAlgebraStandardAugmentationIdeal C G).mul_mem_left k y.2⟩ :
            zcCompletedGroupAlgebraStandardAugmentationIdeal C G) ∈
          zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
            C hC hForm psi hpsi hfopen

Completed-kernel scalars send the standard source augmentation ideal into the finite-stage closed hull of \(I(\ker \psi)I(G)\).

Show Lean proof
theorem zcCompletedGAKernelAugmentationIdealMulStandard_kernelMulStandard_le_of_isClosed
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (hclosed :
      IsClosed
        ((zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi :
          Set (zcCompletedGroupAlgebraStandardAugmentationIdeal C G)))) :
    ∀ k : ZCCompletedGroupAlgebra C G,
      k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) →
      ∀ y : zcCompletedGroupAlgebraStandardAugmentationIdeal C G,
        (⟨k * (y : ZCCompletedGroupAlgebra C G),
          (zcCompletedGroupAlgebraStandardAugmentationIdeal C G).mul_mem_left k y.2⟩ :
            zcCompletedGroupAlgebraStandardAugmentationIdeal C G) ∈
          zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi

If the algebraic product \(I(\ker \psi)I(G)\) is closed in the standard augmentation ideal, then completed-kernel scalars send standard augmentation elements into that product.

Show Lean proof
theorem kernelMulStandard_le_of_toClosedQuotient_inj
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (hinj :
      Function.Injective
        (zcCompletedGroupAlgebraKernelAugmentationQuotientToClosedQuotient
          C hC hForm psi hpsi hfopen)) :
    ∀ k : ZCCompletedGroupAlgebra C G,
      k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) →
      ∀ y : zcCompletedGroupAlgebraStandardAugmentationIdeal C G,
        (⟨k * (y : ZCCompletedGroupAlgebra C G),
          (zcCompletedGroupAlgebraStandardAugmentationIdeal C G).mul_mem_left k y.2⟩ :
            zcCompletedGroupAlgebraStandardAugmentationIdeal C G) ∈
          zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi

If the canonical map from the algebraic source augmentation quotient to the closed finite-stage quotient is injective, then completed-kernel scalars multiply standard augmentation elements into the algebraic product \(I(\ker \psi)I(G)\). This descent step uses finite-stage closed membership and converts it back to algebraic membership through injectivity of the quotient comparison map.

Show Lean proof
theorem zcCompletedGAKerAugQuot_ker_map_smul_eq_zero_of_kernelMulStandard_le
    (hC : ProCGroups.FiniteGroupClass.Hereditary C) (psi : ContinuousMonoidHom G H)
    (hker_mul :
      ∀ k : ZCCompletedGroupAlgebra C G,
        k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) →
        ∀ y : zcCompletedGroupAlgebraStandardAugmentationIdeal C G,
          (⟨k * (y : ZCCompletedGroupAlgebra C G),
            (zcCompletedGroupAlgebraStandardAugmentationIdeal C G).mul_mem_left k y.2⟩ :
              zcCompletedGroupAlgebraStandardAugmentationIdeal C G) ∈
            zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi)
    (k : ZCCompletedGroupAlgebra C G)
    (hk : k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi))
    (x : KernelAugmentationIdealQuotient C psi) :
    k • x = 0

If every completed-kernel scalar sends the standard source augmentation ideal into \(I(\ker \psi)I(G)\), then the completed kernel acts trivially on the quotient.

Show Lean proof
def zcCompletedGroupAlgebraTargetLiftOfSurjective
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi) :
    ZCCompletedGroupAlgebra C H → ZCCompletedGroupAlgebra C G :=
  Function.surjInv
    (zcCompletedGroupAlgebraMap_surjective_of_surjective
      (C := C) (hC := hC) hForm psi hpsi)

Conditional descent of the source action to a completed target \(\mathbb{Z}_C\llbracket H\rrbracket\)-module. The extra hypothesis is exactly the missing kernel-product statement; it is kept explicit so that closure membership is not used as algebraic equality.

@[simp 900]
theorem zcCompletedGroupAlgebraMap_targetLiftOfSurjective
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (a : ZCCompletedGroupAlgebra C H) :
    zcCompletedGroupAlgebraMap C hC psi
        (zcCompletedGroupAlgebraTargetLiftOfSurjective C hC hForm psi hpsi a) = a

For a surjective presentation, the completed group-algebra map sends the chosen target lift of a back to a.

Show Lean proof
@[implicit_reducible]
def zcCompletedGAKerAugQuotTargetCompletedModuleOfSurjective_of_kernelMulStandard_le
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hker_mul :
      ∀ k : ZCCompletedGroupAlgebra C G,
        k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) →
        ∀ y : zcCompletedGroupAlgebraStandardAugmentationIdeal C G,
          (⟨k * (y : ZCCompletedGroupAlgebra C G),
            (zcCompletedGroupAlgebraStandardAugmentationIdeal C G).mul_mem_left k y.2⟩ :
              zcCompletedGroupAlgebraStandardAugmentationIdeal C G) ∈
            zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi) :
    Module (ZCCompletedGroupAlgebra C H) (KernelAugmentationIdealQuotient C psi) := by
  letI : SMul (ZCCompletedGroupAlgebra C H)
      (KernelAugmentationIdealQuotient C psi) :=
    ⟨fun a x => zcCompletedGroupAlgebraTargetLiftOfSurjective
      C hC hForm psi hpsi a • x⟩
  refine (zcCompletedGroupAlgebraMap_surjective_of_surjective
    (C := C) (hC := hC) hForm psi hpsi).moduleLeft
      (zcCompletedGroupAlgebraMap C hC psi) ?_
  intro a x
  change zcCompletedGroupAlgebraTargetLiftOfSurjective C hC hForm psi hpsi
      (zcCompletedGroupAlgebraMap C hC psi a) • x =
    a • x
  have hdiff :
      zcCompletedGroupAlgebraTargetLiftOfSurjective C hC hForm psi hpsi
          (zcCompletedGroupAlgebraMap C hC psi a) - a ∈
        RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) := by
    change zcCompletedGroupAlgebraMap C hC psi
        (zcCompletedGroupAlgebraTargetLiftOfSurjective C hC hForm psi hpsi
          (zcCompletedGroupAlgebraMap C hC psi a) - a) = 0
    rw [map_sub, zcCompletedGroupAlgebraMap_targetLiftOfSurjective, sub_self]
  have hzero :=
    zcCompletedGAKerAugQuot_ker_map_smul_eq_zero_of_kernelMulStandard_le
      C hC psi hker_mul
      (zcCompletedGroupAlgebraTargetLiftOfSurjective C hC hForm psi hpsi
        (zcCompletedGroupAlgebraMap C hC psi a) - a) hdiff x
  rw [sub_smul] at hzero
  exact sub_eq_zero.mp hzero

The kernel-multiple containment hypothesis makes the source augmentation quotient a module over the target completed group algebra, using chosen lifts along the surjective presentation.

@[implicit_reducible]
def zcCompletedGAKerAugQuotTargetCompletedModuleOfSurjective_of_closed_kernelMulStandard
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (hclosed :
      IsClosed
        ((zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi :
          Set (zcCompletedGroupAlgebraStandardAugmentationIdeal C G)))) :
    Module (ZCCompletedGroupAlgebra C H) (KernelAugmentationIdealQuotient C psi) :=
  zcCompletedGAKerAugQuotTargetCompletedModuleOfSurjective_of_kernelMulStandard_le
    C hC hForm psi hpsi
    (zcCompletedGAKernelAugmentationIdealMulStandard_kernelMulStandard_le_of_isClosed
      C hC hForm psi hpsi hfopen hclosed)

Closedness of the kernel-multiple submodule supplies the containment needed to descend the target completed-group-algebra module structure to the source augmentation quotient.

theorem zcCompletedGroupAlgebraKernelAugmentationClosedQuotient_ker_map_smul_eq_zero
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (k : ZCCompletedGroupAlgebra C G)
    (hk : k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi))
    (x : KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :
    k • x = 0

The completed kernel acts trivially on the closed source augmentation quotient.

Show Lean proof
@[implicit_reducible]
def kerAugClosedQuotTargetCompletedModuleOfSurj
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    Module (ZCCompletedGroupAlgebra C H)
      (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) := by
  letI : SMul (ZCCompletedGroupAlgebra C H)
      (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
    ⟨fun a x => zcCompletedGroupAlgebraTargetLiftOfSurjective
      C hC hForm psi hpsi a • x⟩
  refine (zcCompletedGroupAlgebraMap_surjective_of_surjective
    (C := C) (hC := hC) hForm psi hpsi).moduleLeft
      (zcCompletedGroupAlgebraMap C hC psi) ?_
  intro a x
  change zcCompletedGroupAlgebraTargetLiftOfSurjective C hC hForm psi hpsi
      (zcCompletedGroupAlgebraMap C hC psi a) • x =
    a • x
  have hdiff :
      zcCompletedGroupAlgebraTargetLiftOfSurjective C hC hForm psi hpsi
          (zcCompletedGroupAlgebraMap C hC psi a) - a ∈
        RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) := by
    change zcCompletedGroupAlgebraMap C hC psi
        (zcCompletedGroupAlgebraTargetLiftOfSurjective C hC hForm psi hpsi
          (zcCompletedGroupAlgebraMap C hC psi a) - a) = 0
    rw [map_sub, zcCompletedGroupAlgebraMap_targetLiftOfSurjective, sub_self]
  have hzero :=
    zcCompletedGroupAlgebraKernelAugmentationClosedQuotient_ker_map_smul_eq_zero
      C hC hForm psi hpsi hfopen
      (zcCompletedGroupAlgebraTargetLiftOfSurjective C hC hForm psi hpsi
        (zcCompletedGroupAlgebraMap C hC psi a) - a) hdiff x
  rw [sub_smul] at hzero
  exact sub_eq_zero.mp hzero

Unconditional descent of the source action to a completed target \(\mathbb{Z}_C\llbracket H\rrbracket\)-module on the closed source augmentation quotient.

theorem kerAugClosedQuotTargetCompletedModuleOfSurj_map_smul
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (a : ZCCompletedGroupAlgebra C G)
    (x : KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    zcCompletedGroupAlgebraMap C hC psi a • x = a • x

The closed quotient target module action is compatible with mapped scalars.

Show Lean proof
theorem continuous_zcCompletedGAKerAugClosedQuot_source_smul_const
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (x : KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :
    Continuous (fun a : ZCCompletedGroupAlgebra C G => a • x)

Source scalar multiplication on the closed source augmentation quotient is continuous in the source scalar, for a fixed quotient element.

Show Lean proof
theorem continuous_kerAugClosedQuotTargetCompletedModuleOfSurj_smul_const
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (x : KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    Continuous (fun a : ZCCompletedGroupAlgebra C H => a • x)

Descended target scalar multiplication on the closed source augmentation quotient is continuous in the target scalar, for a fixed quotient element.

Show Lean proof
theorem continuous_zcCompletedGroupAlgebraKernelAugmentationClosedQuotient_source_smul
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    Continuous (fun p : ZCCompletedGroupAlgebra C G ×
        KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen =>
      p.1 • p.2)

Source scalar multiplication on the closed source augmentation quotient is jointly continuous.

Show Lean proof
theorem continuous_kerAugClosedQuotTargetCompletedModuleOfSurj_smul
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    Continuous (fun p : ZCCompletedGroupAlgebra C H ×
        KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen =>
      p.1 • p.2)

Descended target scalar multiplication on the closed source augmentation quotient is jointly continuous.

Show Lean proof
theorem continuousSMul_zcCompletedGroupAlgebraKernelAugmentationClosedQuotient_source
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    ContinuousSMul (ZCCompletedGroupAlgebra C G)
      (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) where
  continuous_smul

The closed source augmentation quotient is a topological module for the source completed group algebra.

Show Lean proof
theorem continuousSMul_kerAugClosedQuotTargetCompletedModuleOfSurj
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    ContinuousSMul (ZCCompletedGroupAlgebra C H)
      (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)

The descended target module structure on the closed source augmentation quotient is topological.

Show Lean proof
theorem kerAugClosedQuotTargetCompletedModuleOfSurj_groupLike_smul
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (g : G) (x : KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    zcGroupLike C H (psi g) • x = zcGroupLike C G g • x

Group-like elements act on the closed quotient target module by the induced target action.

Show Lean proof
def zcCompletedGASourceBoundaryToKerAugClosedQuotTargetCompletedCrossedHomOfSurjective
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    ScalarCrossedHom
      (zcCompletedGroupAlgebraScalar C psi.toMonoidHom)
      (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) := by
  letI : Module (ZCCompletedGroupAlgebra C H)
      (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
    kerAugClosedQuotTargetCompletedModuleOfSurj
      C hC hForm psi hpsi hfopen
  exact
    { toFun :=
        zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
          C hC hForm psi hpsi hfopen
      map_mul' := by
        intro g h
        rw [(zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
          C hC hForm psi hpsi hfopen).map_mul]
        congr 1
        change zcGroupLike C G g •
            zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
              C hC hForm psi hpsi hfopen h =
          zcGroupLike C H (psi g) •
            zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
              C hC hForm psi hpsi hfopen h
        exact
          (kerAugClosedQuotTargetCompletedModuleOfSurj_groupLike_smul
            C hC hForm psi hpsi hfopen g
            (zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
              C hC hForm psi hpsi hfopen h)).symm }

The source boundary to the closed source augmentation quotient is a crossed differential for the descended completed target scalars.

theorem zcCompletedGroupAlgebraOpenImageStageRingHom_projection_targetLift
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G)
    (a : ZCCompletedGroupAlgebra C H) :
    zcCompletedGroupAlgebraOpenImageStageRingHom C hC hForm psi hpsi hfopen i
        (zcCompletedGroupAlgebraProjection C G i
          (zcCompletedGroupAlgebraTargetLiftOfSurjective C hC hForm psi hpsi a)) =
      zcCompletedGroupAlgebraProjection C H
        (zcCompletedGroupAlgebraOpenImageTargetIndex C hForm psi hpsi hfopen i) a

Projecting a chosen completed source lift of a target coefficient to a source stage and then passing to the open-image stage recovers the corresponding target finite-stage projection.

Show Lean proof
theorem kerAugIdealClosedQuotStageProj_liftLinear_eq_boundaryLift_preStageMap
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G)
    (x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    kernelAugmentationIdealClosedQuotientStageProjection
        C hC hForm psi hpsi hfopen i
        (crossedDifferentialModuleLiftLinear
          (R := ZCCompletedGroupAlgebra C H)
          (zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
            C hC hForm psi hpsi hfopen) x) =
      kernelAugmentationIdealClosedStageQuotientBoundaryLift
        C hC hForm psi hpsi hfopen i
        (zcCompletedDifferentialModulePreStageMap C psi.toMonoidHom
          (zcCompletedDifferentialModuleOpenImageIndex C hForm psi hpsi hfopen i) x)

The i-th closed augmentation quotient coordinate of the completed source-boundary lift factors through the corresponding open-image finite pre-stage.

Show Lean proof
theorem continuous_kernelAugmentationIdealClosedQuotientStageProjection_liftLinear
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (i : ZCCompletedGroupAlgebraIndex C G) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    @Continuous
      (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
      (KernelAugmentationIdealClosedStageQuotient C hC hForm psi hpsi hfopen i)
      (zcCompletedDifferentialPreModuleNaturalTopology C psi.toMonoidHom)
      inferInstance
      (fun x =>
        kernelAugmentationIdealClosedQuotientStageProjection
          C hC hForm psi hpsi hfopen i
          (crossedDifferentialModuleLiftLinear
            (R := ZCCompletedGroupAlgebra C H)
            (zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
              C hC hForm psi hpsi hfopen) x))

Each finite closed-augmentation coordinate of the pre-quotient source-boundary lift is continuous for the finite-stage pre-module topology.

Show Lean proof
theorem continuous_crossedDiffModuleLiftLinear_sourceBoundaryToKerAugClosedQuot
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    @Continuous
      (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
      (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
      (zcCompletedDifferentialPreModuleNaturalTopology C psi.toMonoidHom)
      inferInstance
      (crossedDifferentialModuleLiftLinear
        (R := ZCCompletedGroupAlgebra C H)
        (zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
          C hC hForm psi hpsi hfopen))

The pre-quotient source-boundary lift to the closed source augmentation quotient is continuous for the finite-stage pre-module topology.

Show Lean proof
def zcSeparatedUniversalDifferentialSourceCompletedCrossedHom
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H) :
    letI : Module (ZCCompletedGroupAlgebra C G)
        (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
      Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
    ScalarCrossedHom
      (zcCompletedGroupAlgebraScalar C (MonoidHom.id G))
      (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) := by
  letI : Module (ZCCompletedGroupAlgebra C G)
      (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
    Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
  exact
    { toFun := zcSeparatedUniversalDifferential C psi.toMonoidHom
      map_mul' := by
        intro g h
        rw [(zcSeparatedUniversalDifferential C psi.toMonoidHom).map_mul]
        congr 1
        change zcGroupLike C H (psi g) •
            zcSeparatedUniversalDifferential C psi.toMonoidHom h =
          zcCompletedGroupAlgebraMap C hC psi (zcGroupLike C G g) •
            zcSeparatedUniversalDifferential C psi.toMonoidHom h
        rw [zcCompletedGroupAlgebraMap_groupLike] }

The separated universal differential is also a crossed differential for source completed group-algebra scalars after restricting scalars along \(\mathbb{Z}_C\llbracket G\rrbracket \to \mathbb{Z}_C\llbracket H\rrbracket\).

def zcCompletedDifferentialModuleIdToZCSeparatedCompletedDifferentialModule
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H) :
    letI : Module (ZCCompletedGroupAlgebra C G)
        (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
      Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
    ZCCompletedDifferentialModule C (MonoidHom.id G) →ₗ[ZCCompletedGroupAlgebra C G]
      ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom := by
  letI : Module (ZCCompletedGroupAlgebra C G)
      (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
    Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
  exact
    crossedHomModuleLift
      (A := ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom)
      (zcCompletedGroupAlgebraScalar C (MonoidHom.id G))
      (zcSeparatedUniversalDifferentialSourceCompletedCrossedHom C hC psi)

The source-identity completed differential module maps to the separated module for \(\psi\) by \(dg \mapsto\) \(d_{\mathrm{sep}}\) g, with source scalars restricted through \(\mathbb{Z}_C\llbracket G\rrbracket\) \(\to\) \(\mathbb{Z}_C\llbracket H\rrbracket\).

@[simp]
theorem zcDiffModuleIdToZCSepDiffModule_universal
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H) (g : G) :
    zcCompletedDifferentialModuleIdToZCSeparatedCompletedDifferentialModule C hC psi
        (zcUniversalDifferential C (MonoidHom.id G) g) =
      zcSeparatedUniversalDifferential C psi.toMonoidHom g

The comparison map from the identity differential module to the separated completed module sends the universal differential to the separated universal differential.

Show Lean proof
theorem zcCompletedDifferentialModuleIdentitySourceStageRingHom_transition_mapStage
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H)
    (i : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom) :
    let sourceIndex : ZCCompletedGroupAlgebraIndex C G :=
      (i.target.1, completedGroupAlgebraComapIndexInClass
        (G := G) (H := H) C hC psi i.target.2)
    let idIndex := zcCompletedDifferentialModuleIdentitySourceIndex C psi.toMonoidHom i
    let hle : sourceIndex ≤ idIndex.target := by
      constructor
      · exact le_rfl
      · exact i.compatible
    ∀ x : ZCCompletedGroupAlgebraStage C G idIndex.target,
      zcCompletedGroupAlgebraMapStage C hC psi i.target
          (zcCompletedGroupAlgebraTransition C G hle x) =
        zcCompletedDifferentialModuleIdentitySourceStageRingHom C psi.toMonoidHom i x

The finite source-identity coefficient map agrees with first projecting a completed source coefficient down to the source-identity stage and then applying the finite target map.

Show Lean proof
theorem zcCompletedDifferentialModuleIdentitySourceStageRingHom_projection_map
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H)
    (i : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom)
    (a : ZCCompletedGroupAlgebra C G) :
    zcCompletedDifferentialModuleIdentitySourceStageRingHom C psi.toMonoidHom i
      (zcCompletedGroupAlgebraProjection C G
        (zcCompletedDifferentialModuleIdentitySourceIndex C psi.toMonoidHom i).target a) =
    zcCompletedGroupAlgebraProjection C H i.target
      (zcCompletedGroupAlgebraMap C hC psi a)

Completed source coefficients viewed at the identity-source stage agree with target finite projections after applying the completed group-algebra map.

Show Lean proof
theorem zcDiffModuleIdToZCSepDiffModule_stageProj
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H)
    (i : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom)
    (x : ZCCompletedDifferentialModule C (MonoidHom.id G)) :
    zcSeparatedCompletedDifferentialModuleStageProjectionAdd C psi.toMonoidHom i
        (zcCompletedDifferentialModuleIdToZCSeparatedCompletedDifferentialModule C hC psi x) =
      zcCompletedDifferentialModuleIdentitySourceStageToStage C psi.toMonoidHom i
        (zcCompletedDifferentialModuleStageProjection C (MonoidHom.id G)
          (zcCompletedDifferentialModuleIdentitySourceIndex C psi.toMonoidHom i) x)

Finite-stage projections of the identity-source lift to the separated \(\psi\)-module are computed by first projecting to the matching source-identity finite stage.

Show Lean proof
theorem zcCompletedDifferentialModuleStageBoundary_identitySourceStageToStage
    (ψ : G →* H)
    (i : ZCCompletedDifferentialModuleIndex C ψ)
    (x : ZCCompletedDifferentialModuleStage C (MonoidHom.id G)
        (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i)) :
    zcCompletedDifferentialModuleStageBoundary C ψ i
        (zcCompletedDifferentialModuleIdentitySourceStageToStage C ψ i x) =
      zcCompletedDifferentialModuleIdentitySourceStageRingHom C ψ i
        (zcCompletedDifferentialModuleStageBoundary C (MonoidHom.id G)
          (zcCompletedDifferentialModuleIdentitySourceIndex C ψ i) x)

The finite comparison from the source-identity stage to the \(\psi\)-stage commutes with the finite Fox boundary.

Show Lean proof
omit [IsTopologicalGroup H] in
theorem zcCompletedDifferentialModuleIdentitySourceStageBoundary_stageProj
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (psi : ContinuousMonoidHom G H)
    (i : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom)
    (x : ZCCompletedDifferentialModule C (MonoidHom.id G)) :
    let j := zcCompletedDifferentialModuleIdentitySourceIndex C psi.toMonoidHom i
    zcCompletedDifferentialModuleStageBoundary C (MonoidHom.id G) j
        (zcCompletedDifferentialModuleStageProjection C (MonoidHom.id G) j x) =
      ((zcCompletedGroupAlgebraStandardAugmentationIdealProjection C j.target
        (zcToStdAugIdeal C G (MonoidHom.id G) x) :
          zcCompletedGroupAlgebraStageAugmentationIdeal C G j.target) :
        ZCCompletedGroupAlgebraStage C G j.target)

Applying the finite identity boundary after the source-identity finite projection recovers the finite projection of the standard augmentation-valued completed Fox tail.

Show Lean proof
theorem zcDiffModuleIdToZCSepDiffModule_eq_zero_of_zcToStandard_eq_zero
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H)
    (x : ZCCompletedDifferentialModule C (MonoidHom.id G))
    (hx :
      zcToStdAugIdeal C G (MonoidHom.id G) x = 0) :
    zcCompletedDifferentialModuleIdToZCSeparatedCompletedDifferentialModule C hC psi x = 0

The identity-source lift to the separated \(\psi\)-module kills the kernel of the standard augmentation-valued completed Fox tail.

Show Lean proof
omit [IsTopologicalGroup G] in
theorem continuous_zcToStdAugIdeal_naturalTopology
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H) :
    @Continuous
      (ZCCompletedDifferentialModule C psi.toMonoidHom)
      (zcCompletedGroupAlgebraStandardAugmentationIdeal C H)
      (zcCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom)
      inferInstance
      (zcToStdAugIdeal C H psi.toMonoidHom)

The standard-augmentation-valued completed Fox tail is continuous for the finite-stage natural topology on the completed differential module.

Show Lean proof
theorem zcSeparatedCompletedDifferentialModule_source_kernel_groupLike_smul
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H) (n : ProfiniteKernelSubgroup psi)
    (x : ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :
    letI : Module (ZCCompletedGroupAlgebra C G)
        (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
      Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
    zcGroupLike C G n.1 • x = x

Kernel group-like source scalars act trivially on the separated module after scalar restriction along \(\mathbb{Z}_C\llbracket G\rrbracket \to \mathbb{Z}_C\llbracket H\rrbracket\).

Show Lean proof
theorem zcSeparatedCompletedDifferentialModule_source_map_smul
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H)
    (a : ZCCompletedGroupAlgebra C G)
    (x : ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :
    letI : Module (ZCCompletedGroupAlgebra C G)
        (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
      Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
    zcCompletedGroupAlgebraMap C hC psi a • x = a • x

Source scalar restriction on the separated module is exactly target scalar multiplication after applying the completed group-algebra map.

Show Lean proof
theorem zcSeparatedCompletedDifferentialModule_source_kernel_sub_one_smul
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H) (n : ProfiniteKernelSubgroup psi)
    (x : ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :
    letI : Module (ZCCompletedGroupAlgebra C G)
        (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
      Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
    (zcGroupLike C G n.1 - 1) • x = 0

Elements of the source kernel augmentation ideal act trivially on the separated module after restricting scalars along the source map.

Show Lean proof
theorem zcDiffModuleIdToZCSepDiffModule_kernel_sub_one_smul
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H) (n : ProfiniteKernelSubgroup psi)
    (x : ZCCompletedDifferentialModule C (MonoidHom.id G)) :
    zcCompletedDifferentialModuleIdToZCSeparatedCompletedDifferentialModule C hC psi
        ((zcGroupLike C G n.1 - 1) • x) = 0

The identity-source lift to the separated module kills source kernel augmentation generators after scalar multiplication.

Show Lean proof
noncomputable def
    stdAugIdealToZCSepDiffOfBoundaryKernel
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H)
    (hker :
      ∀ x : ZCCompletedDifferentialModule C (MonoidHom.id G),
        zcToStdAugIdeal C G (MonoidHom.id G) x = 0 →
          zcCompletedDifferentialModuleIdToZCSeparatedCompletedDifferentialModule
            C hC psi x = 0) :
    letI : Module (ZCCompletedGroupAlgebra C G)
        (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
      Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
    zcCompletedGroupAlgebraStandardAugmentationIdeal C G →ₗ[ZCCompletedGroupAlgebra C G]
      ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom := by
  letI : Module (ZCCompletedGroupAlgebra C G)
      (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
    Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
  let f :=
    zcToStdAugIdeal C G (MonoidHom.id G)
  let L :=
    zcCompletedDifferentialModuleIdToZCSeparatedCompletedDifferentialModule C hC psi
  have hf : Function.Surjective f := by
    exact
      zcToStdAugIdeal_surjective_of_surjective
        C G (MonoidHom.id G) (fun g => ⟨g, rfl⟩)
  have hker_le : LinearMap.ker f ≤ LinearMap.ker L := by
    intro x hx
    rw [LinearMap.mem_ker] at hx ⊢
    exact hker x hx
  exact
    ((LinearMap.ker f).liftQ L hker_le).comp
      (f.quotKerEquivOfSurjective hf).symm.toLinearMap

A conditional source-standard-augmentation map to the separated module. The only remaining well-definedness input is that the identity Fox tail kernel is killed by the source-identity lift to the separated module.

noncomputable def
    stdAugIdealToZCSepDiff
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H) :
    letI : Module (ZCCompletedGroupAlgebra C G)
        (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
      Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
    zcCompletedGroupAlgebraStandardAugmentationIdeal C G →ₗ[ZCCompletedGroupAlgebra C G]
      ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom :=
  stdAugIdealToZCSepDiffOfBoundaryKernel
    C hC psi
    (zcDiffModuleIdToZCSepDiffModule_eq_zero_of_zcToStandard_eq_zero
      C hC psi)

The source-standard-augmentation map to the separated module.

@[simp 900]
theorem
    stdAugIdealToZCSepDiffOfBoundaryKernel_comp_zcToStdAugIdeal
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H)
    (hker :
      ∀ x : ZCCompletedDifferentialModule C (MonoidHom.id G),
        zcToStdAugIdeal C G (MonoidHom.id G) x = 0 →
          zcCompletedDifferentialModuleIdToZCSeparatedCompletedDifferentialModule
            C hC psi x = 0) :
    letI : Module (ZCCompletedGroupAlgebra C G)
        (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
      Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
    (stdAugIdealToZCSepDiffOfBoundaryKernel
        C hC psi hker).comp
      (zcToStdAugIdeal C G (MonoidHom.id G)) =
    zcCompletedDifferentialModuleIdToZCSeparatedCompletedDifferentialModule C hC psi

The conditional map out of the standard augmentation ideal recovers the canonical map from the completed differential module after composing with its quotient map.

Show Lean proof
@[simp]
theorem
    stdAugIdealToZCSepDiff_comp_zcToStdAugIdeal
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H) :
    letI : Module (ZCCompletedGroupAlgebra C G)
        (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
      Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
    (stdAugIdealToZCSepDiff
        C hC psi).comp
      (zcToStdAugIdeal C G (MonoidHom.id G)) =
    zcCompletedDifferentialModuleIdToZCSeparatedCompletedDifferentialModule C hC psi

The standard augmentation-ideal map recovers the canonical separated differential-module map after precomposition with the quotient map.

Show Lean proof
theorem
    stdAugIdealToZCSepDiff_stageBoundary_stageProj
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H)
    (i : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom)
    (s : zcCompletedGroupAlgebraStandardAugmentationIdeal C G) :
    zcCompletedDifferentialModuleStageBoundary C psi.toMonoidHom i
        (zcSeparatedCompletedDifferentialModuleStageProjectionAdd C psi.toMonoidHom i
          (stdAugIdealToZCSepDiff
            C hC psi s)) =
      zcCompletedGroupAlgebraProjection C H i.target
        (zcCompletedGroupAlgebraMap C hC psi
          (s : ZCCompletedGroupAlgebra C G))

Finite-stage boundary formula for the source-standard map into the separated module.

Show Lean proof
theorem
    stdAugIdealToZCSepDiff_stageProj_eq_of_standardProj_eq
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H)
    (i : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom)
    {s t : zcCompletedGroupAlgebraStandardAugmentationIdeal C G}
    (hst :
      zcCompletedGroupAlgebraStandardAugmentationIdealProjection C
          (zcCompletedDifferentialModuleIdentitySourceIndex C psi.toMonoidHom i).target s =
        zcCompletedGroupAlgebraStandardAugmentationIdealProjection C
          (zcCompletedDifferentialModuleIdentitySourceIndex C psi.toMonoidHom i).target t) :
    zcSeparatedCompletedDifferentialModuleStageProjectionAdd C psi.toMonoidHom i
        (stdAugIdealToZCSepDiff
          C hC psi s) =
      zcSeparatedCompletedDifferentialModuleStageProjectionAdd C psi.toMonoidHom i
        (stdAugIdealToZCSepDiff
          C hC psi t)

The finite-stage projection of the source-standard map depends only on the matching source-identity finite projection of the standard augmentation ideal.

Show Lean proof
theorem
    continuous_stdAugIdealToZCSepDiff_stageProj
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H)
    (i : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom) :
    Continuous
      (fun s : zcCompletedGroupAlgebraStandardAugmentationIdeal C G =>
        zcSeparatedCompletedDifferentialModuleStageProjectionAdd C psi.toMonoidHom i
          (stdAugIdealToZCSepDiff
            C hC psi s))

Each finite-stage coordinate of the source-standard map into the separated module is continuous. The coordinate factors through the matching finite standard augmentation projection.

Show Lean proof
theorem
    continuous_stdAugIdealToZCSepDiff_stageProjProduct
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H) :
    Continuous
      (fun s : zcCompletedGroupAlgebraStandardAugmentationIdeal C G =>
        zcSeparatedCompletedDifferentialModuleStageProjectionProduct C psi.toMonoidHom
          (stdAugIdealToZCSepDiff
            C hC psi s))

The product of all finite-stage coordinates of the source-standard map into the separated module is continuous.

Show Lean proof
theorem
    continuous_stdAugIdealToZCSepDiff
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) :
    letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
      zcSeparatedCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom
    @Continuous
      (zcCompletedGroupAlgebraStandardAugmentationIdeal C G)
      (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom)
      inferInstance
      (zcSeparatedCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom)
      (stdAugIdealToZCSepDiff
        C hC psi)

The source-standard map to the separated completed differential module is continuous for the finite-stage quotient topology.

Show Lean proof
@[simp 900]
theorem
    stdAugIdealToZCSepDiffOfBoundaryKernel_boundary
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H)
    (hker :
      ∀ x : ZCCompletedDifferentialModule C (MonoidHom.id G),
        zcToStdAugIdeal C G (MonoidHom.id G) x = 0 →
          zcCompletedDifferentialModuleIdToZCSeparatedCompletedDifferentialModule
            C hC psi x = 0)
    (g : G) :
    stdAugIdealToZCSepDiffOfBoundaryKernel
        C hC psi hker
        ⟨zcCompletedGroupAlgebraBoundary C (MonoidHom.id G) g,
          zcCompletedGroupAlgebraBoundary_mem_standardAugmentationIdeal
            C G (MonoidHom.id G) g⟩ =
      zcSeparatedUniversalDifferential C psi.toMonoidHom g

The conditional augmentation-ideal map sends a group boundary to the separated universal differential of that group element.

Show Lean proof
@[simp]
theorem
    stdAugIdealToZCSepDiff_boundary
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H)
    (g : G) :
    stdAugIdealToZCSepDiff
        C hC psi
        ⟨zcCompletedGroupAlgebraBoundary C (MonoidHom.id G) g,
          zcCompletedGroupAlgebraBoundary_mem_standardAugmentationIdeal
            C G (MonoidHom.id G) g⟩ =
      zcSeparatedUniversalDifferential C psi.toMonoidHom g

The augmentation-ideal map sends a group boundary to the separated universal differential.

Show Lean proof
theorem
    stdAugIdealToZCSepDiffOfBoundaryKernel_kernel_generator_smul
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H)
    (hker :
      ∀ x : ZCCompletedDifferentialModule C (MonoidHom.id G),
        zcToStdAugIdeal C G (MonoidHom.id G) x = 0 →
          zcCompletedDifferentialModuleIdToZCSeparatedCompletedDifferentialModule
            C hC psi x = 0)
    (n : ProfiniteKernelSubgroup psi)
    (s : zcCompletedGroupAlgebraStandardAugmentationIdeal C G) :
    stdAugIdealToZCSepDiffOfBoundaryKernel
        C hC psi hker ((zcGroupLike C G n.1 - 1) • s) = 0

The conditional source-standard map kills each algebraic kernel-product generator.

Show Lean proof
theorem
    stdAugIdealToZCSepDiffOfBoundaryKernel_kills_kernelMulStandard
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H)
    (hker :
      ∀ x : ZCCompletedDifferentialModule C (MonoidHom.id G),
        zcToStdAugIdeal C G (MonoidHom.id G) x = 0 →
          zcCompletedDifferentialModuleIdToZCSeparatedCompletedDifferentialModule
            C hC psi x = 0)
    {x : zcCompletedGroupAlgebraStandardAugmentationIdeal C G}
    (hx : x ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi) :
    stdAugIdealToZCSepDiffOfBoundaryKernel
        C hC psi hker x = 0

The conditional source-standard map kills the algebraic product I(ker psi) I(G).

Show Lean proof
theorem
    stdAugIdealToZCSepDiff_kills_kernelMulStandard
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H)
    {x : zcCompletedGroupAlgebraStandardAugmentationIdeal C G}
    (hx : x ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi) :
    stdAugIdealToZCSepDiff
        C hC psi x = 0

The source-standard map kills the algebraic product I(ker psi) I(G).

Show Lean proof
theorem
    stdAugIdealToZCSepDiffOfBoundaryKernel_kills_kernelMulStandardClosed_of_continuous
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (hker :
      ∀ x : ZCCompletedDifferentialModule C (MonoidHom.id G),
        zcToStdAugIdeal C G (MonoidHom.id G) x = 0 →
          zcCompletedDifferentialModuleIdToZCSeparatedCompletedDifferentialModule
            C hC psi x = 0)
    (hcont :
      letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
        zcSeparatedCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom
      @Continuous
        (zcCompletedGroupAlgebraStandardAugmentationIdeal C G)
        (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom)
        inferInstance
        (zcSeparatedCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom)
        (stdAugIdealToZCSepDiffOfBoundaryKernel
          C hC psi hker))
    {x : zcCompletedGroupAlgebraStandardAugmentationIdeal C G}
    (hx : x ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
        C hC hForm psi hpsi hfopen) :
    stdAugIdealToZCSepDiffOfBoundaryKernel
        C hC psi hker x = 0

If the conditional source-standard map is continuous for the separated quotient topology, then killing the algebraic denominator implies that it kills the finite-stage closed denominator.

Show Lean proof
theorem
    stdAugIdealToZCSepDiff_kills_kernelMulStandardClosed_of_continuous
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (hcont :
      letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
        zcSeparatedCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom
      @Continuous
        (zcCompletedGroupAlgebraStandardAugmentationIdeal C G)
        (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom)
        inferInstance
        (zcSeparatedCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom)
        (stdAugIdealToZCSepDiff
          C hC psi))
    {x : zcCompletedGroupAlgebraStandardAugmentationIdeal C G}
    (hx : x ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
        C hC hForm psi hpsi hfopen) :
    stdAugIdealToZCSepDiff
        C hC psi x = 0

If the source-standard map is continuous for the separated quotient topology, then it kills the closed finite-stage denominator.

Show Lean proof
theorem
    stdAugIdealToZCSepDiff_kills_kernelMulStandardClosed
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    {x : zcCompletedGroupAlgebraStandardAugmentationIdeal C G}
    (hx : x ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
        C hC hForm psi hpsi hfopen) :
    stdAugIdealToZCSepDiff
        C hC psi x = 0

The source-standard map kills the closed finite-stage denominator.

Show Lean proof
noncomputable def
    kerAugIdealQuotToZCSepDiffOfBoundaryKernelOfClosedKill
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (hker :
      ∀ x : ZCCompletedDifferentialModule C (MonoidHom.id G),
        zcToStdAugIdeal C G (MonoidHom.id G) x = 0 →
          zcCompletedDifferentialModuleIdToZCSeparatedCompletedDifferentialModule
            C hC psi x = 0)
    (hclosed_kill :
      ∀ x : zcCompletedGroupAlgebraStandardAugmentationIdeal C G,
        x ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
            C hC hForm psi hpsi hfopen →
          stdAugIdealToZCSepDiffOfBoundaryKernel
            C hC psi hker x = 0) :
    letI : Module (ZCCompletedGroupAlgebra C G)
        (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
      Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
    KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen
      →ₗ[ZCCompletedGroupAlgebra C G]
    ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom := by
  letI : Module (ZCCompletedGroupAlgebra C G)
      (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
    Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
  let M :=
    stdAugIdealToZCSepDiffOfBoundaryKernel
      C hC psi hker
  exact
    (zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
      C hC hForm psi hpsi hfopen).liftQ M
      (by
        intro x hx
        rw [LinearMap.mem_ker]
        exact hclosed_kill x hx)

A conditional reverse map from the closed source augmentation quotient to the separated module. The remaining closed-denominator input is isolated as hclosed_kill.

@[simp 900]
theorem
    kerAugIdealQuotToZCSepDiffOfBoundaryKernelOfClosedKill_boundary
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (hker :
      ∀ x : ZCCompletedDifferentialModule C (MonoidHom.id G),
        zcToStdAugIdeal C G (MonoidHom.id G) x = 0 →
          zcCompletedDifferentialModuleIdToZCSeparatedCompletedDifferentialModule
            C hC psi x = 0)
    (hclosed_kill :
      ∀ x : zcCompletedGroupAlgebraStandardAugmentationIdeal C G,
        x ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
            C hC hForm psi hpsi hfopen →
          stdAugIdealToZCSepDiffOfBoundaryKernel
            C hC psi hker x = 0)
    (g : G) :
    kerAugIdealQuotToZCSepDiffOfBoundaryKernelOfClosedKill
        C hC hForm psi hpsi hfopen hker hclosed_kill
        (Submodule.Quotient.mk
          (p := zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
            C hC hForm psi hpsi hfopen)
          ⟨zcCompletedGroupAlgebraBoundary C (MonoidHom.id G) g,
            zcCompletedGroupAlgebraBoundary_mem_standardAugmentationIdeal
              C G (MonoidHom.id G) g⟩) =
      zcSeparatedUniversalDifferential C psi.toMonoidHom g

The conditional map from the closed augmentation quotient sends the class of a boundary to the separated universal differential.

Show Lean proof
noncomputable def
    kerAugIdealQuotToZCSepDiffLinearOfBoundaryKernelOfClosedKill
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (hker :
      ∀ x : ZCCompletedDifferentialModule C (MonoidHom.id G),
        zcToStdAugIdeal C G (MonoidHom.id G) x = 0 →
          zcCompletedDifferentialModuleIdToZCSeparatedCompletedDifferentialModule
            C hC psi x = 0)
    (hclosed_kill :
      ∀ x : zcCompletedGroupAlgebraStandardAugmentationIdeal C G,
        x ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
            C hC hForm psi hpsi hfopen →
          stdAugIdealToZCSepDiffOfBoundaryKernel
            C hC psi hker x = 0) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen
      →ₗ[ZCCompletedGroupAlgebra C H]
    ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom := by
  letI : Module (ZCCompletedGroupAlgebra C H)
      (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
    kerAugClosedQuotTargetCompletedModuleOfSurj
      C hC hForm psi hpsi hfopen
  letI : Module (ZCCompletedGroupAlgebra C G)
      (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
    Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
  let Q :=
    kerAugIdealQuotToZCSepDiffOfBoundaryKernelOfClosedKill
      C hC hForm psi hpsi hfopen hker hclosed_kill
  refine
    { toFun := Q
      map_add' := by
        intro x y
        exact map_add Q x y
      map_smul' := by
        intro a x
        change Q
            (zcCompletedGroupAlgebraTargetLiftOfSurjective C hC hForm psi hpsi a • x) =
          a • Q x
        rw [map_smul]
        symm
        calc
          a • Q x =
              zcCompletedGroupAlgebraMap C hC psi
                  (zcCompletedGroupAlgebraTargetLiftOfSurjective C hC hForm psi hpsi a) •
                Q x := by
                rw [zcCompletedGroupAlgebraMap_targetLiftOfSurjective]
          _ =
              zcCompletedGroupAlgebraTargetLiftOfSurjective C hC hForm psi hpsi a •
                Q x := by
                exact
                  zcSeparatedCompletedDifferentialModule_source_map_smul
                    C hC psi
                    (zcCompletedGroupAlgebraTargetLiftOfSurjective C hC hForm psi hpsi a)
                    (Q x) }

Target-linear version of the conditional reverse map from the closed source augmentation quotient to the separated module.

@[simp 900]
theorem
    kerAugIdealQuotToZCSepDiffLinearOfBoundaryKernelOfClosedKill_boundary
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (hker :
      ∀ x : ZCCompletedDifferentialModule C (MonoidHom.id G),
        zcToStdAugIdeal C G (MonoidHom.id G) x = 0 →
          zcCompletedDifferentialModuleIdToZCSeparatedCompletedDifferentialModule
            C hC psi x = 0)
    (hclosed_kill :
      ∀ x : zcCompletedGroupAlgebraStandardAugmentationIdeal C G,
        x ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
            C hC hForm psi hpsi hfopen →
          stdAugIdealToZCSepDiffOfBoundaryKernel
            C hC psi hker x = 0)
    (g : G) :
    kerAugIdealQuotToZCSepDiffLinearOfBoundaryKernelOfClosedKill
        C hC hForm psi hpsi hfopen hker hclosed_kill
        (Submodule.Quotient.mk
          (p := zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
            C hC hForm psi hpsi hfopen)
          ⟨zcCompletedGroupAlgebraBoundary C (MonoidHom.id G) g,
            zcCompletedGroupAlgebraBoundary_mem_standardAugmentationIdeal
              C G (MonoidHom.id G) g⟩) =
      zcSeparatedUniversalDifferential C psi.toMonoidHom g

The target-linear conditional quotient map sends each boundary class to the separated universal differential.

Show Lean proof
noncomputable def
    kerAugIdealQuotToZCSepDiffLinearOfBoundaryKernelOfContStdMap
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (hker :
      ∀ x : ZCCompletedDifferentialModule C (MonoidHom.id G),
        zcToStdAugIdeal C G (MonoidHom.id G) x = 0 →
          zcCompletedDifferentialModuleIdToZCSeparatedCompletedDifferentialModule
            C hC psi x = 0)
    (hcont :
      letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
        zcSeparatedCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom
      @Continuous
        (zcCompletedGroupAlgebraStandardAugmentationIdeal C G)
        (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom)
        inferInstance
        (zcSeparatedCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom)
        (stdAugIdealToZCSepDiffOfBoundaryKernel
          C hC psi hker)) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen
      →ₗ[ZCCompletedGroupAlgebra C H]
    ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom :=
  kerAugIdealQuotToZCSepDiffLinearOfBoundaryKernelOfClosedKill
    C hC hForm psi hpsi hfopen hker
    (fun _ hx =>
      stdAugIdealToZCSepDiffOfBoundaryKernel_kills_kernelMulStandardClosed_of_continuous
        C hC hForm psi hpsi hfopen hker hcont hx)

Target-linear reverse map from the closed source augmentation quotient to the separated module, reducing the closed-denominator condition to continuity of the source-standard map.

@[simp 900]
theorem
    kerAugIdealQuotToZCSepDiffLinearOfBoundaryKernelOfContStdMap_boundary
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (hker :
      ∀ x : ZCCompletedDifferentialModule C (MonoidHom.id G),
        zcToStdAugIdeal C G (MonoidHom.id G) x = 0 →
          zcCompletedDifferentialModuleIdToZCSeparatedCompletedDifferentialModule
            C hC psi x = 0)
    (hcont :
      letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
        zcSeparatedCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom
      @Continuous
        (zcCompletedGroupAlgebraStandardAugmentationIdeal C G)
        (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom)
        inferInstance
        (zcSeparatedCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom)
        (stdAugIdealToZCSepDiffOfBoundaryKernel
          C hC psi hker))
    (g : G) :
    kerAugIdealQuotToZCSepDiffLinearOfBoundaryKernelOfContStdMap
        C hC hForm psi hpsi hfopen hker hcont
        (Submodule.Quotient.mk
          (p := zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
            C hC hForm psi hpsi hfopen)
          ⟨zcCompletedGroupAlgebraBoundary C (MonoidHom.id G) g,
            zcCompletedGroupAlgebraBoundary_mem_standardAugmentationIdeal
              C G (MonoidHom.id G) g⟩) =
      zcSeparatedUniversalDifferential C psi.toMonoidHom g

Under continuity of the conditional standard map, the target-linear quotient map sends a boundary class to the separated universal differential.

Show Lean proof
noncomputable def
    kerAugIdealQuotToZCSepDiffOfClosedKill
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (hclosed_kill :
      ∀ x : zcCompletedGroupAlgebraStandardAugmentationIdeal C G,
        x ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
            C hC hForm psi hpsi hfopen →
          stdAugIdealToZCSepDiff
            C hC psi x = 0) :
    letI : Module (ZCCompletedGroupAlgebra C G)
        (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
      Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
    KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen
      →ₗ[ZCCompletedGroupAlgebra C G]
    ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom :=
  kerAugIdealQuotToZCSepDiffOfBoundaryKernelOfClosedKill
    C hC hForm psi hpsi hfopen
    (zcDiffModuleIdToZCSepDiffModule_eq_zero_of_zcToStandard_eq_zero
      C hC psi)
    (fun x hx => by
      simpa [stdAugIdealToZCSepDiff]
        using hclosed_kill x hx)

Reverse map from the closed source augmentation quotient to the separated module, assuming only that the closed denominator is killed by the unconditional source-standard map.

@[simp 900]
theorem
    kerAugIdealQuotToZCSepDiffOfClosedKill_boundary
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (hclosed_kill :
      ∀ x : zcCompletedGroupAlgebraStandardAugmentationIdeal C G,
        x ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
            C hC hForm psi hpsi hfopen →
          stdAugIdealToZCSepDiff
            C hC psi x = 0)
    (g : G) :
    kerAugIdealQuotToZCSepDiffOfClosedKill
        C hC hForm psi hpsi hfopen hclosed_kill
        (Submodule.Quotient.mk
          (p := zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
            C hC hForm psi hpsi hfopen)
          ⟨zcCompletedGroupAlgebraBoundary C (MonoidHom.id G) g,
            zcCompletedGroupAlgebraBoundary_mem_standardAugmentationIdeal
              C G (MonoidHom.id G) g⟩) =
      zcSeparatedUniversalDifferential C psi.toMonoidHom g

If the closed denominator is killed, the resulting quotient map sends a boundary class to the separated universal differential.

Show Lean proof
theorem
    continuous_kerAugIdealQuotToZCSepDiffOfClosedKill
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (hclosed_kill :
      ∀ x : zcCompletedGroupAlgebraStandardAugmentationIdeal C G,
        x ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
            C hC hForm psi hpsi hfopen →
          stdAugIdealToZCSepDiff
            C hC psi x = 0)
    (hcont :
      letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
        zcSeparatedCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom
      @Continuous
        (zcCompletedGroupAlgebraStandardAugmentationIdeal C G)
        (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom)
        inferInstance
        (zcSeparatedCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom)
        (stdAugIdealToZCSepDiff
          C hC psi)) :
    letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
      zcSeparatedCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom
    Continuous
      (kerAugIdealQuotToZCSepDiffOfClosedKill
        C hC hForm psi hpsi hfopen hclosed_kill)

The reverse map from the closed source augmentation quotient to the separated module is continuous once the source-standard map is continuous.

Show Lean proof
noncomputable def
    kerAugIdealQuotToZCSepDiffLinearOfClosedKill
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (hclosed_kill :
      ∀ x : zcCompletedGroupAlgebraStandardAugmentationIdeal C G,
        x ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
            C hC hForm psi hpsi hfopen →
          stdAugIdealToZCSepDiff
            C hC psi x = 0) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen
      →ₗ[ZCCompletedGroupAlgebra C H]
    ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom :=
  kerAugIdealQuotToZCSepDiffLinearOfBoundaryKernelOfClosedKill
    C hC hForm psi hpsi hfopen
    (zcDiffModuleIdToZCSepDiffModule_eq_zero_of_zcToStandard_eq_zero
      C hC psi)
    (fun x hx => by
      simpa [stdAugIdealToZCSepDiff]
        using hclosed_kill x hx)

Target-linear reverse map from the closed source augmentation quotient to the separated module, assuming only that the closed denominator is killed by the unconditional source-standard map.

@[simp 900]
theorem
    kerAugIdealQuotToZCSepDiffLinearOfClosedKill_boundary
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (hclosed_kill :
      ∀ x : zcCompletedGroupAlgebraStandardAugmentationIdeal C G,
        x ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
            C hC hForm psi hpsi hfopen →
          stdAugIdealToZCSepDiff
            C hC psi x = 0)
    (g : G) :
    kerAugIdealQuotToZCSepDiffLinearOfClosedKill
        C hC hForm psi hpsi hfopen hclosed_kill
        (Submodule.Quotient.mk
          (p := zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
            C hC hForm psi hpsi hfopen)
          ⟨zcCompletedGroupAlgebraBoundary C (MonoidHom.id G) g,
            zcCompletedGroupAlgebraBoundary_mem_standardAugmentationIdeal
              C G (MonoidHom.id G) g⟩) =
      zcSeparatedUniversalDifferential C psi.toMonoidHom g

The target-linear map induced by annihilating the closed denominator has the expected value on boundary classes.

Show Lean proof
noncomputable def
    kerAugIdealQuotToZCSepDiffLinearOfContStdMap
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (hcont :
      letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
        zcSeparatedCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom
      @Continuous
        (zcCompletedGroupAlgebraStandardAugmentationIdeal C G)
        (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom)
        inferInstance
        (zcSeparatedCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom)
        (stdAugIdealToZCSepDiff
          C hC psi)) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen
      →ₗ[ZCCompletedGroupAlgebra C H]
    ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom :=
  kerAugIdealQuotToZCSepDiffLinearOfClosedKill
    C hC hForm psi hpsi hfopen
    (fun _ hx =>
      stdAugIdealToZCSepDiff_kills_kernelMulStandardClosed_of_continuous
        C hC hForm psi hpsi hfopen hcont hx)

Target-linear reverse map from the closed source augmentation quotient to the separated module, reducing the closed-denominator condition to continuity of the unconditional source-standard map.

@[simp 900]
theorem
    kerAugIdealQuotToZCSepDiffLinearOfContStdMap_boundary
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (hcont :
      letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
        zcSeparatedCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom
      @Continuous
        (zcCompletedGroupAlgebraStandardAugmentationIdeal C G)
        (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom)
        inferInstance
        (zcSeparatedCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom)
        (stdAugIdealToZCSepDiff
          C hC psi))
    (g : G) :
    kerAugIdealQuotToZCSepDiffLinearOfContStdMap
        C hC hForm psi hpsi hfopen hcont
        (Submodule.Quotient.mk
          (p := zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
            C hC hForm psi hpsi hfopen)
          ⟨zcCompletedGroupAlgebraBoundary C (MonoidHom.id G) g,
            zcCompletedGroupAlgebraBoundary_mem_standardAugmentationIdeal
              C G (MonoidHom.id G) g⟩) =
      zcSeparatedUniversalDifferential C psi.toMonoidHom g

Continuity of the standard map gives a target-linear quotient map with the expected value on boundary classes.

Show Lean proof
theorem
    continuous_kerAugIdealQuotToZCSepDiffLinearOfContStdMap
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (hcont :
      letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
        zcSeparatedCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom
      @Continuous
        (zcCompletedGroupAlgebraStandardAugmentationIdeal C G)
        (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom)
        inferInstance
        (zcSeparatedCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom)
        (stdAugIdealToZCSepDiff
          C hC psi)) :
    letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
      zcSeparatedCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom
    Continuous
      (kerAugIdealQuotToZCSepDiffLinearOfContStdMap
        C hC hForm psi hpsi hfopen hcont)

The target-linear reverse map obtained from a continuous source-standard map is continuous.

Show Lean proof
noncomputable def
    kerAugIdealQuotToZCSepDiffLinear
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen
      →ₗ[ZCCompletedGroupAlgebra C H]
    ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom :=
  kerAugIdealQuotToZCSepDiffLinearOfContStdMap
    C hC hForm psi hpsi hfopen
    (continuous_stdAugIdealToZCSepDiff
      C hC hForm psi)

Target-linear reverse map from the closed source augmentation quotient to the separated module.

@[simp 900]
theorem
    kerAugIdealQuotToZCSepDiffLinear_boundary
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (g : G) :
    kerAugIdealQuotToZCSepDiffLinear
        C hC hForm psi hpsi hfopen
        (Submodule.Quotient.mk
          (p := zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
            C hC hForm psi hpsi hfopen)
          ⟨zcCompletedGroupAlgebraBoundary C (MonoidHom.id G) g,
            zcCompletedGroupAlgebraBoundary_mem_standardAugmentationIdeal
              C G (MonoidHom.id G) g⟩) =
      zcSeparatedUniversalDifferential C psi.toMonoidHom g

The canonical target-linear reverse map sends each boundary class to the separated universal differential.

Show Lean proof
theorem
    continuous_kerAugIdealQuotToZCSepDiffLinear
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
      zcSeparatedCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom
    Continuous
      (kerAugIdealQuotToZCSepDiffLinear
        C hC hForm psi hpsi hfopen)

The target-linear reverse map from the closed source augmentation quotient to the separated module is continuous.

Show Lean proof
def zcCompletedDifferentialModuleToKernelAugmentationClosedQuotientOfSurjective
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    ZCCompletedDifferentialModule C psi.toMonoidHom →ₗ[ZCCompletedGroupAlgebra C H]
      KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen := by
  letI : Module (ZCCompletedGroupAlgebra C H)
      (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
    kerAugClosedQuotTargetCompletedModuleOfSurj
      C hC hForm psi hpsi hfopen
  exact
    crossedHomModuleLift
      (A := KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
      (zcCompletedGroupAlgebraScalar C psi.toMonoidHom)
      (zcCompletedGASourceBoundaryToKerAugClosedQuotTargetCompletedCrossedHomOfSurjective
        C hC hForm psi hpsi hfopen)

The completed universal differential module maps to the closed source augmentation quotient by \(dg \mapsto\) \([g]-1\).

@[simp 900]
theorem zcDiffToKerAugClosedQuotOfSurj_universal
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) (g : G) :
    zcCompletedDifferentialModuleToKernelAugmentationClosedQuotientOfSurjective
        C hC hForm psi hpsi hfopen
        (zcUniversalDifferential C psi.toMonoidHom g) =
      zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
        C hC hForm psi hpsi hfopen g

The closed augmentation-quotient map sends the universal differential to the class of the corresponding augmentation generator.

Show Lean proof
theorem zcDiffToKerAugClosedQuotOfSurj_kills_finiteClosedSubmodule_of_continuous_lift
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    [Nonempty (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom)]
    (hdir : Directed (· ≤ ·)
      (id : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom →
        ZCCompletedDifferentialModuleIndex C psi.toMonoidHom))
    (hcont :
      letI : Module (ZCCompletedGroupAlgebra C H)
          (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
        kerAugClosedQuotTargetCompletedModuleOfSurj
          C hC hForm psi hpsi hfopen
      @Continuous
        (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
        (zcCompletedDifferentialPreModuleNaturalTopology C psi.toMonoidHom)
        inferInstance
        (crossedDifferentialModuleLiftLinear
          (R := ZCCompletedGroupAlgebra C H)
          (zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
            C hC hForm psi hpsi hfopen)))
    {x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G}
    (hx : x ∈ zcCompletedDifferentialRelationFiniteClosedSubmodule C psi.toMonoidHom) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    crossedDifferentialModuleLiftLinear
      (R := ZCCompletedGroupAlgebra C H)
      (zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
        C hC hForm psi hpsi hfopen) x = 0

If the pre-quotient source-boundary lift to the closed augmentation quotient is continuous for the finite-stage pre-module topology, then it kills the finite-stage closed relation denominator. This is the descent criterion needed to factor the algebraic map through the separated completed differential module.

Show Lean proof
theorem zcDiffToKerAugClosedQuotOfSurj_kills_finiteClosedSubmodule_of_continuous_lift_of_surj
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (hcont :
      letI : Module (ZCCompletedGroupAlgebra C H)
          (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
        kerAugClosedQuotTargetCompletedModuleOfSurj
          C hC hForm psi hpsi hfopen
      @Continuous
        (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
        (zcCompletedDifferentialPreModuleNaturalTopology C psi.toMonoidHom)
        inferInstance
        (crossedDifferentialModuleLiftLinear
          (R := ZCCompletedGroupAlgebra C H)
          (zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
            C hC hForm psi hpsi hfopen)))
    {x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G}
    (hx : x ∈ zcCompletedDifferentialRelationFiniteClosedSubmodule C psi.toMonoidHom) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    crossedDifferentialModuleLiftLinear
      (R := ZCCompletedGroupAlgebra C H)
      (zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
        C hC hForm psi hpsi hfopen) x = 0

Version of zcDiffToKerAugClosedQuotOfSurj_kills_finiteClosedSubmodule_of_continuous_lift with nonemptiness and directedness of finite stages supplied by the continuous source map.

Show Lean proof
def zcSepDiffToKerAugClosedQuotOfSurjective
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    [Nonempty (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom)]
    (hdir : Directed (· ≤ ·)
      (id : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom →
        ZCCompletedDifferentialModuleIndex C psi.toMonoidHom))
    (hcont :
      letI : Module (ZCCompletedGroupAlgebra C H)
          (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
        kerAugClosedQuotTargetCompletedModuleOfSurj
          C hC hForm psi hpsi hfopen
      @Continuous
        (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
        (zcCompletedDifferentialPreModuleNaturalTopology C psi.toMonoidHom)
        inferInstance
        (crossedDifferentialModuleLiftLinear
          (R := ZCCompletedGroupAlgebra C H)
          (zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
            C hC hForm psi hpsi hfopen))) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom →ₗ[ZCCompletedGroupAlgebra C H]
      KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen := by
  letI : Module (ZCCompletedGroupAlgebra C H)
      (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
    kerAugClosedQuotTargetCompletedModuleOfSurj
      C hC hForm psi hpsi hfopen
  letI : T1Space
      (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
    t1Space_kernelAugmentationIdealClosedQuotient
      C hC hForm psi hpsi hfopen
  exact
    zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift
      C psi.toMonoidHom hdir
      (zcCompletedGASourceBoundaryToKerAugClosedQuotTargetCompletedCrossedHomOfSurjective
        C hC hForm psi hpsi hfopen)
      hcont

Under the explicit continuity hypothesis for the pre-quotient source-boundary lift, the closed source augmentation quotient receives the separated completed universal differential module.

def zcSepDiffToKerAugClosedQuotOfSurjectiveOfContinuousLift
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (hcont :
      letI : Module (ZCCompletedGroupAlgebra C H)
          (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
        kerAugClosedQuotTargetCompletedModuleOfSurj
          C hC hForm psi hpsi hfopen
      @Continuous
        (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
        (zcCompletedDifferentialPreModuleNaturalTopology C psi.toMonoidHom)
        inferInstance
        (crossedDifferentialModuleLiftLinear
          (R := ZCCompletedGroupAlgebra C H)
          (zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
            C hC hForm psi hpsi hfopen))) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom →ₗ[ZCCompletedGroupAlgebra C H]
      KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen := by
  letI : Nonempty (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom) :=
    nonempty_zcCompletedDifferentialModuleIndex C hC psi
  exact
    zcSepDiffToKerAugClosedQuotOfSurjective
      C hC hForm psi hpsi hfopen
      (directed_zcCompletedDifferentialModuleIndex C hForm hC psi)
      hcont

Public version of the closed-augmentation descent map with finite-stage nonemptiness and directedness supplied by the continuous source map.

@[simp 900]
theorem zcSepDiffToKerAugClosedQuotOfSurjective_universal
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    [Nonempty (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom)]
    (hdir : Directed (· ≤ ·)
      (id : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom →
        ZCCompletedDifferentialModuleIndex C psi.toMonoidHom))
    (hcont :
      letI : Module (ZCCompletedGroupAlgebra C H)
          (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
        kerAugClosedQuotTargetCompletedModuleOfSurj
          C hC hForm psi hpsi hfopen
      @Continuous
        (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
        (zcCompletedDifferentialPreModuleNaturalTopology C psi.toMonoidHom)
        inferInstance
        (crossedDifferentialModuleLiftLinear
          (R := ZCCompletedGroupAlgebra C H)
          (zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
            C hC hForm psi hpsi hfopen)))
    (g : G) :
    zcSepDiffToKerAugClosedQuotOfSurjective
        C hC hForm psi hpsi hfopen hdir hcont
        (zcSeparatedUniversalDifferential C psi.toMonoidHom g) =
      zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
        C hC hForm psi hpsi hfopen g

The separated differential module maps universally to the closed kernel-augmentation quotient in the surjective case.

Show Lean proof
@[simp 900]
theorem zcSepDiffToKerAugClosedQuotOfSurjectiveOfContinuousLift_universal
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (hcont :
      letI : Module (ZCCompletedGroupAlgebra C H)
          (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
        kerAugClosedQuotTargetCompletedModuleOfSurj
          C hC hForm psi hpsi hfopen
      @Continuous
        (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
        (zcCompletedDifferentialPreModuleNaturalTopology C psi.toMonoidHom)
        inferInstance
        (crossedDifferentialModuleLiftLinear
          (R := ZCCompletedGroupAlgebra C H)
          (zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
            C hC hForm psi hpsi hfopen)))
    (g : G) :
    zcSepDiffToKerAugClosedQuotOfSurjectiveOfContinuousLift
        C hC hForm psi hpsi hfopen hcont
        (zcSeparatedUniversalDifferential C psi.toMonoidHom g) =
      zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
        C hC hForm psi hpsi hfopen g

The lifted map from the separated completed differential module to the closed augmentation-kernel quotient sends each separated universal differential to the corresponding boundary quotient.

Show Lean proof
theorem zcSepDiffToKerAugClosedQuotOfSurjective_comp_toSep
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    [Nonempty (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom)]
    (hdir : Directed (· ≤ ·)
      (id : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom →
        ZCCompletedDifferentialModuleIndex C psi.toMonoidHom))
    (hcont :
      letI : Module (ZCCompletedGroupAlgebra C H)
          (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
        kerAugClosedQuotTargetCompletedModuleOfSurj
          C hC hForm psi hpsi hfopen
      @Continuous
        (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
        (zcCompletedDifferentialPreModuleNaturalTopology C psi.toMonoidHom)
        inferInstance
        (crossedDifferentialModuleLiftLinear
          (R := ZCCompletedGroupAlgebra C H)
          (zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
            C hC hForm psi hpsi hfopen))) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    (zcSepDiffToKerAugClosedQuotOfSurjective
        C hC hForm psi hpsi hfopen hdir hcont).comp
      (zcCompletedDifferentialModuleToSeparated C psi.toMonoidHom) =
    zcCompletedDifferentialModuleToKernelAugmentationClosedQuotientOfSurjective
      C hC hForm psi hpsi hfopen

The separated closed-augmentation map is the factorization of the algebraic closed-augmentation map through \(A_{\psi}(C) \to A_{\psi}(C)_{\mathrm{sep}}\).

Show Lean proof
theorem zcSepDiffToKerAugClosedQuotOfSurjectiveOfContinuousLift_comp_toSep
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (hcont :
      letI : Module (ZCCompletedGroupAlgebra C H)
          (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
        kerAugClosedQuotTargetCompletedModuleOfSurj
          C hC hForm psi hpsi hfopen
      @Continuous
        (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
        (zcCompletedDifferentialPreModuleNaturalTopology C psi.toMonoidHom)
        inferInstance
        (crossedDifferentialModuleLiftLinear
          (R := ZCCompletedGroupAlgebra C H)
          (zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
            C hC hForm psi hpsi hfopen))) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    (zcSepDiffToKerAugClosedQuotOfSurjectiveOfContinuousLift
        C hC hForm psi hpsi hfopen hcont).comp
      (zcCompletedDifferentialModuleToSeparated C psi.toMonoidHom) =
    zcCompletedDifferentialModuleToKernelAugmentationClosedQuotientOfSurjective
      C hC hForm psi hpsi hfopen

The continuous-lift map to the closed kernel-augmentation quotient composes with separation as expected.

Show Lean proof
theorem continuous_zcSepDiffToKerAugClosedQuotOfSurjective
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    [Nonempty (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom)]
    (hdir : Directed (· ≤ ·)
      (id : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom →
        ZCCompletedDifferentialModuleIndex C psi.toMonoidHom))
    (hcont :
      letI : Module (ZCCompletedGroupAlgebra C H)
          (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
        kerAugClosedQuotTargetCompletedModuleOfSurj
          C hC hForm psi hpsi hfopen
      @Continuous
        (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
        (zcCompletedDifferentialPreModuleNaturalTopology C psi.toMonoidHom)
        inferInstance
        (crossedDifferentialModuleLiftLinear
          (R := ZCCompletedGroupAlgebra C H)
          (zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
            C hC hForm psi hpsi hfopen))) :
    letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
      zcSeparatedCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    @Continuous
      (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom)
      (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
      (zcSeparatedCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom)
      inferInstance
      (zcSepDiffToKerAugClosedQuotOfSurjective
        C hC hForm psi hpsi hfopen hdir hcont)

The descended forward map to the closed augmentation quotient is continuous once the pre-quotient source-boundary lift is continuous.

Show Lean proof
theorem continuous_zcSepDiffToKerAugClosedQuotOfSurjectiveOfContinuousLift
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (hcont :
      letI : Module (ZCCompletedGroupAlgebra C H)
          (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
        kerAugClosedQuotTargetCompletedModuleOfSurj
          C hC hForm psi hpsi hfopen
      @Continuous
        (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
        (zcCompletedDifferentialPreModuleNaturalTopology C psi.toMonoidHom)
        inferInstance
        (crossedDifferentialModuleLiftLinear
          (R := ZCCompletedGroupAlgebra C H)
          (zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
            C hC hForm psi hpsi hfopen))) :
    letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
      zcSeparatedCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    @Continuous
      (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom)
      (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
      (zcSeparatedCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom)
      inferInstance
      (zcSepDiffToKerAugClosedQuotOfSurjectiveOfContinuousLift
        C hC hForm psi hpsi hfopen hcont)

Continuity of the forward map when the finite-stage index data are supplied by the continuous source map.

Show Lean proof
theorem zcDiffToKerAugClosedQuotOfSurj_surj
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    Function.Surjective
      (zcCompletedDifferentialModuleToKernelAugmentationClosedQuotientOfSurjective
        C hC hForm psi hpsi hfopen)

The map from the completed differential module to the closed augmentation quotient is surjective when finite-stage representatives can be lifted.

Show Lean proof
theorem zcSepDiffToKerAugClosedQuotOfSurjective_surj
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    [Nonempty (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom)]
    (hdir : Directed (· ≤ ·)
      (id : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom →
        ZCCompletedDifferentialModuleIndex C psi.toMonoidHom))
    (hcont :
      letI : Module (ZCCompletedGroupAlgebra C H)
          (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
        kerAugClosedQuotTargetCompletedModuleOfSurj
          C hC hForm psi hpsi hfopen
      @Continuous
        (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
        (zcCompletedDifferentialPreModuleNaturalTopology C psi.toMonoidHom)
        inferInstance
        (crossedDifferentialModuleLiftLinear
          (R := ZCCompletedGroupAlgebra C H)
          (zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
            C hC hForm psi hpsi hfopen))) :
    Function.Surjective
      (zcSepDiffToKerAugClosedQuotOfSurjective
        C hC hForm psi hpsi hfopen hdir hcont)

The separated closed-augmentation map is surjective under the same pre-quotient continuity hypothesis needed for the descent.

Show Lean proof
theorem zcSepDiffToKerAugClosedQuotOfSurjectiveOfContinuousLift_surj
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (hcont :
      letI : Module (ZCCompletedGroupAlgebra C H)
          (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
        kerAugClosedQuotTargetCompletedModuleOfSurj
          C hC hForm psi hpsi hfopen
      @Continuous
        (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
        (zcCompletedDifferentialPreModuleNaturalTopology C psi.toMonoidHom)
        inferInstance
        (crossedDifferentialModuleLiftLinear
          (R := ZCCompletedGroupAlgebra C H)
          (zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
            C hC hForm psi hpsi hfopen))) :
    Function.Surjective
      (zcSepDiffToKerAugClosedQuotOfSurjectiveOfContinuousLift
        C hC hForm psi hpsi hfopen hcont)

The continuous-lift map to the closed kernel-augmentation quotient is surjective.

Show Lean proof
def zcSeparatedCompletedDifferentialModuleToKernelAugmentationClosedQuotient
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom →ₗ[ZCCompletedGroupAlgebra C H]
      KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen := by
  let hcont :=
    continuous_crossedDiffModuleLiftLinear_sourceBoundaryToKerAugClosedQuot
      C hC hForm psi hpsi hfopen
  exact
    zcSepDiffToKerAugClosedQuotOfSurjectiveOfContinuousLift
      C hC hForm psi hpsi hfopen hcont

The separated completed universal differential module maps to the closed source augmentation quotient by \(dg \mapsto\) \([g]-1\). The pre-quotient lift continuity is supplied by the finite-stage factorization theorem.

@[simp]
theorem zcSepDiffToKerAugClosedQuot_universal
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) (g : G) :
    zcSeparatedCompletedDifferentialModuleToKernelAugmentationClosedQuotient
        C hC hForm psi hpsi hfopen
        (zcSeparatedUniversalDifferential C psi.toMonoidHom g) =
      zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationClosedQuotient
        C hC hForm psi hpsi hfopen g

The separated closed augmentation-quotient map sends the separated universal differential to the closed augmentation quotient class.

Show Lean proof
theorem zcSepDiffToKerAugClosedQuot_comp_toSep
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    (zcSeparatedCompletedDifferentialModuleToKernelAugmentationClosedQuotient
        C hC hForm psi hpsi hfopen).comp
      (zcCompletedDifferentialModuleToSeparated C psi.toMonoidHom) =
    zcCompletedDifferentialModuleToKernelAugmentationClosedQuotientOfSurjective
      C hC hForm psi hpsi hfopen

The unconditional separated closed-augmentation map factors the algebraic map through \(A_{\psi}(C) \to A_{\psi}(C)_{\mathrm{sep}}\).

Show Lean proof
theorem continuous_zcSepDiffToKerAugClosedQuot
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
      zcSeparatedCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    @Continuous
      (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom)
      (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)
      (zcSeparatedCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom)
      inferInstance
      (zcSeparatedCompletedDifferentialModuleToKernelAugmentationClosedQuotient
        C hC hForm psi hpsi hfopen)

The separated closed-augmentation map is continuous, with the pre-quotient lift continuity provided by the finite-stage factorization theorem.

Show Lean proof
theorem zcSepDiffToKerAugClosedQuot_surj
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    Function.Surjective
      (zcSeparatedCompletedDifferentialModuleToKernelAugmentationClosedQuotient
        C hC hForm psi hpsi hfopen)

The separated map to the closed kernel-augmentation quotient is surjective.

Show Lean proof
@[simp]
theorem kerAugIdealQuotToZCSepDiffLinear_mk
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (x : zcCompletedGroupAlgebraStandardAugmentationIdeal C G) :
    kerAugIdealQuotToZCSepDiffLinear
        C hC hForm psi hpsi hfopen
        (Submodule.Quotient.mk
          (p := zcCompletedGroupAlgebraKernelAugmentationIdealMulStandardClosed
            C hC hForm psi hpsi hfopen) x) =
      stdAugIdealToZCSepDiff
        C hC psi x

The reverse map from the closed augmentation quotient to the separated differential module is evaluated on quotient classes by the constructed linear representative.

Show Lean proof
theorem kerAugIdealQuotToZCSepDiffLinear_comp_zcSepDiffToKerAugClosedQuot
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    (kerAugIdealQuotToZCSepDiffLinear
        C hC hForm psi hpsi hfopen).comp
      (zcSeparatedCompletedDifferentialModuleToKernelAugmentationClosedQuotient
        C hC hForm psi hpsi hfopen) =
    LinearMap.id

Composing the reverse closed-augmentation map with the forward separated map gives the identity.

Show Lean proof
theorem zcSepDiffToKerAugClosedQuot_comp_kerAugIdealQuotToZCSepDiffLinear
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    (zcSeparatedCompletedDifferentialModuleToKernelAugmentationClosedQuotient
        C hC hForm psi hpsi hfopen).comp
      (kerAugIdealQuotToZCSepDiffLinear
        C hC hForm psi hpsi hfopen) =
    LinearMap.id

Composing the forward separated map with the reverse closed-augmentation map gives the identity.

Show Lean proof
def zcSepDiffEquivKerAugClosedQuot_of_surj
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom
      ≃ₗ[ZCCompletedGroupAlgebra C H]
    KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen := by
  letI : Module (ZCCompletedGroupAlgebra C H)
      (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
    kerAugClosedQuotTargetCompletedModuleOfSurj
      C hC hForm psi hpsi hfopen
  exact
    LinearEquiv.ofLinear
      (zcSeparatedCompletedDifferentialModuleToKernelAugmentationClosedQuotient
        C hC hForm psi hpsi hfopen)
      (kerAugIdealQuotToZCSepDiffLinear
        C hC hForm psi hpsi hfopen)
      (zcSepDiffToKerAugClosedQuot_comp_kerAugIdealQuotToZCSepDiffLinear
        C hC hForm psi hpsi hfopen)
      (kerAugIdealQuotToZCSepDiffLinear_comp_zcSepDiffToKerAugClosedQuot
        C hC hForm psi hpsi hfopen)

The separated completed differential module is the closed source augmentation quotient for a surjective open continuous homomorphism.

@[simp]
theorem zcSepDiffEquivKerAugClosedQuot_of_surj_apply
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (x : ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :
    zcSepDiffEquivKerAugClosedQuot_of_surj
        C hC hForm psi hpsi hfopen x =
      zcSeparatedCompletedDifferentialModuleToKernelAugmentationClosedQuotient
        C hC hForm psi hpsi hfopen x

The Fox-coordinate equivalence is evaluated by the finite-stage coordinate formula in the completed differential complex.

Show Lean proof
@[simp]
theorem zcSepDiffEquivKerAugClosedQuot_of_surj_symm_apply
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (x : KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :
    (zcSepDiffEquivKerAugClosedQuot_of_surj
        C hC hForm psi hpsi hfopen).symm x =
      kerAugIdealQuotToZCSepDiffLinear
        C hC hForm psi hpsi hfopen x

The inverse Fox-coordinate equivalence is evaluated by reconstructing the class from its completed coordinate data.

Show Lean proof
def zcApsiEquivKerAugClosedQuot_of_surj
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    ZCApsi C psi.toMonoidHom ≃ₗ[ZCCompletedGroupAlgebra C H]
      KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen :=
  zcSepDiffEquivKerAugClosedQuot_of_surj
    C hC hForm psi hpsi hfopen

The closed source augmentation quotient equivalence identifies \(A_{\psi}(C)\) over \(\mathbb{Z}_C\) with the separated completed differential module, rather than with the raw algebraic quotient.

@[simp]
theorem zcApsiEquivKerAugClosedQuot_of_surj_apply
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (x : ZCApsi C psi.toMonoidHom) :
    zcApsiEquivKerAugClosedQuot_of_surj
        C hC hForm psi hpsi hfopen x =
      zcSeparatedCompletedDifferentialModuleToKernelAugmentationClosedQuotient
        C hC hForm psi hpsi hfopen x

The Fox-coordinate equivalence is evaluated by the finite-stage coordinate formula in the completed differential complex.

Show Lean proof
@[simp]
theorem zcApsiEquivKerAugClosedQuot_of_surj_symm_apply
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (x : KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :
    (zcApsiEquivKerAugClosedQuot_of_surj
        C hC hForm psi hpsi hfopen).symm x =
      kerAugIdealQuotToZCSepDiffLinear
        C hC hForm psi hpsi hfopen x

The inverse Fox-coordinate equivalence is evaluated by reconstructing the class from its completed coordinate data.

Show Lean proof
theorem zcCompletedGAKerAugQuotTargetCompletedModuleOfSurjective_map_smul
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hker_mul :
      ∀ k : ZCCompletedGroupAlgebra C G,
        k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) →
        ∀ y : zcCompletedGroupAlgebraStandardAugmentationIdeal C G,
          (⟨k * (y : ZCCompletedGroupAlgebra C G),
            (zcCompletedGroupAlgebraStandardAugmentationIdeal C G).mul_mem_left k y.2⟩ :
              zcCompletedGroupAlgebraStandardAugmentationIdeal C G) ∈
            zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi)
    (a : ZCCompletedGroupAlgebra C G) (x : KernelAugmentationIdealQuotient C psi) :
    letI : Module (ZCCompletedGroupAlgebra C H) (KernelAugmentationIdealQuotient C psi) :=
      zcCompletedGAKerAugQuotTargetCompletedModuleOfSurjective_of_kernelMulStandard_le
        C hC hForm psi hpsi hker_mul
    zcCompletedGroupAlgebraMap C hC psi a • x = a • x

For a surjective target map, the completed target scalar action on the kernel-augmentation quotient is compatible with applying the induced algebra map.

Show Lean proof
theorem zcCompletedGAKerAugQuotTargetCompletedModuleOfSurjective_groupLike_smul
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hker_mul :
      ∀ k : ZCCompletedGroupAlgebra C G,
        k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) →
        ∀ y : zcCompletedGroupAlgebraStandardAugmentationIdeal C G,
          (⟨k * (y : ZCCompletedGroupAlgebra C G),
            (zcCompletedGroupAlgebraStandardAugmentationIdeal C G).mul_mem_left k y.2⟩ :
              zcCompletedGroupAlgebraStandardAugmentationIdeal C G) ∈
            zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi)
    (g : G) (x : KernelAugmentationIdealQuotient C psi) :
    letI : Module (ZCCompletedGroupAlgebra C H) (KernelAugmentationIdealQuotient C psi) :=
      zcCompletedGAKerAugQuotTargetCompletedModuleOfSurjective_of_kernelMulStandard_le
        C hC hForm psi hpsi hker_mul
    zcGroupLike C H (psi g) • x = zcGroupLike C G g • x

In the descended target module structure, the group-like element of \(\psi(g)\) acts in the same way as the source group-like element of \(g\).

Show Lean proof
def sourceBoundaryToKerAugTargetCrossedHomOfSurjectiveOfKernelMulStandardLe
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hker_mul :
      ∀ k : ZCCompletedGroupAlgebra C G,
        k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) →
        ∀ y : zcCompletedGroupAlgebraStandardAugmentationIdeal C G,
          (⟨k * (y : ZCCompletedGroupAlgebra C G),
            (zcCompletedGroupAlgebraStandardAugmentationIdeal C G).mul_mem_left k y.2⟩ :
              zcCompletedGroupAlgebraStandardAugmentationIdeal C G) ∈
            zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi) :
    letI : Module (ZCCompletedGroupAlgebra C H) (KernelAugmentationIdealQuotient C psi) :=
      zcCompletedGAKerAugQuotTargetCompletedModuleOfSurjective_of_kernelMulStandard_le
        C hC hForm psi hpsi hker_mul
    ScalarCrossedHom
      (zcCompletedGroupAlgebraScalar C psi.toMonoidHom)
      (KernelAugmentationIdealQuotient C psi) := by
  letI : Module (ZCCompletedGroupAlgebra C H) (KernelAugmentationIdealQuotient C psi) :=
    zcCompletedGAKerAugQuotTargetCompletedModuleOfSurjective_of_kernelMulStandard_le
      C hC hForm psi hpsi hker_mul
  exact
    { toFun := zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationQuotient C psi
      map_mul' := by
        intro g h
        rw [(zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationQuotient
          C psi).map_mul]
        congr 1
        change zcGroupLike C G g •
            zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationQuotient C psi h =
          zcGroupLike C H (psi g) •
            zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationQuotient C psi h
        exact
          (zcCompletedGAKerAugQuotTargetCompletedModuleOfSurjective_groupLike_smul
            C hC hForm psi hpsi hker_mul g
            (zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationQuotient
              C psi h)).symm }

Under the explicit kernel-product hypothesis, the source boundary is a crossed differential for the descended completed target scalars.

def zcDiffToKerAugQuotOfSurj_of_kernelMulStandard_le
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hker_mul :
      ∀ k : ZCCompletedGroupAlgebra C G,
        k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) →
        ∀ y : zcCompletedGroupAlgebraStandardAugmentationIdeal C G,
          (⟨k * (y : ZCCompletedGroupAlgebra C G),
            (zcCompletedGroupAlgebraStandardAugmentationIdeal C G).mul_mem_left k y.2⟩ :
              zcCompletedGroupAlgebraStandardAugmentationIdeal C G) ∈
            zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi) :
    letI : Module (ZCCompletedGroupAlgebra C H) (KernelAugmentationIdealQuotient C psi) :=
      zcCompletedGAKerAugQuotTargetCompletedModuleOfSurjective_of_kernelMulStandard_le
        C hC hForm psi hpsi hker_mul
    ZCCompletedDifferentialModule C psi.toMonoidHom →ₗ[ZCCompletedGroupAlgebra C H]
      KernelAugmentationIdealQuotient C psi := by
  letI : Module (ZCCompletedGroupAlgebra C H) (KernelAugmentationIdealQuotient C psi) :=
    zcCompletedGAKerAugQuotTargetCompletedModuleOfSurjective_of_kernelMulStandard_le
      C hC hForm psi hpsi hker_mul
  exact
    crossedHomModuleLift
      (A := KernelAugmentationIdealQuotient C psi)
      (zcCompletedGroupAlgebraScalar C psi.toMonoidHom)
      (sourceBoundaryToKerAugTargetCrossedHomOfSurjectiveOfKernelMulStandardLe
        C hC hForm psi hpsi hker_mul)

Under the explicit kernel-product hypothesis, the completed universal differential module maps to the algebraic source augmentation quotient by \(dg \mapsto [g]-1\). The hypothesis is the condition needed for the algebraic quotient \(I(G) / I(\ker \psi)I(G)\) to carry the completed target \(\mathbb{Z}_C\llbracket H\rrbracket\)-module structure.

@[simp 900]
theorem zcDiffToKerAugQuotOfSurj_of_kernelMulStandard_le_universal
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hker_mul :
      ∀ k : ZCCompletedGroupAlgebra C G,
        k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) →
        ∀ y : zcCompletedGroupAlgebraStandardAugmentationIdeal C G,
          (⟨k * (y : ZCCompletedGroupAlgebra C G),
            (zcCompletedGroupAlgebraStandardAugmentationIdeal C G).mul_mem_left k y.2⟩ :
              zcCompletedGroupAlgebraStandardAugmentationIdeal C G) ∈
            zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi)
    (g : G) :
    zcDiffToKerAugQuotOfSurj_of_kernelMulStandard_le
        C hC hForm psi hpsi hker_mul
        (zcUniversalDifferential C psi.toMonoidHom g) =
      zcCompletedGroupAlgebraSourceBoundaryToKernelAugmentationQuotient C psi g

Under the kernel-product hypothesis, the algebraic source augmentation quotient map sends the universal differential to the class of \([g]-1\).

Show Lean proof
theorem zcDiffToKerAugQuotOfSurj_of_kernelMulStandard_le_surj
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hker_mul :
      ∀ k : ZCCompletedGroupAlgebra C G,
        k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) →
        ∀ y : zcCompletedGroupAlgebraStandardAugmentationIdeal C G,
          (⟨k * (y : ZCCompletedGroupAlgebra C G),
            (zcCompletedGroupAlgebraStandardAugmentationIdeal C G).mul_mem_left k y.2⟩ :
              zcCompletedGroupAlgebraStandardAugmentationIdeal C G) ∈
            zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi) :
    Function.Surjective
      (zcDiffToKerAugQuotOfSurj_of_kernelMulStandard_le
        C hC hForm psi hpsi hker_mul)

The algebraic map \(A_{\psi}(C) \to I(G) / I(\ker \psi)I(G)\) is onto once the algebraic quotient has the completed target scalar action supplied by the explicit kernel-product hypothesis.

Show Lean proof
def zcCompletedGAKerAugQuotToClosedQuotientTargetLinear_of_kernelMulStandard_le
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (hker_mul :
      ∀ k : ZCCompletedGroupAlgebra C G,
        k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) →
        ∀ y : zcCompletedGroupAlgebraStandardAugmentationIdeal C G,
          (⟨k * (y : ZCCompletedGroupAlgebra C G),
            (zcCompletedGroupAlgebraStandardAugmentationIdeal C G).mul_mem_left k y.2⟩ :
              zcCompletedGroupAlgebraStandardAugmentationIdeal C G) ∈
            zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi) :
    letI : Module (ZCCompletedGroupAlgebra C H) (KernelAugmentationIdealQuotient C psi) :=
      zcCompletedGAKerAugQuotTargetCompletedModuleOfSurjective_of_kernelMulStandard_le
        C hC hForm psi hpsi hker_mul
    letI : Module (ZCCompletedGroupAlgebra C H)
        (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
      kerAugClosedQuotTargetCompletedModuleOfSurj
        C hC hForm psi hpsi hfopen
    KernelAugmentationIdealQuotient C psi →ₗ[ZCCompletedGroupAlgebra C H]
      KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen := by
  letI : Module (ZCCompletedGroupAlgebra C H) (KernelAugmentationIdealQuotient C psi) :=
    zcCompletedGAKerAugQuotTargetCompletedModuleOfSurjective_of_kernelMulStandard_le
      C hC hForm psi hpsi hker_mul
  letI : Module (ZCCompletedGroupAlgebra C H)
      (KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen) :=
    kerAugClosedQuotTargetCompletedModuleOfSurj
      C hC hForm psi hpsi hfopen
  let Q :=
    zcCompletedGroupAlgebraKernelAugmentationQuotientToClosedQuotient
      C hC hForm psi hpsi hfopen
  refine
    { toFun := Q
      map_add' := by
        intro x y
        exact map_add Q x y
      map_smul' := by
        intro a x
        change Q
            (zcCompletedGroupAlgebraTargetLiftOfSurjective C hC hForm psi hpsi a • x) =
          a • Q x
        rw [map_smul]
        symm
        calc
          a • Q x =
              zcCompletedGroupAlgebraMap C hC psi
                  (zcCompletedGroupAlgebraTargetLiftOfSurjective C hC hForm psi hpsi a) •
                Q x := by
                rw [zcCompletedGroupAlgebraMap_targetLiftOfSurjective]
          _ =
              zcCompletedGroupAlgebraTargetLiftOfSurjective C hC hForm psi hpsi a • Q x := by
                exact
                  kerAugClosedQuotTargetCompletedModuleOfSurj_map_smul
                    C hC hForm psi hpsi hfopen
                    (zcCompletedGroupAlgebraTargetLiftOfSurjective C hC hForm psi hpsi a)
                    (Q x) }

Under the explicit kernel-product hypothesis, the natural map from the algebraic source augmentation quotient to the closed quotient is \(\mathbb{Z}_C\llbracket H\rrbracket\)-linear.

@[simp 900]
theorem zcCompletedGAKerAugQuotToClosedQuotientTargetLinear_of_kernelMulStandard_le_mk
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (hker_mul :
      ∀ k : ZCCompletedGroupAlgebra C G,
        k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) →
        ∀ y : zcCompletedGroupAlgebraStandardAugmentationIdeal C G,
          (⟨k * (y : ZCCompletedGroupAlgebra C G),
            (zcCompletedGroupAlgebraStandardAugmentationIdeal C G).mul_mem_left k y.2⟩ :
              zcCompletedGroupAlgebraStandardAugmentationIdeal C G) ∈
            zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi)
    (x : zcCompletedGroupAlgebraStandardAugmentationIdeal C G) :
    zcCompletedGAKerAugQuotToClosedQuotientTargetLinear_of_kernelMulStandard_le
        C hC hForm psi hpsi hfopen hker_mul (Submodule.Quotient.mk x) =
      (Submodule.Quotient.mk x :
        KernelAugmentationIdealClosedQuotient C hC hForm psi hpsi hfopen)

The natural map from the algebraic source augmentation quotient to the closed quotient sends each algebraic quotient class to its closed quotient class.

Show Lean proof
theorem zcDiffToKerAugClosedQuotOfSurj_eq_toClosed_comp_quotient_of_kernelMulStandard_le
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
    (hfopen : IsOpenMap psi)
    (hker_mul :
      ∀ k : ZCCompletedGroupAlgebra C G,
        k ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) →
        ∀ y : zcCompletedGroupAlgebraStandardAugmentationIdeal C G,
          (⟨k * (y : ZCCompletedGroupAlgebra C G),
            (zcCompletedGroupAlgebraStandardAugmentationIdeal C G).mul_mem_left k y.2⟩ :
              zcCompletedGroupAlgebraStandardAugmentationIdeal C G) ∈
            zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi) :
    (zcCompletedGAKerAugQuotToClosedQuotientTargetLinear_of_kernelMulStandard_le
        C hC hForm psi hpsi hfopen hker_mul).comp
      (zcDiffToKerAugQuotOfSurj_of_kernelMulStandard_le
        C hC hForm psi hpsi hker_mul) =
    zcCompletedDifferentialModuleToKernelAugmentationClosedQuotientOfSurjective
      C hC hForm psi hpsi hfopen

The algebraic quotient map followed by the natural closed-quotient map is the closed quotient map already constructed directly from \(A_{\psi}(C)\).

Show Lean proof
theorem zcCompletedDifferentialModule_sourceKernelGroupLikeSubOne_smul_eq_zero
    (hC : ProCGroups.FiniteGroupClass.Hereditary C) (psi : ContinuousMonoidHom G H)
    (n : ProfiniteKernelSubgroup psi) (x : ZCCompletedDifferentialModule C psi.toMonoidHom) :
    letI : Module (ZCCompletedGroupAlgebra C G)
        (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
      Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
    (zcGroupLike C G n.1 - 1) • x = 0

Source kernel group-like differences act trivially on \(A_{\psi}(C)\) after restricting scalars along \(\mathbb{Z}_C\llbracket G\rrbracket \to \mathbb{Z}_C\llbracket H\rrbracket\).

Show Lean proof
theorem zcCompletedDifferentialModule_kernelAugmentationIdealMulStandard_smul_eq_zero
    (hC : ProCGroups.FiniteGroupClass.Hereditary C) (psi : ContinuousMonoidHom G H)
    (y : zcCompletedGroupAlgebraStandardAugmentationIdeal C G)
    (hy : y ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMulStandard C psi)
    (x : ZCCompletedDifferentialModule C psi.toMonoidHom) :
    letI : Module (ZCCompletedGroupAlgebra C G)
        (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
      Module.compHom _ (zcCompletedGroupAlgebraMap C hC psi)
    (y : ZCCompletedGroupAlgebra C G) • x = 0

The algebraic product \(I(\ker \psi)I(G)\) acts trivially on \(A_{\psi}(C)\) after restricting scalars along \(\mathbb{Z}_C\llbracket G\rrbracket \to \mathbb{Z}_C\llbracket H\rrbracket\).

Show Lean proof