FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.SubtypeLinear
Fox Differential / Completed / Coefficient Rings / Prime-Power Augmentation Ideal / Subtype Linear.
def primePowerCompletedGroupAlgebraAugmentationIdealAddEquivAddSubgroup :
PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G ≃+
primePowerCompletedGroupAlgebraAugmentationAddSubgroup (ℓ := ℓ) (G := G) where
toFun x := by
refine ⟨(ofPrimePowerCompletedGroupAlgebraAugmentationIdeal
(ℓ := ℓ) (G := G) x).1, ?_⟩
simp only [SetLike.coe_mem]
invFun x :=
toPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) <|
⟨x.1, by
simp only [Subtype.coe_prop]⟩
left_inv := by
intro x
exact toPrimePowerCompletedGroupAlgebraAugmentationIdeal_of
(ℓ := ℓ) (G := G) x
right_inv := by
intro x
apply Subtype.ext
let y : PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G) :=
⟨x.1, by
simp only [Subtype.coe_prop]⟩
exact congrArg Subtype.val
(ofPrimePowerCompletedGroupAlgebraAugmentationIdeal_to
(ℓ := ℓ) (G := G) y)
map_add' x y := by
apply Subtype.ext
apply (primePowerCompletedGroupAlgebraSystem ℓ G).ext
intro i
rflThe inverse-limit augmentation ideal is additively equivalent to the additive kernel of the canonical prime-power augmentation.
def primePowerCompletedGroupAlgebraAugmentationIdealLinearEquivAddSubgroup :
PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G ≃ₗ[ℤ]
primePowerCompletedGroupAlgebraAugmentationAddSubgroup (ℓ := ℓ) (G := G) :=
(primePowerCompletedGroupAlgebraAugmentationIdealAddEquivAddSubgroup
(ℓ := ℓ) (G := G)).toIntLinearEquivThe inverse-limit augmentation ideal is linearly equivalent to the additive kernel of the canonical prime-power augmentation.
def primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear :
PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G →ₗ[ℤ]
PrimePowerCompletedGroupAlgebra ℓ G :=
(primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear
(ℓ := ℓ) (G := G)).comp
(primePowerCompletedGroupAlgebraAugmentationIdealLinearEquivAddSubgroup
(ℓ := ℓ) (G := G)).toLinearMapThe canonical inclusion of the inverse-limit augmentation ideal into the prime-power completed group algebra.
theorem primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear_apply
(x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear
(ℓ := ℓ) (G := G) x =
(ofPrimePowerCompletedGroupAlgebraAugmentationIdeal
(ℓ := ℓ) (G := G) x).1The augmentation map is evaluated by projecting to the corresponding finite group-algebra stage and summing coefficients via the usual group-algebra augmentation.
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 primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraCoeffLinear :
PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G →ₗ[PrimePowerCompletedCoeff ℓ G]
PrimePowerCompletedGroupAlgebra ℓ G where
toFun := fun x =>
(ofPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) x).1
map_add' := by
intro x y
apply (primePowerCompletedGroupAlgebraSystem ℓ G).ext
intro i
change (((primePowerCompletedGroupAlgebraAugmentationIdealProjection
(ℓ := ℓ) (G := G) i x +
primePowerCompletedGroupAlgebraAugmentationIdealProjection
(ℓ := ℓ) (G := G) i y :
primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i) :
PrimePowerCompletedGroupAlgebraStage ℓ G i)) =
primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
((ofPrimePowerCompletedGroupAlgebraAugmentationIdeal
(ℓ := ℓ) (G := G) x).1 +
(ofPrimePowerCompletedGroupAlgebraAugmentationIdeal
(ℓ := ℓ) (G := G) y).1)
rw [primePowerCompletedGroupAlgebraProjection_add,
primePowerCompletedGroupAlgebraProjection_ofAugmentationIdeal,
primePowerCompletedGroupAlgebraProjection_ofAugmentationIdeal]
rfl
map_smul' := by
intro a x
apply (primePowerCompletedGroupAlgebraSystem ℓ G).ext
intro i
change (((primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
primePowerCompletedGroupAlgebraAugmentationIdealProjection
(ℓ := ℓ) (G := G) i x :
primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i) :
PrimePowerCompletedGroupAlgebraStage ℓ G i) =
primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
(a • (ofPrimePowerCompletedGroupAlgebraAugmentationIdeal
(ℓ := ℓ) (G := G) x).1)
rw [primePowerCompletedGroupAlgebraProjection_smul,
primePowerCompletedGroupAlgebraProjection_ofAugmentationIdeal]
rflThe canonical inclusion of the inverse-limit augmentation ideal into the prime-power completed group algebra, viewed over the completed coefficient ring.
theorem primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraCoeffLinear_apply
(x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraCoeffLinear
(ℓ := ℓ) (G := G) x =
(ofPrimePowerCompletedGroupAlgebraAugmentationIdeal
(ℓ := ℓ) (G := G) x).1The 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 primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear_injective :
Function.Injective
(primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear
(ℓ := ℓ) (G := G))The canonical linear inclusion of the completed augmentation ideal is injective.
Show proof
by
intro x y hxy
apply (primePowerCompletedGroupAlgebraAugmentationIdealLinearEquivAddSubgroup
(ℓ := ℓ) (G := G)).injective
exact
(primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear_injective
(ℓ := ℓ) (G := G)) hxyProof. 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 exact_primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear :
Function.Exact
(primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear
(ℓ := ℓ) (G := G))
(primePowerCompletedGroupAlgebraAugmentationLinear (ℓ := ℓ) (G := G))The linear inclusion of the prime-power completed augmentation ideal has image equal to the kernel of the prime-power augmentation.
Show proof
by
intro x
constructor
· intro hx
rcases
(exact_primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear
(ℓ := ℓ) (G := G) x).1 hx with
⟨y, hy⟩
refine ⟨(primePowerCompletedGroupAlgebraAugmentationIdealLinearEquivAddSubgroup
(ℓ := ℓ) (G := G)).symm y, ?_⟩
simpa [primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear] using hy
· rintro ⟨y, rfl⟩
let z :=
(primePowerCompletedGroupAlgebraAugmentationIdealLinearEquivAddSubgroup
(ℓ := ℓ) (G := G)) y
exact
(exact_primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear
(ℓ := ℓ) (G := G)
((primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear
(ℓ := ℓ) (G := G)) z)).2
⟨z, rfl⟩Proof. An element killed by augmentation is repackaged as an element of the completed augmentation ideal, and an element coming from the augmentation ideal is killed by the augmentation. This identifies the image of the inclusion with the augmentation kernel.
□theorem primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear_shortExact :
Function.Injective
(primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear
(ℓ := ℓ) (G := G)) ∧
Function.Exact
(primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear
(ℓ := ℓ) (G := G))
(primePowerCompletedGroupAlgebraAugmentationLinear (ℓ := ℓ) (G := G)) ∧
Function.Surjective
(primePowerCompletedGroupAlgebraAugmentationLinear (ℓ := ℓ) (G := G))The canonical augmentation sequence with augmentation ideal as kernel is short exact: the inclusion is injective, its image is the kernel of augmentation, and the augmentation is surjective.
Show proof
by
refine ⟨
primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear_injective
(ℓ := ℓ) (G := G),
exact_primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear
(ℓ := ℓ) (G := G),
primePowerCompletedGroupAlgebraAugmentationLinear_surjective (ℓ := ℓ) (G := G)⟩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 primePowerCompletedGroupAlgebraAugmentationCoeffLinear_surjective :
Function.Surjective
(primePowerCompletedGroupAlgebraAugmentationCoeffLinear (ℓ := ℓ) (G := G))The coefficient-linear form of the prime-power completed augmentation is surjective.
Show proof
by
simpa [primePowerCompletedGroupAlgebraAugmentationCoeffLinear] using
primePowerCompletedGroupAlgebraAugmentation_surjective (ℓ := ℓ) (G := G)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 primePowerCompletedGAAugmentationIdealToGACoeffLinear_inj :
Function.Injective
(primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraCoeffLinear
(ℓ := ℓ) (G := G))The canonical linear inclusion of the completed augmentation ideal is injective.
Show proof
by
intro x y hxy
apply primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear_injective
(ℓ := ℓ) (G := G)
simpa [primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraCoeffLinear,
primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear] using hxyProof. 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 exact_primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraCoeffLinear :
Function.Exact
(primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraCoeffLinear
(ℓ := ℓ) (G := G))
(primePowerCompletedGroupAlgebraAugmentationCoeffLinear (ℓ := ℓ) (G := G))The coefficient-linear inclusion of the prime-power completed augmentation ideal has image equal to the kernel of the coefficient-linear augmentation.
Show proof
by
simpa [primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraCoeffLinear,
primePowerCompletedGroupAlgebraAugmentationCoeffLinear,
primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear,
primePowerCompletedGroupAlgebraAugmentationLinear]
using
exact_primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraLinear
(ℓ := ℓ) (G := G)Proof. This is the coefficient-linear restatement of the corresponding \(\mathbb{Z}\)-linear exactness result. Unfold the coefficient-linear maps and reuse the exactness of the canonical inclusion followed by the prime-power augmentation.
□theorem primePowerCompletedGAAugmentationIdealToGACoeffLinear_shortExact :
Function.Injective
(primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraCoeffLinear
(ℓ := ℓ) (G := G)) ∧
Function.Exact
(primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraCoeffLinear
(ℓ := ℓ) (G := G))
(primePowerCompletedGroupAlgebraAugmentationCoeffLinear (ℓ := ℓ) (G := G)) ∧
Function.Surjective
(primePowerCompletedGroupAlgebraAugmentationCoeffLinear (ℓ := ℓ) (G := G))The canonical augmentation sequence with augmentation ideal as kernel is short exact: the inclusion is injective, its image is the kernel of augmentation, and the augmentation is surjective.
Show proof
by
refine ⟨
primePowerCompletedGAAugmentationIdealToGACoeffLinear_inj
(ℓ := ℓ) (G := G),
exact_primePowerCompletedGroupAlgebraAugmentationIdealToGroupAlgebraCoeffLinear
(ℓ := ℓ) (G := G),
primePowerCompletedGroupAlgebraAugmentationCoeffLinear_surjective (ℓ := ℓ) (G := G)⟩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.
□