FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebra
This module sets up the finite-stage and inverse-limit description of the construction. It records the stage maps, projections, and comparison lemmas used to pass back to the completed object.
import
- Mathlib.Algebra.MonoidAlgebra.MapDomain
- ProCGroups.ProC.OpenNormalSubgroups.ProCGroup
abbrev CompletedGroupAlgebraIndexInClass (C : ProCGroups.FiniteGroupClass.{u}) :=
OrderDual (OpenNormalSubgroupInClass C G)The index set for a completed group algebra over finite quotients belonging to a class \(C\).
abbrev CompletedGroupAlgebraQuotientInClass
(C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) : Type _ :=
(openNormalSubgroupInClassSystem C G).X Udef completedGroupAlgebraTransitionInClass
(C : ProCGroups.FiniteGroupClass.{u})
{U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
CompletedGroupAlgebraStageInClass G C V →+*
CompletedGroupAlgebraStageInClass G C U :=
MonoidAlgebra.mapDomainRingHom ℤ
(OpenNormalSubgroupInClass.map
(C := C) (G := G)
(U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)The transition map between two class-restricted completed-group-algebra stages.
theorem completedGroupAlgebraTransitionInClass_id
(C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
completedGroupAlgebraTransitionInClass G C (le_rfl : U ≤ U) = RingHom.id _The transition map attached to the identity refinement is the identity homomorphism in the Fox differential construction.
Show proof
by
rw [completedGroupAlgebraTransitionInClass, OpenNormalSubgroupInClass.map_id]
exact MonoidAlgebra.mapDomainRingHom_id
(R := ℤ) (M := CompletedGroupAlgebraQuotientInClass G C U)Proof. Unfold the class-restricted completed group algebra as an inverse limit over finite quotients in the chosen finite-group class. The projections, transition maps, comap indices, and stage group algebras are defined coordinatewise on finite quotient stages. Compatibility under refinement and the class-closure hypotheses assemble the inverse-limit object and its functorial maps.
□theorem completedGroupAlgebraTransitionInClass_comp
(C : ProCGroups.FiniteGroupClass.{u})
{U V W : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) (hVW : V ≤ W) :
(completedGroupAlgebraTransitionInClass G C hUV).comp
(completedGroupAlgebraTransitionInClass G C hVW) =
completedGroupAlgebraTransitionInClass G C (hUV.trans hVW)The finite-stage transition maps compose compatibly along chains of quotient refinements.
Show proof
by
rw [completedGroupAlgebraTransitionInClass, completedGroupAlgebraTransitionInClass,
completedGroupAlgebraTransitionInClass, ← MonoidAlgebra.mapDomainRingHom_comp]
congr 1
exact OpenNormalSubgroupInClass.map_comp
(C := C) (G := G)
(U := OrderDual.ofDual U) (V := OrderDual.ofDual V) (W := OrderDual.ofDual W)
hUV hVWProof. Unfold the class-restricted completed group algebra as an inverse limit over finite quotients in the chosen finite-group class. The projections, transition maps, comap indices, and stage group algebras are defined coordinatewise on finite quotient stages. Compatibility under refinement and the class-closure hypotheses assemble the inverse-limit object and its functorial maps.
□def completedGroupAlgebraSystemInClass
(C : ProCGroups.FiniteGroupClass.{u}) :
InverseSystem (I := CompletedGroupAlgebraIndexInClass G C) where
X := CompletedGroupAlgebraStageInClass G C
topologicalSpace := fun _ => ⊥
map := fun {U V} hUV => completedGroupAlgebraTransitionInClass G C hUV
continuous_map := by
intro U V hUV
letI : TopologicalSpace (CompletedGroupAlgebraStageInClass G C U) := ⊥
letI : TopologicalSpace (CompletedGroupAlgebraStageInClass G C V) := ⊥
letI : DiscreteTopology (CompletedGroupAlgebraStageInClass G C V) := ⟨rfl⟩
exact continuous_of_discreteTopology
map_id := by
intro U
funext x
exact congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraTransitionInClass_id G C U)) x
map_comp := by
intro U V W hUV hVW
funext x
exact congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraTransitionInClass_comp G C hUV hVW)) xThe class-restricted inverse system of finite-stage integral group rings.
def completedGroupAlgebraStageMapInClass
(C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
MonoidAlgebra ℤ G →+* CompletedGroupAlgebraStageInClass G C U :=
MonoidAlgebra.mapDomainRingHom ℤ
(openNormalSubgroupInClassProj (C := C) (G := G) U)theorem completedGroupAlgebraStageMapInClass_of
(C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) (g : G) :
completedGroupAlgebraStageMapInClass G C U (MonoidAlgebra.of ℤ _ g) =
MonoidAlgebra.single (openNormalSubgroupInClassProj (C := C) (G := G) U g) 1The finite-stage group-like map sends a group element to the corresponding singleton basis element in the quotient group algebra in the Fox differential construction.
Show proof
by
classical
simp only [completedGroupAlgebraStageMapInClass, MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk,
OneHom.coe_mk, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]
rflProof. Unfold the class-restricted completed group algebra as an inverse limit over finite quotients in the chosen finite-group class. The projections, transition maps, comap indices, and stage group algebras are defined coordinatewise on finite quotient stages. Compatibility under refinement and the class-closure hypotheses assemble the inverse-limit object and its functorial maps.
□theorem completedGroupAlgebraStageMapInClass_compatible
(C : ProCGroups.FiniteGroupClass.{u})
{U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
(completedGroupAlgebraTransitionInClass G C hUV).comp
(completedGroupAlgebraStageMapInClass G C V) =
completedGroupAlgebraStageMapInClass G C UThe class-restricted completed group-algebra stage map is compatible with transition maps and coordinate projections in the Fox differential construction.
Show proof
by
rw [completedGroupAlgebraTransitionInClass, completedGroupAlgebraStageMapInClass,
completedGroupAlgebraStageMapInClass, ← MonoidAlgebra.mapDomainRingHom_comp]
congr 1Proof. Unfold the class-restricted completed group algebra as an inverse limit over finite quotients in the chosen finite-group class. The projections, transition maps, comap indices, and stage group algebras are defined coordinatewise on finite quotient stages. Compatibility under refinement and the class-closure hypotheses assemble the inverse-limit object and its functorial maps.
□def CompletedGroupAlgebraCompatibleInClass
(C : ProCGroups.FiniteGroupClass.{u})
(x : ∀ U : CompletedGroupAlgebraIndexInClass G C,
CompletedGroupAlgebraStageInClass G C U) : Prop :=
(completedGroupAlgebraSystemInClass G C).Compatible xCompatibility for a class-restricted completed group algebra family.
abbrev CompletedGroupAlgebraInClass (C : ProCGroups.FiniteGroupClass.{u}) : Type _ :=
{x : ∀ U : CompletedGroupAlgebraIndexInClass G C,
CompletedGroupAlgebraStageInClass G C U //
CompletedGroupAlgebraCompatibleInClass G C x}The class-restricted completed group algebra as an inverse-limit subtype.
def completedGroupAlgebraProjectionInClass
(C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
CompletedGroupAlgebraInClass G C → CompletedGroupAlgebraStageInClass G C U :=
(completedGroupAlgebraSystemInClass G C).projection Udef completedGroupAlgebraComapIndexInClass
(C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
(ψ : ContinuousMonoidHom G H) (U : CompletedGroupAlgebraIndexInClass H C) :
CompletedGroupAlgebraIndexInClass G C := by
let V : OpenNormalSubgroup H := (OrderDual.ofDual U).1
let W : OpenNormalSubgroup G := OpenNormalSubgroup.comap ψ.toMonoidHom ψ.continuous_toFun V
refine OrderDual.toDual ⟨W, ?_⟩
let f : G ⧸ (W : Subgroup G) →* H ⧸ (V : Subgroup H) :=
QuotientGroup.map _ _ ψ.toMonoidHom (by
intro g hg
simpa [W] using hg)
have hf : Function.Injective f := by
intro x y hxy
rcases QuotientGroup.mk'_surjective (W : Subgroup G) x with ⟨a, rfl⟩
rcases QuotientGroup.mk'_surjective (W : Subgroup G) y with ⟨b, rfl⟩
apply QuotientGroup.eq.2
change ψ (a⁻¹ * b) ∈ (V : Subgroup H)
have hv : (ψ a)⁻¹ * ψ b ∈ (V : Subgroup H) := QuotientGroup.eq.1 hxy
simpa using hv
exact hC.of_injective (OrderDual.ofDual U).2 f hfPull back a class-restricted finite quotient along a continuous homomorphism. The hereditary hypothesis is the precise extra closure property needed: the pulled-back quotient embeds into the target quotient, so membership in \(C\) follows from closure under subgroups.
def completedGroupAlgebraComapQuotientMapInClass
(C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
(ψ : ContinuousMonoidHom G H) (U : CompletedGroupAlgebraIndexInClass H C) :
CompletedGroupAlgebraQuotientInClass G C
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ U) →*
CompletedGroupAlgebraQuotientInClass H C U := by
let V : OpenNormalSubgroup H := (OrderDual.ofDual U).1
let W : OpenNormalSubgroup G := OpenNormalSubgroup.comap ψ.toMonoidHom ψ.continuous_toFun V
exact QuotientGroup.map _ _ ψ.toMonoidHom (by
intro g hg
simpa [W, completedGroupAlgebraComapIndexInClass] using hg)The finite quotient map induced by a continuous homomorphism after pulling back the stage.
theorem completedGroupAlgebraComapQuotientMapInClass_mk
(C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
(ψ : ContinuousMonoidHom G H) (U : CompletedGroupAlgebraIndexInClass H C) (g : G) :
completedGroupAlgebraComapQuotientMapInClass
(G := G) (H := H) C hC ψ U
(QuotientGroup.mk'
((((OrderDual.ofDual
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ U)).1 :
OpenNormalSubgroup G) : Subgroup G)) g) =
QuotientGroup.mk' ((((OrderDual.ofDual U).1 : OpenNormalSubgroup H) : Subgroup H))
(ψ g)The pullback quotient map sends the class of a source element to the class of its image in the target quotient in the Fox differential construction.
Show proof
rflProof. Unfold the class-restricted completed group algebra as an inverse limit over finite quotients in the chosen finite-group class. The projections, transition maps, comap indices, and stage group algebras are defined coordinatewise on finite quotient stages. Compatibility under refinement and the class-closure hypotheses assemble the inverse-limit object and its functorial maps.
□theorem completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
(C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
(ψ : ContinuousMonoidHom G H) (hψ : Function.Surjective ψ)
(U : CompletedGroupAlgebraIndexInClass H C) :
Function.Surjective
(completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hC ψ U)The \(C\)-indexed pullback quotient map on completed group algebras is surjective when the underlying map is surjective.
Show proof
by
intro h
rcases QuotientGroup.mk'_surjective
((((OrderDual.ofDual U).1 : OpenNormalSubgroup H) : Subgroup H)) h with ⟨a, rfl⟩
rcases hψ a with ⟨g, rfl⟩
refine ⟨QuotientGroup.mk'
((((OrderDual.ofDual
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ U)).1 :
OpenNormalSubgroup G) : Subgroup G)) g, ?_⟩
rw [completedGroupAlgebraComapQuotientMapInClass_mk]Proof. Unfold the class-restricted completed group algebra as an inverse limit over finite quotients in the chosen finite-group class. The projections, transition maps, comap indices, and stage group algebras are defined coordinatewise on finite quotient stages. Compatibility under refinement and the class-closure hypotheses assemble the inverse-limit object and its functorial maps.
□theorem completedGroupAlgebraComapIndexInClass_mono
(C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
(ψ : ContinuousMonoidHom G H) {U V : CompletedGroupAlgebraIndexInClass H C}
(hUV : U ≤ V) :
completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ U ≤
completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ VComap indices are monotone with respect to refinement of open normal subgroups.
Show proof
by
change
Subgroup.comap ψ.toMonoidHom
(((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H) ≤
Subgroup.comap ψ.toMonoidHom
(((OrderDual.ofDual U).1 : OpenNormalSubgroup H) : Subgroup H)
exact Subgroup.comap_mono hUVProof. Unfold the class-restricted completed group algebra as an inverse limit over finite quotients in the chosen finite-group class. The projections, transition maps, comap indices, and stage group algebras are defined coordinatewise on finite quotient stages. Compatibility under refinement and the class-closure hypotheses assemble the inverse-limit object and its functorial maps.
□theorem completedGroupAlgebraComapQuotientMapInClass_compatible
(C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
(ψ : ContinuousMonoidHom G H) {U V : CompletedGroupAlgebraIndexInClass H C}
(hUV : U ≤ V) :
(OpenNormalSubgroupInClass.map
(C := C) (G := H)
(U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV).comp
(completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hC ψ V) =
(completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hC ψ U).comp
(OpenNormalSubgroupInClass.map
(C := C) (G := G)
(U := OrderDual.ofDual
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ U))
(V := OrderDual.ofDual
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ V))
(completedGroupAlgebraComapIndexInClass_mono (G := G) (H := H) C hC ψ hUV))The class-restricted completed group-algebra pullback quotient map is compatible with transition maps and coordinate projections in the Fox differential construction.
Show proof
by
ext q
rcases QuotientGroup.mk'_surjective
((((OrderDual.ofDual
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ V)).1 :
OpenNormalSubgroup G) : Subgroup G)) q with ⟨g, rfl⟩
rflProof. Unfold the class-restricted completed group algebra as an inverse limit over finite quotients in the chosen finite-group class. The projections, transition maps, comap indices, and stage group algebras are defined coordinatewise on finite quotient stages. Compatibility under refinement and the class-closure hypotheses assemble the inverse-limit object and its functorial maps.
□theorem completedGroupAlgebraComapIndexInClass_id
(C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
(U : CompletedGroupAlgebraIndexInClass G C) :
completedGroupAlgebraComapIndexInClass (G := G) (H := G) C hC
(ContinuousMonoidHom.id G) U = UPulling a finite quotient back along the identity continuous homomorphism gives the same class-restricted index. This is intentionally an equality theorem, since dependent inverse-limit indices are often not definitionally equal after target naturality rewrites.
Show proof
by
apply OrderDual.ofDual.injective
ext x
simp only [completedGroupAlgebraComapIndexInClass, ContinuousMonoidHom.coe_toMonoidHom,
OrderDual.ofDual_toDual, OpenNormalSubgroup.toSubgroup_comap, Subsemigroup.mem_carrier,
Submonoid.mem_toSubsemigroup, Subgroup.mem_toSubmonoid, Subgroup.mem_comap, MonoidHom.coe_coe,
ContinuousMonoidHom.id_toFun, OpenSubgroup.mem_toSubgroup]Proof. Unfold the class-restricted completed group algebra as an inverse limit over finite quotients in the chosen finite-group class. The projections, transition maps, comap indices, and stage group algebras are defined coordinatewise on finite quotient stages. Compatibility under refinement and the class-closure hypotheses assemble the inverse-limit object and its functorial maps.
□theorem completedGroupAlgebraComapIndexInClass_comp
(C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
{K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
(φ : G →ₜ* H) (ψ : H →ₜ* K) (U : CompletedGroupAlgebraIndexInClass K C) :
completedGroupAlgebraComapIndexInClass (G := G) (H := K) C hC (ψ.comp φ) U =
completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC φ
(completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC ψ U)Pullback of class-restricted finite quotients is functorial for continuous target maps. This is the index-level rewrite needed when the two inverse-limit stage indices produced by a composite target map are propositionally, but not definitionally, the same.
Show proof
by
apply OrderDual.ofDual.injective
ext x
simp only [completedGroupAlgebraComapIndexInClass, ContinuousMonoidHom.coe_toMonoidHom,
OrderDual.ofDual_toDual, OpenNormalSubgroup.toSubgroup_comap, Subsemigroup.mem_carrier,
Submonoid.mem_toSubsemigroup, Subgroup.mem_toSubmonoid, Subgroup.mem_comap, MonoidHom.coe_coe,
ContinuousMonoidHom.comp_toFun, OpenSubgroup.mem_toSubgroup]Proof. Unfold the class-restricted completed group algebra as an inverse limit over finite quotients in the chosen finite-group class. The projections, transition maps, comap indices, and stage group algebras are defined coordinatewise on finite quotient stages. Compatibility under refinement and the class-closure hypotheses assemble the inverse-limit object and its functorial maps.
□theorem completedGroupAlgebraComapIndexInClass_top
(C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
(ψ : G →ₜ* H) :
completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ
(OrderDual.toDual (OpenNormalSubgroupInClass.top (C := C) (G := H))) =
OrderDual.toDual (OpenNormalSubgroupInClass.top (C := C) (G := G))Pulling back the canonical trivial quotient gives the canonical trivial quotient.
Show proof
by
apply OrderDual.ofDual.injective
ext x
simp only [completedGroupAlgebraComapIndexInClass, ContinuousMonoidHom.coe_toMonoidHom,
OrderDual.ofDual_toDual, OpenNormalSubgroup.toSubgroup_comap, Subsemigroup.mem_carrier,
Submonoid.mem_toSubsemigroup, Subgroup.mem_toSubmonoid, Subgroup.mem_comap, MonoidHom.coe_coe,
OpenSubgroup.mem_toSubgroup]
constructor <;> intro _ <;> trivialProof. Unfold the class-restricted completed group algebra as an inverse limit over finite quotients in the chosen finite-group class. The projections, transition maps, comap indices, and stage group algebras are defined coordinatewise on finite quotient stages. Compatibility under refinement and the class-closure hypotheses assemble the inverse-limit object and its functorial maps.
□