FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.Kernel
This module develops the augmentation side of the construction. It identifies the relevant kernels and ideals and compares the finite-stage and completed forms.
import
def groupAlgebraMapDomainKernelAugmentationIdeal (f : A →* B) :
Ideal (MonoidAlgebra R A) :=
Ideal.span (Set.range fun k : f.ker => MonoidAlgebra.of R A k.1 - 1)The ideal in \(R[A]\) generated by \([k]-1\) for \(k \in \ker f\).
theorem groupAlgebraMapDomainKernelAugmentationGenerator_mem
(f : A →* B) (k : f.ker) :
MonoidAlgebra.of R A k.1 - 1 ∈
groupAlgebraMapDomainKernelAugmentationIdeal (R := R) fA kernel augmentation generator lies in the group-algebra kernel-augmentation ideal.
Show proof
Ideal.subset_span (Set.mem_range_self k)Proof. Use the finite-stage augmentation maps of \(\mathbb{Z}_C\llbracket H\rrbracket\). The completed augmentation ideal is detected by all finite-stage projections: membership is equivalent to vanishing under every finite augmentation, and the standard generators \([h]-1\) project to the corresponding finite-stage generators. Closure, range, and inverse-limit statements follow from compatibility of finite-stage augmentation ideals under transition maps and from checking the formulas on group-like generators.
□theorem groupAlgebra_mapDomainRingHom_smul
(f : A →* B) (r : R) (x : MonoidAlgebra R A) :
MonoidAlgebra.mapDomainRingHom R f (r • x) =
r • MonoidAlgebra.mapDomainRingHom R f xThe domain group-algebra map is compatible with scalar multiplication.
Show proof
by
rw [Algebra.smul_def, Algebra.smul_def, RingHom.map_mul]
simp only [MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self, RingHom.coe_id, Function.comp_apply, id_eq,
MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single, map_one]Proof. Use the finite-stage augmentation maps of \(\mathbb{Z}_C\llbracket H\rrbracket\). The completed augmentation ideal is detected by all finite-stage projections: membership is equivalent to vanishing under every finite augmentation, and the standard generators \([h]-1\) project to the corresponding finite-stage generators. Closure, range, and inverse-limit statements follow from compatibility of finite-stage augmentation ideals under transition maps and from checking the formulas on group-like generators.
□def groupAlgebraMapDomainTargetSection
(f : A →* B) (hf : Function.Surjective f) :
MonoidAlgebra R B →ₗ[R] MonoidAlgebra R A :=
Finsupp.linearCombination R
(fun b : B => MonoidAlgebra.of R A (Function.surjInv hf b))
@[simp]A chosen linear section of the group-algebra map induced by a surjective group homomorphism.
theorem groupAlgebraMapDomainTargetSection_of
(f : A →* B) (hf : Function.Surjective f) (b : B) :
groupAlgebraMapDomainTargetSection (R := R) f hf
(MonoidAlgebra.of R B b) =
MonoidAlgebra.of R A (Function.surjInv hf b)The domain-target section sends a group element to the corresponding group-algebra basis element.
Show proof
by
change
Finsupp.linearCombination R
(fun b : B => MonoidAlgebra.of R A (Function.surjInv hf b))
(Finsupp.single b (1 : R)) =
MonoidAlgebra.of R A (Function.surjInv hf b)
rw [Finsupp.linearCombination_single, one_smul]Proof. Use the finite-stage augmentation maps of \(\mathbb{Z}_C\llbracket H\rrbracket\). The completed augmentation ideal is detected by all finite-stage projections: membership is equivalent to vanishing under every finite augmentation, and the standard generators \([h]-1\) project to the corresponding finite-stage generators. Closure, range, and inverse-limit statements follow from compatibility of finite-stage augmentation ideals under transition maps and from checking the formulas on group-like generators.
□theorem groupAlgebraMapDomain_targetSection
(f : A →* B) (hf : Function.Surjective f) (y : MonoidAlgebra R B) :
MonoidAlgebra.mapDomainRingHom R f
(groupAlgebraMapDomainTargetSection (R := R) f hf y) = yThe chosen group-algebra section is a right inverse to the map induced by \(f\).
Show proof
by
classical
refine MonoidAlgebra.induction_on
(p := fun y : MonoidAlgebra R B =>
MonoidAlgebra.mapDomainRingHom R f
(groupAlgebraMapDomainTargetSection (R := R) f hf y) = y)
y ?single ?add ?smul
· intro b
rw [groupAlgebraMapDomainTargetSection_of]
rw [show MonoidAlgebra.mapDomainRingHom R f
(MonoidAlgebra.of R A (Function.surjInv hf b)) =
MonoidAlgebra.of R B (f (Function.surjInv hf b)) by
simp only [MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk, OneHom.coe_mk,
MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]]
exact congrArg (MonoidAlgebra.of R B) (Function.surjInv_eq hf b)
· intro x y hx hy
rw [map_add, map_add, hx, hy]
· intro a y hy
rw [show groupAlgebraMapDomainTargetSection (R := R) f hf (a • y) =
a • groupAlgebraMapDomainTargetSection (R := R) f hf y by
exact (groupAlgebraMapDomainTargetSection (R := R) f hf).map_smul a y]
rw [groupAlgebra_mapDomainRingHom_smul, hy]Proof. Use the finite-stage augmentation maps of \(\mathbb{Z}_C\llbracket H\rrbracket\). The completed augmentation ideal is detected by all finite-stage projections: membership is equivalent to vanishing under every finite augmentation, and the standard generators \([h]-1\) project to the corresponding finite-stage generators. Closure, range, and inverse-limit statements follow from compatibility of finite-stage augmentation ideals under transition maps and from checking the formulas on group-like generators.
□theorem groupAlgebraMapDomain_sourceBasis_sub_targetSection_mem_kernelAugmentationIdeal
(f : A →* B) (hf : Function.Surjective f) (a : A) :
MonoidAlgebra.of R A a -
groupAlgebraMapDomainTargetSection (R := R) f hf
(MonoidAlgebra.mapDomainRingHom R f (MonoidAlgebra.of R A a)) ∈
groupAlgebraMapDomainKernelAugmentationIdeal (R := R) fA source basis element minus the chosen lift of its target image lies in the kernel augmentation ideal.
Show proof
by
let t : B := f a
let lift : A := Function.surjInv hf t
let q : f.ker :=
⟨lift⁻¹ * a, by
change f (lift⁻¹ * a) = 1
rw [map_mul, map_inv]
have hlift : f lift = t := Function.surjInv_eq hf t
rw [hlift]
simp only [inv_mul_cancel, t]⟩
have hsection :
groupAlgebraMapDomainTargetSection (R := R) f hf
(MonoidAlgebra.mapDomainRingHom R f (MonoidAlgebra.of R A a)) =
MonoidAlgebra.of R A lift := by
rw [show MonoidAlgebra.mapDomainRingHom R f (MonoidAlgebra.of R A a) =
MonoidAlgebra.of R B (f a) by
simp only [MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk, OneHom.coe_mk,
MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]]
simpa [t, lift, MonoidAlgebra.of, MonoidAlgebra.single] using
groupAlgebraMapDomainTargetSection_of (R := R) f hf (f a)
rw [hsection]
have hmul :
MonoidAlgebra.of R A lift *
(MonoidAlgebra.of R A q.1 - 1) =
MonoidAlgebra.of R A a - MonoidAlgebra.of R A lift := by
simp only [MonoidAlgebra.of_apply]
rw [mul_sub, MonoidAlgebra.single_mul_single, mul_one]
simp only [mul_inv_cancel_left, mul_one, q]
rw [← hmul]
exact
(groupAlgebraMapDomainKernelAugmentationIdeal (R := R) f).mul_mem_left _
(groupAlgebraMapDomainKernelAugmentationGenerator_mem (R := R) f q)Proof. Use the finite-stage augmentation maps of \(\mathbb{Z}_C\llbracket H\rrbracket\). The completed augmentation ideal is detected by all finite-stage projections: membership is equivalent to vanishing under every finite augmentation, and the standard generators \([h]-1\) project to the corresponding finite-stage generators. Closure, range, and inverse-limit statements follow from compatibility of finite-stage augmentation ideals under transition maps and from checking the formulas on group-like generators.
□theorem groupAlgebraMapDomain_sub_targetSection_map_mem_kernelAugmentationIdeal
(f : A →* B) (hf : Function.Surjective f) (x : MonoidAlgebra R A) :
x - groupAlgebraMapDomainTargetSection (R := R) f hf
(MonoidAlgebra.mapDomainRingHom R f x) ∈
groupAlgebraMapDomainKernelAugmentationIdeal (R := R) fEvery group-algebra element differs from the chosen lift of its target image by an element of the kernel augmentation ideal.
Show proof
by
classical
refine MonoidAlgebra.induction_on
(p := fun x : MonoidAlgebra R A =>
x - groupAlgebraMapDomainTargetSection (R := R) f hf
(MonoidAlgebra.mapDomainRingHom R f x) ∈
groupAlgebraMapDomainKernelAugmentationIdeal (R := R) f)
x ?single ?add ?smul
· intro a
exact
groupAlgebraMapDomain_sourceBasis_sub_targetSection_mem_kernelAugmentationIdeal
(R := R) f hf a
· intro x y hx hy
have hcalc :
x + y - groupAlgebraMapDomainTargetSection (R := R) f hf
(MonoidAlgebra.mapDomainRingHom R f (x + y)) =
(x - groupAlgebraMapDomainTargetSection (R := R) f hf
(MonoidAlgebra.mapDomainRingHom R f x)) +
(y - groupAlgebraMapDomainTargetSection (R := R) f hf
(MonoidAlgebra.mapDomainRingHom R f y)) := by
rw [map_add, map_add]
abel
rw [hcalc]
exact (groupAlgebraMapDomainKernelAugmentationIdeal (R := R) f).add_mem hx hy
· intro r x hx
have hcalc :
r • x - groupAlgebraMapDomainTargetSection (R := R) f hf
(MonoidAlgebra.mapDomainRingHom R f (r • x)) =
r • (x - groupAlgebraMapDomainTargetSection (R := R) f hf
(MonoidAlgebra.mapDomainRingHom R f x)) := by
rw [groupAlgebra_mapDomainRingHom_smul, map_smul, smul_sub]
rw [hcalc]
rw [Algebra.smul_def]
exact (groupAlgebraMapDomainKernelAugmentationIdeal (R := R) f).mul_mem_left _ hxProof. Use the finite-stage augmentation maps of \(\mathbb{Z}_C\llbracket H\rrbracket\). The completed augmentation ideal is detected by all finite-stage projections: membership is equivalent to vanishing under every finite augmentation, and the standard generators \([h]-1\) project to the corresponding finite-stage generators. Closure, range, and inverse-limit statements follow from compatibility of finite-stage augmentation ideals under transition maps and from checking the formulas on group-like generators.
□theorem groupAlgebraMapDomainRingHom_ker_eq_kernelAugmentationIdeal_of_surjective
(f : A →* B) (hf : Function.Surjective f) :
RingHom.ker (MonoidAlgebra.mapDomainRingHom R f) =
groupAlgebraMapDomainKernelAugmentationIdeal (R := R) fFor a surjective group map, the kernel of R[A] \(\to\) R[B] is generated by the augmentation generators attached to kernel f.
Show proof
by
apply le_antisymm
· intro x hx
have hxmap : MonoidAlgebra.mapDomainRingHom R f x = 0 :=
(RingHom.mem_ker).1 hx
have hdiff :=
groupAlgebraMapDomain_sub_targetSection_map_mem_kernelAugmentationIdeal
(R := R) f hf x
rw [hxmap, map_zero, sub_zero] at hdiff
exact hdiff
· refine Ideal.span_le.2 ?_
rintro _ ⟨k, rfl⟩
change MonoidAlgebra.mapDomainRingHom R f
(MonoidAlgebra.of R A k.1 - 1) = 0
rw [map_sub, map_one]
have hk : f k.1 = 1 := MonoidHom.mem_ker.mp k.2
simp only [MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk, OneHom.coe_mk,
MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single, hk, MonoidAlgebra.one_def, sub_self]Proof. Use the finite-stage augmentation maps of \(\mathbb{Z}_C\llbracket H\rrbracket\). The completed augmentation ideal is detected by all finite-stage projections: membership is equivalent to vanishing under every finite augmentation, and the standard generators \([h]-1\) project to the corresponding finite-stage generators. Closure, range, and inverse-limit statements follow from compatibility of finite-stage augmentation ideals under transition maps and from checking the formulas on group-like generators.
□def zcCompletedGroupAlgebraKernelAugmentationIdealMul
(psi : ContinuousMonoidHom G H) :
Ideal (ZCCompletedGroupAlgebra C G) :=
Ideal.span
(Set.range fun n : ProfiniteKernelSubgroup psi =>
zcGroupLike C G n.1 - 1)The algebraic ideal in \(\mathbb{Z}_C\llbracket G\rrbracket\) generated by completed augmentation generators coming from the kernel of \(\psi\).
theorem zcGroupLike_sub_one_mem_kernelAugmentationIdealMul
(psi : ContinuousMonoidHom G H) (n : ProfiniteKernelSubgroup psi) :
zcGroupLike C G n.1 - 1 ∈
zcCompletedGroupAlgebraKernelAugmentationIdealMul C psiA kernel augmentation generator lies in the algebraic kernel-augmentation ideal.
Show proof
Ideal.subset_span (Set.mem_range_self n)Proof. Use the finite-stage augmentation maps of \(\mathbb{Z}_C\llbracket H\rrbracket\). The completed augmentation ideal is detected by all finite-stage projections: membership is equivalent to vanishing under every finite augmentation, and the standard generators \([h]-1\) project to the corresponding finite-stage generators. Closure, range, and inverse-limit statements follow from compatibility of finite-stage augmentation ideals under transition maps and from checking the formulas on group-like generators.
□theorem zcCompletedGroupAlgebraKernelAugmentationIdealMul_le_standardAugmentationIdeal
(psi : ContinuousMonoidHom G H) :
zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi ≤
zcCompletedGroupAlgebraStandardAugmentationIdeal C GThe kernel-augmentation ideal is contained in the standard source augmentation ideal.
Show proof
by
refine Ideal.span_le.2 ?_
rintro _ ⟨n, rfl⟩
exact zcGroupLike_sub_one_mem_standardAugmentationIdeal C G n.1Proof. Use the finite-stage augmentation maps of \(\mathbb{Z}_C\llbracket H\rrbracket\). The completed augmentation ideal is detected by all finite-stage projections: membership is equivalent to vanishing under every finite augmentation, and the standard generators \([h]-1\) project to the corresponding finite-stage generators. Closure, range, and inverse-limit statements follow from compatibility of finite-stage augmentation ideals under transition maps and from checking the formulas on group-like generators.
□theorem zcGroupLike_sub_mem_kernelAugmentationIdealMul_of_map_eq
(psi : ContinuousMonoidHom G H) {g₁ g₂ : G} (h : psi g₁ = psi g₂) :
zcGroupLike C G g₁ - zcGroupLike C G g₂ ∈
zcCompletedGroupAlgebraKernelAugmentationIdealMul C psiSource group-like elements with the same target differ by an element of the algebraic kernel-augmentation ideal.
Show proof
by
let n : ProfiniteKernelSubgroup psi :=
⟨g₂⁻¹ * g₁, by
change psi (g₂⁻¹ * g₁) = 1
rw [map_mul, map_inv, h]
simp only [inv_mul_cancel]⟩
have hgen :
zcGroupLike C G n.1 - 1 ∈
zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi :=
zcGroupLike_sub_one_mem_kernelAugmentationIdealMul C psi n
have hmul :
zcGroupLike C G g₂ * (zcGroupLike C G n.1 - 1) ∈
zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi :=
(zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi).mul_mem_left
(zcGroupLike C G g₂) hgen
have hidentity :
zcGroupLike C G g₂ * (zcGroupLike C G n.1 - 1) =
zcGroupLike C G g₁ - zcGroupLike C G g₂ := by
rw [mul_sub, ← map_mul, mul_one]
simp only [mul_inv_cancel_left, n]
simpa [hidentity] using hmulProof. Use the finite-stage augmentation maps of \(\mathbb{Z}_C\llbracket H\rrbracket\). The completed augmentation ideal is detected by all finite-stage projections: membership is equivalent to vanishing under every finite augmentation, and the standard generators \([h]-1\) project to the corresponding finite-stage generators. Closure, range, and inverse-limit statements follow from compatibility of finite-stage augmentation ideals under transition maps and from checking the formulas on group-like generators.
□theorem zcCompletedGroupAlgebraKernelAugmentationIdealMul_le_ker_map
(psi : ContinuousMonoidHom G H) :
zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi ≤
RingHom.ker (zcCompletedGroupAlgebraMap C hC psi)The algebraic kernel-augmentation ideal maps to zero under the completed target map.
Show proof
by
refine Ideal.span_le.2 ?_
rintro x ⟨n, rfl⟩
change zcCompletedGroupAlgebraMap C hC psi (zcGroupLike C G n.1 - 1) = 0
rw [map_sub, map_one, zcCompletedGroupAlgebraMap_groupLike]
have hn : psi n.1 = 1 := by
exact MonoidHom.mem_ker.mp
(show n.1 ∈ psi.toMonoidHom.ker from n.2)
rw [hn]
simp only [map_one, sub_self]Proof. Use the finite-stage augmentation maps of \(\mathbb{Z}_C\llbracket H\rrbracket\). The completed augmentation ideal is detected by all finite-stage projections: membership is equivalent to vanishing under every finite augmentation, and the standard generators \([h]-1\) project to the corresponding finite-stage generators. Closure, range, and inverse-limit statements follow from compatibility of finite-stage augmentation ideals under transition maps and from checking the formulas on group-like generators.
□theorem isClosed_zcCompletedGroupAlgebraMap_ker
[Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)]
(psi : ContinuousMonoidHom G H) :
IsClosed
((RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) :
Ideal (ZCCompletedGroupAlgebra C G)) : Set (ZCCompletedGroupAlgebra C G))The kernel of the completed target map is closed in the inverse-limit topology.
Show proof
by
change IsClosed ((zcCompletedGroupAlgebraMap C hC psi) ⁻¹'
({0} : Set (ZCCompletedGroupAlgebra C H)))
exact isClosed_singleton.preimage
(continuous_zcCompletedGroupAlgebraMap C hC psi)Proof. Use the finite-stage augmentation maps of \(\mathbb{Z}_C\llbracket H\rrbracket\). The completed augmentation ideal is detected by all finite-stage projections: membership is equivalent to vanishing under every finite augmentation, and the standard generators \([h]-1\) project to the corresponding finite-stage generators. Closure, range, and inverse-limit statements follow from compatibility of finite-stage augmentation ideals under transition maps and from checking the formulas on group-like generators.
□theorem closure_zcCompletedGroupAlgebraKernelAugmentationIdealMul_le_ker_map
[Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)]
(psi : ContinuousMonoidHom G H) :
closure
((zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi :
Ideal (ZCCompletedGroupAlgebra C G)) : Set (ZCCompletedGroupAlgebra C G)) ≤
((RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) :
Ideal (ZCCompletedGroupAlgebra C G)) : Set (ZCCompletedGroupAlgebra C G))The closure of the algebraic kernel-augmentation ideal is contained in the completed kernel.
Show proof
by
exact closure_minimal
(by
intro x hx
exact zcCompletedGroupAlgebraKernelAugmentationIdealMul_le_ker_map
C hC psi hx)
(isClosed_zcCompletedGroupAlgebraMap_ker C hC psi)Proof. Use the finite-stage augmentation maps of \(\mathbb{Z}_C\llbracket H\rrbracket\). The completed augmentation ideal is detected by all finite-stage projections: membership is equivalent to vanishing under every finite augmentation, and the standard generators \([h]-1\) project to the corresponding finite-stage generators. Closure, range, and inverse-limit statements follow from compatibility of finite-stage augmentation ideals under transition maps and from checking the formulas on group-like generators.
□theorem zcCompletedGAMapStageRelationAugmentationGenerator_mem_proj_kernelAugmentationIdealMul
(psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
(i : ZCCompletedGroupAlgebraIndex C H)
(q :
(completedGroupAlgebraComapQuotientMapInClass
(G := G) (H := H) C hC psi i.2).ker) :
∃ y ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi,
zcCompletedGroupAlgebraProjection C G
(i.1, completedGroupAlgebraComapIndexInClass
(G := G) (H := H) C hC psi i.2) y =
zcCompletedGroupAlgebraMapStageRelationAugmentationGenerator C hC psi i qA finite target-stage relation-augmentation generator is the projection of an algebraic kernel-augmentation generator in \(\mathbb{Z}_C\llbracket G\rrbracket\).
Show proof
by
let U : Subgroup H := (((OrderDual.ofDual i.2).1 : OpenNormalSubgroup H) : Subgroup H)
let V : Subgroup G :=
((((OrderDual.ofDual
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi i.2)).1 :
OpenNormalSubgroup G) : Subgroup G))
rcases QuotientGroup.mk'_surjective V q.1 with ⟨g, hg⟩
have hmap1 :
completedGroupAlgebraComapQuotientMapInClass
(G := G) (H := H) C hC psi i.2 q.1 = 1 := by
exact MonoidHom.mem_ker.mp
(show q.1 ∈ (completedGroupAlgebraComapQuotientMapInClass
(G := G) (H := H) C hC psi i.2).ker from q.2)
have hpsi_g_U : psi g ∈ U := by
rw [← hg, completedGroupAlgebraComapQuotientMapInClass_mk] at hmap1
exact (QuotientGroup.eq_one_iff (N := U) (psi g)).1 hmap1
rcases hpsi (psi g)⁻¹ with ⟨t, ht⟩
have htV : t ∈ V := by
change psi t ∈ U
rw [ht]
exact U.inv_mem hpsi_g_U
let n : ProfiniteKernelSubgroup psi := ⟨g * t, by
change psi (g * t) = 1
rw [map_mul, ht]
simp only [mul_inv_cancel]⟩
refine ⟨zcGroupLike C G n.1 - 1,
zcGroupLike_sub_one_mem_kernelAugmentationIdealMul C psi n, ?_⟩
have hqeq :
(QuotientGroup.mk' V (g * t) :
CompletedGroupAlgebraQuotientInClass G C
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi i.2)) =
q.1 := by
rw [← hg]
apply QuotientGroup.eq.2
simpa [V, mul_assoc] using V.inv_mem htV
change
MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass G C
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi i.2))
(QuotientGroup.mk' V (g * t)) - 1 =
MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass G C
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi i.2)) q.1 - 1
rw [hqeq]Proof. Use the finite-stage augmentation maps of \(\mathbb{Z}_C\llbracket H\rrbracket\). The completed augmentation ideal is detected by all finite-stage projections: membership is equivalent to vanishing under every finite augmentation, and the standard generators \([h]-1\) project to the corresponding finite-stage generators. Closure, range, and inverse-limit statements follow from compatibility of finite-stage augmentation ideals under transition maps and from checking the formulas on group-like generators.
□theorem zcCompletedGAMapStageRelationAugmentationIdeal_mem_proj_kernelAugmentationIdealMul
(psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
(i : ZCCompletedGroupAlgebraIndex C H)
(x : zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC psi i) :
∃ y ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi,
zcCompletedGroupAlgebraProjection C G
(i.1, completedGroupAlgebraComapIndexInClass
(G := G) (H := H) C hC psi i.2) y =
(x :
ZCCompletedGroupAlgebraStage C G
(i.1, completedGroupAlgebraComapIndexInClass
(G := G) (H := H) C hC psi i.2))Every element of a finite target-stage relation-augmentation ideal is the projection of an element of the algebraic completed kernel-augmentation ideal.
Show proof
by
let sourceIndex : ZCCompletedGroupAlgebraIndex C G :=
(i.1, completedGroupAlgebraComapIndexInClass
(G := G) (H := H) C hC psi i.2)
let R := ZCCompletedGroupAlgebraStage C G sourceIndex
let I := zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC psi i
let P : R → Prop := fun z =>
∃ y ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi,
zcCompletedGroupAlgebraProjection C G sourceIndex y = z
have hxSpan :
(x : R) ∈ Submodule.span R
(Set.range (zcCompletedGroupAlgebraMapStageRelationAugmentationGenerator C hC psi i)) := by
change (x : R) ∈ zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC psi i
exact x.2
refine Submodule.span_induction (p := fun z _ => P z) ?_ ?_ ?_ ?_ hxSpan
· rintro _ ⟨q, rfl⟩
exact
zcCompletedGAMapStageRelationAugmentationGenerator_mem_proj_kernelAugmentationIdealMul
C hC psi hpsi i q
· exact ⟨0, (zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi).zero_mem, by simp only [zcCompletedGroupAlgebraProjection_zero]⟩
· intro x y _ _ hx hy
rcases hx with ⟨x', hx'mem, hx'proj⟩
rcases hy with ⟨y', hy'mem, hy'proj⟩
refine ⟨x' + y',
(zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi).add_mem hx'mem hy'mem, ?_⟩
simp only [zcCompletedGroupAlgebraProjection_add, hx'proj, hy'proj]
· intro a x _ hx
rcases hx with ⟨x', hx'mem, hx'proj⟩
rcases zcCompletedGroupAlgebraProjection_surjective C G sourceIndex a with ⟨a', ha'⟩
refine ⟨a' * x',
(zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi).mul_mem_left a' hx'mem, ?_⟩
rw [zcCompletedGroupAlgebraProjection_mul, ha', hx'proj]
rflProof. Use the finite-stage augmentation maps of \(\mathbb{Z}_C\llbracket H\rrbracket\). The completed augmentation ideal is detected by all finite-stage projections: membership is equivalent to vanishing under every finite augmentation, and the standard generators \([h]-1\) project to the corresponding finite-stage generators. Closure, range, and inverse-limit statements follow from compatibility of finite-stage augmentation ideals under transition maps and from checking the formulas on group-like generators.
□theorem zcCompletedGAMapDomainKernelAugmentationIdeal_mem_proj_kernelAugmentationIdealMul
(psi : ContinuousMonoidHom G H)
(i : ZCCompletedGroupAlgebraIndex C G)
{Q : Type u} [Group Q]
(qmap : CompletedGroupAlgebraQuotientInClass G C i.2 →* Q)
(hkerLift :
∀ q : qmap.ker,
∃ n : ProfiniteKernelSubgroup psi,
QuotientGroup.mk'
((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup G) : Subgroup G)) n.1 =
q.1)
(x : ZCCompletedGroupAlgebraStage C G i)
(hx :
x ∈ groupAlgebraMapDomainKernelAugmentationIdeal
(R := ModNCompletedCoeff i.1.modulus) qmap) :
∃ y ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi,
zcCompletedGroupAlgebraProjection C G i y =
xA finite source-stage ideal generated by kernel classes of a quotient map is the projection of the algebraic completed kernel-augmentation ideal, provided every finite kernel class has a representative in the actual kernel of \(\psi\).
Show proof
by
let R := ZCCompletedGroupAlgebraStage C G i
let I :=
groupAlgebraMapDomainKernelAugmentationIdeal
(R := ModNCompletedCoeff i.1.modulus) qmap
let P : R → Prop := fun z =>
∃ y ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi,
zcCompletedGroupAlgebraProjection C G i y = z
have hxSpan :
x ∈ Submodule.span R
(Set.range fun q : qmap.ker =>
MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass G C i.2) q.1 - 1) := by
change x ∈ I
exact hx
refine Submodule.span_induction (p := fun z _ => P z) ?_ ?_ ?_ ?_ hxSpan
· rintro _ ⟨q, rfl⟩
rcases hkerLift q with ⟨n, hn⟩
refine ⟨zcGroupLike C G n.1 - 1,
zcGroupLike_sub_one_mem_kernelAugmentationIdealMul C psi n, ?_⟩
change
MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass G C i.2)
(QuotientGroup.mk'
((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup G) : Subgroup G)) n.1) - 1 =
MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass G C i.2) q.1 - 1
rw [hn]
· exact ⟨0, (zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi).zero_mem, by simp only [zcCompletedGroupAlgebraProjection_zero]⟩
· intro x y _ _ hx hy
rcases hx with ⟨x', hx'mem, hx'proj⟩
rcases hy with ⟨y', hy'mem, hy'proj⟩
refine ⟨x' + y',
(zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi).add_mem hx'mem hy'mem, ?_⟩
simp only [zcCompletedGroupAlgebraProjection_add, hx'proj, hy'proj]
· intro a x _ hx
rcases hx with ⟨x', hx'mem, hx'proj⟩
rcases zcCompletedGroupAlgebraProjection_surjective C G i a with ⟨a', ha'⟩
refine ⟨a' * x',
(zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi).mul_mem_left a' hx'mem, ?_⟩
rw [zcCompletedGroupAlgebraProjection_mul, ha', hx'proj]
rflProof. Use the finite-stage augmentation maps of \(\mathbb{Z}_C\llbracket H\rrbracket\). The completed augmentation ideal is detected by all finite-stage projections: membership is equivalent to vanishing under every finite augmentation, and the standard generators \([h]-1\) project to the corresponding finite-stage generators. Closure, range, and inverse-limit statements follow from compatibility of finite-stage augmentation ideals under transition maps and from checking the formulas on group-like generators.
□def zcCompletedGroupAlgebraOpenImageIndexInClass
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
(hfopen : IsOpenMap psi)
(i : ZCCompletedGroupAlgebraIndex C G) :
CompletedGroupAlgebraIndexInClass H C :=
OrderDual.toDual
(OpenNormalSubgroupInClass.mapOpenNormal_of_formation
(C := C) (G := G) hForm psi hfopen hpsi (OrderDual.ofDual i.2))The target quotient obtained by pushing a source quotient forward along an open surjective map.
def zcCompletedGroupAlgebraOpenImageTargetIndex
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
(hfopen : IsOpenMap psi)
(i : ZCCompletedGroupAlgebraIndex C G) :
ZCCompletedGroupAlgebraIndex C H :=
(i.1, zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)The two-parameter target stage whose group quotient is the open image of a source stage.
theorem zcCompletedGroupAlgebraOpenImage_comapIndex_le
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
(hfopen : IsOpenMap psi)
(i : ZCCompletedGroupAlgebraIndex C G) :
completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi
(zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i) ≤
i.2The comap of the open image quotient is coarser than the original source quotient.
Show proof
by
let U : OpenNormalSubgroupInClass C G := OrderDual.ofDual i.2
let W : OpenNormalSubgroupInClass C H :=
OpenNormalSubgroupInClass.mapOpenNormal_of_formation
(C := C) (G := G) hForm psi hfopen hpsi U
intro g hg
change psi g ∈ ((W.1 : OpenNormalSubgroup H) : Subgroup H)
change psi g ∈
((OpenNormalSubgroup.map psi hfopen hpsi (U.1 : OpenNormalSubgroup G) :
OpenNormalSubgroup H) : Subgroup H)
exact ⟨g, hg, rfl⟩Proof. Use that the target homomorphism is open and surjective. The image of an open normal source stage is an open normal subgroup of the target, giving a finite target quotient and an induced quotient map from the source stage. The formulas for representatives, kernel lifts, surjectivity, and refinement compatibility are checked on cosets, then used as the finite-stage data for the completed group-algebra map.
□def zcCompletedGroupAlgebraOpenImageQuotientMap
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
(hfopen : IsOpenMap psi)
(i : ZCCompletedGroupAlgebraIndex C G) :
CompletedGroupAlgebraQuotientInClass G C i.2 →*
CompletedGroupAlgebraQuotientInClass H C
(zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i) :=
(completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hC psi
(zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)).comp
(OpenNormalSubgroupInClass.map
(C := C) (G := G)
(U := OrderDual.ofDual
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi
(zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)))
(V := OrderDual.ofDual i.2)
(zcCompletedGroupAlgebraOpenImage_comapIndex_le C hC hForm psi hpsi hfopen i))
@[simp 900]The source-stage quotient map \(G/U \to H/\psi(U)\) attached to an open surjective map.
theorem zcCompletedGroupAlgebraOpenImageQuotientMap_mk
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
(hfopen : IsOpenMap psi)
(i : ZCCompletedGroupAlgebraIndex C G) (g : G) :
zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i
(QuotientGroup.mk'
((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup G) : Subgroup G)) g) =
QuotientGroup.mk'
((((OrderDual.ofDual
(zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)).1 :
OpenNormalSubgroup H) : Subgroup H)) (psi g)The open-image quotient map sends a group-like class to its corresponding finite-stage quotient representative.
Show proof
by
rw [zcCompletedGroupAlgebraOpenImageQuotientMap]
change completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hC psi
(zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)
(QuotientGroup.mk'
((((OrderDual.ofDual
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi
(zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i))).1 :
OpenNormalSubgroup G) : Subgroup G)) g) =
QuotientGroup.mk'
((((OrderDual.ofDual
(zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)).1 :
OpenNormalSubgroup H) : Subgroup H)) (psi g)
rw [completedGroupAlgebraComapQuotientMapInClass_mk]Proof. Use that the target homomorphism is open and surjective. The image of an open normal source stage is an open normal subgroup of the target, giving a finite target quotient and an induced quotient map from the source stage. The formulas for representatives, kernel lifts, surjectivity, and refinement compatibility are checked on cosets, then used as the finite-stage data for the completed group-algebra map.
□theorem zcCompletedGroupAlgebraOpenImageQuotientMap_surjective
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
(hfopen : IsOpenMap psi)
(i : ZCCompletedGroupAlgebraIndex C G) :
Function.Surjective
(zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i)The source-stage quotient map to the open image quotient is surjective.
Show proof
by
intro q
rcases QuotientGroup.mk'_surjective
((((OrderDual.ofDual
(zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)).1 :
OpenNormalSubgroup H) : Subgroup H)) q with
⟨h, rfl⟩
rcases hpsi h with ⟨g, rfl⟩
refine ⟨QuotientGroup.mk'
((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup G) : Subgroup G)) g, ?_⟩
rw [zcCompletedGroupAlgebraOpenImageQuotientMap_mk]Proof. Use that the target homomorphism is open and surjective. The image of an open normal source stage is an open normal subgroup of the target, giving a finite target quotient and an induced quotient map from the source stage. The formulas for representatives, kernel lifts, surjectivity, and refinement compatibility are checked on cosets, then used as the finite-stage data for the completed group-algebra map.
□theorem zcCompletedGroupAlgebraOpenImageQuotientMap_kernel_lift
(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,
∃ n : ProfiniteKernelSubgroup psi,
QuotientGroup.mk'
((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup G) : Subgroup G)) n.1 =
q.1Kernel classes of the source-stage quotient map lift to actual elements in the kernel of \(\psi\).
Show proof
by
intro q
let U : OpenNormalSubgroupInClass C G := OrderDual.ofDual i.2
let W : OpenNormalSubgroupInClass C H :=
OpenNormalSubgroupInClass.mapOpenNormal_of_formation
(C := C) (G := G) hForm psi hfopen hpsi U
rcases QuotientGroup.mk'_surjective ((U.1 : OpenNormalSubgroup G) : Subgroup G) q.1 with
⟨g, hg⟩
have hmap1 :
zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i q.1 = 1 :=
MonoidHom.mem_ker.mp q.2
have hpsi_g_W : psi g ∈ ((W.1 : OpenNormalSubgroup H) : Subgroup H) := by
rw [← hg] at hmap1
change
QuotientGroup.mk' ((W.1 : OpenNormalSubgroup H) : Subgroup H) (psi g) = 1 at hmap1
exact (QuotientGroup.eq_one_iff (N := ((W.1 : OpenNormalSubgroup H) : Subgroup H))
(psi g)).1 hmap1
rcases hpsi_g_W with ⟨u, hu, hpsi_u⟩
change psi u = psi g at hpsi_u
let n : ProfiniteKernelSubgroup psi := ⟨g * u⁻¹, by
change psi (g * u⁻¹) = 1
rw [map_mul, map_inv, hpsi_u]
simp only [mul_inv_cancel]⟩
refine ⟨n, ?_⟩
rw [← hg]
apply QuotientGroup.eq.2
simpa [n, mul_assoc] using (U.1 : OpenNormalSubgroup G).inv_mem huProof. Use that the target homomorphism is open and surjective. The image of an open normal source stage is an open normal subgroup of the target, giving a finite target quotient and an induced quotient map from the source stage. The formulas for representatives, kernel lifts, surjectivity, and refinement compatibility are checked on cosets, then used as the finite-stage data for the completed group-algebra map.
□theorem zcCompletedGroupAlgebraOpenImageQuotientMap_stage_eq
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
(hfopen : IsOpenMap psi)
(i : ZCCompletedGroupAlgebraIndex C G) :
MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff i.1.modulus)
(zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i) =
(zcCompletedGroupAlgebraMapStage C hC psi
(zcCompletedGroupAlgebraOpenImageTargetIndex C hForm psi hpsi hfopen i)).comp
(zcCompletedGroupAlgebraTransition C G
(show
(i.1,
completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi
(zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)) ≤ i from
⟨le_rfl,
zcCompletedGroupAlgebraOpenImage_comapIndex_le C hC hForm psi hpsi hfopen i⟩))The source-stage quotient map is the finite-stage map obtained by first transitioning to the comap of the open image and then applying the completed target-map stage.
Show proof
by
rw [zcCompletedGroupAlgebraOpenImageQuotientMap, MonoidAlgebra.mapDomainRingHom_comp]
simp only [zcCompletedGroupAlgebraOpenImageTargetIndex, zcCompletedGroupAlgebraMapStage,
zcCompletedGroupAlgebraTransition, modNCompletedGroupAlgebraStageCoeffMapInClass_rfl,
modNCompletedGroupAlgebraTransitionInClass, RingHomCompTriple.comp_eq]Proof. Use that the target homomorphism is open and surjective. The image of an open normal source stage is an open normal subgroup of the target, giving a finite target quotient and an induced quotient map from the source stage. The formulas for representatives, kernel lifts, surjectivity, and refinement compatibility are checked on cosets, then used as the finite-stage data for the completed group-algebra map.
□theorem zcCompletedGAProj_mem_openImage_kernelAugmentationIdeal_of_mem_ker
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
(hfopen : IsOpenMap psi)
(i : ZCCompletedGroupAlgebraIndex C G)
(x : ZCCompletedGroupAlgebra C G)
(hx : x ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi)) :
zcCompletedGroupAlgebraProjection C G i x ∈
groupAlgebraMapDomainKernelAugmentationIdeal
(R := ModNCompletedCoeff i.1.modulus)
(zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i)A completed-kernel element projects at any source stage into the finite kernel-augmentation ideal for the source-stage quotient map to the open image.
Show proof
by
have hmapzero : zcCompletedGroupAlgebraMap C hC psi x = 0 :=
(RingHom.mem_ker).1 hx
have htargetzero :
zcCompletedGroupAlgebraProjection C H
(zcCompletedGroupAlgebraOpenImageTargetIndex C hForm psi hpsi hfopen i)
(zcCompletedGroupAlgebraMap C hC psi x) = 0 := by
rw [hmapzero]
simp only [zcCompletedGroupAlgebraProjection_zero]
have hsource :
(i.1,
completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC psi
(zcCompletedGroupAlgebraOpenImageIndexInClass C hForm psi hpsi hfopen i)) ≤ i :=
⟨le_rfl, zcCompletedGroupAlgebraOpenImage_comapIndex_le C hC hForm psi hpsi hfopen i⟩
have hstagezero :
zcCompletedGroupAlgebraMapStage C hC psi
(zcCompletedGroupAlgebraOpenImageTargetIndex C hForm psi hpsi hfopen i)
(zcCompletedGroupAlgebraTransition C G hsource
(zcCompletedGroupAlgebraProjection C G i x)) = 0 := by
rw [zcCompletedGroupAlgebraTransition_projection]
simpa [zcCompletedGroupAlgebraOpenImageTargetIndex, zcCompletedGroupAlgebraProjection_map]
using htargetzero
have hqzero :
MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff i.1.modulus)
(zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i)
(zcCompletedGroupAlgebraProjection C G i x) = 0 := by
rw [zcCompletedGroupAlgebraOpenImageQuotientMap_stage_eq C hC hForm psi hpsi hfopen i]
exact hstagezero
have hxker :
zcCompletedGroupAlgebraProjection C G i x ∈
RingHom.ker
(MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff i.1.modulus)
(zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i)) := by
rw [RingHom.mem_ker]
exact hqzero
rwa [groupAlgebraMapDomainRingHom_ker_eq_kernelAugmentationIdeal_of_surjective
(R := ModNCompletedCoeff i.1.modulus)
(zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i)
(zcCompletedGroupAlgebraOpenImageQuotientMap_surjective C hC hForm psi hpsi hfopen i)]
at hxkerProof. Use that the target homomorphism is open and surjective. The image of an open normal source stage is an open normal subgroup of the target, giving a finite target quotient and an induced quotient map from the source stage. The formulas for representatives, kernel lifts, surjectivity, and refinement compatibility are checked on cosets, then used as the finite-stage data for the completed group-algebra map.
□theorem zcCompletedGAMap_sourceStageKernel_mem_proj_kernelAugmentationIdealMul_of_openMap_surj
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
(hfopen : IsOpenMap psi)
(i : ZCCompletedGroupAlgebraIndex C G)
(x : ZCCompletedGroupAlgebra C G)
(hx : x ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC psi)) :
∃ y ∈ zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi,
zcCompletedGroupAlgebraProjection C G i y =
zcCompletedGroupAlgebraProjection C G i xAny source-stage projection of a completed-kernel element is the projection of an element of the algebraic completed kernel-augmentation ideal.
Show proof
by
exact
zcCompletedGAMapDomainKernelAugmentationIdeal_mem_proj_kernelAugmentationIdealMul
C psi i
(zcCompletedGroupAlgebraOpenImageQuotientMap C hC hForm psi hpsi hfopen i)
(zcCompletedGroupAlgebraOpenImageQuotientMap_kernel_lift C hC hForm psi hpsi hfopen i)
(zcCompletedGroupAlgebraProjection C G i x)
(zcCompletedGAProj_mem_openImage_kernelAugmentationIdeal_of_mem_ker
C hC hForm psi hpsi hfopen i x hx)Proof. Use the finite-stage augmentation maps of \(\mathbb{Z}_C\llbracket H\rrbracket\). The completed augmentation ideal is detected by all finite-stage projections: membership is equivalent to vanishing under every finite augmentation, and the standard generators \([h]-1\) project to the corresponding finite-stage generators. Closure, range, and inverse-limit statements follow from compatibility of finite-stage augmentation ideals under transition maps and from checking the formulas on group-like generators.
□theorem closure_zcCompletedGAKernelAugmentationIdealMul_eq_ker_map_of_openMap_surj
[Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)]
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(psi : ContinuousMonoidHom G H) (hpsi : Function.Surjective psi)
(hfopen : IsOpenMap psi) :
closure
((zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi :
Ideal (ZCCompletedGroupAlgebra C G)) : Set (ZCCompletedGroupAlgebra C G)) =
((RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) :
Ideal (ZCCompletedGroupAlgebra C G)) : Set (ZCCompletedGroupAlgebra C G))For an open surjective target map, the completed kernel is the closure of the algebraic kernel-augmentation ideal generated by \([n]-1\) for \(n \in \ker \psi\).
Show proof
by
let S := zcCompletedGroupAlgebraSystem C G
let Y : Set (ZCCompletedGroupAlgebra C G) :=
(zcCompletedGroupAlgebraKernelAugmentationIdealMul C psi :
Set (ZCCompletedGroupAlgebra C G))
let K : Set (ZCCompletedGroupAlgebra C G) :=
(RingHom.ker (zcCompletedGroupAlgebraMap C hC psi) :
Set (ZCCompletedGroupAlgebra C G))
letI : Nonempty (ZCCompletedGroupAlgebraIndex C G) :=
⟨(ProCIntegerIndex.terminal (C := C) inferInstance, zcCompletedGroupAlgebraTopIndex C G)⟩
letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, TopologicalSpace (S.X i) := fun _ =>
inferInstance
letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, CompactSpace (S.X i) := fun i => by
dsimp [S, zcCompletedGroupAlgebraSystem]
infer_instance
letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, T2Space (S.X i) := fun i => by
dsimp [S, zcCompletedGroupAlgebraSystem]
infer_instance
have hdir : Directed (· ≤ ·) (id : ZCCompletedGroupAlgebraIndex C G →
ZCCompletedGroupAlgebraIndex C G) :=
directed_zcCompletedGroupAlgebraIndex (C := C) (H := G) hForm
refine le_antisymm ?_ ?_
· intro x hx
exact closure_zcCompletedGroupAlgebraKernelAugmentationIdealMul_le_ker_map
C hC psi hx
· intro x hx
have hxClosure : x ∈ closure Y := by
rw [S.mem_isClosed_iff_forall_projection_mem hdir isClosed_closure]
intro i
rcases
zcCompletedGAMap_sourceStageKernel_mem_proj_kernelAugmentationIdealMul_of_openMap_surj
C hC hForm psi hpsi hfopen i x (by simpa [K] using hx) with
⟨y, hy, hyproj⟩
refine ⟨y, subset_closure (by simpa [Y] using hy), ?_⟩
exact hyproj
simpa [Y] using hxClosureProof. Use the finite-stage augmentation maps of \(\mathbb{Z}_C\llbracket H\rrbracket\). The completed augmentation ideal is detected by all finite-stage projections: membership is equivalent to vanishing under every finite augmentation, and the standard generators \([h]-1\) project to the corresponding finite-stage generators. Closure, range, and inverse-limit statements follow from compatibility of finite-stage augmentation ideals under transition maps and from checking the formulas on group-like generators.
□