ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.Kernel
The principal declarations in this module are:
groupAlgebraMapDomainKernelAugmentationIdealThe ideal in \(R[A]\) generated by \([k]-1\) for \(k \in \ker f\). -groupAlgebraMapDomainTargetSectionA chosen linear section of the group-algebra map induced by a surjective group homomorphism. -groupAlgebraMapDomainKernelAugmentationGenerator_memA kernel augmentation generator lies in the group-algebra kernel-augmentation ideal. -groupAlgebra_mapDomainRingHom_smulThe domain group-algebra map is compatible with scalar multiplication.
imports
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 Lean proof
Ideal.subset_span (Set.mem_range_self k)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 Lean proof
by
rw [Algebra.smul_def, Algebra.smul_def, RingHom.map_mul]
simp only [MonoidAlgebra.mapDomainRingHom_apply,
MonoidAlgebra.mapDomain_algebraMap]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))).comp
(MonoidAlgebra.coeffLinearEquiv R).toLinearMapA chosen linear section of the group-algebra map induced by a surjective group homomorphism.
@[simp]
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 Lean proof
by
change
Finsupp.linearCombination R
(fun b : B => MonoidAlgebra.of R A (Function.surjInv hf b))
(MonoidAlgebra.of R B b).coeff =
MonoidAlgebra.of R A (Function.surjInv hf b)
rw [MonoidAlgebra.of_apply, MonoidAlgebra.coeff_single,
Finsupp.linearCombination_single, one_smul]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 Lean 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.mapDomainRingHom_apply,
MonoidAlgebra.of_apply, MonoidAlgebra.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]
Theorem
FoxDifferential.groupAlgebraMapDomain_sourceBasis_sub_targetSection_mem_kernelAugmentationIdeal
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 Lean 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.mapDomainRingHom_apply,
MonoidAlgebra.of_apply, MonoidAlgebra.mapDomain_single]]
simpa only [t, lift] 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)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 Lean 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 _ hxtheorem 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 Lean 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.mapDomainRingHom_apply, MonoidAlgebra.of_apply,
MonoidAlgebra.mapDomain_single, hk, MonoidAlgebra.one_def, sub_self]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\).
omit [IsTopologicalGroup H] in
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 Lean proof
Ideal.subset_span (Set.mem_range_self n)
Theorem
FoxDifferential.zcCompletedGroupAlgebraKernelAugmentationIdealMul_le_standardAugmentationIdeal
omit [IsTopologicalGroup H] in
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 Lean proof
by
refine Ideal.span_le.2 ?_
rintro _ ⟨n, rfl⟩
exact zcGroupLike_sub_one_mem_standardAugmentationIdeal C G n.1omit [IsTopologicalGroup H] in
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 Lean 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 hmultheorem 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 Lean 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]theorem isClosed_zcCompletedGroupAlgebraMap_ker
(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 Lean proof
by
change IsClosed ((zcCompletedGroupAlgebraMap C hC psi) ⁻¹'
({0} : Set (ZCCompletedGroupAlgebra C H)))
exact isClosed_singleton.preimage
(continuous_zcCompletedGroupAlgebraMap C hC psi)theorem closure_zcCompletedGroupAlgebraKernelAugmentationIdealMul_le_ker_map
(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 Lean proof
by
exact closure_minimal
(by
intro x hx
exact zcCompletedGroupAlgebraKernelAugmentationIdealMul_le_ker_map
C hC psi hx)
(isClosed_zcCompletedGroupAlgebraMap_ker C hC psi)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 Lean 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]
Theorem
FoxDifferential.zcCompletedGAMapStageRelationAugmentationIdeal_mem_proj_kernelAugmentationIdealMul
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 Lean 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]
rfl
Theorem
FoxDifferential.zcCompletedGAMapDomainKernelAugmentationIdeal_mem_proj_kernelAugmentationIdealMul
omit [IsTopologicalGroup H] in
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 Lean 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]
rfldef 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.
omit [IsTopologicalGroup G] in
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 Lean 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⟩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))The source-stage quotient map \(G/U \to H/\psi(U)\) attached to an open surjective map.
@[simp 900]
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 Lean 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]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 Lean 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]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 Lean 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 hutheorem 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 Lean proof
by
rw [zcCompletedGroupAlgebraOpenImageQuotientMap, MonoidAlgebra.mapDomainRingHom_comp]
rw [zcCompletedGroupAlgebraMapStage]
simp only [zcCompletedGroupAlgebraOpenImageTargetIndex]
congr 1
rw [zcCompletedGroupAlgebraTransition,
modNCompletedGroupAlgebraStageCoeffMapInClass_rfl, RingHom.id_comp]
rfltheorem 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 Lean 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]
convert htargetzero using 1
rfl
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 hxkertheorem 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 Lean 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)theorem closure_zcCompletedGAKernelAugmentationIdealMul_eq_ker_map_of_openMap_surj
[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 Lean 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]
change @CompactSpace (ZCCompletedGroupAlgebraStage C G i) ⊥
letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
letI : Finite (ZCCompletedGroupAlgebraStage C G i) :=
finite_modNCompletedGroupAlgebraStageInClass
(n := i.1.modulus) (G := G) C i.2
exact Finite.compactSpace
letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, T2Space (S.X i) := fun i => by
dsimp [S, zcCompletedGroupAlgebraSystem]
change @T2Space (ZCCompletedGroupAlgebraStage C G i) ⊥
exact @DiscreteTopology.toT2Space _ ⊥ ⟨rfl⟩
have hdir : Directed (· ≤ ·) (id : ZCCompletedGroupAlgebraIndex C G →
ZCCompletedGroupAlgebraIndex C G) :=
directed_zcCompletedGroupAlgebraIndex_of_formation (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 hxClosureS :
(show S.inverseLimit from x) ∈
closure (show Set S.inverseLimit from 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 ?_, ?_⟩
· convert hy using 1
rfl
exact hyproj
convert hxClosureS using 1 <;>
rfl