FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.AugmentationIdeal
This module develops the augmentation side of the construction. It identifies the relevant kernels and ideals and compares the finite-stage and completed forms.
def modNCompletedGroupAlgebraStageAugmentationIdeal (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
Ideal (ModNCompletedGroupAlgebraStage n G U) :=
RingHom.ker (modNCompletedGroupAlgebraStageAugmentation n G U)The augmentation ideal on one residue-coefficient finite stage.
def modNCompletedGroupAlgebraAugmentationKernel :
Set (ModNCompletedGroupAlgebra n G) :=
{x | modNCompletedGroupAlgebraAugmentation n G x = 0}The kernel of the canonical augmentation on the residue-coefficient completed group algebra.
abbrev ModNCompletedGroupAlgebraAugmentationKernel :=
{x : ModNCompletedGroupAlgebra n G // x ∈ modNCompletedGroupAlgebraAugmentationKernel n G}The kernel of the canonical augmentation is viewed as a subtype.
theorem mem_modNCompletedGroupAlgebraStageAugmentationIdeal_iff
{U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} {x : ModNCompletedGroupAlgebraStage n G U} :
x ∈ modNCompletedGroupAlgebraStageAugmentationIdeal n G U ↔
modNCompletedGroupAlgebraStageAugmentation n G U x = 0Membership in a mod-\(N\) finite-stage augmentation ideal is equivalent to vanishing under the stage augmentation map.
Show proof
by
rw [modNCompletedGroupAlgebraStageAugmentationIdeal, RingHom.mem_ker]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 mem_modNCompletedGroupAlgebraAugmentationKernel_iff
{x : ModNCompletedGroupAlgebra n G} :
x ∈ modNCompletedGroupAlgebraAugmentationKernel n G ↔
modNCompletedGroupAlgebraAugmentation n G x = 0Membership in the relevant augmentation kernel or augmentation ideal is equivalent to the corresponding vanishing condition.
Show proof
by
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 mem_modNCompletedGroupAlgebraProjection_stageAugmentationIdeal_iff
{U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} {x : ModNCompletedGroupAlgebra n G} :
modNCompletedGroupAlgebraProjection n G U x ∈
modNCompletedGroupAlgebraStageAugmentationIdeal n G U ↔
x ∈ modNCompletedGroupAlgebraAugmentationKernel n GA mod-\(N\) completed group-algebra element projects into the stage augmentation ideal iff it lies in the completed augmentation kernel.
Show proof
by
rw [mem_modNCompletedGroupAlgebraStageAugmentationIdeal_iff,
mem_modNCompletedGroupAlgebraAugmentationKernel_iff]
change modNCompletedGroupAlgebraAugmentationAt n G U x = 0 ↔
modNCompletedGroupAlgebraAugmentation n G x = 0
rw [modNCompletedGroupAlgebraAugmentation_eq_at (n := n) (G := G) U x]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 modNCompletedGroupAlgebraStageAugmentationIdealTransition
{U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
modNCompletedGroupAlgebraStageAugmentationIdeal n G V →
modNCompletedGroupAlgebraStageAugmentationIdeal n G U :=
fun x => ⟨modNCompletedGroupAlgebraTransition n G hUV x.1, by
rw [mem_modNCompletedGroupAlgebraStageAugmentationIdeal_iff]
have hcomp := congrFun
(congrArg DFunLike.coe
(modNCompletedGroupAlgebraStageAugmentation_compatible
(n := n) (G := G) (U := U) (V := V) hUV))
x.1
rw [RingHom.comp_apply] at hcomp
exact hcomp.trans
((mem_modNCompletedGroupAlgebraStageAugmentationIdeal_iff
(n := n) (G := G) (U := V) (x := x.1)).1 x.2)⟩The transition maps on the residue-coefficient finite-stage augmentation ideals.
theorem modNCompletedGroupAlgebraStageAugmentationIdealTransition_val
{U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V)
(x : modNCompletedGroupAlgebraStageAugmentationIdeal n G V) :
((modNCompletedGroupAlgebraStageAugmentationIdealTransition
(n := n) (G := G) hUV x : modNCompletedGroupAlgebraStageAugmentationIdeal n G U) :
ModNCompletedGroupAlgebraStage n G U) =
modNCompletedGroupAlgebraTransition n G hUV x.1The transition map between finite-stage augmentation ideals is evaluated by the corresponding stage transition.
Show proof
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.
□def modNCompletedGroupAlgebraAugmentationIdealSystem :
InverseSystem (I := _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) where
X := fun U => ↥(modNCompletedGroupAlgebraStageAugmentationIdeal n G U)
topologicalSpace := fun _ => ⊥
map := fun {U V} hUV => modNCompletedGroupAlgebraStageAugmentationIdealTransition
(n := n) (G := G) hUV
continuous_map := by
intro U V hUV
letI : TopologicalSpace (modNCompletedGroupAlgebraStageAugmentationIdeal n G U) := ⊥
letI : TopologicalSpace (modNCompletedGroupAlgebraStageAugmentationIdeal n G V) := ⊥
letI : DiscreteTopology (modNCompletedGroupAlgebraStageAugmentationIdeal n G V) := ⟨rfl⟩
exact continuous_of_discreteTopology
map_id := by
intro U
funext x
apply Subtype.ext
exact congrFun
(congrArg DFunLike.coe (modNCompletedGroupAlgebraTransition_id (n := n) (G := G) U))
x.1
map_comp := by
intro U V W hUV hVW
funext x
apply Subtype.ext
exact congrFun
(congrArg DFunLike.coe
(modNCompletedGroupAlgebraTransition_comp (n := n) (G := G) hUV hVW))
x.1The inverse system of residue-coefficient finite-stage augmentation ideals.
abbrev ModNCompletedGroupAlgebraAugmentationIdeal :=
(modNCompletedGroupAlgebraAugmentationIdealSystem n G).inverseLimitThe inverse-limit object of the residue-coefficient finite-stage augmentation ideals.
abbrev modNCompletedGroupAlgebraAugmentationIdealProjection (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
ModNCompletedGroupAlgebraAugmentationIdeal n G →
modNCompletedGroupAlgebraStageAugmentationIdeal n G U :=
(modNCompletedGroupAlgebraAugmentationIdealSystem n G).projection UThe projection from the residue-coefficient augmentation-ideal inverse limit to one stage.
def toModNCompletedGroupAlgebraAugmentationIdeal :
ModNCompletedGroupAlgebraAugmentationKernel n G →
ModNCompletedGroupAlgebraAugmentationIdeal n G := by
intro x
refine ⟨fun U => ⟨modNCompletedGroupAlgebraProjection n G U x.1, ?_⟩, ?_⟩
· exact (mem_modNCompletedGroupAlgebraProjection_stageAugmentationIdeal_iff
(n := n) (G := G) (U := U) (x := x.1)).2
((mem_modNCompletedGroupAlgebraAugmentationKernel_iff
(n := n) (G := G) (x := x.1)).1 x.2)
· intro U V hUV
apply Subtype.ext
exact (modNCompletedGroupAlgebraSystem n G).projection_compatible x.1 U V hUVA residue-coefficient augmentation-kernel point determines a compatible family in the finite-stage augmentation ideals.
theorem modNCompletedGroupAlgebraAugmentationIdealProjection_to
(x : ModNCompletedGroupAlgebraAugmentationKernel n G) (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
((modNCompletedGroupAlgebraAugmentationIdealProjection (n := n) (G := G) U
(toModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G) x)) :
ModNCompletedGroupAlgebraStage n G U) =
modNCompletedGroupAlgebraProjection n G U x.1The projection-to-stage map is one direction of the completed augmentation-ideal stage equivalence.
Show proof
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.
□def ofModNCompletedGroupAlgebraAugmentationIdeal :
ModNCompletedGroupAlgebraAugmentationIdeal n G →
ModNCompletedGroupAlgebraAugmentationKernel n G := by
intro x
let y : ModNCompletedGroupAlgebra n G := ⟨fun U => (x.1 U).1, by
intro U V hUV
exact congrArg Subtype.val (x.2 U V hUV)⟩
refine ⟨y, ?_⟩
have hterm :
modNCompletedGroupAlgebraProjection n G (_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G) y ∈
modNCompletedGroupAlgebraStageAugmentationIdeal n G
(_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G) := by
change (x.1 (_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G)).1 ∈
modNCompletedGroupAlgebraStageAugmentationIdeal n G
(_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G)
exact (x.1 (_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G)).2
exact (mem_modNCompletedGroupAlgebraAugmentationKernel_iff (n := n) (G := G) (x := y)).2
((mem_modNCompletedGroupAlgebraProjection_stageAugmentationIdeal_iff
(n := n) (G := G) (U := _root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G) (x := y)).1 hterm)A compatible family of finite-stage augmentation-ideal elements determines a residue-coefficient completed augmentation-kernel point.
theorem modNCompletedGroupAlgebraProjection_ofAugmentationIdeal
(x : ModNCompletedGroupAlgebraAugmentationIdeal n G) (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
modNCompletedGroupAlgebraProjection n G U
(ofModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G) x).1 =
((modNCompletedGroupAlgebraAugmentationIdealProjection (n := n) (G := G) U x) :
ModNCompletedGroupAlgebraStage n G U)Projecting an element of the completed augmentation ideal gives its corresponding finite-stage augmentation-ideal coordinate.
Show proof
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 ofModNCompletedGroupAlgebraAugmentationIdeal_to
(x : ModNCompletedGroupAlgebraAugmentationKernel n G) :
ofModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G)
(toModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G) x) = xThe completion-to-stage map is one direction of the completed augmentation-ideal stage equivalence.
Show proof
by
apply Subtype.ext
apply (modNCompletedGroupAlgebraSystem n G).ext
intro U
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 toModNCompletedGroupAlgebraAugmentationIdeal_of
(x : ModNCompletedGroupAlgebraAugmentationIdeal n G) :
toModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G)
(ofModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G) x) = xThe stage-to-completion map is one direction of the completed augmentation-ideal stage equivalence.
Show proof
by
apply (modNCompletedGroupAlgebraAugmentationIdealSystem n G).ext
intro U
apply Subtype.ext
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.
□def modNCompletedGroupAlgebraAugmentationKernelEquivInverseLimit :
ModNCompletedGroupAlgebraAugmentationKernel n G ≃
ModNCompletedGroupAlgebraAugmentationIdeal n G where
toFun := toModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G)
invFun := ofModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G)
left_inv := ofModNCompletedGroupAlgebraAugmentationIdeal_to (n := n) (G := G)
right_inv := toModNCompletedGroupAlgebraAugmentationIdeal_of (n := n) (G := G)The residue-coefficient completed augmentation kernel is canonically equivalent to the inverse limit of the finite-stage augmentation ideals.
theorem modNCompletedGroupAlgebraAugmentationKernelEquivInverseLimit_apply
(x : ModNCompletedGroupAlgebraAugmentationKernel n G) :
modNCompletedGroupAlgebraAugmentationKernelEquivInverseLimit (n := n) (G := G) x =
toModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G) xThe augmentation map is evaluated by projecting to the corresponding finite group-algebra stage and summing coefficients via the usual group-algebra augmentation.
Show proof
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 modNCompletedGroupAlgebraAugmentationKernelEquivInverseLimit_symm_apply
(x : ModNCompletedGroupAlgebraAugmentationIdeal n G) :
(modNCompletedGroupAlgebraAugmentationKernelEquivInverseLimit (n := n) (G := G)).symm x =
ofModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G) xThe augmentation map is evaluated by projecting to the corresponding finite group-algebra stage and summing coefficients via the usual group-algebra augmentation.
Show proof
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.
□