CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Augmentation.Completed
noncomputable def completedGroupAlgebraCoefficientMap
(R : Type u) (G : Type v) (RG : Type w) [CommRing R] [Group G] [Ring RG]
(dense : RingHom (MonoidAlgebra R G) RG) : RingHom R RG :=
dense.comp (algebraMap R (MonoidAlgebra R G))The coefficient map \(R \to R[G]\) attached to a dense map from the abstract group algebra.
theorem completedGroupAlgebraCoefficientMap_apply
(R : Type u) (G : Type v) (RG : Type w) [CommRing R] [Group G] [Ring RG]
(dense : RingHom (MonoidAlgebra R G) RG) (r : R) :
completedGroupAlgebraCoefficientMap R G RG dense r =
dense (algebraMap R (MonoidAlgebra R G) r)The coefficient-change map is evaluated coordinatewise: the support in the finite quotient is unchanged and every coefficient is carried through the given ring homomorphism.
Show proof
rflProof. Reduce to the finite group-algebra stage. The finite group supplies a finite discrete basis, and the profinite coefficient ring controls the topology through its open ideals and finite quotients. The augmentation, group-like, functoriality, and continuity formulas are checked on basis elements and extended by additivity, linearity, or multiplicativity. The product topology identifies the finite group algebra with a finite product of coefficient modules.
□def hasCompletedGroupAlgebraAugmentation
(R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
[Group G] [Ring RG] [TopologicalSpace RG]
(dense : RingHom (MonoidAlgebra R G) RG) : Prop :=
Exists fun ε : RingHom RG R =>
And (ε.comp dense = groupAlgebraAugmentation R G) (Continuous ε)A completed group algebra model has a continuous augmentation when its dense abstract group-algebra map admits a continuous extension of the abstract augmentation.
noncomputable def completedGroupAlgebraAugmentation
(R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
[Group G] [Ring RG] [TopologicalSpace RG]
{dense : RingHom (MonoidAlgebra R G) RG}
(haug : hasCompletedGroupAlgebraAugmentation R G RG dense) : RingHom RG R :=
Classical.choose haugThe continuous augmentation extracted from completed group algebra augmentation data.
theorem completedGroupAlgebraAugmentation_comp_dense
(R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
[Group G] [Ring RG] [TopologicalSpace RG]
{dense : RingHom (MonoidAlgebra R G) RG}
(haug : hasCompletedGroupAlgebraAugmentation R G RG dense) :
(completedGroupAlgebraAugmentation R G RG haug).comp dense =
groupAlgebraAugmentation R GThe completed augmentation extends the abstract augmentation along the dense algebraic map.
Show proof
(Classical.choose_spec haug).1Proof. Reduce to the finite group-algebra stage. The finite group supplies a finite discrete basis, and the profinite coefficient ring controls the topology through its open ideals and finite quotients. The augmentation, group-like, functoriality, and continuity formulas are checked on basis elements and extended by additivity, linearity, or multiplicativity. The product topology identifies the finite group algebra with a finite product of coefficient modules.
□theorem continuous_completedGroupAlgebraAugmentation
(R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
[Group G] [Ring RG] [TopologicalSpace RG]
{dense : RingHom (MonoidAlgebra R G) RG}
(haug : hasCompletedGroupAlgebraAugmentation R G RG dense) :
Continuous (completedGroupAlgebraAugmentation R G RG haug)The augmentation extracted from the completed augmentation package is continuous.
Show proof
(Classical.choose_spec haug).2Proof. Reduce to the finite group-algebra stage. The finite group supplies a finite discrete basis, and the profinite coefficient ring controls the topology through its open ideals and finite quotients. The augmentation, group-like, functoriality, and continuity formulas are checked on basis elements and extended by additivity, linearity, or multiplicativity. The product topology identifies the finite group algebra with a finite product of coefficient modules.
□theorem completedGroupAlgebraAugmentation_comp_coefficientMap
(R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
[Group G] [Ring RG] [TopologicalSpace RG]
{dense : RingHom (MonoidAlgebra R G) RG}
(haug : hasCompletedGroupAlgebraAugmentation R G RG dense) :
(completedGroupAlgebraAugmentation R G RG haug).comp
(completedGroupAlgebraCoefficientMap R G RG dense) = RingHom.id RThe coefficient map is a section of the completed augmentation.
Show proof
by
ext r
have h := congrArg
(fun f : RingHom (MonoidAlgebra R G) R => f (algebraMap R (MonoidAlgebra R G) r))
(completedGroupAlgebraAugmentation_comp_dense R G RG haug)
simpa [completedGroupAlgebraCoefficientMap] using hProof. Reduce to the finite group-algebra stage. The finite group supplies a finite discrete basis, and the profinite coefficient ring controls the topology through its open ideals and finite quotients. The augmentation, group-like, functoriality, and continuity formulas are checked on basis elements and extended by additivity, linearity, or multiplicativity. The product topology identifies the finite group algebra with a finite product of coefficient modules.
□noncomputable def completedGroupAlgebraAugmentationIdeal
(R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
[Group G] [Ring RG] [TopologicalSpace RG]
{dense : RingHom (MonoidAlgebra R G) RG}
(haug : hasCompletedGroupAlgebraAugmentation R G RG dense) : Ideal RG :=
RingHom.ker (completedGroupAlgebraAugmentation R G RG haug)The augmentation ideal of a completed group algebra model with augmentation data.
theorem mem_completedGroupAlgebraAugmentationIdeal_iff
(R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
[Group G] [Ring RG] [TopologicalSpace RG]
{dense : RingHom (MonoidAlgebra R G) RG}
(haug : hasCompletedGroupAlgebraAugmentation R G RG dense) (x : RG) :
x ∈ completedGroupAlgebraAugmentationIdeal R G RG haug ↔
completedGroupAlgebraAugmentation R G RG haug x = 0A completed finite group-algebra element lies in the completed augmentation ideal iff its completed augmentation is zero.
Show proof
Iff.rflProof. Reduce to the finite group-algebra stage. The finite group supplies a finite discrete basis, and the profinite coefficient ring controls the topology through its open ideals and finite quotients. The augmentation, group-like, functoriality, and continuity formulas are checked on basis elements and extended by additivity, linearity, or multiplicativity. The product topology identifies the finite group algebra with a finite product of coefficient modules.
□theorem completedGroupAlgebraAugmentation_surjective
(R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
[Group G] [Ring RG] [TopologicalSpace RG]
{dense : RingHom (MonoidAlgebra R G) RG}
(haug : hasCompletedGroupAlgebraAugmentation R G RG dense) :
Function.Surjective (completedGroupAlgebraAugmentation R G RG haug)The completed augmentation is split by the completed coefficient map.
Show proof
by
intro r
refine ⟨completedGroupAlgebraCoefficientMap R G RG dense r, ?_⟩
have h := congrArg (fun f : RingHom R R => f r)
(completedGroupAlgebraAugmentation_comp_coefficientMap R G RG haug)
simpa using hProof. Reduce to the finite group-algebra stage. The finite group supplies a finite discrete basis, and the profinite coefficient ring controls the topology through its open ideals and finite quotients. The augmentation, group-like, functoriality, and continuity formulas are checked on basis elements and extended by additivity, linearity, or multiplicativity. The product topology identifies the finite group algebra with a finite product of coefficient modules.
□theorem completedGroupAlgebraAugmentationIdeal_subtype_injective
(R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
[Group G] [Ring RG] [TopologicalSpace RG]
{dense : RingHom (MonoidAlgebra R G) RG}
(haug : hasCompletedGroupAlgebraAugmentation R G RG dense) :
Function.Injective
(fun x : completedGroupAlgebraAugmentationIdeal R G RG haug => (x : RG))The inclusion of the completed augmentation ideal into the completed group algebra model is injective.
Show proof
by
intro x y hxy
exact Subtype.ext hxyProof. Reduce to the finite group-algebra stage. The finite group supplies a finite discrete basis, and the profinite coefficient ring controls the topology through its open ideals and finite quotients. The augmentation, group-like, functoriality, and continuity formulas are checked on basis elements and extended by additivity, linearity, or multiplicativity. The product topology identifies the finite group algebra with a finite product of coefficient modules.
□theorem exact_completedGroupAlgebraAugmentationIdeal_subtype
(R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
[Group G] [Ring RG] [TopologicalSpace RG]
{dense : RingHom (MonoidAlgebra R G) RG}
(haug : hasCompletedGroupAlgebraAugmentation R G RG dense) :
Function.Exact
(fun x : completedGroupAlgebraAugmentationIdeal R G RG haug => (x : RG))
(completedGroupAlgebraAugmentation R G RG haug)The completed augmentation ideal is exactly the kernel of the completed augmentation.
Show proof
by
intro x
constructor
· intro hx
exact ⟨⟨x, hx⟩, rfl⟩
· rintro ⟨y, rfl⟩
exact y.2Proof. Reduce to the finite group-algebra stage. The finite group supplies a finite discrete basis, and the profinite coefficient ring controls the topology through its open ideals and finite quotients. The augmentation, group-like, functoriality, and continuity formulas are checked on basis elements and extended by additivity, linearity, or multiplicativity. The product topology identifies the finite group algebra with a finite product of coefficient modules.
□theorem completedGroupAlgebraAugmentation_shortExact
(R : Type u) (G : Type v) (RG : Type w) [CommRing R] [TopologicalSpace R]
[Group G] [Ring RG] [TopologicalSpace RG]
{dense : RingHom (MonoidAlgebra R G) RG}
(haug : hasCompletedGroupAlgebraAugmentation R G RG dense) :
Function.Injective
(fun x : completedGroupAlgebraAugmentationIdeal R G RG haug => (x : RG)) ∧
Function.Exact
(fun x : completedGroupAlgebraAugmentationIdeal R G RG haug => (x : RG))
(completedGroupAlgebraAugmentation R G RG haug) ∧
Function.Surjective (completedGroupAlgebraAugmentation R G RG haug)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
exact ⟨completedGroupAlgebraAugmentationIdeal_subtype_injective R G RG haug,
exact_completedGroupAlgebraAugmentationIdeal_subtype R G RG haug,
completedGroupAlgebraAugmentation_surjective R G RG haug⟩Proof. Reduce to the finite group-algebra stage. The finite group supplies a finite discrete basis, and the profinite coefficient ring controls the topology through its open ideals and finite quotients. The augmentation, group-like, functoriality, and continuity formulas are checked on basis elements and extended by additivity, linearity, or multiplicativity. The product topology identifies the finite group algebra with a finite product of coefficient modules.
□theorem finiteGroupAlgebra_hasCompletedGroupAlgebraAugmentation
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
[Group G] [Finite G] :
letI : TopologicalSpace (MonoidAlgebra R G)In the finite-group case, the finite group algebra carries the completed augmentation data induced by the ordinary augmentation.
Show proof
finiteGroupAlgebraTopology R G
hasCompletedGroupAlgebraAugmentation R G (MonoidAlgebra R G)
(RingHom.id (MonoidAlgebra R G)) := by
letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
refine Exists.intro (groupAlgebraAugmentation R G) ?_
exact And.intro (RingHom.comp_id (groupAlgebraAugmentation R G))
(finiteGroupAlgebra_augmentation_continuous R G)Proof. Reduce to the finite group-algebra stage. The finite group supplies a finite discrete basis, and the profinite coefficient ring controls the topology through its open ideals and finite quotients. The augmentation, group-like, functoriality, and continuity formulas are checked on basis elements and extended by additivity, linearity, or multiplicativity. The product topology identifies the finite group algebra with a finite product of coefficient modules.
□