CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.UnitRepresentation
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.
noncomputable def groupAlgebraUnitRepresentation
(R : Type u) (G : Type v) [CommRing R] [Group G] :
G →* (MonoidAlgebra R G)ˣ where
toFun g :=
{ val := MonoidAlgebra.of R G g
inv := MonoidAlgebra.of R G g⁻¹
val_inv := by
rw [← map_mul]
simp only [MonoidAlgebra.of, mul_inv_cancel, MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.one_def]
inv_val := by
rw [← map_mul]
simp only [MonoidAlgebra.of, inv_mul_cancel, MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.one_def]}
map_one' := by
ext x
simp only [MonoidAlgebra.of, MonoidHom.coe_mk, OneHom.coe_mk, Units.val_one, MonoidAlgebra.one_def]
map_mul' := by
intro g h
ext x
simp only [MonoidAlgebra.of, MonoidHom.coe_mk, OneHom.coe_mk, Units.val_mul, MonoidAlgebra.single_mul_single,
mul_one]The canonical embedding of a group into the units of its abstract group algebra.
theorem groupAlgebraUnitRepresentation_val
(R : Type u) (G : Type v) [CommRing R] [Group G] (g : G) :
((groupAlgebraUnitRepresentation R G g : (MonoidAlgebra R G)ˣ) :
MonoidAlgebra R G) = MonoidAlgebra.of R G gThe value of the abstract unit representation is the corresponding group-like basis element.
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.
□noncomputable def completedGroupAlgebraUnitRepresentation
(R : Type u) (G : Type v) (RG : Type w) [CommRing R] [Group G] [Ring RG]
(dense : MonoidAlgebra R G →+* RG) : G →* RGˣ :=
(Units.map dense.toMonoidHom).comp (groupAlgebraUnitRepresentation R G)A completed group algebra model receives the canonical unit representation of \(G\) through the dense abstract group-algebra map.
theorem completedGroupAlgebraUnitRepresentation_val
(R : Type u) (G : Type v) (RG : Type w) [CommRing R] [Group G] [Ring RG]
(dense : MonoidAlgebra R G →+* RG) (g : G) :
((completedGroupAlgebraUnitRepresentation R G RG dense g : RGˣ) : RG) =
dense (MonoidAlgebra.of R G g)The value of the completed unit representation is the dense image of the group-like basis element.
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 completedGroupAlgebraAugmentation_unitRepresentation_val
(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) (g : G) :
completedGroupAlgebraAugmentation R G RG haug
((completedGroupAlgebraUnitRepresentation R G RG dense g : RGˣ) : RG) = 1The completed unit representation has augmentation 1.
Show proof
by
have h := congrArg (fun f : RingHom (MonoidAlgebra R G) R => f (MonoidAlgebra.of R G g))
(completedGroupAlgebraAugmentation_comp_dense 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 completedGroupAlgebra_unit_sub_one_mem_augmentationIdeal
(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) (g : G) :
((completedGroupAlgebraUnitRepresentation R G RG dense g : RGˣ) : RG) - 1 ∈
completedGroupAlgebraAugmentationIdeal R G RG haugThe completed group-like difference \(g-1\) lies in the completed augmentation ideal.
Show proof
by
change completedGroupAlgebraAugmentation R G RG haug
(((completedGroupAlgebraUnitRepresentation R G RG dense g : RGˣ) : RG) - 1) = 0
rw [map_sub, completedGroupAlgebraAugmentation_unitRepresentation_val R G RG haug g, 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.
□noncomputable def unitRepresentationDistribMulAction
(G : Type u) (S : Type v) (A : Type w) [Group G] [Ring S] [AddCommGroup A]
[Module S A] (ρ : G →* Sˣ) : DistribMulAction G A where
smul g a := ((ρ g : Sˣ) : S) • a
one_smul := by
intro a
change (((ρ (1 : G) : Sˣ) : S) • a) = a
rw [map_one]
exact one_smul S a
mul_smul := by
intro g h a
change (((ρ (g * h) : Sˣ) : S) • a) =
(((ρ g : Sˣ) : S) • (((ρ h : Sˣ) : S) • a))
rw [map_mul]
exact mul_smul (((ρ g : Sˣ) : S)) (((ρ h : Sˣ) : S)) a
smul_zero := by
intro g
change (((ρ g : Sˣ) : S) • (0 : A)) = 0
exact smul_zero (((ρ g : Sˣ) : S))
smul_add := by
intro g a b
change (((ρ g : Sˣ) : S) • (a + b)) =
((ρ g : Sˣ) : S) • a + ((ρ g : Sˣ) : S) • b
exact smul_add (((ρ g : Sˣ) : S)) a bPull back a ring-module structure along a unit representation of a group. This is the algebraic core of Proposition 5.3.6(a).
theorem unitRepresentation_continuousSMul
(G : Type u) (S : Type v) (A : Type w) [Group G] [TopologicalSpace G] [Ring S]
[TopologicalSpace S] [AddCommGroup A] [TopologicalSpace A] [Module S A]
[ContinuousSMul S A] (ρ : G →* Sˣ)
(hρ : Continuous fun g : G => ((ρ g : Sˣ) : S)) :
letI : DistribMulAction G AThe pulled-back action is continuous whenever the unit representation is continuous after forgetting to the coefficient ring.
Show proof
unitRepresentationDistribMulAction G S A ρ
ContinuousSMul G A := by
letI : DistribMulAction G A := unitRepresentationDistribMulAction G S A ρ
refine ContinuousSMul.mk ?_
dsimp [unitRepresentationDistribMulAction]
have hpair : Continuous fun p : G × A => (((ρ p.1 : Sˣ) : S), p.2) :=
(hρ.comp continuous_fst).prodMk continuous_snd
exact (show Continuous (fun p : S × A => p.1 • p.2) from continuous_smul).comp hpairProof. 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_module_induces_continuous_gmodule
(R : Type u) (G : Type v) (A : Type w) [CommRing R] [TopologicalSpace R]
[Group G] [TopologicalSpace G] [Finite G] [DiscreteTopology G]
[AddCommGroup A] [TopologicalSpace A] [Module (MonoidAlgebra R G) A]
(hsmul : letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
ContinuousSMul (MonoidAlgebra R G) A) :
letI : TopologicalSpace (MonoidAlgebra R G)Finite-stage version of Proposition 5.3.6(a): a module over the finite group algebra inherits the continuous \(G\)-module structure coming from the canonical group-like units.
Show proof
finiteGroupAlgebraTopology R G
letI : DistribMulAction G A :=
unitRepresentationDistribMulAction G (MonoidAlgebra R G) A
(groupAlgebraUnitRepresentation R G)
ContinuousSMul G A := by
classical
letI : Fintype G := Fintype.ofFinite G
letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
letI : ContinuousSMul (MonoidAlgebra R G) A := hsmul
letI : DistribMulAction G A :=
unitRepresentationDistribMulAction G (MonoidAlgebra R G) A
(groupAlgebraUnitRepresentation R G)
exact unitRepresentation_continuousSMul G (MonoidAlgebra R G) A
(groupAlgebraUnitRepresentation R G) continuous_of_discreteTopologyProof. 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 completedGroupAlgebra_module_induces_gmodule
(R : Type u) (G : Type v) (RG A : Type w) [CommRing R] [Group G] [Ring RG]
[AddCommGroup A] [Module RG A] (dense : MonoidAlgebra R G →+* RG) :
Nonempty (DistribMulAction G A)Proposition 5.3.6(a), model-independent form: a module over a completed group algebra inherits the natural algebraic \(G\)-module structure.
Show proof
by
exact ⟨unitRepresentationDistribMulAction G RG A
(completedGroupAlgebraUnitRepresentation R G RG dense)⟩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 completedGroupAlgebra_module_induces_continuous_gmodule
(R : Type u) (G : Type v) (RG A : Type w) [CommRing R] [TopologicalSpace G]
[Group G] [Ring RG] [TopologicalSpace RG] [AddCommGroup A] [TopologicalSpace A]
[Module RG A] [ContinuousSMul RG A] (dense : MonoidAlgebra R G →+* RG)
(hdenseG : Continuous fun g : G => dense (MonoidAlgebra.of R G g)) :
letI : DistribMulAction G ATopological version of the unit-representation construction, once the canonical unit representation is known to be continuous after forgetting to the completed group algebra model.
Show proof
unitRepresentationDistribMulAction G RG A
(completedGroupAlgebraUnitRepresentation R G RG dense)
ContinuousSMul G A := by
exact unitRepresentation_continuousSMul G RG A
(completedGroupAlgebraUnitRepresentation R G RG dense) (by simpa using hdenseG)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.
□