FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.Stage
Fox Differential / Completed / Coefficient Rings / Prime-Power Augmentation Ideal / Stage.
def primePowerCompletedGroupAlgebraStageAugmentationIdeal
(i : PrimePowerCompletedGroupAlgebraIndex G) :
Ideal (PrimePowerCompletedGroupAlgebraStage ℓ G i) := by
letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
exact RingHom.ker (modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2)The augmentation ideal on one prime-power finite stage.
instance instFinitePrimePowerCompletedGroupAlgebraStageAugmentationIdeal
(i : PrimePowerCompletedGroupAlgebraIndex G) :
Finite ↥(primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i) := by
classical
letI : Finite (PrimePowerCompletedGroupAlgebraStage ℓ G i) :=
instFinitePrimePowerCompletedGroupAlgebraStage (ℓ := ℓ) (G := G) i
refine Finite.of_injective Subtype.val ?_
intro x y hxy
exact Subtype.ext hxyThe prime-power completed group-algebra stage augmentation ideal is finite.
def primePowerCompletedGroupAlgebraAugmentationKernel :
Set (PrimePowerCompletedGroupAlgebra ℓ G) :=
{x | primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G) x =
(Zero.zero : PrimePowerCompletedCoeff ℓ G)}The kernel of the canonical prime-power augmentation.
abbrev PrimePowerCompletedGroupAlgebraAugmentationKernel :=
{x : PrimePowerCompletedGroupAlgebra ℓ G //
x ∈ primePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G)}The kernel of the canonical prime-power augmentation is viewed as a subtype.
theorem mem_primePowerCompletedGroupAlgebraStageAugmentationIdeal_iff
{i : PrimePowerCompletedGroupAlgebraIndex G}
{x : PrimePowerCompletedGroupAlgebraStage ℓ G i} :
x ∈ primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i ↔
modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2 x = 0Membership in a prime-power finite-stage augmentation ideal is equivalent to vanishing under the stage augmentation map.
Show proof
by
rw [primePowerCompletedGroupAlgebraStageAugmentationIdeal, RingHom.mem_ker]Proof. Work with the prime-power completed augmentation ideal as the coordinatewise kernel of the finite-stage augmentations. Addition, scalar multiplication, inclusion into the completed group algebra, subtype linear maps, and limit equivalences are checked after every prime-power finite stage. The augmentation ideal condition is preserved by transition maps, and inverse-limit extensionality assembles the completed augmentation-ideal statements.
□theorem mem_primePowerCompletedGroupAlgebraAugmentationKernel_iff
{x : PrimePowerCompletedGroupAlgebra ℓ G} :
x ∈ primePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G) ↔
primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G) x =
(Zero.zero : PrimePowerCompletedCoeff ℓ G)Membership in the relevant augmentation kernel or augmentation ideal is equivalent to the corresponding vanishing condition.
Show proof
by
rflProof. Work with the prime-power completed augmentation ideal as the coordinatewise kernel of the finite-stage augmentations. Addition, scalar multiplication, inclusion into the completed group algebra, subtype linear maps, and limit equivalences are checked after every prime-power finite stage. The augmentation ideal condition is preserved by transition maps, and inverse-limit extensionality assembles the completed augmentation-ideal statements.
□theorem mem_primePowerCompletedGroupAlgebraAugmentationKernel_iff_forall
{x : PrimePowerCompletedGroupAlgebra ℓ G} :
x ∈ primePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G) ↔
∀ i : PrimePowerCompletedGroupAlgebraIndex G,
modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
(primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x) = 0Membership in the prime-power augmentation kernel is equivalent to vanishing after every finite-stage augmentation.
Show proof
by
constructor
· intro hx i
have hx0 :
primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G) x =
(Zero.zero : PrimePowerCompletedCoeff ℓ G) :=
(mem_primePowerCompletedGroupAlgebraAugmentationKernel_iff
(ℓ := ℓ) (G := G) (x := x)).1 hx
have hi := congrArg
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i) hx0
simpa [primePowerCompletedCoeffProjection_augmentation]
using hi
· intro hx
rw [mem_primePowerCompletedGroupAlgebraAugmentationKernel_iff]
apply (primePowerCompletedCoeffSystem ℓ G).ext
intro i
simpa [primePowerCompletedCoeffProjection_augmentation] using hx iProof. Work with the prime-power completed augmentation ideal as the coordinatewise kernel of the finite-stage augmentations. Addition, scalar multiplication, inclusion into the completed group algebra, subtype linear maps, and limit equivalences are checked after every prime-power finite stage. The augmentation ideal condition is preserved by transition maps, and inverse-limit extensionality assembles the completed augmentation-ideal statements.
□def primePowerCompletedGroupAlgebraStageAugmentationIdealTransition
{i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j) :
primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j →
primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i := by
intro x
refine ⟨primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij x.1, ?_⟩
rw [mem_primePowerCompletedGroupAlgebraStageAugmentationIdeal_iff]
letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
have hcomp := congrFun
(congrArg DFunLike.coe
(primePowerCompletedGroupAlgebraStageAugmentation_comp_transition
(ℓ := ℓ) (G := G) hij))
x.1
rw [RingHom.comp_apply] at hcomp
have hx0 :
modNCompletedGroupAlgebraStageAugmentation (ℓ ^ j.1) G j.2 x.1 = 0 :=
(mem_primePowerCompletedGroupAlgebraStageAugmentationIdeal_iff
(ℓ := ℓ) (G := G) (i := j) (x := x.1)).1 x.2
simpa [hx0] using hcompThe transition maps on the prime-power finite-stage augmentation ideals.
theorem primePowerCompletedGroupAlgebraStageAugmentationIdealTransition_val
{i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j)
(x : primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j) :
((primePowerCompletedGroupAlgebraStageAugmentationIdealTransition
(ℓ := ℓ) (G := G) hij x :
primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i) :
PrimePowerCompletedGroupAlgebraStage ℓ G i) =
primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij x.1The transition map between finite-stage augmentation ideals is evaluated by the corresponding stage transition.
Show proof
rflProof. Work with the prime-power completed augmentation ideal as the coordinatewise kernel of the finite-stage augmentations. Addition, scalar multiplication, inclusion into the completed group algebra, subtype linear maps, and limit equivalences are checked after every prime-power finite stage. The augmentation ideal condition is preserved by transition maps, and inverse-limit extensionality assembles the completed augmentation-ideal statements.
□def primePowerCompletedGroupAlgebraAugmentationIdealSystem :
InverseSystem (I := PrimePowerCompletedGroupAlgebraIndex G) where
X := fun i => ↥(primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i)
topologicalSpace := fun _ => ⊥
map := fun {i j} hij =>
primePowerCompletedGroupAlgebraStageAugmentationIdealTransition
(ℓ := ℓ) (G := G) hij
continuous_map := by
intro i j hij
letI : TopologicalSpace
(primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i) := ⊥
letI : TopologicalSpace
(primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j) := ⊥
letI : DiscreteTopology
(primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j) := ⟨rfl⟩
exact continuous_of_discreteTopology
map_id := by
intro i
funext x
apply Subtype.ext
exact congrFun
(congrArg DFunLike.coe
(primePowerCompletedGroupAlgebraTransition_id (ℓ := ℓ) (G := G) i)) x.1
map_comp := by
intro i j k hij hjk
funext x
apply Subtype.ext
exact congrFun
(congrArg DFunLike.coe
(primePowerCompletedGroupAlgebraTransition_comp (ℓ := ℓ) (G := G) hij hjk))
x.1The inverse system of prime-power finite-stage augmentation ideals.
abbrev PrimePowerCompletedGroupAlgebraAugmentationIdeal :=
(primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).inverseLimitThe inverse-limit object of the prime-power augmentation-ideal system.
abbrev primePowerCompletedGroupAlgebraAugmentationIdealProjection
(i : PrimePowerCompletedGroupAlgebraIndex G) :
PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G →
primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i :=
(primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).projection iThe projection from the prime-power augmentation-ideal inverse limit to one stage.