FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.Basic
Fox Differential / Completed / Coefficient Rings / Completed Group Algebra Mod N / Within a Class / Basic.
import
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebra
- Mathlib.Data.ZMod.Basic
abbrev ModNCompletedCoeff : Type := ZMod nThe coefficient ring \(\mathbb{Z}/n\mathbb{Z}\) used in one residue-coefficient stage.
abbrev ModNCompletedGroupRing (H : Type*) : Type _ :=
MonoidAlgebra (ModNCompletedCoeff n) HThe group ring \((\mathbb{Z}/n\mathbb{Z})[H]\) used in the residue-coefficient tower.
abbrev ModNCompletedGroupAlgebraStageInClass
(C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) : Type _ :=
ModNCompletedGroupRing n (CompletedGroupAlgebraQuotientInClass G C U)The residue-coefficient stage over a class-restricted finite quotient \(G/U\).
theorem finite_modNCompletedGroupAlgebraStageInClass
(C : ProCGroups.FiniteGroupClass.{u})
(hFinite : ∀ {Q : Type u} [Group Q], C Q → Finite Q)
(U : CompletedGroupAlgebraIndexInClass G C) :
Finite (ModNCompletedGroupAlgebraStageInClass n G C U)Each \(C\)-indexed finite stage of the mod-\(n\) completed group algebra is finite.
Show proof
by
classical
letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
hFinite (OrderDual.ofDual U).2
letI : Fintype (CompletedGroupAlgebraQuotientInClass G C U) := Fintype.ofFinite _
letI : DecidableEq (CompletedGroupAlgebraQuotientInClass G C U) := Classical.decEq _
letI : NeZero n := ⟨Nat.ne_of_gt (show 0 < n from Fact.out)⟩
letI : Fintype (ModNCompletedCoeff n) := Fintype.ofEquiv (Fin n) (ZMod.finEquiv n)
letI :
Finite (CompletedGroupAlgebraQuotientInClass G C U → ModNCompletedCoeff n) := by
letI :
Fintype (CompletedGroupAlgebraQuotientInClass G C U → ModNCompletedCoeff n) :=
inferInstance
exact Finite.of_fintype _
let f :
ModNCompletedGroupAlgebraStageInClass n G C U →
CompletedGroupAlgebraQuotientInClass G C U → ModNCompletedCoeff n := fun x q => x q
refine Finite.of_injective f ?_
intro x y hxy
ext q
exact congrFun hxy qProof. Unfold the mod-\(n\) completed group algebra as the inverse limit over finite group quotients with fixed coefficient ring \(\mathbb{Z}/n\mathbb{Z}\). Projections, transitions, augmentation, coefficient reduction, and algebra operations are computed coordinatewise at finite group-algebra stages. Compatibility under quotient refinement and inverse-limit extensionality assemble the completed statements.
□def modNCompletedGroupAlgebraTransitionInClass
(C : ProCGroups.FiniteGroupClass.{u})
{U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
ModNCompletedGroupAlgebraStageInClass n G C V →+*
ModNCompletedGroupAlgebraStageInClass n G C U :=
MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n)
(OpenNormalSubgroupInClass.map
(C := C) (G := G)
(U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)The transition map between class-restricted residue-coefficient stages.
theorem modNCompletedGroupAlgebraTransitionInClass_of
(C : ProCGroups.FiniteGroupClass.{u})
{U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)
(g : CompletedGroupAlgebraQuotientInClass G C V) :
modNCompletedGroupAlgebraTransitionInClass n G C hUV
(MonoidAlgebra.of (ModNCompletedCoeff n) _ g) =
MonoidAlgebra.single
((OpenNormalSubgroupInClass.map
(C := C) (G := G)
(U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) g) 1The transition map sends a group-like basis element to the basis element supported at its image in the coarser quotient in the Fox differential construction.
Show proof
by
classical
simp only [modNCompletedGroupAlgebraTransitionInClass, MonoidAlgebra.of, MonoidAlgebra.single,
MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]
rflProof. Unfold the mod-\(n\) completed group algebra as the inverse limit over finite group quotients with fixed coefficient ring \(\mathbb{Z}/n\mathbb{Z}\). Projections, transitions, augmentation, coefficient reduction, and algebra operations are computed coordinatewise at finite group-algebra stages. Compatibility under quotient refinement and inverse-limit extensionality assemble the completed statements.
□theorem modNCompletedGroupAlgebraTransitionInClass_single
(C : ProCGroups.FiniteGroupClass.{u})
{U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)
(q : CompletedGroupAlgebraQuotientInClass G C V)
(a : ModNCompletedCoeff n) :
modNCompletedGroupAlgebraTransitionInClass n G C hUV
(MonoidAlgebra.single q a) =
MonoidAlgebra.single
((OpenNormalSubgroupInClass.map
(C := C) (G := G)
(U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q) aThe \(C\)-indexed transition map between finite stages sends a singleton supported at a class of the finer quotient to the singleton supported at its image in the coarser quotient, preserving the coefficient.
Show proof
by
classical
simp only [modNCompletedGroupAlgebraTransitionInClass, MonoidAlgebra.mapDomainRingHom_apply,
Finsupp.mapDomain_single]
rflProof. Unfold the mod-\(n\) completed group algebra as the inverse limit over finite group quotients with fixed coefficient ring \(\mathbb{Z}/n\mathbb{Z}\). Projections, transitions, augmentation, coefficient reduction, and algebra operations are computed coordinatewise at finite group-algebra stages. Compatibility under quotient refinement and inverse-limit extensionality assemble the completed statements.
□theorem modNCompletedGroupAlgebraTransitionInClass_id
(C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
modNCompletedGroupAlgebraTransitionInClass n 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 [modNCompletedGroupAlgebraTransitionInClass, OpenNormalSubgroupInClass.map_id]
exact MonoidAlgebra.mapDomainRingHom_id
(R := ModNCompletedCoeff n) (M := CompletedGroupAlgebraQuotientInClass G C U)Proof. Unfold the mod-\(n\) completed group algebra as the inverse limit over finite group quotients with fixed coefficient ring \(\mathbb{Z}/n\mathbb{Z}\). Projections, transitions, augmentation, coefficient reduction, and algebra operations are computed coordinatewise at finite group-algebra stages. Compatibility under quotient refinement and inverse-limit extensionality assemble the completed statements.
□theorem modNCompletedGroupAlgebraTransitionInClass_comp
(C : ProCGroups.FiniteGroupClass.{u})
{U V W : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) (hVW : V ≤ W) :
(modNCompletedGroupAlgebraTransitionInClass n G C hUV).comp
(modNCompletedGroupAlgebraTransitionInClass n G C hVW) =
modNCompletedGroupAlgebraTransitionInClass n G C (hUV.trans hVW)The finite-stage transition maps compose compatibly along chains of quotient refinements.
Show proof
by
rw [modNCompletedGroupAlgebraTransitionInClass, modNCompletedGroupAlgebraTransitionInClass,
modNCompletedGroupAlgebraTransitionInClass, ← 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 mod-\(n\) completed group algebra as the inverse limit over finite group quotients with fixed coefficient ring \(\mathbb{Z}/n\mathbb{Z}\). Projections, transitions, augmentation, coefficient reduction, and algebra operations are computed coordinatewise at finite group-algebra stages. Compatibility under quotient refinement and inverse-limit extensionality assemble the completed statements.
□def modNCompletedGroupAlgebraSystemInClass
(C : ProCGroups.FiniteGroupClass.{u}) :
InverseSystem (I := CompletedGroupAlgebraIndexInClass G C) where
X := ModNCompletedGroupAlgebraStageInClass n G C
topologicalSpace := fun _ => ⊥
map := fun {U V} hUV => modNCompletedGroupAlgebraTransitionInClass n G C hUV
continuous_map := by
intro U V hUV
letI : TopologicalSpace (ModNCompletedGroupAlgebraStageInClass n G C U) := ⊥
letI : TopologicalSpace (ModNCompletedGroupAlgebraStageInClass n G C V) := ⊥
letI : DiscreteTopology (ModNCompletedGroupAlgebraStageInClass n G C V) := ⟨rfl⟩
exact continuous_of_discreteTopology
map_id := by
intro U
funext x
exact congrFun
(congrArg DFunLike.coe
(modNCompletedGroupAlgebraTransitionInClass_id n G C U)) x
map_comp := by
intro U V W hUV hVW
funext x
exact congrFun
(congrArg DFunLike.coe
(modNCompletedGroupAlgebraTransitionInClass_comp n G C hUV hVW)) xThe class-restricted inverse system \(U \mapsto (\mathbb{Z}/n\mathbb{Z})[G/U]\).
theorem modNCompletedGroupAlgebraTransitionInClass_surjective
(C : ProCGroups.FiniteGroupClass.{u})
{U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
Function.Surjective (modNCompletedGroupAlgebraTransitionInClass n G C hUV)The finite-stage transition map is surjective, with preimages obtained by lifting quotient representatives.
Show proof
by
intro x
induction x using Finsupp.induction with
| zero =>
exact ⟨0, map_zero _⟩
| single_add q a x _ _ ih =>
rcases OpenNormalSubgroupInClass.map_surjective
(C := C) (G := G)
(U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV q with
⟨q', hq'⟩
rcases ih with ⟨y, hy⟩
refine
⟨(MonoidAlgebra.single q' a : ModNCompletedGroupAlgebraStageInClass n G C V) + y,
?_⟩
rw [map_add, modNCompletedGroupAlgebraTransitionInClass_single, hy, hq']Proof. Unfold the mod-\(n\) completed group algebra as the inverse limit over finite group quotients with fixed coefficient ring \(\mathbb{Z}/n\mathbb{Z}\). Projections, transitions, augmentation, coefficient reduction, and algebra operations are computed coordinatewise at finite group-algebra stages. Compatibility under quotient refinement and inverse-limit extensionality assemble the completed statements.
□def modNCompletedGroupAlgebraStageMapInClass
(C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
ModNCompletedGroupRing n G →+* ModNCompletedGroupAlgebraStageInClass n G C U :=
MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n)
(openNormalSubgroupInClassProj (C := C) (G := G) U)The quotient map \((\mathbb{Z}/n\mathbb{Z})[G] \to (\mathbb{Z}/n\mathbb{Z})[G/U]\) for a class-restricted stage.
theorem modNCompletedGroupAlgebraStageMapInClass_of
(C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) (g : G) :
modNCompletedGroupAlgebraStageMapInClass n G C U
(MonoidAlgebra.of (ModNCompletedCoeff n) _ 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 [modNCompletedGroupAlgebraStageMapInClass, MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk,
OneHom.coe_mk, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]
rflProof. Unfold the mod-\(n\) completed group algebra as the inverse limit over finite group quotients with fixed coefficient ring \(\mathbb{Z}/n\mathbb{Z}\). Projections, transitions, augmentation, coefficient reduction, and algebra operations are computed coordinatewise at finite group-algebra stages. Compatibility under quotient refinement and inverse-limit extensionality assemble the completed statements.
□theorem modNCompletedGroupAlgebraStageMapInClass_compatible
(C : ProCGroups.FiniteGroupClass.{u})
{U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
(modNCompletedGroupAlgebraTransitionInClass n G C hUV).comp
(modNCompletedGroupAlgebraStageMapInClass n G C V) =
modNCompletedGroupAlgebraStageMapInClass n G C UThe class-restricted mod-\(n\) completed group-algebra stage maps are compatible with quotient refinement.
Show proof
by
rw [modNCompletedGroupAlgebraTransitionInClass, modNCompletedGroupAlgebraStageMapInClass,
modNCompletedGroupAlgebraStageMapInClass, ← MonoidAlgebra.mapDomainRingHom_comp]
congr 1Proof. Unfold the mod-\(n\) completed group-algebra stage map. Refinement of finite quotients gives the same quotient support map, and the coefficient ring \(\mathbb{Z}/n\mathbb{Z}\) is unchanged, so the two transition composites agree on basis elements and hence by linearity.
□def ModNCompletedGroupAlgebraCompatibleInClass
(C : ProCGroups.FiniteGroupClass.{u})
(x : ∀ U : CompletedGroupAlgebraIndexInClass G C,
ModNCompletedGroupAlgebraStageInClass n G C U) : Prop :=
(modNCompletedGroupAlgebraSystemInClass n G C).Compatible xCompatibility for a class-restricted residue-coefficient completed group algebra family.
abbrev ModNCompletedGroupAlgebraInClass (C : ProCGroups.FiniteGroupClass.{u}) : Type _ :=
{x : ∀ U : CompletedGroupAlgebraIndexInClass G C,
ModNCompletedGroupAlgebraStageInClass n G C U //
ModNCompletedGroupAlgebraCompatibleInClass n G C x}The class-restricted residue-coefficient completed group algebra as an inverse-limit subtype.
def modNCompletedGroupAlgebraProjectionInClass
(C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
ModNCompletedGroupAlgebraInClass n G C →
ModNCompletedGroupAlgebraStageInClass n G C U :=
(modNCompletedGroupAlgebraSystemInClass n G C).projection UThe projection from the class-restricted residue-coefficient completed group algebra to a stage.