FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.LimitEquiv
Fox Differential / Completed / Coefficient Rings / Prime-Power Augmentation Ideal / Limit Equivalence.
theorem primePowerCompletedGroupAlgebraAugmentationIdealProjection_zero
(i : PrimePowerCompletedGroupAlgebraIndex G) :
primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i
(0 : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) = 0The finite-stage augmentation-ideal projection is compatible with zero.
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 primePowerCompletedGroupAlgebraAugmentationIdealProjection_add
(i : PrimePowerCompletedGroupAlgebraIndex G)
(x y : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i (x + y) =
primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i x +
primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i yThe finite-stage augmentation-ideal projection is compatible with addition.
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 primePowerCompletedGroupAlgebraAugmentationIdealProjection_neg
(i : PrimePowerCompletedGroupAlgebraIndex G)
(x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i (-x) =
-primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i xThe finite-stage augmentation-ideal projection is compatible with negation.
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 primePowerCompletedGroupAlgebraAugmentationIdealProjection_sub
(i : PrimePowerCompletedGroupAlgebraIndex G)
(x y : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i (x - y) =
primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i x -
primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i yThe finite-stage augmentation-ideal projection is compatible with subtraction.
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 primePowerCompletedGroupAlgebraAugmentationIdealProjection_nsmul
(i : PrimePowerCompletedGroupAlgebraIndex G)
(m : ℕ) (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i (m • x) =
m • primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i xThe finite-stage augmentation-ideal projection is compatible with natural-number scalar multiplication.
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 primePowerCompletedGroupAlgebraAugmentationIdealProjection_zsmul
(i : PrimePowerCompletedGroupAlgebraIndex G)
(m : ℤ) (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i (m • x) =
m • primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i xThe finite-stage augmentation-ideal projection is compatible with integer scalar multiplication.
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 primePowerCompletedGroupAlgebraAugmentationIdealProjection_smul
(i : PrimePowerCompletedGroupAlgebraIndex G)
(a : PrimePowerCompletedCoeff ℓ G)
(x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i (a • x) =
(primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i xThe finite-stage augmentation-ideal projection is compatible with scalar multiplication.
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.
□def toPrimePowerCompletedGroupAlgebraAugmentationIdeal :
PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G) →
PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G := by
intro x
refine ⟨fun i => ⟨primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x.1, ?_⟩, ?_⟩
· exact (mem_primePowerCompletedGroupAlgebraStageAugmentationIdeal_iff
(ℓ := ℓ) (G := G) (i := i)
(x := primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x.1)).2
((mem_primePowerCompletedGroupAlgebraAugmentationKernel_iff_forall
(ℓ := ℓ) (G := G) (x := x.1)).1 x.2 i)
· intro i j hij
apply Subtype.ext
exact (primePowerCompletedGroupAlgebraSystem ℓ G).projection_compatible x.1 i j hijA prime-power augmentation-kernel point determines a compatible family in the finite-stage augmentation ideals.
theorem primePowerCompletedGroupAlgebraAugmentationIdealProjection_to
(x : PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G))
(i : PrimePowerCompletedGroupAlgebraIndex G) :
((primePowerCompletedGroupAlgebraAugmentationIdealProjection
(ℓ := ℓ) (G := G) i
(toPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) x)) :
PrimePowerCompletedGroupAlgebraStage ℓ G i) =
primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x.1The projection-to-stage map is one direction of the completed augmentation-ideal stage equivalence.
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 ofPrimePowerCompletedGroupAlgebraAugmentationIdeal :
PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G →
PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G) := by
intro x
let y : PrimePowerCompletedGroupAlgebra ℓ G := ⟨fun i => (x.1 i).1, by
intro i j hij
exact congrArg Subtype.val (x.2 i j hij)⟩
refine ⟨y, ?_⟩
exact (mem_primePowerCompletedGroupAlgebraAugmentationKernel_iff_forall
(ℓ := ℓ) (G := G) (x := y)).2 (fun i =>
(mem_primePowerCompletedGroupAlgebraStageAugmentationIdeal_iff
(ℓ := ℓ) (G := G) (i := i) (x := (x.1 i).1)).1 (x.1 i).2)A compatible family of prime-power finite-stage augmentation-ideal elements determines a prime-power augmentation-kernel point.
theorem primePowerCompletedGroupAlgebraProjection_ofAugmentationIdeal
(x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G)
(i : PrimePowerCompletedGroupAlgebraIndex G) :
primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
(ofPrimePowerCompletedGroupAlgebraAugmentationIdeal
(ℓ := ℓ) (G := G) x).1 =
((primePowerCompletedGroupAlgebraAugmentationIdealProjection
(ℓ := ℓ) (G := G) i x) :
PrimePowerCompletedGroupAlgebraStage ℓ G i)Projecting an element of the completed augmentation ideal gives its corresponding finite-stage augmentation-ideal coordinate.
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.
□theorem ofPrimePowerCompletedGroupAlgebraAugmentationIdeal_to
(x : PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G)) :
ofPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G)
(toPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (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 (primePowerCompletedGroupAlgebraSystem ℓ G).ext
intro i
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 toPrimePowerCompletedGroupAlgebraAugmentationIdeal_of
(x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
toPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G)
(ofPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) x) = xThe stage-to-completion map is one direction of the completed augmentation-ideal stage equivalence.
Show proof
by
apply (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).ext
intro i
apply Subtype.ext
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 primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit :
PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G) ≃
PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G where
toFun := toPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G)
invFun := ofPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G)
left_inv := ofPrimePowerCompletedGroupAlgebraAugmentationIdeal_to (ℓ := ℓ) (G := G)
right_inv := toPrimePowerCompletedGroupAlgebraAugmentationIdeal_of (ℓ := ℓ) (G := G)The prime-power completed augmentation kernel is canonically equivalent to the inverse limit of the prime-power finite-stage augmentation ideals.
theorem primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit_apply
(x : PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G)) :
primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit
(ℓ := ℓ) (G := G) x =
toPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (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. 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 primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit_symm_apply
(x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
(primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit
(ℓ := ℓ) (G := G)).symm x =
ofPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (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. 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.
□