FoxDifferential.Completed.ProCIntegerCoefficients.Naturality
import
def zcCompletedGroupAlgebraMapStage
(φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K) :
ZCCompletedGroupAlgebraStage C H
(i.1, completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2) →+*
ZCCompletedGroupAlgebraStage C K i :=
MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff i.1.modulus)
(completedGroupAlgebraComapQuotientMapInClass (G := H) (H := K) C hC φ i.2)
@[simp]The finite-stage component of the target map on \(\mathbb{Z}_C\llbracket H\rrbracket\).
theorem zcCompletedGroupAlgebraMapStage_of
(φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K)
(q : CompletedGroupAlgebraQuotientInClass H C
(completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ i.2)) :
zcCompletedGroupAlgebraMapStage C hC φ i
(MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus) _ q) =
MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus) _
(completedGroupAlgebraComapQuotientMapInClass (G := H) (H := K) C hC φ i.2 q)The induced finite-stage target map sends a singleton supported at a quotient class to the singleton supported at its image, preserving the coefficient.
Show proof
by
simp only [zcCompletedGroupAlgebraMapStage, MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk,
OneHom.coe_mk, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]Proof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□theorem zcCompletedGroupAlgebraMapStage_single
(φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K)
(q : CompletedGroupAlgebraQuotientInClass H C
(completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ i.2))
(a : ModNCompletedCoeff i.1.modulus) :
zcCompletedGroupAlgebraMapStage C hC φ i (MonoidAlgebra.single q a) =
MonoidAlgebra.single
(completedGroupAlgebraComapQuotientMapInClass (G := H) (H := K) C hC φ i.2 q) aThe induced finite-stage target map sends a singleton supported at a quotient class to the singleton supported at its image, preserving the coefficient.
Show proof
by
simp only [zcCompletedGroupAlgebraMapStage, MonoidAlgebra.single, MonoidAlgebra.mapDomainRingHom_apply,
Finsupp.mapDomain_single]Proof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□theorem zcCompletedGroupAlgebraMapStage_surjective_of_surjective
(φ : H →ₜ* K) (hφ : Function.Surjective φ)
(i : ZCCompletedGroupAlgebraIndex C K) :
Function.Surjective (zcCompletedGroupAlgebraMapStage C hC φ i)A surjective target homomorphism induces a surjective map on every finite \(\mathbb{Z}_C\)-coefficient, \(C\)-quotient stage of the completed group algebra.
Show proof
by
simpa [zcCompletedGroupAlgebraMapStage, MonoidAlgebra.mapDomainRingHom_apply] using
(Finsupp.mapDomain_surjective (M := ModNCompletedCoeff i.1.modulus)
(completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
(G := H) (H := K) C hC φ hφ i.2))Proof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□theorem zcCompletedGroupAlgebraMapStage_smul
(φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K)
(a : ModNCompletedCoeff i.1.modulus)
(x :
ZCCompletedGroupAlgebraStage C H
(i.1, completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2)) :
zcCompletedGroupAlgebraMapStage C hC φ i (a • x) =
a • zcCompletedGroupAlgebraMapStage C hC φ i xA finite-stage target map is linear over the common residue coefficient ring.
Show proof
by
rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
rw [Algebra.smul_def, Algebra.smul_def, RingHom.map_mul]
simp only [zcCompletedGroupAlgebraMapStage, map_intCast, MonoidAlgebra.mapDomainRingHom_apply]Proof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□def zcCompletedGroupAlgebraMapStageKernelIdeal
(φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K) :
Ideal
(ZCCompletedGroupAlgebraStage C H
(i.1, completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2)) :=
RingHom.ker (zcCompletedGroupAlgebraMapStage C hC φ i)
@[simp]The kernel ideal of a finite-stage target map on completed group algebras.
theorem mem_zcCompletedGroupAlgebraMapStageKernelIdeal_iff
(φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K)
{x :
ZCCompletedGroupAlgebraStage C H
(i.1, completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2)} :
x ∈ zcCompletedGroupAlgebraMapStageKernelIdeal C hC φ i ↔
zcCompletedGroupAlgebraMapStage C hC φ i x = 0Membership in the completed group-algebra stage-map kernel ideal is equivalent to vanishing of the corresponding finite-stage coordinate.
Show proof
by
rw [zcCompletedGroupAlgebraMapStageKernelIdeal, RingHom.mem_ker]Proof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□def zcCompletedGroupAlgebraMapStageRelationAugmentationGenerator
(φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K)
(q :
(completedGroupAlgebraComapQuotientMapInClass
(G := H) (H := K) C hC φ i.2).ker) :
ZCCompletedGroupAlgebraStage C H
(i.1, completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2) :=
MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass H C
(completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2)) q.1 - 1The finite-stage relation augmentation generator attached to an element of the quotient kernel.
def zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal
(φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K) :
Ideal
(ZCCompletedGroupAlgebraStage C H
(i.1, completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2)) :=
Ideal.span
(Set.range
(zcCompletedGroupAlgebraMapStageRelationAugmentationGenerator C hC φ i))The finite-stage relation augmentation ideal for a target map.
theorem zcCompletedGroupAlgebraMapStageRelationAugmentationGenerator_mem_kernelIdeal
(φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K)
(q :
(completedGroupAlgebraComapQuotientMapInClass
(G := H) (H := K) C hC φ i.2).ker) :
zcCompletedGroupAlgebraMapStageRelationAugmentationGenerator C hC φ i q ∈
zcCompletedGroupAlgebraMapStageKernelIdeal C hC φ iA finite-stage relation augmentation generator lies in the kernel ideal.
Show proof
by
rw [mem_zcCompletedGroupAlgebraMapStageKernelIdeal_iff]
change zcCompletedGroupAlgebraMapStage C hC φ i
(MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass H C
(completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2)) q.1 - 1) = 0
rw [map_sub, map_one, zcCompletedGroupAlgebraMapStage_of]
have hq :
completedGroupAlgebraComapQuotientMapInClass
(G := H) (H := K) C hC φ i.2 q.1 = 1 := by
exact MonoidHom.mem_ker.mp
(show (q : CompletedGroupAlgebraQuotientInClass H C
(completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2)) ∈
(completedGroupAlgebraComapQuotientMapInClass
(G := H) (H := K) C hC φ i.2).ker from q.2)
rw [hq]
simp only [MonoidAlgebra.of, MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.one_def, sub_self]Proof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□theorem zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal_le_kernelIdeal
(φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K) :
zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC φ i ≤
zcCompletedGroupAlgebraMapStageKernelIdeal C hC φ iThe finite-stage relation augmentation ideal is contained in the finite-stage kernel ideal.
Show proof
by
refine Ideal.span_le.2 ?_
rintro x ⟨q, rfl⟩
exact zcCompletedGroupAlgebraMapStageRelationAugmentationGenerator_mem_kernelIdeal
C hC φ i qProof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□def zcCompletedGroupAlgebraMapStageTargetSection
(φ : H →ₜ* K) (hφ : Function.Surjective φ)
(i : ZCCompletedGroupAlgebraIndex C K) :
ZCCompletedGroupAlgebraStage C K i →ₗ[ModNCompletedCoeff i.1.modulus]
ZCCompletedGroupAlgebraStage C H
(i.1, completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2) :=
Finsupp.linearCombination (ModNCompletedCoeff i.1.modulus)
(fun q : CompletedGroupAlgebraQuotientInClass K C i.2 =>
MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass H C
(completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2))
(Function.surjInv
(completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
(G := H) (H := K) C hC φ hφ i.2) q))
@[simp 900]A linear section of a surjective finite-stage target map, obtained by choosing a source quotient lift for each target quotient basis element.
theorem zcCompletedGroupAlgebraMapStageTargetSection_of
(φ : H →ₜ* K) (hφ : Function.Surjective φ)
(i : ZCCompletedGroupAlgebraIndex C K)
(q : CompletedGroupAlgebraQuotientInClass K C i.2) :
zcCompletedGroupAlgebraMapStageTargetSection C hC φ hφ i
(MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass K C i.2) q) =
MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass H C
(completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2))
(Function.surjInv
(completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
(G := H) (H := K) C hC φ hφ i.2) q)The induced finite-stage target map sends a singleton supported at a quotient class to the singleton supported at its image, preserving the coefficient.
Show proof
by
change
(Finsupp.linearCombination (ModNCompletedCoeff i.1.modulus)
(fun q : CompletedGroupAlgebraQuotientInClass K C i.2 =>
MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass H C
(completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2))
(Function.surjInv
(completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
(G := H) (H := K) C hC φ hφ i.2) q)))
(Finsupp.single q (1 : ModNCompletedCoeff i.1.modulus)) = _
rw [Finsupp.linearCombination_single, one_smul]Proof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□theorem zcCompletedGroupAlgebraMapStage_targetSection
(φ : H →ₜ* K) (hφ : Function.Surjective φ)
(i : ZCCompletedGroupAlgebraIndex C K)
(y : ZCCompletedGroupAlgebraStage C K i) :
zcCompletedGroupAlgebraMapStage C hC φ i
(zcCompletedGroupAlgebraMapStageTargetSection C hC φ hφ i y) = yShow proof
by
classical
refine MonoidAlgebra.induction_on
(p := fun y : ZCCompletedGroupAlgebraStage C K i =>
zcCompletedGroupAlgebraMapStage C hC φ i
(zcCompletedGroupAlgebraMapStageTargetSection C hC φ hφ i y) = y)
y ?single ?add ?smul
· intro q
rw [zcCompletedGroupAlgebraMapStageTargetSection_of,
zcCompletedGroupAlgebraMapStage_of]
exact congrArg
(MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass K C i.2))
(Function.surjInv_eq
(completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
(G := H) (H := K) C hC φ hφ i.2) q)
· intro x y hx hy
rw [map_add, map_add, hx, hy]
· intro a y hy
rw [map_smul, zcCompletedGroupAlgebraMapStage_smul, hy]Proof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□theorem zcCompletedGAMapStage_sourceBasis_sub_targetSection_mem_relationAugmentationIdeal
(φ : H →ₜ* K) (hφ : Function.Surjective φ)
(i : ZCCompletedGroupAlgebraIndex C K)
(s :
CompletedGroupAlgebraQuotientInClass H C
(completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2)) :
MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass H C
(completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2)) s -
zcCompletedGroupAlgebraMapStageTargetSection C hC φ hφ i
(zcCompletedGroupAlgebraMapStage C hC φ i
(MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass H C
(completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2)) s)) ∈
zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC φ iAt a finite completed group-algebra stage, a source basis element minus the chosen lift of its target image lies in the relation augmentation ideal.
Show proof
by
let f :=
completedGroupAlgebraComapQuotientMapInClass
(G := H) (H := K) C hC φ i.2
let hfsurj :
Function.Surjective f :=
completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
(G := H) (H := K) C hC φ hφ i.2
let t : CompletedGroupAlgebraQuotientInClass K C i.2 := f s
let lift :
CompletedGroupAlgebraQuotientInClass H C
(completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2) :=
Function.surjInv hfsurj t
let q : f.ker :=
⟨lift⁻¹ * s, by
change f (lift⁻¹ * s) = 1
rw [map_mul, map_inv]
have hlift : f lift = t := Function.surjInv_eq hfsurj t
rw [hlift]
simp only [inv_mul_cancel, t]⟩
have hsection :
zcCompletedGroupAlgebraMapStageTargetSection C hC φ hφ i
(zcCompletedGroupAlgebraMapStage C hC φ i
(MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass H C
(completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2)) s)) =
MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass H C
(completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2)) lift := by
rw [zcCompletedGroupAlgebraMapStage_of,
zcCompletedGroupAlgebraMapStageTargetSection_of]
rw [hsection]
have hmul :
MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass H C
(completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2)) lift *
zcCompletedGroupAlgebraMapStageRelationAugmentationGenerator C hC φ i q =
MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass H C
(completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2)) s -
MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass H C
(completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2)) lift := by
simp only [zcCompletedGroupAlgebraMapStageRelationAugmentationGenerator, q,
MonoidAlgebra.of_apply]
rw [mul_sub, MonoidAlgebra.single_mul_single, mul_one]
simp only [mul_inv_cancel_left, mul_one]
rw [← hmul]
exact
(zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC φ i).mul_mem_left _
(Ideal.subset_span ⟨q, rfl⟩)Proof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□theorem zcCompletedGAMapStage_sub_targetSection_map_mem_relationAugmentationIdeal
(φ : H →ₜ* K) (hφ : Function.Surjective φ)
(i : ZCCompletedGroupAlgebraIndex C K)
(x :
ZCCompletedGroupAlgebraStage C H
(i.1, completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2)) :
x - zcCompletedGroupAlgebraMapStageTargetSection C hC φ hφ i
(zcCompletedGroupAlgebraMapStage C hC φ i x) ∈
zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC φ iAt a finite completed group-algebra stage, every source element minus the chosen lift of its target image lies in the relation augmentation ideal.
Show proof
by
classical
refine MonoidAlgebra.induction_on
(p := fun x :
ZCCompletedGroupAlgebraStage C H
(i.1, completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2) =>
x - zcCompletedGroupAlgebraMapStageTargetSection C hC φ hφ i
(zcCompletedGroupAlgebraMapStage C hC φ i x) ∈
zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC φ i)
x ?single ?add ?smul
· intro s
exact
zcCompletedGAMapStage_sourceBasis_sub_targetSection_mem_relationAugmentationIdeal
C hC φ hφ i s
· intro x y hx hy
have hcalc :
x + y - zcCompletedGroupAlgebraMapStageTargetSection C hC φ hφ i
(zcCompletedGroupAlgebraMapStage C hC φ i (x + y)) =
(x - zcCompletedGroupAlgebraMapStageTargetSection C hC φ hφ i
(zcCompletedGroupAlgebraMapStage C hC φ i x)) +
(y - zcCompletedGroupAlgebraMapStageTargetSection C hC φ hφ i
(zcCompletedGroupAlgebraMapStage C hC φ i y)) := by
rw [map_add, map_add]
abel
rw [hcalc]
exact
(zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC φ i).add_mem hx hy
· intro a x hx
have hmap_smul :
zcCompletedGroupAlgebraMapStage C hC φ i (a • x) =
a • zcCompletedGroupAlgebraMapStage C hC φ i x :=
zcCompletedGroupAlgebraMapStage_smul C hC φ i a x
have hcalc :
a • x - zcCompletedGroupAlgebraMapStageTargetSection C hC φ hφ i
(zcCompletedGroupAlgebraMapStage C hC φ i (a • x)) =
a • (x - zcCompletedGroupAlgebraMapStageTargetSection C hC φ hφ i
(zcCompletedGroupAlgebraMapStage C hC φ i x)) := by
rw [hmap_smul, map_smul, smul_sub]
rw [hcalc]
rw [Algebra.smul_def]
exact
(zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC φ i).mul_mem_left _ hxProof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□theorem zcCompletedGAMapStageKernelIdeal_eq_relationAugmentationIdeal_of_surj
(φ : H →ₜ* K) (hφ : Function.Surjective φ)
(i : ZCCompletedGroupAlgebraIndex C K) :
zcCompletedGroupAlgebraMapStageKernelIdeal C hC φ i =
zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC φ iIn each finite stage, the kernel of a surjective target map is exactly the relation augmentation ideal generated by the kernel of the finite quotient map.
Show proof
by
apply le_antisymm
· intro x hx
have hxmap :
zcCompletedGroupAlgebraMapStage C hC φ i x = 0 :=
(mem_zcCompletedGroupAlgebraMapStageKernelIdeal_iff
(C := C) (hC := hC) φ i).1 hx
have hdiff :=
zcCompletedGAMapStage_sub_targetSection_map_mem_relationAugmentationIdeal
C hC φ hφ i x
rw [hxmap, map_zero, sub_zero] at hdiff
exact hdiff
· exact zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal_le_kernelIdeal C hC φ iProof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□theorem zcCompletedGroupAlgebraMapStage_compatible
(φ : H →ₜ* K)
{i j : ZCCompletedGroupAlgebraIndex C K} (hij : i ≤ j) :
(zcCompletedGroupAlgebraTransition C K hij).comp
(zcCompletedGroupAlgebraMapStage C hC φ j) =
(zcCompletedGroupAlgebraMapStage C hC φ i).comp
(zcCompletedGroupAlgebraTransition C H
(show
(i.1, completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2) ≤
(j.1, completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ j.2) from
⟨hij.1,
completedGroupAlgebraComapIndexInClass_mono
(G := H) (H := K) C hC φ hij.2⟩))Show proof
by
letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
apply RingHom.ext
intro x
refine MonoidAlgebra.induction_on
(p := fun x =>
((zcCompletedGroupAlgebraTransition C K hij).comp
(zcCompletedGroupAlgebraMapStage C hC φ j)) x =
((zcCompletedGroupAlgebraMapStage C hC φ i).comp
(zcCompletedGroupAlgebraTransition C H
(show
(i.1, completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2) ≤
(j.1, completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ j.2) from
⟨hij.1,
completedGroupAlgebraComapIndexInClass_mono
(G := H) (H := K) C hC φ hij.2⟩))) x)
x ?_ ?_ ?_
· intro q
rw [RingHom.comp_apply, RingHom.comp_apply,
zcCompletedGroupAlgebraMapStage_of, zcCompletedGroupAlgebraTransition_of,
zcCompletedGroupAlgebraTransition_of]
change
MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass K C i.2)
((OpenNormalSubgroupInClass.map
(C := C) (G := K)
(U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2)
(completedGroupAlgebraComapQuotientMapInClass
(G := H) (H := K) C hC φ j.2 q)) =
zcCompletedGroupAlgebraMapStage C hC φ i
(MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass H C
(completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ i.2))
((OpenNormalSubgroupInClass.map
(C := C) (G := H)
(U := OrderDual.ofDual
(completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ i.2))
(V := OrderDual.ofDual
(completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ j.2))
(completedGroupAlgebraComapIndexInClass_mono
(G := H) (H := K) C hC φ hij.2)) q))
rw [zcCompletedGroupAlgebraMapStage_of]
exact congrArg (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass K C i.2))
(congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraComapQuotientMapInClass_compatible
(G := H) (H := K) C hC φ hij.2)) q)
· intro x y hx hy
rw [map_add, map_add, hx, hy]
· intro a x hx
rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
rw [Algebra.smul_def, RingHom.map_mul, RingHom.map_mul, hx]
simp only [zcCompletedGroupAlgebraTransition, modNCompletedGroupAlgebraStageCoeffMapInClass,
modNCompletedGroupRingCoeffMap, AlgHom.toRingHom_eq_coe, zcCompletedGroupAlgebraMapStage, map_intCast,
RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, MonoidAlgebra.mapDomainRingHom_apply]Proof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□def zcCompletedGroupAlgebraMap (φ : H →ₜ* K) :
ZCCompletedGroupAlgebra C H →+* ZCCompletedGroupAlgebra C K where
toFun x := ⟨fun i =>
zcCompletedGroupAlgebraMapStage C hC φ i
(zcCompletedGroupAlgebraProjection C H
(i.1, completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2) x), by
intro i j hij
let hsource :
(i.1, completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ i.2) ≤
(j.1, completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ j.2) :=
⟨hij.1, completedGroupAlgebraComapIndexInClass_mono
(G := H) (H := K) C hC φ hij.2⟩
have hx := x.2
(i.1, completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ i.2)
(j.1, completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ j.2)
hsource
have hcompat := congrFun
(congrArg DFunLike.coe
(zcCompletedGroupAlgebraMapStage_compatible C hC φ hij))
(zcCompletedGroupAlgebraProjection C H
(j.1, completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ j.2) x)
rw [RingHom.comp_apply, RingHom.comp_apply] at hcompat
rw [hx] at hcompat
simpa using hcompat⟩
map_zero' := by
apply Subtype.ext
funext i
simp only [zcCompletedGroupAlgebraMapStage, zcCompletedGroupAlgebraProjection_zero,
MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_zero]
map_add' := by
intro x y
apply Subtype.ext
funext i
simp only [zcCompletedGroupAlgebraProjection_add, map_add]
map_one' := by
apply Subtype.ext
funext i
simp only [zcCompletedGroupAlgebraMapStage, zcCompletedGroupAlgebraProjection_one,
MonoidAlgebra.mapDomainRingHom_apply, MonoidAlgebra.mapDomain_one]
map_mul' := by
intro x y
apply Subtype.ext
funext i
simp only [zcCompletedGroupAlgebraProjection_mul, map_mul]
@[simp]The completed group-algebra map \(\mathbb{Z}_C\llbracket H\rrbracket\) \(\to\) \(\mathbb{Z}_C\llbracket K\rrbracket\) induced by a continuous homomorphism \(H \to K\).
theorem zcCompletedGroupAlgebraProjection_map
(φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K)
(x : ZCCompletedGroupAlgebra C H) :
zcCompletedGroupAlgebraProjection C K i (zcCompletedGroupAlgebraMap C hC φ x) =
zcCompletedGroupAlgebraMapStage C hC φ i
(zcCompletedGroupAlgebraProjection C H
(i.1, completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2) x)The \(\mathbb{Z}_C\)-completed group-algebra projection is computed by the corresponding finite-stage coordinate map.
Show proof
rflProof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□theorem mem_zcCompletedGroupAlgebraMap_ker_iff_stageKernelIdeal
(φ : H →ₜ* K) (x : ZCCompletedGroupAlgebra C H) :
x ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC φ) ↔
∀ i : ZCCompletedGroupAlgebraIndex C K,
zcCompletedGroupAlgebraProjection C H
(i.1, completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2) x ∈
zcCompletedGroupAlgebraMapStageKernelIdeal C hC φ iMembership in the kernel of the completed target map is exactly membership in the kernel of every target-indexed finite stage.
Show proof
by
constructor
· intro hx i
rw [mem_zcCompletedGroupAlgebraMapStageKernelIdeal_iff]
have hmap : zcCompletedGroupAlgebraMap C hC φ x = 0 :=
(RingHom.mem_ker).1 hx
have hi := congrArg (zcCompletedGroupAlgebraProjection C K i) hmap
simpa [zcCompletedGroupAlgebraProjection_map] using hi
· intro hstage
rw [RingHom.mem_ker]
apply Subtype.ext
funext i
change zcCompletedGroupAlgebraProjection C K i (zcCompletedGroupAlgebraMap C hC φ x) =
zcCompletedGroupAlgebraProjection C K i (0 : ZCCompletedGroupAlgebra C K)
rw [zcCompletedGroupAlgebraProjection_map]
have hi :
zcCompletedGroupAlgebraMapStage C hC φ i
(zcCompletedGroupAlgebraProjection C H
(i.1, completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2) x) = 0 :=
(mem_zcCompletedGroupAlgebraMapStageKernelIdeal_iff
(C := C) (hC := hC) φ i).1 (hstage i)
simpa using hiProof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□theorem mem_zcCompletedGAMap_ker_iff_stageRelationAugmentationIdeal_of_surj
(φ : H →ₜ* K) (hφ : Function.Surjective φ)
(x : ZCCompletedGroupAlgebra C H) :
x ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC φ) ↔
∀ i : ZCCompletedGroupAlgebraIndex C K,
zcCompletedGroupAlgebraProjection C H
(i.1, completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ i.2) x ∈
zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC φ iFor a surjective target map, membership in the completed kernel is equivalently membership in the explicit relation-augmentation ideal at every target-indexed finite stage.
Show proof
by
constructor
· intro hx i
have hi := (mem_zcCompletedGroupAlgebraMap_ker_iff_stageKernelIdeal
C hC φ x).1 hx i
rwa [zcCompletedGAMapStageKernelIdeal_eq_relationAugmentationIdeal_of_surj
C hC φ hφ i] at hi
· intro hstage
exact (mem_zcCompletedGroupAlgebraMap_ker_iff_stageKernelIdeal C hC φ x).2
(fun i => by
rw [zcCompletedGAMapStageKernelIdeal_eq_relationAugmentationIdeal_of_surj
C hC φ hφ i]
exact hstage i)
@[simp]Proof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□theorem zcCompletedGroupAlgebraMap_groupLike
(φ : H →ₜ* K) (h : H) :
zcCompletedGroupAlgebraMap C hC φ (zcGroupLike C H h) =
zcGroupLike C K (φ h)The completed target map sends a group-like element to the group-like element represented by its image under the target homomorphism.
Show proof
by
apply Subtype.ext
funext i
change
zcCompletedGroupAlgebraProjection C K i
(zcCompletedGroupAlgebraMap C hC φ (zcGroupLike C H h)) =
zcCompletedGroupAlgebraProjection C K i (zcGroupLike C K (φ h))
rw [zcCompletedGroupAlgebraProjection_map,
zcCompletedGroupAlgebraProjection_groupLike,
zcCompletedGroupAlgebraProjection_groupLike,
zcCompletedGroupAlgebraMapStage_of]
exact congrArg
(MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass K C i.2))
(completedGroupAlgebraComapQuotientMapInClass_mk
(G := H) (H := K) C hC φ i.2 h)
@[simp]Proof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□theorem zcCompletedGroupAlgebraMap_scalar
{G : Type v} [Group G] (φ : H →ₜ* K) (ψ : G →* H) (g : G) :
zcCompletedGroupAlgebraMap C hC φ (zcCompletedGroupAlgebraScalar C ψ g) =
zcCompletedGroupAlgebraScalar C (φ.toMonoidHom.comp ψ) gThe completed target map is linear over the induced map on coefficient group algebras.
Show proof
by
simp only [zcCompletedGroupAlgebraScalar, MonoidHom.coe_comp, Function.comp_apply,
zcCompletedGroupAlgebraMap_groupLike, ContinuousMonoidHom.coe_toMonoidHom, MonoidHom.coe_coe]
@[simp]Proof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□theorem zcCompletedGroupAlgebraMap_boundary
{G : Type v} [Group G] (φ : H →ₜ* K) (ψ : G →* H) (g : G) :
zcCompletedGroupAlgebraMap C hC φ (zcCompletedGroupAlgebraBoundary C ψ g) =
zcCompletedGroupAlgebraBoundary C (φ.toMonoidHom.comp ψ) gThe completed target map is compatible with the corresponding boundary map.
Show proof
by
simp only [zcCompletedGroupAlgebraBoundary, map_sub, zcCompletedGroupAlgebraMap_groupLike, map_one,
ContinuousMonoidHom.coe_toMonoidHom, MonoidHom.coe_comp, MonoidHom.coe_coe, Function.comp_apply]Proof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□theorem zcCompletedGroupAlgebraMapStage_augmentation
(φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K) :
(modNCompletedGroupAlgebraStageAugmentationInClass i.1.modulus K C i.2).comp
(zcCompletedGroupAlgebraMapStage C hC φ i) =
modNCompletedGroupAlgebraStageAugmentationInClass i.1.modulus H C
(completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ i.2)Show proof
by
letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
apply RingHom.ext
intro y
let U := i.2
let V := completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ U
let P := fun y =>
((modNCompletedGroupAlgebraStageAugmentationInClass i.1.modulus K C U).comp
(zcCompletedGroupAlgebraMapStage C hC φ i)) y =
(modNCompletedGroupAlgebraStageAugmentationInClass i.1.modulus H C V) y
change P y
refine MonoidAlgebra.induction_on (p := P) y ?_ ?_ ?_
· intro q
dsimp [P]
rw [zcCompletedGroupAlgebraMapStage_single]
simp only [modNCompletedGroupAlgebraStageAugmentationInClass_single, V]
· intro a b ha hb
dsimp [P] at ha hb ⊢
rw [RingHom.map_add, map_add, ha, hb, map_add]
· intro a y hy
dsimp [P] at hy ⊢
rw [Algebra.smul_def, RingHom.map_mul, RingHom.map_mul, hy]
have hcoeff :
((modNCompletedGroupAlgebraStageAugmentationInClass i.1.modulus K C U).comp
(zcCompletedGroupAlgebraMapStage C hC φ i))
(algebraMap (ModNCompletedCoeff i.1.modulus)
(ZCCompletedGroupAlgebraStage C H (i.1, V)) a) =
(modNCompletedGroupAlgebraStageAugmentationInClass i.1.modulus H C V)
(algebraMap (ModNCompletedCoeff i.1.modulus)
(ZCCompletedGroupAlgebraStage C H (i.1, V)) a) := by
rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
simp only [modNCompletedGroupAlgebraStageAugmentationInClass, zcCompletedGroupAlgebraMapStage, map_intCast, U,
V]
have hcoeff' :
(modNCompletedGroupAlgebraStageAugmentationInClass i.1.modulus K C U)
((zcCompletedGroupAlgebraMapStage C hC φ i)
(algebraMap (ModNCompletedCoeff i.1.modulus)
(ZCCompletedGroupAlgebraStage C H (i.1, V)) a)) =
(modNCompletedGroupAlgebraStageAugmentationInClass i.1.modulus H C V)
(algebraMap (ModNCompletedCoeff i.1.modulus)
(ZCCompletedGroupAlgebraStage C H (i.1, V)) a) := by
simpa [RingHom.comp_apply] using hcoeff
rw [hcoeff', map_mul]Proof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□theorem zcCompletedGroupAlgebraAugmentation_map
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
(φ : H →ₜ* K) (x : ZCCompletedGroupAlgebra C H) :
zcCompletedGroupAlgebraAugmentation C K (zcCompletedGroupAlgebraMap C hC φ x) =
zcCompletedGroupAlgebraAugmentation C H xCompleted augmentation is natural for target maps.
Show proof
by
ext i
change zcCompletedGroupAlgebraAugmentationFamily C K
(zcCompletedGroupAlgebraMap C hC φ x) i =
zcCompletedGroupAlgebraAugmentationFamily C H x i
let U : CompletedGroupAlgebraIndexInClass K C := zcCompletedGroupAlgebraTopIndex C K
let V : CompletedGroupAlgebraIndexInClass H C := zcCompletedGroupAlgebraTopIndex C H
have hV :
completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ U = V := by
simp only [zcCompletedGroupAlgebraTopIndex, completedGroupAlgebraComapIndexInClass_top, U, V]
dsimp [zcCompletedGroupAlgebraAugmentationFamily]
change
(modNCompletedGroupAlgebraStageAugmentationInClass i.modulus K C U)
(zcCompletedGroupAlgebraProjection C K (i, U)
(zcCompletedGroupAlgebraMap C hC φ x)) =
(modNCompletedGroupAlgebraStageAugmentationInClass i.modulus H C V)
(zcCompletedGroupAlgebraProjection C H (i, V) x)
rw [zcCompletedGroupAlgebraProjection_map]
cases hV
let y := zcCompletedGroupAlgebraProjection C H
(i, completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ U) x
change
(modNCompletedGroupAlgebraStageAugmentationInClass i.modulus K C U)
(zcCompletedGroupAlgebraMapStage C hC φ (i, U) y) =
(modNCompletedGroupAlgebraStageAugmentationInClass i.modulus H C
(completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ U)) y
exact congrFun
(congrArg DFunLike.coe
(zcCompletedGroupAlgebraMapStage_augmentation C hC φ (i, U))) yProof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□theorem zcCompletedGroupAlgebraMap_id :
zcCompletedGroupAlgebraMap C hC (ContinuousMonoidHom.id H) =
RingHom.id (ZCCompletedGroupAlgebra C H)The target map on completed \(\mathbb{Z}_C\) group algebras induced by the identity homomorphism is the identity ring homomorphism.
Show proof
by
apply RingHom.ext
intro x
apply Subtype.ext
funext i
change zcCompletedGroupAlgebraProjection C H i
(zcCompletedGroupAlgebraMap C hC (ContinuousMonoidHom.id H) x) =
zcCompletedGroupAlgebraProjection C H i x
rw [zcCompletedGroupAlgebraProjection_map]
have hfull :
(i.1, completedGroupAlgebraComapIndexInClass (G := H) (H := H) C hC
(ContinuousMonoidHom.id H) i.2) = i := by
cases i
simp only [completedGroupAlgebraComapIndexInClass_id]
cases hfull
change zcCompletedGroupAlgebraMapStage C hC (ContinuousMonoidHom.id H) i (x.1 i) =
x.1 i
refine MonoidAlgebra.induction_on
(p := fun y => zcCompletedGroupAlgebraMapStage C hC (ContinuousMonoidHom.id H) i y = y)
(x.1 i) ?_ ?_ ?_
· intro q
rcases QuotientGroup.mk'_surjective
((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup H) : Subgroup H)) q with
⟨g, rfl⟩
rw [zcCompletedGroupAlgebraMapStage_of]
rfl
· intro a b ha hb
rw [map_add, ha, hb]
· intro a y hy
rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
rw [Algebra.smul_def, RingHom.map_mul, hy]
simp only [zcCompletedGroupAlgebraMapStage, map_intCast]Proof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□theorem zcCompletedGroupAlgebraMap_comp
{L : Type u} [Group L] [TopologicalSpace L] [IsTopologicalGroup L]
(φ : H →ₜ* K) (ψ : K →ₜ* L) :
zcCompletedGroupAlgebraMap C hC (ψ.comp φ) =
(zcCompletedGroupAlgebraMap C hC ψ).comp
(zcCompletedGroupAlgebraMap C hC φ)Target maps on completed \(\mathbb{Z}_C\) group algebras compose functorially.
Show proof
by
apply RingHom.ext
intro x
apply Subtype.ext
funext i
change zcCompletedGroupAlgebraProjection C L i
(zcCompletedGroupAlgebraMap C hC (ψ.comp φ) x) =
zcCompletedGroupAlgebraProjection C L i
(zcCompletedGroupAlgebraMap C hC ψ (zcCompletedGroupAlgebraMap C hC φ x))
rw [zcCompletedGroupAlgebraProjection_map]
rw [zcCompletedGroupAlgebraProjection_map]
let j : ZCCompletedGroupAlgebraIndex C K :=
(i.1, completedGroupAlgebraComapIndexInClass (G := K) (H := L) C hC ψ i.2)
change zcCompletedGroupAlgebraMapStage C hC (ψ.comp φ) i
(zcCompletedGroupAlgebraProjection C H
(i.1, completedGroupAlgebraComapIndexInClass
(G := H) (H := L) C hC (ψ.comp φ) i.2) x) =
zcCompletedGroupAlgebraMapStage C hC ψ i
(zcCompletedGroupAlgebraProjection C K j
(zcCompletedGroupAlgebraMap C hC φ x))
rw [zcCompletedGroupAlgebraProjection_map]
have hidx :
(i.1, completedGroupAlgebraComapIndexInClass
(G := H) (H := L) C hC (ψ.comp φ) i.2) =
(j.1, completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ j.2) := by
subst j
simp only [completedGroupAlgebraComapIndexInClass_comp]
cases hidx
change zcCompletedGroupAlgebraMapStage C hC (ψ.comp φ) i
(zcCompletedGroupAlgebraProjection C H
(j.1, completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ j.2) x) =
zcCompletedGroupAlgebraMapStage C hC ψ i
(zcCompletedGroupAlgebraMapStage C hC φ j
(zcCompletedGroupAlgebraProjection C H
(j.1, completedGroupAlgebraComapIndexInClass
(G := H) (H := K) C hC φ j.2) x))
let P := fun y =>
zcCompletedGroupAlgebraMapStage C hC (ψ.comp φ) i y =
zcCompletedGroupAlgebraMapStage C hC ψ i
(zcCompletedGroupAlgebraMapStage C hC φ j y)
change P (zcCompletedGroupAlgebraProjection C H
(j.1, completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ j.2) x)
refine MonoidAlgebra.induction_on
(p := P)
(zcCompletedGroupAlgebraProjection C H
(j.1, completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ j.2) x)
?_ ?_ ?_
· intro q
refine QuotientGroup.induction_on q ?_
intro g
dsimp [P]
rw [zcCompletedGroupAlgebraMapStage_single]
rw [zcCompletedGroupAlgebraMapStage_single]
rw [zcCompletedGroupAlgebraMapStage_single]
rfl
· intro a b ha hb
dsimp [P] at ha hb
dsimp [P]
rw [map_add, map_add, map_add, ha, hb]
· intro a y hy
dsimp [P] at hy
dsimp [P]
let t : ℤ := Classical.choose (ZMod.intCast_surjective a)
have ht : (t : ModNCompletedCoeff j.1.modulus) = a :=
Classical.choose_spec (ZMod.intCast_surjective a)
rw [← ht, Algebra.smul_def, RingHom.map_mul, RingHom.map_mul, RingHom.map_mul, hy]
simp only [zcCompletedGroupAlgebraMapStage, map_intCast, MonoidAlgebra.mapDomainRingHom_apply]Proof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□def zcCompletedDifferentialModuleTargetMap
(ψ : G →* H) (φ : H →ₜ* K) :
letI : Module (ZCCompletedGroupAlgebra C H)
(ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ)) :=
Module.compHom _ (zcCompletedGroupAlgebraMap C hC φ)
ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ) := by
letI : Module (ZCCompletedGroupAlgebra C H)
(ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ)) :=
Module.compHom _ (zcCompletedGroupAlgebraMap C hC φ)
exact
zcCompletedDifferentialModuleLift
(A := ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ))
C ψ (fun g => zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g) (by
intro g h
change zcUniversalDifferential C (φ.toMonoidHom.comp ψ) (g * h) =
zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g +
zcCompletedGroupAlgebraScalar C ψ g •
zcUniversalDifferential C (φ.toMonoidHom.comp ψ) h
rw [zcUniversalDifferential_mul]
change zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g +
zcCompletedGroupAlgebraScalar C (φ.toMonoidHom.comp ψ) g •
zcUniversalDifferential C (φ.toMonoidHom.comp ψ) h =
zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g +
zcCompletedGroupAlgebraMap C hC φ (zcCompletedGroupAlgebraScalar C ψ g) •
zcUniversalDifferential C (φ.toMonoidHom.comp ψ) h
rw [zcCompletedGroupAlgebraMap_scalar])
@[simp 900]Target functoriality for the completed universal differential module. The codomain is regarded as a \(\mathbb{Z}_C\llbracket H\rrbracket\)-module by restriction of scalars along the completed group-algebra map induced by \(\varphi : H \to K\), and the universal differential \(d_{\psi}(g)\) is sent to \(d_{\varphi\circ\psi}(g)\).
theorem zcCompletedDifferentialModuleTargetMap_universal
(ψ : G →* H) (φ : H →ₜ* K) (g : G) :
letI : Module (ZCCompletedGroupAlgebra C H)
(ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ))The universal target map on the completed differential module is determined by the target homomorphism at finite stages.
Show proof
Module.compHom _ (zcCompletedGroupAlgebraMap C hC φ)
zcCompletedDifferentialModuleTargetMap C hC ψ φ
(zcUniversalDifferential C ψ g) =
zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g := by
letI : Module (ZCCompletedGroupAlgebra C H)
(ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ)) :=
Module.compHom _ (zcCompletedGroupAlgebraMap C hC φ)
exact
zcCompletedDifferentialModuleLift_universal
(A := ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ))
C ψ (fun g => zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g) (by
intro g h
change zcUniversalDifferential C (φ.toMonoidHom.comp ψ) (g * h) =
zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g +
zcCompletedGroupAlgebraScalar C ψ g •
zcUniversalDifferential C (φ.toMonoidHom.comp ψ) h
rw [zcUniversalDifferential_mul]
change zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g +
zcCompletedGroupAlgebraScalar C (φ.toMonoidHom.comp ψ) g •
zcUniversalDifferential C (φ.toMonoidHom.comp ψ) h =
zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g +
zcCompletedGroupAlgebraMap C hC φ (zcCompletedGroupAlgebraScalar C ψ g) •
zcUniversalDifferential C (φ.toMonoidHom.comp ψ) h
rw [zcCompletedGroupAlgebraMap_scalar])
gProof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□theorem zcUniversalDifferential_eq_zero_of_target
(ψ : G →* H) (φ : H →ₜ* K) {g : G}
(hg : zcUniversalDifferential C ψ g = 0) :
zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g = 0Completed universal zero descends along a target homomorphism.
Show proof
by
letI : Module (ZCCompletedGroupAlgebra C H)
(ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ)) :=
Module.compHom _ (zcCompletedGroupAlgebraMap C hC φ)
rw [← zcCompletedDifferentialModuleTargetMap_universal C hC ψ φ g, hg, map_zero]Proof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□theorem zcUniversalDifferential_eq_zero_of_source_target
(ψ : G →* H) (ψ' : G' →* K) (f : G →* G') (φ : H →ₜ* K)
(hcomm : ψ'.comp f = φ.toMonoidHom.comp ψ) {g : G}
(hg : zcUniversalDifferential C ψ g = 0) :
zcUniversalDifferential C ψ' (f g) = 0Vanishing of the completed universal differential descends along a commuting source-target square. In the finite-quotient form used in Magnus arguments, the relation \(\psi'\circ f = \varphi\circ\psi\) carries the vanishing of \(d_{\psi}(g)\) to the vanishing of \(d_{\psi'}(f(g))\).
Show proof
by
have ht :
zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g = 0 :=
zcUniversalDifferential_eq_zero_of_target C hC ψ φ hg
have hs :
zcUniversalDifferential C (ψ'.comp f) g = 0 := by
rw [hcomm]
exact ht
exact zcUniversalDifferential_eq_zero_of_source C ψ' f hsProof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□def zcFreeFoxCoordinatesMap (φ : H →ₜ* K) :
ZCFreeFoxCoordinates C (X := X) (H := H) →
ZCFreeFoxCoordinates C (X := X) (H := K) :=
fun a x => zcCompletedGroupAlgebraMap C hC φ (a x)A continuous homomorphism of target groups pushes completed Fox-coordinate vectors forward.
theorem zcFreeFoxCoordinatesMap_apply
(φ : H →ₜ* K) (a : ZCFreeFoxCoordinates C (X := X) (H := H)) (x : X) :
zcFreeFoxCoordinatesMap (X := X) C hC φ a x =
zcCompletedGroupAlgebraMap C hC φ (a x)The target push-forward map on completed free Fox-coordinate vectors is computed coordinatewise by the completed group-algebra map.
Show proof
rflProof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□theorem zcFreeFoxCoordinatesMap_id
(a : ZCFreeFoxCoordinates C (X := X) (H := H)) :
zcFreeFoxCoordinatesMap (X := X) C hC (ContinuousMonoidHom.id H) a = aThe coordinatewise target map induced by the identity homomorphism is the identity map.
Show proof
by
funext x
simp only [zcFreeFoxCoordinatesMap, zcCompletedGroupAlgebraMap_id, RingHom.id_apply]Proof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□theorem zcFreeFoxCoordinatesMap_comp
{L : Type v} [Group L] [TopologicalSpace L] [IsTopologicalGroup L]
(φ : H →ₜ* K) (ψ : K →ₜ* L)
(a : ZCFreeFoxCoordinates C (X := X) (H := H)) :
zcFreeFoxCoordinatesMap (X := X) C hC (ψ.comp φ) a =
zcFreeFoxCoordinatesMap (X := X) C hC ψ
(zcFreeFoxCoordinatesMap (X := X) C hC φ a)Coordinatewise target maps on completed Fox-coordinate vectors compose functorially.
Show proof
by
funext x
simp only [zcFreeFoxCoordinatesMap, zcCompletedGroupAlgebraMap_comp, RingHom.coe_comp, Function.comp_apply]Proof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□theorem zcFreeGroupFoxDerivativeVector_mapTarget
(ψ : FreeGroup X →* H) (φ : H →ₜ* K) (w : FreeGroup X) :
zcFreeGroupFoxDerivativeVector C (φ.toMonoidHom.comp ψ) w =
zcFreeFoxCoordinatesMap (X := X) C hC φ (zcFreeGroupFoxDerivativeVector C ψ w)Completed free-group Fox derivatives are natural under target pushforward.
Show proof
by
let delta : FreeGroup X → ZCFreeFoxCoordinates C (X := X) (H := K) :=
fun w => zcFreeFoxCoordinatesMap (X := X) C hC φ (zcFreeGroupFoxDerivativeVector C ψ w)
have hdelta :
IsCrossedDifferential
(zcCompletedGroupAlgebraScalar C (φ.toMonoidHom.comp ψ)) delta := by
intro u v
funext x
simp only [zcFreeFoxCoordinatesMap_apply, zcFreeGroupFoxDerivativeVector_mul,
zcCompletedGroupAlgebraScalar_apply, Pi.add_apply, Pi.smul_apply, smul_eq_mul, map_add, map_mul,
zcCompletedGroupAlgebraMap_groupLike, ContinuousMonoidHom.coe_toMonoidHom, MonoidHom.coe_comp, MonoidHom.coe_coe,
Function.comp_apply, delta]
have hbasis :
∀ x : X, delta (FreeGroup.of x) = Pi.single x (1 : ZCCompletedGroupAlgebra C K) := by
intro x
funext y
by_cases hxy : x = y
· subst y
simp only [zcFreeFoxCoordinatesMap_apply, zcFreeGroupFoxDerivativeVector_of, Pi.single_eq_same, map_one,
delta]
· simp only [zcFreeFoxCoordinatesMap_apply, zcFreeGroupFoxDerivativeVector_of, ne_eq, hxy, not_false_eq_true,
Pi.single_eq_of_ne', map_zero, delta]
have hdelta_eq :
delta = zcFreeGroupFoxDerivativeVector C (φ.toMonoidHom.comp ψ) :=
zcFreeGroupFoxDerivativeVector_unique C (φ.toMonoidHom.comp ψ) delta hdelta hbasis
rw [← congrFun hdelta_eq w]Proof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□theorem zcFreeGroupFoxDerivative_mapTarget
(ψ : FreeGroup X →* H) (φ : H →ₜ* K) (w : FreeGroup X) (x : X) :
zcFreeGroupFoxDerivative C (φ.toMonoidHom.comp ψ) x w =
zcCompletedGroupAlgebraMap C hC φ (zcFreeGroupFoxDerivative C ψ x w)Changing the target group maps each completed Fox derivative through the completed group-algebra map.
Show proof
by
have h := congrFun (zcFreeGroupFoxDerivativeVector_mapTarget C hC ψ φ w) x
simpa [zcFreeGroupFoxDerivative, zcFreeFoxCoordinatesMap] using hProof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□theorem zcFreeGroupFoxBoundary_mapTarget
(ψ : FreeGroup X →* H) (φ : H →ₜ* K)
(v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
zcCompletedGroupAlgebraMap C hC φ (zcFreeGroupFoxBoundary C ψ v) =
zcFreeGroupFoxBoundary C (φ.toMonoidHom.comp ψ)
(zcFreeFoxCoordinatesMap (X := X) C hC φ v)The completed Fox boundary is natural under target maps.
Show proof
by
simp only [zcFreeGroupFoxBoundary_apply, map_sum, map_mul, map_sub, zcCompletedGroupAlgebraMap_groupLike,
map_one, ContinuousMonoidHom.coe_toMonoidHom, zcFreeFoxCoordinatesMap, MonoidHom.coe_comp, MonoidHom.coe_coe,
Function.comp_apply]Proof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□theorem zcFreeGroupFoxBoundary_derivativeVector_mapTarget
(ψ : FreeGroup X →* H) (φ : H →ₜ* K) (w : FreeGroup X) :
zcCompletedGroupAlgebraMap C hC φ
(zcFreeGroupFoxBoundary C ψ (zcFreeGroupFoxDerivativeVector C ψ w)) =
zcFreeGroupFoxBoundary C (φ.toMonoidHom.comp ψ)
(zcFreeGroupFoxDerivativeVector C (φ.toMonoidHom.comp ψ) w)Target naturality carries the boundary of the completed Fox derivative vector to the boundary of the mapped derivative vector.
Show proof
by
rw [zcFreeGroupFoxBoundary_mapTarget, ← zcFreeGroupFoxDerivativeVector_mapTarget]Proof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□theorem zcFreeGroupFoxDerivative_euler_formula_mapTarget
(ψ : FreeGroup X →* H) (φ : H →ₜ* K) (w : FreeGroup X) :
zcCompletedGroupAlgebraMap C hC φ (zcGroupLike C H (ψ w) - 1) =
∑ i : X,
zcFreeGroupFoxDerivative C (φ.toMonoidHom.comp ψ) i w *
(zcGroupLike C K ((φ.toMonoidHom.comp ψ) (FreeGroup.of i)) - 1)The target-mapped completed Euler formula expresses the mapped boundary as the sum of mapped Fox derivatives times generator boundaries.
Show proof
by
simpa [zcCompletedGroupAlgebraBoundary] using
zcFreeGroupFoxDerivative_fundamental_formula C (φ.toMonoidHom.comp ψ) wProof. Use the finite-stage maps induced by the target homomorphism on \(\mathbb{Z}_C\)-completed group algebras. At each stage, a group-like basis element is sent to the basis element represented by its image in the target quotient, while coefficients are preserved or transported by the given coefficient map. Compatibility with quotient refinement gives the completed map; continuity, kernel ideals, augmentation, boundary compatibility, composition, and surjectivity are checked stagewise and then assembled by inverse-limit extensionality.
□