Complete group algebras

In this file we state basic definitions of complete group algebras.

We introduce the scoped notation R[ˣG] for the MonoidAlgebra.

If R is a commutative semiring, G is a topological group, s is a subset of open normal subgroups, then CompleteGroupAlgebra R G s is defined to be the Type corresponding to the subalgebra (CompleteGroupAlgebra.toSubalgebra R G s) of the background ring Π N ∈ s, R[ˣG/N] (CompleteGroupAlgebra.BackgroundRing R G s), consisting of elements satisfy certain compatibility conditions. Mathematically, it is the inverse limit of R[ˣG/N] as N runs over elements in s. We don't use category theory packages here as currently AlgebraCat doesn't support Semiring.

We introduce the scoped notationR⟦ˣG⟧ for the CompleteGroupAlgebra R G Set.univ, namely, the N is allowed to be all open normal subgroups.

The natural injection from CompleteGroupAlgebra R G s to the background ring is Subalgebra.val (CompleteGroupAlgebra.toSubalgebra R G s). Its injectivity is Subtype.val_injective, hopefully Lean will figure out what the implicit argument is. If x is an element of CompleteGroupAlgebra R G s, its image in the background ring is just x.1, and the proof that it satisfies the compatibility conditions is just x.2.

Two elements in CompleteGroupAlgebra R G s are equal, if and only if their images in the background ring are equal, if and only if their images in R[ˣG/N] are equal for all N ∈ s. To achieve this, one may use tactic ext1, resp. ext N ⟨hN⟩ : 3.

If N ∈ s, CompleteGroupAlgebra.proj R G s N is the natural projection map from CompleteGroupAlgebra R G s to R[ˣG/N]. If x is an element of CompleteGroupAlgebra R G s, then its image under this map is just x.1 N (CompleteGroupAlgebra.proj_apply).

In general, if M is a normal subgroup such that there exists some N ∈ s such that N ≤ M, then CompleteGroupAlgebra.projOfExistsLE is a map from CompleteGroupAlgebra R G s to R[ˣG/M], defined by using a random N ∈ s such that N ≤ M.

...

The universal property of R⟦ˣG⟧ is that, if there is a family of maps S → R[ˣG/N] satisfying compatibility conditions, then they lift to a map S → R⟦ˣG⟧ (CompleteGroupAlgebra.lift), and such lift is unique (CompleteGroupAlgebra.eq_lift_of_proj_comp_eq).

...

Currently we only defined the multiplicative version (i.e. no CompleteAddGroupAlgebra yet).

Things should go to mathlib

def MonoidAlgebra.«term_[ˣ_]» : Lean.TrailingParserDescr

The monoid algebra over a semiring k generated by the monoid G. It is the type of finite formal k-linear combinations of terms of G, endowed with the convolution product.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MonoidAlgebra.linearEquivOfSubsingleton (R : Type u_1) (G : Type u_2) [Semiring R] [Inhabited G] [Subsingleton G] : MonoidAlgebra R G ≃ₗ[R] R

If G has only one element, then R[ˣG] is just R.

Equations

• MonoidAlgebra.linearEquivOfSubsingleton R G = Finsupp.LinearEquiv.finsuppUnique R R G

@[simp]

theorem MonoidAlgebra.linearEquivOfSubsingleton_apply (R : Type u_1) (G : Type u_2) [Semiring R] [Inhabited G] [Subsingleton G] (x : MonoidAlgebra R G) : (linearEquivOfSubsingleton R G) x = x default

@[simp]

theorem MonoidAlgebra.linearEquivOfSubsingleton_symm_apply (R : Type u_1) (G : Type u_2) [Semiring R] [Inhabited G] [Subsingleton G] (x : R) : (linearEquivOfSubsingleton R G).symm x = single default x

theorem MonoidAlgebra.eq_single_default_of_subsingleton (R : Type u_1) (G : Type u_2) [Semiring R] [Inhabited G] [Subsingleton G] (x : MonoidAlgebra R G) : x = single default (x default)

noncomputable def MonoidAlgebra.algEquivOfSubsingleton (R : Type u_1) (G : Type u_2) [CommSemiring R] [Monoid G] [Subsingleton G] : MonoidAlgebra R G ≃ₐ[R] R

If G has only one element, then R[ˣG] is just R.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MonoidAlgebra.algEquivOfSubsingleton_apply (R : Type u_1) (G : Type u_2) [CommSemiring R] [Monoid G] [Subsingleton G] (x : MonoidAlgebra R G) : (algEquivOfSubsingleton R G) x = x 1

@[simp]

theorem MonoidAlgebra.algEquivOfSubsingleton_symm_apply (R : Type u_1) (G : Type u_2) [CommSemiring R] [Monoid G] [Subsingleton G] (x : R) : (algEquivOfSubsingleton R G).symm x = single 1 x

instance OpenNormalSubgroup.instTop (G : Type u_2) [Group G] [TopologicalSpace G] : Top (OpenNormalSubgroup G)

Equations

• OpenNormalSubgroup.instTop G = { top := let __src := ⊤; { toOpenSubgroup := __src, isNormal' := ⋯ } }

Definition of complete group algebra

@[reducible, inline]

abbrev CompleteGroupAlgebra.BackgroundRing (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) : Type (max u_2 u_1)

The background ring Π N ∈ s, R[ˣG/N] of CompleteAddGroupAlgebra.

Equations

• CompleteGroupAlgebra.BackgroundRing R G s = (⦃N : OpenNormalSubgroup G⦄ → PLift (N ∈ s) → MonoidAlgebra R (G ⧸ ↑N.toOpenSubgroup))

noncomputable def CompleteGroupAlgebra.toSubalgebra (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) : Subalgebra R (BackgroundRing R G s)

The complete group algebra as a subalgebra of BackgroundRing.

Equations

• One or more equations did not get rendered due to their size.

theorem CompleteGroupAlgebra.mem_toSubalgebra (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) {x : BackgroundRing R G s} : x ∈ toSubalgebra R G s ↔ ∀ ⦃N₁ N₂ : OpenNormalSubgroup G⦄ (hN₁ : N₁ ∈ s) (hN₂ : N₂ ∈ s) (hle : N₁ ≤ N₂), (MonoidAlgebra.mapDomainAlgHom R R (QuotientGroup.map (↑N₁.toOpenSubgroup) (↑N₂.toOpenSubgroup) (MonoidHom.id G) hle)) (x { down := hN₁ }) = x { down := hN₂ }

@[reducible, inline]

abbrev CompleteGroupAlgebra (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) : Type (max u_1 u_2)

The CompleteGroupAlgebra as a Type. The scoped notation R⟦ˣG⟧ is CompleteGroupAlgebra R G Set.univ.

Equations

• CompleteGroupAlgebra R G s = ↥(CompleteGroupAlgebra.toSubalgebra R G s)

def CompleteGroupAlgebra.«term_⟦ˣ_⟧» : Lean.TrailingParserDescr

The CompleteGroupAlgebra as a Type. The scoped notation R⟦ˣG⟧ is CompleteGroupAlgebra R G Set.univ.

Equations

• One or more equations did not get rendered due to their size.

Projection maps

noncomputable def CompleteGroupAlgebra.proj (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) {N : OpenNormalSubgroup G} (hN : N ∈ s) : CompleteGroupAlgebra R G s →ₐ[R] MonoidAlgebra R (G ⧸ ↑N.toOpenSubgroup)

The proj is the natural map from CompleteGroupAlgebra R G s to R[ˣG/N] for N ∈ s.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CompleteGroupAlgebra.proj_apply (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) {N : OpenNormalSubgroup G} (hN : N ∈ s) (x : CompleteGroupAlgebra R G s) : (proj R G s hN) x = ↑x { down := hN }

theorem CompleteGroupAlgebra.mapDomainAlgHom_comp_proj (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) {N : OpenNormalSubgroup G} (hN : N ∈ s) {N' : OpenNormalSubgroup G} (hN' : N' ∈ s) (hle : N ≤ N') : (MonoidAlgebra.mapDomainAlgHom R R (QuotientGroup.map (↑N.toOpenSubgroup) (↑N'.toOpenSubgroup) (MonoidHom.id G) hle)).comp (proj R G s hN) = proj R G s hN'

theorem CompleteGroupAlgebra.mapDomainAlgHom_comp_proj_eq_mapDomainAlgHom_comp_proj (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) {N : OpenNormalSubgroup G} (hN : N ∈ s) {N' : OpenNormalSubgroup G} (hN' : N' ∈ s) {N'' : Subgroup G} [N''.Normal] (hle : ↑N.toOpenSubgroup ≤ N'') (hle' : ↑N'.toOpenSubgroup ≤ N'') (hexists : ∃ M ∈ s, M ≤ N ∧ M ≤ N') : (MonoidAlgebra.mapDomainAlgHom R R (QuotientGroup.map (↑N.toOpenSubgroup) N'' (MonoidHom.id G) hle)).comp (proj R G s hN) = (MonoidAlgebra.mapDomainAlgHom R R (QuotientGroup.map (↑N'.toOpenSubgroup) N'' (MonoidHom.id G) hle')).comp (proj R G s hN')

theorem CompleteGroupAlgebra.mapDomainAlgHom_comp_proj_eq_mapDomainAlgHom_comp_proj' (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) {N : OpenNormalSubgroup G} (hN : N ∈ s) {N' : OpenNormalSubgroup G} (hN' : N' ∈ s) {N'' : Subgroup G} [N''.Normal] (hle : ↑N.toOpenSubgroup ≤ N'') (hle' : ↑N'.toOpenSubgroup ≤ N'') (hs : DirectedOn GE.ge s) : (MonoidAlgebra.mapDomainAlgHom R R (QuotientGroup.map (↑N.toOpenSubgroup) N'' (MonoidHom.id G) hle)).comp (proj R G s hN) = (MonoidAlgebra.mapDomainAlgHom R R (QuotientGroup.map (↑N'.toOpenSubgroup) N'' (MonoidHom.id G) hle')).comp (proj R G s hN')

noncomputable def CompleteGroupAlgebra.projOfExistsLE (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) (M : Subgroup G) [M.Normal] (hM : ∃ N ∈ s, ↑N.toOpenSubgroup ≤ M) : CompleteGroupAlgebra R G s →ₐ[R] MonoidAlgebra R (G ⧸ M)

If M is a normal subgroup such that there exists some N ∈ s such that N ≤ M, then projOfExistsLE is a map from CompleteGroupAlgebra R G s to R[ˣG/M], defined by using a random N ∈ s such that N ≤ M.

Equations

• One or more equations did not get rendered due to their size.

theorem CompleteGroupAlgebra.projOfExistsLE_eq_proj (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) {M : OpenNormalSubgroup G} (hM : M ∈ s) : projOfExistsLE R G s ↑M.toOpenSubgroup ⋯ = proj R G s hM

If M ∈ s, then the projOfExistsLE for M is equal to the proj for M.

theorem CompleteGroupAlgebra.projOfExistsLE_eq_mapDomainAlgHom_comp_proj (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) (M : Subgroup G) [M.Normal] {N : OpenNormalSubgroup G} (hN : N ∈ s) (hle : ↑N.toOpenSubgroup ≤ M) (hs : DirectedOn GE.ge s) : projOfExistsLE R G s M ⋯ = (MonoidAlgebra.mapDomainAlgHom R R (QuotientGroup.map (↑N.toOpenSubgroup) M (MonoidHom.id G) hle)).comp (proj R G s hN)

The definition of projOfExistsLE is independent of the choice of N ∈ s such that N ≤ M, provided that s is directed, i.e. for any N₁, N₂ ∈ s there exists N₃ ∈ s such that N₃ ≤ N₁ and N₃ ≤ N₂.

theorem CompleteGroupAlgebra.mapDomainAlgHom_comp_projOfExistsLE (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) (M : Subgroup G) [M.Normal] (hM : ∃ N ∈ s, ↑N.toOpenSubgroup ≤ M) (M' : Subgroup G) [M'.Normal] (hle : M ≤ M') (hs : DirectedOn GE.ge s) : (MonoidAlgebra.mapDomainAlgHom R R (QuotientGroup.map M M' (MonoidHom.id G) hle)).comp (projOfExistsLE R G s M hM) = projOfExistsLE R G s M' ⋯

noncomputable def CompleteGroupAlgebra.augmentation (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) (hs : s.Nonempty) : CompleteGroupAlgebra R G s →ₐ[R] R

If s is not empty, then augmentation is a map from CompleteGroupAlgebra R G s to R.

Equations

• CompleteGroupAlgebra.augmentation R G s hs = (↑(MonoidAlgebra.algEquivOfSubsingleton R (G ⧸ ⊤))).comp (CompleteGroupAlgebra.projOfExistsLE R G s ⊤ ⋯)

theorem CompleteGroupAlgebra.augmentation_apply_of_top_mem (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) (x : CompleteGroupAlgebra R G s) (h : ⊤ ∈ s) : (augmentation R G s ⋯) x = (↑x { down := h }) 1

Universal property of complete group algebra

noncomputable def CompleteGroupAlgebra.lift (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) {S : Type u_3} [Semiring S] [Algebra R S] (f : ⦃N : OpenNormalSubgroup G⦄ → N ∈ s → S →ₐ[R] MonoidAlgebra R (G ⧸ ↑N.toOpenSubgroup)) (hf : ∀ ⦃N₁ N₂ : OpenNormalSubgroup G⦄ (hN₁ : N₁ ∈ s) (hN₂ : N₂ ∈ s) (hle : N₁ ≤ N₂), (MonoidAlgebra.mapDomainAlgHom R R (QuotientGroup.map (↑N₁.toOpenSubgroup) (↑N₂.toOpenSubgroup) (MonoidHom.id G) hle)).comp (f hN₁) = f hN₂) : S →ₐ[R] CompleteGroupAlgebra R G s

If a family of maps S → R[ˣG/N] for N ∈ S satisfy compatibility conditions, then they lift to a map S → CompleteGroupAlgebra R G s.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CompleteGroupAlgebra.lift_apply_coe (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) {S : Type u_3} [Semiring S] [Algebra R S] {f : ⦃N : OpenNormalSubgroup G⦄ → N ∈ s → S →ₐ[R] MonoidAlgebra R (G ⧸ ↑N.toOpenSubgroup)} {hf : ∀ ⦃N₁ N₂ : OpenNormalSubgroup G⦄ (hN₁ : N₁ ∈ s) (hN₂ : N₂ ∈ s) (hle : N₁ ≤ N₂), (MonoidAlgebra.mapDomainAlgHom R R (QuotientGroup.map (↑N₁.toOpenSubgroup) (↑N₂.toOpenSubgroup) (MonoidHom.id G) hle)).comp (f hN₁) = f hN₂} (x : S) {N : OpenNormalSubgroup G} (hN : N ∈ s) : ↑((lift R G s f hf) x) { down := hN } = (f hN) x

theorem CompleteGroupAlgebra.proj_comp_lift (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) {S : Type u_3} [Semiring S] [Algebra R S] {f : ⦃N : OpenNormalSubgroup G⦄ → N ∈ s → S →ₐ[R] MonoidAlgebra R (G ⧸ ↑N.toOpenSubgroup)} {hf : ∀ ⦃N₁ N₂ : OpenNormalSubgroup G⦄ (hN₁ : N₁ ∈ s) (hN₂ : N₂ ∈ s) (hle : N₁ ≤ N₂), (MonoidAlgebra.mapDomainAlgHom R R (QuotientGroup.map (↑N₁.toOpenSubgroup) (↑N₂.toOpenSubgroup) (MonoidHom.id G) hle)).comp (f hN₁) = f hN₂} {N : OpenNormalSubgroup G} (hN : N ∈ s) : (proj R G s hN).comp (lift R G s f hf) = f hN

theorem CompleteGroupAlgebra.eq_lift_of_proj_comp_eq (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) {S : Type u_3} [Semiring S] [Algebra R S] {f : ⦃N : OpenNormalSubgroup G⦄ → N ∈ s → S →ₐ[R] MonoidAlgebra R (G ⧸ ↑N.toOpenSubgroup)} {hf : ∀ ⦃N₁ N₂ : OpenNormalSubgroup G⦄ (hN₁ : N₁ ∈ s) (hN₂ : N₂ ∈ s) (hle : N₁ ≤ N₂), (MonoidAlgebra.mapDomainAlgHom R R (QuotientGroup.map (↑N₁.toOpenSubgroup) (↑N₂.toOpenSubgroup) (MonoidHom.id G) hle)).comp (f hN₁) = f hN₂} (g : S →ₐ[R] CompleteGroupAlgebra R G s) (hg : ∀ ⦃N : OpenNormalSubgroup G⦄ (hN : N ∈ s), (proj R G s hN).comp g = f hN) : g = lift R G s f hf

The lift map S → CompleteGroupAlgebra R G s is unique.

noncomputable def CompleteGroupAlgebra.ofMonoidAlgebra (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) : MonoidAlgebra R G →ₐ[R] CompleteGroupAlgebra R G s

The natural map from R[ˣG] to CompleteGroupAlgebra R G s.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CompleteGroupAlgebra.ofMonoidAlgebra_apply_coe (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) (x : MonoidAlgebra R G) {N : OpenNormalSubgroup G} (hN : N ∈ s) : ↑((ofMonoidAlgebra R G s) x) { down := hN } = (MonoidAlgebra.mapDomainAlgHom R R (QuotientGroup.mk' ↑N.toOpenSubgroup)) x

theorem CompleteGroupAlgebra.proj_comp_ofMonoidAlgebra (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) {N : OpenNormalSubgroup G} (hN : N ∈ s) : (proj R G s hN).comp (ofMonoidAlgebra R G s) = MonoidAlgebra.mapDomainAlgHom R R (QuotientGroup.mk' ↑N.toOpenSubgroup)

theorem CompleteGroupAlgebra.projOfExistsLE_comp_ofMonoidAlgebra (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) (M : Subgroup G) [M.Normal] (hM : ∃ N ∈ s, ↑N.toOpenSubgroup ≤ M) : (projOfExistsLE R G s M hM).comp (ofMonoidAlgebra R G s) = MonoidAlgebra.mapDomainAlgHom R R (QuotientGroup.mk' M)

noncomputable def CompleteGroupAlgebra.algHomOfCoinitial (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s t : Set (OpenNormalSubgroup G)) (hs : DirectedOn GE.ge s) (hts : IsCoinitialFor t s) : CompleteGroupAlgebra R G s →ₐ[R] CompleteGroupAlgebra R G t

If s is directed and t is coinitial for s, then there is a natural map from CompleteGroupAlgebra R G s to CompleteGroupAlgebra R G t.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CompleteGroupAlgebra.algHomOfCoinitial_self (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) (hs : DirectedOn GE.ge s) : algHomOfCoinitial R G s s hs ⋯ = AlgHom.id R (CompleteGroupAlgebra R G s)

@[simp]

theorem CompleteGroupAlgebra.algHomOfCoinitial_comp (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s t u : Set (OpenNormalSubgroup G)) (hs : DirectedOn GE.ge s) (hts : IsCoinitialFor t s) (ht : DirectedOn GE.ge t) (hut : IsCoinitialFor u t) : (algHomOfCoinitial R G t u ht hut).comp (algHomOfCoinitial R G s t hs hts) = algHomOfCoinitial R G s u hs ⋯

noncomputable def CompleteGroupAlgebra.algEquivOfCoinitial (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s t : Set (OpenNormalSubgroup G)) (hs : DirectedOn GE.ge s) (hts : IsCoinitialFor t s) (ht : DirectedOn GE.ge t) (hst : IsCoinitialFor s t) : CompleteGroupAlgebra R G s ≃ₐ[R] CompleteGroupAlgebra R G t

If s, t are directed and are coinitial for each other, then there is a natural isomorphism of CompleteGroupAlgebra R G s and CompleteGroupAlgebra R G t.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CompleteGroupAlgebra.coe_algEquivOfCoinitial (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s t : Set (OpenNormalSubgroup G)) (hs : DirectedOn GE.ge s) (hts : IsCoinitialFor t s) (ht : DirectedOn GE.ge t) (hst : IsCoinitialFor s t) : ↑(algEquivOfCoinitial R G s t hs hts ht hst) = algHomOfCoinitial R G s t hs hts

@[simp]

theorem CompleteGroupAlgebra.algEquivOfCoinitial_symm (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s t : Set (OpenNormalSubgroup G)) (hs : DirectedOn GE.ge s) (hts : IsCoinitialFor t s) (ht : DirectedOn GE.ge t) (hst : IsCoinitialFor s t) : (algEquivOfCoinitial R G s t hs hts ht hst).symm = algEquivOfCoinitial R G t s ht hst hs hts

theorem CompleteGroupAlgebra.coe_algEquivOfCoinitial_symm (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s t : Set (OpenNormalSubgroup G)) (hs : DirectedOn GE.ge s) (hts : IsCoinitialFor t s) (ht : DirectedOn GE.ge t) (hst : IsCoinitialFor s t) : ↑(algEquivOfCoinitial R G s t hs hts ht hst).symm = algHomOfCoinitial R G t s ht hst

@[simp]

theorem CompleteGroupAlgebra.algEquivOfCoinitial_apply (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s t : Set (OpenNormalSubgroup G)) (hs : DirectedOn GE.ge s) (hts : IsCoinitialFor t s) (ht : DirectedOn GE.ge t) (hst : IsCoinitialFor s t) (x : CompleteGroupAlgebra R G s) : (algEquivOfCoinitial R G s t hs hts ht hst) x = (algHomOfCoinitial R G s t hs hts) x

theorem CompleteGroupAlgebra.algEquivOfCoinitial_symm_apply (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s t : Set (OpenNormalSubgroup G)) (hs : DirectedOn GE.ge s) (hts : IsCoinitialFor t s) (ht : DirectedOn GE.ge t) (hst : IsCoinitialFor s t) (x : CompleteGroupAlgebra R G t) : (algEquivOfCoinitial R G s t hs hts ht hst).symm x = (algHomOfCoinitial R G t s ht hst) x

Elements of form r • [g]

noncomputable def CompleteGroupAlgebra.single (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) (g : G) : R →ₗ[R] CompleteGroupAlgebra R G s

The linear map which maps r to r • [g] in R⟦ˣG⟧.

Equations

• CompleteGroupAlgebra.single R G s g = { toFun := fun (r : R) => ⟨fun (x : OpenNormalSubgroup G) (x_1 : PLift (x ∈ s)) => MonoidAlgebra.single (↑g) r, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem CompleteGroupAlgebra.single_apply_coe (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) (g : G) (r : R) {N : OpenNormalSubgroup G} (hN : N ∈ s) : ↑((single R G s g) r) { down := hN } = MonoidAlgebra.single (↑g) r

theorem CompleteGroupAlgebra.one_def (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) : 1 = (single R G s 1) 1

@[simp]

theorem CompleteGroupAlgebra.projOfExistsLE_single (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) (M : Subgroup G) [M.Normal] (hM : ∃ N ∈ s, ↑N.toOpenSubgroup ≤ M) (g : G) (r : R) : (projOfExistsLE R G s M hM) ((single R G s g) r) = MonoidAlgebra.single (↑g) r

@[simp]

theorem CompleteGroupAlgebra.augmentation_single (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) (hs : s.Nonempty) (g : G) (r : R) : (augmentation R G s hs) ((single R G s g) r) = r

@[simp]

theorem CompleteGroupAlgebra.ofMonoidAlgebra_single (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s : Set (OpenNormalSubgroup G)) (g : G) (r : R) : (ofMonoidAlgebra R G s) (MonoidAlgebra.single g r) = (single R G s g) r

@[simp]

theorem CompleteGroupAlgebra.algHomOfCoinitial_single (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (s t : Set (OpenNormalSubgroup G)) (hs : DirectedOn GE.ge s) (hts : IsCoinitialFor t s) (g : G) (r : R) : (algHomOfCoinitial R G s t hs hts) ((single R G s g) r) = (single R G t g) r