Complete group algebras (experimental)

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

Recall that there is the scoped notation R[G] for MonoidAlgebra in mathlib.

If R is a commutative semiring, G is a topological group, then CompleteGroupAlgebra R G (with scpoed notation R⟦G⟧) is defined to be the inverse limit of R[G/N] (Algebra.InverseLimit) as N runs over all open normal subgroups of G. It is an R-algebra.

Currently we only defined the multiplicative version. For additive version, please use CompleteGroupAlgebra R (Multiplicative G) instead.

Augmentation map (TODO: should go to mathlib ???)

noncomputable def MonoidAlgebra.augmentation (R : Type u_1) (G : Type u_2) [CommSemiring R] [Monoid G] : MonoidAlgebra R G →ₐ[R] R

The augmentation is the map from R[G] to R sending 1 • g to 1 for all g in G.

Equations

• MonoidAlgebra.augmentation R G = (MonoidAlgebra.lift R R G) 1

theorem MonoidAlgebra.augmentation_apply (R : Type u_1) (G : Type u_2) [CommSemiring R] [Monoid G] (x : MonoidAlgebra R G) : (augmentation R G) x = x.coeff.sum fun (x : G) (r : R) => r

@[simp]

theorem MonoidAlgebra.augmentation_single (R : Type u_1) (G : Type u_2) [CommSemiring R] [Monoid G] (g : G) (r : R) : (augmentation R G) (single g r) = r

theorem MonoidAlgebra.augmentation_comp_lsingle (R : Type u_1) (G : Type u_2) [CommSemiring R] [Monoid G] (g : G) : ↑(augmentation R G) ∘ₗ lsingle g = LinearMap.id

theorem MonoidAlgebra.augmentation_surjective (R : Type u_1) (G : Type u_2) [CommSemiring R] [Monoid G] : Function.Surjective ⇑(augmentation R G)

@[simp]

theorem MonoidAlgebra.augmentation_comp_mapDomainAlgHom (R : Type u_1) (G : Type u_2) [CommSemiring R] [Monoid G] (H : Type u_3) [Monoid H] (f : G →* H) : (augmentation R H).comp (mapDomainAlgHom R R f) = augmentation R G

Definition of complete group algebra

@[reducible, inline]

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

The CompleteGroupAlgebra R G (with scpoed notation R⟦G⟧) is the inverse limit (Algebra.InverseLimit) of R[G/N] as N runs over open normal subgroups of G.

Equations

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

def CompleteGroupAlgebra.«term__⟦_⟧» : Lean.TrailingParserDescr

The CompleteGroupAlgebra R G (with scpoed notation R⟦G⟧) is the inverse limit (Algebra.InverseLimit) of R[G/N] as N runs over open normal subgroups of G.

Equations

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

def CompleteGroupAlgebra.unexpander : Lean.PrettyPrinter.Unexpander

Unexpander for CompleteGroupAlgebra.

Equations

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

theorem CompleteGroupAlgebra.ext (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] {x y : CompleteGroupAlgebra R G} (hxy : ∀ (N : OpenNormalSubgroup G), ↑x N = ↑y N) : x = y

theorem CompleteGroupAlgebra.ext_iff {R : Type u_1} [CommSemiring R] {G : Type u_2} [Group G] [TopologicalSpace G] {x y : CompleteGroupAlgebra R G} : x = y ↔ ∀ (N : OpenNormalSubgroup G), ↑x N = ↑y N

Projection maps

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

The proj is the natural map from R⟦G⟧ to R[G/N] for an open normal subgroup N.

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] (N : OpenNormalSubgroup G) (x : CompleteGroupAlgebra R G) : (proj R G N) x = ↑x N

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

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

theorem CompleteGroupAlgebra.eq_of_proj_comp_eq (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] {S : Type u_3} [Semiring S] [Algebra R S] {f g : S →ₐ[R] CompleteGroupAlgebra R G} (hfg : ∀ (N : OpenNormalSubgroup G), (proj R G N).comp f = (proj R G N).comp g) : f = g

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

The augmentation is the map from R⟦G⟧ to R.

Equations

• CompleteGroupAlgebra.augmentation R G = (MonoidAlgebra.augmentation R (G ⧸ ↑⊤.toOpenSubgroup)).comp (CompleteGroupAlgebra.proj R G ⊤)

theorem CompleteGroupAlgebra.augmentation_apply (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (x : CompleteGroupAlgebra R G) : (augmentation R G) x = (↑x ⊤).coeff 1

theorem CompleteGroupAlgebra.augmentation_eq_augmentation_comp_proj (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (N : OpenNormalSubgroup G) : augmentation R G = (MonoidAlgebra.augmentation R (G ⧸ ↑N.toOpenSubgroup)).comp (proj R G N)

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 : Type u_3} [Semiring S] [Algebra R S] (f : (N : OpenNormalSubgroup G) → S →ₐ[R] MonoidAlgebra R (G ⧸ ↑N.toOpenSubgroup)) (hf : ∀ ⦃N₁ N₂ : OpenNormalSubgroup G⦄ (hle : N₁ ≤ N₂), (MonoidAlgebra.mapDomainAlgHom R R (QuotientGroup.map (↑N₁.toOpenSubgroup) (↑N₂.toOpenSubgroup) (MonoidHom.id G) hle)).comp (f N₁) = f N₂) : S →ₐ[R] CompleteGroupAlgebra R G

If a family of maps S → R[G/N] satisfy compatibility conditions, then they lift to a map S → R⟦G⟧.

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 : Type u_3} [Semiring S] [Algebra R S] {f : (N : OpenNormalSubgroup G) → S →ₐ[R] MonoidAlgebra R (G ⧸ ↑N.toOpenSubgroup)} {hf : ∀ ⦃N₁ N₂ : OpenNormalSubgroup G⦄ (hle : N₁ ≤ N₂), (MonoidAlgebra.mapDomainAlgHom R R (QuotientGroup.map (↑N₁.toOpenSubgroup) (↑N₂.toOpenSubgroup) (MonoidHom.id G) hle)).comp (f N₁) = f N₂} (x : S) (N : OpenNormalSubgroup G) : ↑((lift R G f hf) x) N = (f N) x

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

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

The lift map S → R⟦G⟧ is unique.

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

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

The natural map from R[G] to R⟦G⟧.

Equations

• CompleteGroupAlgebra.ofMonoidAlgebra R G = CompleteGroupAlgebra.lift R G (fun (N : OpenNormalSubgroup G) => MonoidAlgebra.mapDomainAlgHom R R (QuotientGroup.mk' ↑N.toOpenSubgroup)) ⋯

@[simp]

theorem CompleteGroupAlgebra.ofMonoidAlgebra_apply_coe (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (x : MonoidAlgebra R G) (N : OpenNormalSubgroup G) : ↑((ofMonoidAlgebra R G) x) N = (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] (N : OpenNormalSubgroup G) : (proj R G N).comp (ofMonoidAlgebra R G) = MonoidAlgebra.mapDomainAlgHom R R (QuotientGroup.mk' ↑N.toOpenSubgroup)

theorem CompleteGroupAlgebra.proj_surjective (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (N : OpenNormalSubgroup G) : Function.Surjective ⇑(proj R G N)

theorem CompleteGroupAlgebra.augmentation_surjective (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] : Function.Surjective ⇑(augmentation R G)

theorem CompleteGroupAlgebra.ker_ofMonoidAlgebra_eq_iInf (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] : RingHom.ker (ofMonoidAlgebra R G) = ⨅ (N : OpenNormalSubgroup G), RingHom.ker (MonoidAlgebra.mapDomainAlgHom R R (QuotientGroup.mk' ↑N.toOpenSubgroup))

theorem CompleteGroupAlgebra.ofMonoidAlgebra_injective (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : Function.Injective ⇑(ofMonoidAlgebra R G)

If G is a profinite group (i.e. it is CompactSpace and TotallyDisconnectedSpace), then the natural map R[G] → R⟦G⟧ is injective.

Elements of form r • [g]

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

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

Equations

• CompleteGroupAlgebra.single R G g = { toFun := fun (r : R) => ⟨fun (x : (OpenNormalSubgroup G)ᵒᵈ) => 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] (g : G) (r : R) (N : OpenNormalSubgroup G) : ↑((single R G g) r) N = MonoidAlgebra.single (↑g) r

theorem CompleteGroupAlgebra.proj_comp_single (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (g : G) (N : OpenNormalSubgroup G) : ↑(proj R G N) ∘ₗ single R G g = MonoidAlgebra.lsingle ↑g

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

@[simp]

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

theorem CompleteGroupAlgebra.augmentation_comp_single (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (g : G) : ↑(augmentation R G) ∘ₗ single R G g = LinearMap.id

@[simp]

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

theorem CompleteGroupAlgebra.ofMonoidAlgebra_comp_lsingle (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (g : G) : ↑(ofMonoidAlgebra R G) ∘ₗ MonoidAlgebra.lsingle g = single R G g

theorem CompleteGroupAlgebra.single_injective (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (g : G) : Function.Injective ⇑(single R G g)

@[simp]

theorem CompleteGroupAlgebra.single_eq_zero (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (g : G) (r : R) : (single R G g) r = 0 ↔ r = 0

theorem CompleteGroupAlgebra.single_ne_zero (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (g : G) (r : R) : (single R G g) r ≠ 0 ↔ r ≠ 0

@[simp]

theorem CompleteGroupAlgebra.single_mul_single (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (g g' : G) (r r' : R) : (single R G g) r * (single R G g') r' = (single R G (g * g')) (r * r')

@[simp]

theorem CompleteGroupAlgebra.single_pow (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (g : G) (r : R) (n : ℕ) : (single R G g) r ^ n = (single R G (g ^ n)) (r ^ n)

The map g ↦ [g]

noncomputable def CompleteGroupAlgebra.of (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] : G →* CompleteGroupAlgebra R G

The map which maps g to [g] in R⟦G⟧.

Equations

• CompleteGroupAlgebra.of R G = (↑(CompleteGroupAlgebra.ofMonoidAlgebra R G)).comp (MonoidAlgebra.of R G)

@[simp]

theorem CompleteGroupAlgebra.of_apply (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (x : G) : (of R G) x = (single R G x) 1

theorem CompleteGroupAlgebra.proj_comp_of (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] (N : OpenNormalSubgroup G) : (↑(proj R G N)).comp (of R G) = (MonoidAlgebra.of R (G ⧸ ↑N.toOpenSubgroup)).comp (QuotientGroup.mk' ↑N.toOpenSubgroup)

theorem CompleteGroupAlgebra.of_injective (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [Nontrivial R] : Function.Injective ⇑(of R G)

If G is a profinite group (i.e. it is CompactSpace and TotallyDisconnectedSpace) and R is not trivial, then the map G → R⟦G⟧, g ↦ [g] is injective.

The map R⟦G⟧ → R⟦H⟧ induced by G → H

noncomputable def CompleteGroupAlgebra.map (R : Type u_1) [CommSemiring R] {G : Type u_2} [Group G] [TopologicalSpace G] {H : Type u_3} [Group H] [TopologicalSpace H] (f : G →* H) (hf : Continuous ⇑f) : CompleteGroupAlgebra R G →ₐ[R] CompleteGroupAlgebra R H

The map R⟦G⟧ → R⟦H⟧ induced by a continuous group homomorphism G → H.

Equations

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

theorem CompleteGroupAlgebra.map_apply_coe (R : Type u_1) [CommSemiring R] {G : Type u_2} [Group G] [TopologicalSpace G] {H : Type u_3} [Group H] [TopologicalSpace H] (f : G →* H) (hf : Continuous ⇑f) (x : CompleteGroupAlgebra R G) (N : OpenNormalSubgroup H) : ↑((map R f hf) x) N = (MonoidAlgebra.mapDomainAlgHom R R (QuotientGroup.map (↑(OpenNormalSubgroup.comap f hf N).toOpenSubgroup) (↑N.toOpenSubgroup) f ⋯)) ((proj R G (OpenNormalSubgroup.comap f hf N)) x)

theorem CompleteGroupAlgebra.proj_comp_map (R : Type u_1) [CommSemiring R] {G : Type u_2} [Group G] [TopologicalSpace G] {H : Type u_3} [Group H] [TopologicalSpace H] (f : G →* H) (hf : Continuous ⇑f) (N : OpenNormalSubgroup H) : (proj R H N).comp (map R f hf) = (MonoidAlgebra.mapDomainAlgHom R R (QuotientGroup.map (↑(OpenNormalSubgroup.comap f hf N).toOpenSubgroup) (↑N.toOpenSubgroup) f ⋯)).comp (proj R G (OpenNormalSubgroup.comap f hf N))

@[simp]

theorem CompleteGroupAlgebra.map_single (R : Type u_1) [CommSemiring R] {G : Type u_2} [Group G] [TopologicalSpace G] {H : Type u_3} [Group H] [TopologicalSpace H] (f : G →* H) (hf : Continuous ⇑f) (g : G) (r : R) : (map R f hf) ((single R G g) r) = (single R H (f g)) r

theorem CompleteGroupAlgebra.map_comp_ofMonoidAlgebra (R : Type u_1) [CommSemiring R] {G : Type u_2} [Group G] [TopologicalSpace G] {H : Type u_3} [Group H] [TopologicalSpace H] (f : G →* H) (hf : Continuous ⇑f) : (map R f hf).comp (ofMonoidAlgebra R G) = (ofMonoidAlgebra R H).comp (MonoidAlgebra.mapDomainAlgHom R R f)

theorem CompleteGroupAlgebra.map_comp_of (R : Type u_1) [CommSemiring R] {G : Type u_2} [Group G] [TopologicalSpace G] {H : Type u_3} [Group H] [TopologicalSpace H] (f : G →* H) (hf : Continuous ⇑f) : (↑(map R f hf)).comp (of R G) = (of R H).comp f

@[simp]

theorem CompleteGroupAlgebra.augmentation_map (R : Type u_1) [CommSemiring R] {G : Type u_2} [Group G] [TopologicalSpace G] {H : Type u_3} [Group H] [TopologicalSpace H] (f : G →* H) (hf : Continuous ⇑f) (x : CompleteGroupAlgebra R G) : (augmentation R H) ((map R f hf) x) = (augmentation R G) x

@[simp]

theorem CompleteGroupAlgebra.augmentation_comp_map (R : Type u_1) [CommSemiring R] {G : Type u_2} [Group G] [TopologicalSpace G] {H : Type u_3} [Group H] [TopologicalSpace H] (f : G →* H) (hf : Continuous ⇑f) : (augmentation R H).comp (map R f hf) = augmentation R G

@[simp]

theorem CompleteGroupAlgebra.map_id (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] : map R (MonoidHom.id G) ⋯ = AlgHom.id R (CompleteGroupAlgebra R G)

theorem CompleteGroupAlgebra.map_comp_map (R : Type u_1) [CommSemiring R] {G : Type u_2} [Group G] [TopologicalSpace G] {H : Type u_3} [Group H] [TopologicalSpace H] (f : G →* H) (hf : Continuous ⇑f) {K : Type u_4} [Group K] [TopologicalSpace K] (g : H →* K) (hg : Continuous ⇑g) : (map R g hg).comp (map R f hf) = map R (g.comp f) ⋯

The map R⟦G⟧ ≃ R⟦H⟧ induced by G ≃ H

noncomputable def CompleteGroupAlgebra.congr (R : Type u_1) [CommSemiring R] {G : Type u_2} [Group G] [TopologicalSpace G] {H : Type u_3} [Group H] [TopologicalSpace H] (f : G ≃ₜ* H) : CompleteGroupAlgebra R G ≃ₐ[R] CompleteGroupAlgebra R H

The map R⟦G⟧ ≃ R⟦H⟧ induced by a continuous group isomorphism G ≃ H.

Equations

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

@[simp]

theorem CompleteGroupAlgebra.coe_congr (R : Type u_1) [CommSemiring R] {G : Type u_2} [Group G] [TopologicalSpace G] {H : Type u_3} [Group H] [TopologicalSpace H] (f : G ≃ₜ* H) : ↑(congr R f) = map R ↑f ⋯

@[simp]

theorem CompleteGroupAlgebra.congr_symm (R : Type u_1) [CommSemiring R] {G : Type u_2} [Group G] [TopologicalSpace G] {H : Type u_3} [Group H] [TopologicalSpace H] (f : G ≃ₜ* H) : (congr R f).symm = congr R f.symm

theorem CompleteGroupAlgebra.coe_congr_symm (R : Type u_1) [CommSemiring R] {G : Type u_2} [Group G] [TopologicalSpace G] {H : Type u_3} [Group H] [TopologicalSpace H] (f : G ≃ₜ* H) : ↑(congr R f).symm = map R ↑f.symm ⋯

@[simp]

theorem CompleteGroupAlgebra.congr_single (R : Type u_1) [CommSemiring R] {G : Type u_2} [Group G] [TopologicalSpace G] {H : Type u_3} [Group H] [TopologicalSpace H] (f : G ≃ₜ* H) (g : G) (r : R) : (congr R f) ((single R G g) r) = (single R H (f g)) r

@[simp]

theorem CompleteGroupAlgebra.congr_refl (R : Type u_1) [CommSemiring R] (G : Type u_2) [Group G] [TopologicalSpace G] : congr R (ContinuousMulEquiv.refl G) = AlgEquiv.refl

theorem CompleteGroupAlgebra.congr_trans_congr (R : Type u_1) [CommSemiring R] {G : Type u_2} [Group G] [TopologicalSpace G] {H : Type u_3} [Group H] [TopologicalSpace H] (f : G ≃ₜ* H) {K : Type u_4} [Group K] [TopologicalSpace K] (g : H ≃ₜ* K) : (congr R f).trans (congr R g) = congr R (f.trans g)

Isomorphism to inverse limit by taking a neighborhood basis

noncomputable def CompleteGroupAlgebra.equivInverseLimit.auxIndex {G : Type u_2} [Group G] [TopologicalSpace G] {I : Type u_3} [Preorder I] (N : I → OpenNormalSubgroup G) (hN : (nhds 1).HasAntitoneBasis fun (i : I) => ↑(N i)) (M : OpenNormalSubgroup G) : I

If { N_i } is a family of open normal subgroups forming a neighborhood basis of 1, then given any open normal subgroup M, there exists i such that N_i ≤ M.

Equations

• CompleteGroupAlgebra.equivInverseLimit.auxIndex N hN M = ⋯.choose

theorem CompleteGroupAlgebra.equivInverseLimit.auxIndex_spec {G : Type u_2} [Group G] [TopologicalSpace G] {I : Type u_3} [Preorder I] (N : I → OpenNormalSubgroup G) (hN : (nhds 1).HasAntitoneBasis fun (i : I) => ↑(N i)) (M : OpenNormalSubgroup G) : N (auxIndex N hN M) ≤ M

@[reducible, inline]

abbrev CompleteGroupAlgebra.InverseLimit (R : Type u_1) [CommSemiring R] {G : Type u_2} [Group G] [TopologicalSpace G] {I : Type u_3} [Preorder I] (N : I → OpenNormalSubgroup G) (hN : (nhds 1).HasAntitoneBasis fun (i : I) => ↑(N i)) : Type (max u_3 u_1 u_2)

If { N_i } is a family of open normal subgroups forming a neighborhood basis of 1, then CompleteGroupAlgebra.InverseLimit is the inverse limit of R[G/N_i].

Equations

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

noncomputable def CompleteGroupAlgebra.toInverseLimit (R : Type u_1) [CommSemiring R] {G : Type u_2} [Group G] [TopologicalSpace G] {I : Type u_3} [Preorder I] (N : I → OpenNormalSubgroup G) (hN : (nhds 1).HasAntitoneBasis fun (i : I) => ↑(N i)) : CompleteGroupAlgebra R G →ₐ[R] InverseLimit R N hN

If { N_i } is a family of open normal subgroups forming a neighborhood basis of 1, then there is a map from R⟦G⟧ to the inverse limit of R[G/N_i].

Equations

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

noncomputable def CompleteGroupAlgebra.ofInverseLimit (R : Type u_1) [CommSemiring R] {G : Type u_2} [Group G] [TopologicalSpace G] {I : Type u_3} [Preorder I] (N : I → OpenNormalSubgroup G) (hN : (nhds 1).HasAntitoneBasis fun (i : I) => ↑(N i)) [IsDirected I LE.le] : InverseLimit R N hN →ₐ[R] CompleteGroupAlgebra R G

If { N_i } is a family of open normal subgroups forming a neighborhood basis of 1, then there is a map from the inverse limit of R[G/N_i] to R⟦G⟧.

Equations

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

theorem CompleteGroupAlgebra.toInverseLimit_comp_ofInverseLimit (R : Type u_1) [CommSemiring R] {G : Type u_2} [Group G] [TopologicalSpace G] {I : Type u_3} [Preorder I] (N : I → OpenNormalSubgroup G) (hN : (nhds 1).HasAntitoneBasis fun (i : I) => ↑(N i)) [IsDirected I LE.le] : (toInverseLimit R N hN).comp (ofInverseLimit R N hN) = AlgHom.id R (InverseLimit R N hN)

theorem CompleteGroupAlgebra.ofInverseLimit_comp_toInverseLimit (R : Type u_1) [CommSemiring R] {G : Type u_2} [Group G] [TopologicalSpace G] {I : Type u_3} [Preorder I] (N : I → OpenNormalSubgroup G) (hN : (nhds 1).HasAntitoneBasis fun (i : I) => ↑(N i)) [IsDirected I LE.le] : (ofInverseLimit R N hN).comp (toInverseLimit R N hN) = AlgHom.id R (CompleteGroupAlgebra R G)

noncomputable def CompleteGroupAlgebra.equivInverseLimit (R : Type u_1) [CommSemiring R] {G : Type u_2} [Group G] [TopologicalSpace G] {I : Type u_3} [Preorder I] (N : I → OpenNormalSubgroup G) (hN : (nhds 1).HasAntitoneBasis fun (i : I) => ↑(N i)) [IsDirected I LE.le] : CompleteGroupAlgebra R G ≃ₐ[R] InverseLimit R N hN

If { N_i } is a family of open normal subgroups forming a neighborhood basis of 1, then there is an isomorphism from R⟦G⟧ to the inverse limit of R[G/N_i].

Equations

• CompleteGroupAlgebra.equivInverseLimit R N hN = AlgEquiv.ofAlgHom (CompleteGroupAlgebra.toInverseLimit R N hN) (CompleteGroupAlgebra.ofInverseLimit R N hN) ⋯ ⋯