CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Augmentation.Abstract
This module develops the maps induced by continuous homomorphisms. It organizes the relevant quotient pullbacks and finite-stage maps, then proves the compatibility statements needed for the completed construction.
Imported by
- CompletedGroupAlgebra
- CompletedGroupAlgebra.ProfiniteModules
- CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra
- CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Augmentation
- CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Augmentation.Completed
- FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.FiniteStage
noncomputable def groupAlgebraAugmentation
(R : Type u) (G : Type v) [CommRing R] [Group G] :
MonoidAlgebra R G →+* R :=
(MonoidAlgebra.lift R R G (1 : MonoidHom G R)).toRingHomThe augmentation map \(R[G] \to R\), sending every group-like basis element to \(1\).
theorem groupAlgebraAugmentation_of
(R : Type u) (G : Type v) [CommRing R] [Group G] (g : G) :
groupAlgebraAugmentation R G (MonoidAlgebra.of R G g) = 1On a group-like basis element, the abstract augmentation is 1.
Show proof
by
simp only [groupAlgebraAugmentation, AlgHom.toRingHom_eq_coe, MonoidAlgebra.of_apply, RingHom.coe_coe,
MonoidAlgebra.lift_single, MonoidHom.one_apply, smul_eq_mul, mul_one]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 groupAlgebraAugmentation_single
(R : Type u) (G : Type v) [CommRing R] [Group G] (g : G) (r : R) :
groupAlgebraAugmentation R G (MonoidAlgebra.single g r) = rOn a finitely supported singleton, the abstract augmentation returns its coefficient.
Show proof
by
simp only [groupAlgebraAugmentation, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, MonoidAlgebra.lift_single,
MonoidHom.one_apply, smul_eq_mul, mul_one]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 groupAlgebraAugmentation_algebraMap
(R : Type u) (G : Type v) [CommRing R] [Group G] (r : R) :
groupAlgebraAugmentation R G (algebraMap R (MonoidAlgebra R G) r) = rThe abstract augmentation restricts to the identity on coefficient scalars.
Show proof
by
simp only [groupAlgebraAugmentation, AlgHom.toRingHom_eq_coe, MonoidAlgebra.coe_algebraMap,
Algebra.algebraMap_self, RingHom.coe_id, Function.comp_apply, id_eq, RingHom.coe_coe, MonoidAlgebra.lift_single,
MonoidHom.one_apply, smul_eq_mul, mul_one]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 groupAlgebraAugmentation_surjective
(R : Type u) (G : Type v) [CommRing R] [Group G] :
Function.Surjective (groupAlgebraAugmentation R G)The abstract group-algebra augmentation is split by the coefficient inclusion.
Show proof
by
intro r
refine ⟨algebraMap R (MonoidAlgebra R G) r, ?_⟩
simp only [MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self, RingHom.coe_id, Function.comp_apply, id_eq,
groupAlgebraAugmentation_single]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.
□noncomputable def groupAlgebraAugmentationLinearMap
(R : Type u) (G : Type v) [CommRing R] [Group G] :
MonoidAlgebra R G →ₗ[R] R where
toFun := groupAlgebraAugmentation R G
map_add' := by
intro x y
exact map_add (groupAlgebraAugmentation R G) x y
map_smul' := by
intro r x
simp only [Algebra.smul_def, MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self, RingHom.coe_id,
Function.comp_apply, id_eq, map_mul, groupAlgebraAugmentation_single, RingHom.id_apply]The augmentation map \(R[G] \to R\) is viewed as an \(R\)-linear map.
theorem groupAlgebraAugmentationLinearMap_apply
(R : Type u) (G : Type v) [CommRing R] [Group G] (x : MonoidAlgebra R G) :
groupAlgebraAugmentationLinearMap R G x = groupAlgebraAugmentation R 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. 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 groupAlgebraAugmentationLinearMap_surjective
(R : Type u) (G : Type v) [CommRing R] [Group G] :
Function.Surjective (groupAlgebraAugmentationLinearMap R G)The \(R\)-linear augmentation is split by the coefficient inclusion.
Show proof
by
simpa [groupAlgebraAugmentationLinearMap] using groupAlgebraAugmentation_surjective R GProof. 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 groupAlgebraAugmentationIdeal
(R : Type u) (G : Type v) [CommRing R] [Group G] :
Ideal (MonoidAlgebra R G) :=
RingHom.ker (groupAlgebraAugmentation R G)The augmentation ideal of an abstract group algebra.
noncomputable def groupAlgebraAugmentationIdealSubmodule
(R : Type u) (G : Type v) [CommRing R] [Group G] :
Submodule R (MonoidAlgebra R G) :=
(groupAlgebraAugmentationIdeal R G).restrictScalars RThe augmentation ideal of an abstract group algebra, regarded as an \(R\)-submodule.
theorem mem_groupAlgebraAugmentationIdeal_iff
(R : Type u) (G : Type v) [CommRing R] [Group G] (x : MonoidAlgebra R G) :
x ∈ groupAlgebraAugmentationIdeal R G ↔ groupAlgebraAugmentation R G x = 0An abstract group-algebra element lies in the augmentation ideal iff its 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 mem_groupAlgebraAugmentationIdealSubmodule_iff
(R : Type u) (G : Type v) [CommRing R] [Group G] (x : MonoidAlgebra R G) :
x ∈ groupAlgebraAugmentationIdealSubmodule R G ↔ groupAlgebraAugmentation R G x = 0An abstract group-algebra element lies in the augmentation ideal submodule iff its 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 groupAlgebraAugmentationIdeal_subtype_injective
(R : Type u) (G : Type v) [CommRing R] [Group G] :
Function.Injective
(fun x : groupAlgebraAugmentationIdeal R G => (x : MonoidAlgebra R G))The inclusion of the abstract augmentation ideal into the group algebra 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_groupAlgebraAugmentationIdeal_subtype
(R : Type u) (G : Type v) [CommRing R] [Group G] :
Function.Exact
(fun x : groupAlgebraAugmentationIdeal R G => (x : MonoidAlgebra R G))
(groupAlgebraAugmentation R G)The abstract augmentation ideal is exactly the kernel of the 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 groupAlgebraAugmentation_shortExact
(R : Type u) (G : Type v) [CommRing R] [Group G] :
Function.Injective
(fun x : groupAlgebraAugmentationIdeal R G => (x : MonoidAlgebra R G)) ∧
Function.Exact
(fun x : groupAlgebraAugmentationIdeal R G => (x : MonoidAlgebra R G))
(groupAlgebraAugmentation R G) ∧
Function.Surjective (groupAlgebraAugmentation R 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
exact ⟨groupAlgebraAugmentationIdeal_subtype_injective R G,
exact_groupAlgebraAugmentationIdeal_subtype R G,
groupAlgebraAugmentation_surjective 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.
□noncomputable def groupAlgebraAugmentationIdealSubmoduleSubtypeLinearMap
(R : Type u) (G : Type v) [CommRing R] [Group G] :
groupAlgebraAugmentationIdealSubmodule R G →ₗ[R] MonoidAlgebra R G :=
(groupAlgebraAugmentationIdealSubmodule R G).subtypeThe inclusion of the abstract augmentation ideal into the group algebra as an \(R\)-linear map.
theorem groupAlgebraAugmentationIdealSubmoduleSubtypeLinearMap_injective
(R : Type u) (G : Type v) [CommRing R] [Group G] :
Function.Injective (groupAlgebraAugmentationIdealSubmoduleSubtypeLinearMap R G)The subtype linear map from the abstract augmentation-ideal submodule into the group algebra is injective.
Show proof
by
intro x y hxy
exact Subtype.ext hxyProof. This is the injectivity of the subtype map for the augmentation-ideal submodule: two submodule elements are equal once their underlying group-algebra elements are equal.
□theorem exact_groupAlgebraAugmentationIdealSubmoduleSubtypeLinearMap
(R : Type u) (G : Type v) [CommRing R] [Group G] :
Function.Exact
(groupAlgebraAugmentationIdealSubmoduleSubtypeLinearMap R G)
(groupAlgebraAugmentationLinearMap R G)The abstract augmentation ideal is the kernel of the \(R\)-linear 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 groupAlgebraAugmentationLinearMap_shortExact
(R : Type u) (G : Type v) [CommRing R] [Group G] :
Function.Injective (groupAlgebraAugmentationIdealSubmoduleSubtypeLinearMap R G) ∧
Function.Exact
(groupAlgebraAugmentationIdealSubmoduleSubtypeLinearMap R G)
(groupAlgebraAugmentationLinearMap R G) ∧
Function.Surjective (groupAlgebraAugmentationLinearMap R 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
exact ⟨groupAlgebraAugmentationIdealSubmoduleSubtypeLinearMap_injective R G,
exact_groupAlgebraAugmentationIdealSubmoduleSubtypeLinearMap R G,
groupAlgebraAugmentationLinearMap_surjective 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.
□noncomputable def groupAlgebraAugmentationGenerator
(R : Type u) (G : Type v) [CommRing R] [Group G] (g : G) :
MonoidAlgebra R G :=
MonoidAlgebra.of R G g - 1The standard generator \(g-1\) of the abstract augmentation ideal.
noncomputable def groupAlgebraAugmentationGeneratorIdeal
(R : Type u) (G : Type v) [CommRing R] [Group G] :
Ideal (MonoidAlgebra R G) :=
Ideal.span (Set.range (groupAlgebraAugmentationGenerator R G))The ideal generated by the standard abstract augmentation generators \(g-1\).
theorem groupAlgebraAugmentationGenerator_mem_augmentationIdeal
(R : Type u) (G : Type v) [CommRing R] [Group G] (g : G) :
groupAlgebraAugmentationGenerator R G g ∈ groupAlgebraAugmentationIdeal R GA standard abstract augmentation generator lies in the augmentation ideal.
Show proof
by
simp only [groupAlgebraAugmentationGenerator, MonoidAlgebra.of_apply, mem_groupAlgebraAugmentationIdeal_iff,
map_sub, groupAlgebraAugmentation_single, map_one, sub_self]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 groupAlgebraAugmentationGenerator_mem_generatorIdeal
(R : Type u) (G : Type v) [CommRing R] [Group G] (g : G) :
groupAlgebraAugmentationGenerator R G g ∈
groupAlgebraAugmentationGeneratorIdeal R GA standard abstract augmentation generator lies in the ideal generated by such generators.
Show proof
by
exact Ideal.subset_span ⟨g, rfl⟩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 groupAlgebraAugmentationGeneratorIdeal_le_augmentationIdeal
(R : Type u) (G : Type v) [CommRing R] [Group G] :
groupAlgebraAugmentationGeneratorIdeal R G ≤ groupAlgebraAugmentationIdeal R GThe standard-generator ideal is contained in the abstract augmentation ideal.
Show proof
by
refine Ideal.span_le.2 ?_
rintro _ ⟨g, rfl⟩
exact groupAlgebraAugmentationGenerator_mem_augmentationIdeal R G gProof. 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 exists_mem_groupAlgebraAugmentationGeneratorIdeal_add
(R : Type u) (G : Type v) [CommRing R] [Group G] (x : MonoidAlgebra R G) :
∃ y ∈ groupAlgebraAugmentationGeneratorIdeal R G,
x = y + algebraMap R (MonoidAlgebra R G) (groupAlgebraAugmentation R G x)Every abstract group-algebra element differs from its augmentation scalar by an element of the standard-generator ideal.
Show proof
by
refine MonoidAlgebra.induction_on
(p := fun x : MonoidAlgebra R G =>
∃ y ∈ groupAlgebraAugmentationGeneratorIdeal R G,
x = y + algebraMap R (MonoidAlgebra R G) (groupAlgebraAugmentation R G x))
x ?_ ?_ ?_
· intro g
refine
⟨groupAlgebraAugmentationGenerator R G g,
groupAlgebraAugmentationGenerator_mem_generatorIdeal R G g, ?_⟩
rw [groupAlgebraAugmentationGenerator, groupAlgebraAugmentation_of]
change MonoidAlgebra.of R G g =
(MonoidAlgebra.of R G g - 1) +
algebraMap R (MonoidAlgebra R G) (1 : R)
rw [map_one]
rw [sub_add_cancel]
· intro x z hx hz
rcases hx with ⟨y, hy, hxy⟩
rcases hz with ⟨w, hw, hwz⟩
refine ⟨y + w, (groupAlgebraAugmentationGeneratorIdeal R G).add_mem hy hw, ?_⟩
have hy0 : groupAlgebraAugmentation R G y = 0 :=
(mem_groupAlgebraAugmentationIdeal_iff R G y).1
(groupAlgebraAugmentationGeneratorIdeal_le_augmentationIdeal R G hy)
have hw0 : groupAlgebraAugmentation R G w = 0 :=
(mem_groupAlgebraAugmentationIdeal_iff R G w).1
(groupAlgebraAugmentationGeneratorIdeal_le_augmentationIdeal R G hw)
rw [hxy, hwz, map_add]
simp only [MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self, RingHom.coe_id, Function.comp_apply, id_eq,
add_left_comm, add_assoc, map_add, hy0, groupAlgebraAugmentation_single, zero_add, hw0]
· intro r x hx
rcases hx with ⟨y, hy, hxy⟩
refine ⟨r • y, ?_, ?_⟩
· have hy' :
algebraMap R (MonoidAlgebra R G) r * y ∈
groupAlgebraAugmentationGeneratorIdeal R G :=
(groupAlgebraAugmentationGeneratorIdeal R G).mul_mem_left _ hy
simpa [Algebra.smul_def] using hy'
· have hy0 : groupAlgebraAugmentation R G y = 0 :=
(mem_groupAlgebraAugmentationIdeal_iff R G y).1
(groupAlgebraAugmentationGeneratorIdeal_le_augmentationIdeal R G hy)
rw [hxy, smul_add]
simp only [Algebra.smul_def, MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self, RingHom.coe_id,
Function.comp_apply, id_eq, MonoidAlgebra.single_mul_single, mul_one, map_add, map_mul,
groupAlgebraAugmentation_single, hy0, mul_zero, zero_add]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 groupAlgebraAugmentationGeneratorIdeal_eq_augmentationIdeal
(R : Type u) (G : Type v) [CommRing R] [Group G] :
groupAlgebraAugmentationGeneratorIdeal R G = groupAlgebraAugmentationIdeal R GThe abstract augmentation ideal is generated by the standard elements \(g-1\).
Show proof
by
refine le_antisymm
(groupAlgebraAugmentationGeneratorIdeal_le_augmentationIdeal R G) ?_
intro x hx
rcases exists_mem_groupAlgebraAugmentationGeneratorIdeal_add R G x with ⟨y, hy, hxy⟩
have haug : groupAlgebraAugmentation R G x = 0 :=
(mem_groupAlgebraAugmentationIdeal_iff R G x).1 hx
rw [hxy, haug]
simpa using hyProof. 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 groupAlgebraAugmentationGeneratorSubtype
(R : Type u) (G : Type v) [CommRing R] [Group G] (g : G) :
groupAlgebraAugmentationIdeal R G :=
⟨groupAlgebraAugmentationGenerator R G g,
groupAlgebraAugmentationGenerator_mem_augmentationIdeal R G g⟩The standard generators \(g-1\), viewed inside the augmentation ideal.
theorem groupAlgebraAugmentationGeneratorSubtype_span_eq_top
(R : Type u) (G : Type v) [CommRing R] [Group G] :
Submodule.span (MonoidAlgebra R G)
(Set.range (groupAlgebraAugmentationGeneratorSubtype R G)) = ⊤The augmentation ideal is spanned by the standard generators viewed in the ideal itself.
Show proof
by
have hspan :
Submodule.span (MonoidAlgebra R G)
(Set.range fun g =>
(⟨groupAlgebraAugmentationGenerator R G g,
groupAlgebraAugmentationGenerator_mem_augmentationIdeal R G g⟩ :
groupAlgebraAugmentationIdeal R G)) = ⊤ := by
rw [Submodule.span_range_subtype_eq_top_iff
(p := groupAlgebraAugmentationIdeal R G)
(s := groupAlgebraAugmentationGenerator R G)
(hs := groupAlgebraAugmentationGenerator_mem_augmentationIdeal R G)]
simpa [groupAlgebraAugmentationGeneratorIdeal] using
congrArg
(fun I : Ideal (MonoidAlgebra R G) =>
(I : Submodule (MonoidAlgebra R G) (MonoidAlgebra R G)))
(groupAlgebraAugmentationGeneratorIdeal_eq_augmentationIdeal R G)
simpa [groupAlgebraAugmentationGeneratorSubtype] using hspanProof. 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_augmentation_apply_eq_sum
(R : Type u) (G : Type v) [CommRing R] [Group G] [Finite G]
(x : MonoidAlgebra R G) :
letI : Fintype GOn a finite group algebra, the augmentation is the finite sum of coordinates.
Show proof
Fintype.ofFinite G
groupAlgebraAugmentation R G x = ∑ g : G, x g := by
classical
letI : Fintype G := Fintype.ofFinite G
calc
groupAlgebraAugmentation R G x = x.sum (fun _ r => r) := by
simp only [groupAlgebraAugmentation, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, MonoidAlgebra.lift_apply,
MonoidHom.one_apply, smul_eq_mul, mul_one]
_ = ∑ g : G, x g := by
exact Finsupp.sum_fintype x (fun _ r => r) (by intro g; simp only)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_algebraMap_continuous
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
[Group G] [Finite G] :
letI : TopologicalSpace (MonoidAlgebra R G)The coefficient inclusion into a finite-stage group algebra is continuous for the product topology.
Show proof
finiteGroupAlgebraTopology R G
Continuous (algebraMap R (MonoidAlgebra R G)) := by
classical
letI : Fintype G := Fintype.ofFinite G
letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
let e : MonoidAlgebra R G ≃ (G → R) := Finsupp.equivFunOnFinite
have he : Topology.IsInducing (e : MonoidAlgebra R G → G → R) :=
Topology.IsInducing.induced e
rw [he.continuous_iff]
apply continuous_pi
intro g
change Continuous fun r : R => (algebraMap R (MonoidAlgebra R G) r) g
by_cases hg : g = 1
· subst g
simpa [MonoidAlgebra.coe_algebraMap] using (continuous_id : Continuous fun r : R => r)
· rw [show (fun r : R => (algebraMap R (MonoidAlgebra R G) r) g) =
(fun _ : R => 0) from by
funext r
simp only [MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self, RingHom.coe_id, Function.comp_apply, id_eq,
ne_eq, hg, not_false_eq_true, Finsupp.single_eq_of_ne]]
exact continuous_constProof. 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_augmentation_continuous
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
[Group G] [Finite G] :
letI : TopologicalSpace (MonoidAlgebra R G)The augmentation map is continuous on each finite-stage group algebra.
Show proof
finiteGroupAlgebraTopology R G
Continuous (groupAlgebraAugmentation R G) := by
classical
letI : Fintype G := Fintype.ofFinite G
letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
change Continuous (fun x : MonoidAlgebra R G => groupAlgebraAugmentation R G x)
rw [show (fun x : MonoidAlgebra R G => groupAlgebraAugmentation R G x) =
(fun x : MonoidAlgebra R G => ∑ g : G, x g) from by
funext x
exact finiteGroupAlgebra_augmentation_apply_eq_sum R G x]
apply continuous_finset_sum
intro g _hg
exact finiteGroupAlgebra_coordinate_continuous R G gProof. 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 groupAlgebraAugmentation_mapDomainRingHom
(R : Type u) (G : Type v) (H : Type w) [CommRing R] [Group G] [Group H]
(φ : G →* H) (x : MonoidAlgebra R G) :
groupAlgebraAugmentation R H (MonoidAlgebra.mapDomainRingHom R φ x) =
groupAlgebraAugmentation R G xThe augmentation is natural for the finite-stage group-algebra functor.
Show proof
by
have hhom :
(groupAlgebraAugmentation R H).comp (MonoidAlgebra.mapDomainRingHom R φ) =
groupAlgebraAugmentation R G :=
MonoidAlgebra.ringHom_ext
(f := (groupAlgebraAugmentation R H).comp (MonoidAlgebra.mapDomainRingHom R φ))
(g := groupAlgebraAugmentation R G)
(by intro r; simp only [groupAlgebraAugmentation, AlgHom.toRingHom_eq_coe, RingHom.coe_comp, RingHom.coe_coe,
Function.comp_apply, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single, map_one,
MonoidAlgebra.lift_single, smul_eq_mul, mul_one])
(by intro g; simp only [groupAlgebraAugmentation, AlgHom.toRingHom_eq_coe, RingHom.coe_comp, RingHom.coe_coe,
Function.comp_apply, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single, MonoidAlgebra.lift_single,
MonoidHom.one_apply, smul_eq_mul, mul_one])
exact congrArg (fun f : MonoidAlgebra R G →+* R => f x) hhomProof. 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 groupAlgebraAugmentation_mapRangeRingHom
(R : Type u) (S : Type w) (G : Type v) [CommRing R] [CommRing S] [Group G]
(f : R →+* S) (x : MonoidAlgebra R G) :
groupAlgebraAugmentation S G (MonoidAlgebra.mapRangeRingHom G f x) =
f (groupAlgebraAugmentation R G x)The augmentation is natural in the coefficient ring.
Show proof
by
have hhom :
(groupAlgebraAugmentation S G).comp (MonoidAlgebra.mapRangeRingHom G f) =
f.comp (groupAlgebraAugmentation R G) :=
MonoidAlgebra.ringHom_ext
(f := (groupAlgebraAugmentation S G).comp (MonoidAlgebra.mapRangeRingHom G f))
(g := f.comp (groupAlgebraAugmentation R G))
(by intro r; simp only [groupAlgebraAugmentation, AlgHom.toRingHom_eq_coe, RingHom.coe_comp, RingHom.coe_coe,
Function.comp_apply, MonoidAlgebra.mapRangeRingHom_single, MonoidAlgebra.lift_single, MonoidHom.one_apply,
smul_eq_mul, mul_one])
(by intro g; simp only [groupAlgebraAugmentation, AlgHom.toRingHom_eq_coe, RingHom.coe_comp, RingHom.coe_coe,
Function.comp_apply, MonoidAlgebra.mapRangeRingHom_single, map_one, MonoidAlgebra.lift_single, MonoidHom.one_apply,
smul_eq_mul, mul_one])
exact congrArg (fun h : MonoidAlgebra R G →+* S => h x) hhomProof. 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.
□