Equivariant homomorphisms and invariant C⋆-subalgebras

This file develops the functorial layer of point-norm continuous C⋆-actions. An equivariant homomorphism is a nonunital complex star-algebra homomorphism commuting with the actions. Invariant nonunital star subalgebras can be mapped and pulled back along such homomorphisms, and their topological closures remain invariant.

A closed invariant star subalgebra inherits the restricted point-norm continuous action. Its canonical inclusion into the ambient algebra is equivariant. These constructions are the coefficient-side input for functoriality and ideal exact sequences of crossed products.

The conventions follow Dana Williams, Crossed Products of C-Algebras*, Chapter 2.

structure TauCeti.CStarAction.Hom {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] (α : CStarAction G A) (β : CStarAction G B) extends A →⋆ₙₐ[ℂ] B : Type (max u_2 u_3)

An equivariant nonunital star-algebra homomorphism between C⋆-actions.

• toFun : A → B
• map_smul' (m : ℂ) (x : A) : self.toFun (m • x) = (MonoidHom.id ℂ) m • self.toFun x
• map_zero' : self.toFun 0 = 0
• map_add' (x y : A) : self.toFun (x + y) = self.toFun x + self.toFun y
• map_mul' (x y : A) : self.toFun (x * y) = self.toFun x * self.toFun y
• map_star' (a : A) : self.toFun (star a) = star (self.toFun a)
• map_action' (g : G) (a : A) : self.toNonUnitalStarAlgHom ((α g) a) = (β g) (self.toNonUnitalStarAlgHom a)

  The homomorphism commutes with the action of every group element.

theorem TauCeti.CStarAction.Hom.toNonUnitalStarAlgHom_injective {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] {α : CStarAction G A} {β : CStarAction G B} : Function.Injective toNonUnitalStarAlgHom

The underlying star-algebra homomorphism determines an equivariant homomorphism.

@[instance_reducible]

instance TauCeti.CStarAction.Hom.instFunLike {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] {α : CStarAction G A} {β : CStarAction G B} : FunLike (α.Hom β) A B

instance TauCeti.CStarAction.Hom.instNonUnitalAlgHomClassComplex {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] {α : CStarAction G A} {β : CStarAction G B} : NonUnitalAlgHomClass (α.Hom β) ℂ A B

instance TauCeti.CStarAction.Hom.instStarHomClass {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] {α : CStarAction G A} {β : CStarAction G B} : StarHomClass (α.Hom β) A B

@[instance_reducible]

instance TauCeti.CStarAction.Hom.instCoeOutNonUnitalStarAlgHomComplex {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] {α : CStarAction G A} {β : CStarAction G B} : CoeOut (α.Hom β) (A →⋆ₙₐ[ℂ] B)

@[simp]

theorem TauCeti.CStarAction.Hom.coe_toNonUnitalStarAlgHom {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] {α : CStarAction G A} {β : CStarAction G B} (f : α.Hom β) : ⇑f.toNonUnitalStarAlgHom = ⇑f

@[simp]

theorem TauCeti.CStarAction.Hom.coe_mk {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] {α : CStarAction G A} {β : CStarAction G B} (f : A →⋆ₙₐ[ℂ] B) (hf : ∀ (g : G) (a : A), f ((α g) a) = (β g) (f a)) : ⇑{ toNonUnitalStarAlgHom := f, map_action' := hf } = ⇑f

theorem TauCeti.CStarAction.Hom.ext {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] {α : CStarAction G A} {β : CStarAction G B} {f g : α.Hom β} (h : ∀ (a : A), f a = g a) : f = g

Two equivariant homomorphisms are equal if they agree on every coefficient.

theorem TauCeti.CStarAction.Hom.ext_iff {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] {α : CStarAction G A} {β : CStarAction G B} {f g : α.Hom β} : f = g ↔ ∀ (a : A), f a = g a

@[simp]

theorem TauCeti.CStarAction.Hom.map_action {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] {α : CStarAction G A} {β : CStarAction G B} (f : α.Hom β) (g : G) (a : A) : f ((α g) a) = (β g) (f a)

An equivariant homomorphism commutes with the group actions.

def TauCeti.CStarAction.Hom.id {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) : α.Hom α

The identity equivariant homomorphism of a C⋆-action.

@[simp]

theorem TauCeti.CStarAction.Hom.id_toNonUnitalStarAlgHom {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) : (Hom.id α).toNonUnitalStarAlgHom = NonUnitalStarAlgHom.id ℂ A

@[simp]

theorem TauCeti.CStarAction.Hom.coe_id {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) : ⇑(Hom.id α) = id

@[simp]

theorem TauCeti.CStarAction.Hom.id_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) (a : A) : (Hom.id α) a = a

def TauCeti.CStarAction.Hom.comp {G : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] [NonUnitalCStarAlgebra C] {α : CStarAction G A} {β : CStarAction G B} {γ : CStarAction G C} (g : β.Hom γ) (f : α.Hom β) : α.Hom γ

Composition of equivariant homomorphisms.

@[simp]

theorem TauCeti.CStarAction.Hom.comp_toNonUnitalStarAlgHom {G : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] [NonUnitalCStarAlgebra C] {α : CStarAction G A} {β : CStarAction G B} {γ : CStarAction G C} (g : β.Hom γ) (f : α.Hom β) : (g.comp f).toNonUnitalStarAlgHom = g.comp f.toNonUnitalStarAlgHom

@[simp]

theorem TauCeti.CStarAction.Hom.coe_comp {G : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] [NonUnitalCStarAlgebra C] {α : CStarAction G A} {β : CStarAction G B} {γ : CStarAction G C} (g : β.Hom γ) (f : α.Hom β) : ⇑(g.comp f) = ⇑g ∘ ⇑f

@[simp]

theorem TauCeti.CStarAction.Hom.comp_apply {G : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] [NonUnitalCStarAlgebra C] {α : CStarAction G A} {β : CStarAction G B} {γ : CStarAction G C} (g : β.Hom γ) (f : α.Hom β) (a : A) : (g.comp f) a = g (f a)

@[simp]

theorem TauCeti.CStarAction.Hom.comp_id {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] {α : CStarAction G A} {β : CStarAction G B} (f : α.Hom β) : f.comp (Hom.id α) = f

@[simp]

theorem TauCeti.CStarAction.Hom.id_comp {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] {α : CStarAction G A} {β : CStarAction G B} (f : α.Hom β) : (Hom.id β).comp f = f

@[simp]

theorem TauCeti.CStarAction.Hom.comp_assoc {G : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] [NonUnitalCStarAlgebra C] {α : CStarAction G A} {β : CStarAction G B} {γ : CStarAction G C} {D : Type u_5} [NonUnitalCStarAlgebra D] {δ : CStarAction G D} (h : γ.Hom δ) (g : β.Hom γ) (f : α.Hom β) : (h.comp g).comp f = h.comp (g.comp f)

Composition of equivariant homomorphisms is associative.

theorem IsInvariant.apply_mem {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] {s : Set A} {α : TauCeti.CStarAction G A} (hs : IsInvariant (fun (g : G) (a : A) => (α g) a) s) (g : G) {a : A} (ha : a ∈ s) : (α g) a ∈ s

Apply invariance to a member of the set.

theorem IsInvariant.image_eq {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] {α : TauCeti.CStarAction G A} {s : Set A} (hs : IsInvariant (fun (g : G) (a : A) => (α g) a) s) (g : G) : ⇑(α g) '' s = s

Invariance under a group action can equivalently be stated as equality with every image.

theorem IsInvariant.iff_image_eq {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] {α : TauCeti.CStarAction G A} {s : Set A} : IsInvariant (fun (g : G) (a : A) => (α g) a) s ↔ ∀ (g : G), ⇑(α g) '' s = s

A set is invariant exactly when every group element maps it onto itself.

theorem IsInvariant.topologicalClosure {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] {s : Set A} {α : TauCeti.CStarAction G A} (hs : IsInvariant (fun (g : G) (a : A) => (α g) a) s) : IsInvariant (fun (g : G) (a : A) => (α g) a) (closure s)

The topological closure of an invariant set is invariant.

theorem IsInvariant.topologicalClosure_subalgebra {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] {S : NonUnitalStarSubalgebra ℂ A} {α : TauCeti.CStarAction G A} (hS : IsInvariant (fun (g : G) (a : A) => (α g) a) ↑S) : IsInvariant (fun (g : G) (a : A) => (α g) a) ↑S.topologicalClosure

The topological closure of an invariant star subalgebra is invariant.

@[simp]

theorem IsInvariant.top {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] (α : TauCeti.CStarAction G A) : IsInvariant (fun (g : G) (a : A) => (α g) a) Set.univ

The universal set is invariant under every C⋆-action.

@[simp]

theorem IsInvariant.singleton_zero {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] (α : TauCeti.CStarAction G A) : IsInvariant (fun (g : G) (a : A) => (α g) a) {0}

The zero singleton is invariant under every C⋆-action.

theorem IsInvariant.map {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] {s : Set A} {α : TauCeti.CStarAction G A} {β : TauCeti.CStarAction G B} (hs : IsInvariant (fun (g : G) (a : A) => (α g) a) s) (f : α.Hom β) : IsInvariant (fun (g : G) (b : B) => (β g) b) (⇑f '' s)

The image of an invariant set under an equivariant homomorphism is invariant.

theorem IsInvariant.map_subalgebra {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] {S : NonUnitalStarSubalgebra ℂ A} {α : TauCeti.CStarAction G A} {β : TauCeti.CStarAction G B} (hS : IsInvariant (fun (g : G) (a : A) => (α g) a) ↑S) (f : α.Hom β) : IsInvariant (fun (g : G) (b : B) => (β g) b) ↑(NonUnitalStarSubalgebra.map f.toNonUnitalStarAlgHom S)

The image of an invariant star subalgebra under an equivariant homomorphism is invariant.

theorem IsInvariant.comap {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] {t : Set B} {α : TauCeti.CStarAction G A} {β : TauCeti.CStarAction G B} (ht : IsInvariant (fun (g : G) (b : B) => (β g) b) t) (f : α.Hom β) : IsInvariant (fun (g : G) (a : A) => (α g) a) (⇑f ⁻¹' t)

The preimage of an invariant set under an equivariant homomorphism is invariant.

theorem IsInvariant.comap_subalgebra {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] {T : NonUnitalStarSubalgebra ℂ B} {α : TauCeti.CStarAction G A} {β : TauCeti.CStarAction G B} (hT : IsInvariant (fun (g : G) (b : B) => (β g) b) ↑T) (f : α.Hom β) : IsInvariant (fun (g : G) (a : A) => (α g) a) ↑(NonUnitalStarSubalgebra.comap f.toNonUnitalStarAlgHom T)

The preimage of an invariant star subalgebra under an equivariant homomorphism is invariant.

theorem IsInvariant.range {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] {α : TauCeti.CStarAction G A} {β : TauCeti.CStarAction G B} (f : α.Hom β) : IsInvariant (fun (g : G) (b : B) => (β g) b) ↑f.range

The range of an equivariant homomorphism is an invariant star subalgebra.

def IsInvariant.restrictEquiv {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] {S : NonUnitalStarSubalgebra ℂ A} {α : TauCeti.CStarAction G A} (hS : IsInvariant (fun (g : G) (a : A) => (α g) a) ↑S) (g : G) : ↥S ≃⋆ₐ[ℂ] ↥S

Restrict an automorphism from an action to an invariant star subalgebra.

@[simp]

theorem IsInvariant.coe_restrictEquiv {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] {S : NonUnitalStarSubalgebra ℂ A} {α : TauCeti.CStarAction G A} (hS : IsInvariant (fun (g : G) (a : A) => (α g) a) ↑S) (g : G) : ⇑(hS.restrictEquiv g) = fun (a : ↥S) => ⟨(α g) ↑a, ⋯⟩

@[simp]

theorem IsInvariant.restrictEquiv_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] {S : NonUnitalStarSubalgebra ℂ A} {α : TauCeti.CStarAction G A} (hS : IsInvariant (fun (g : G) (a : A) => (α g) a) ↑S) (g : G) (a : ↥S) : (hS.restrictEquiv g) a = ⟨(α g) ↑a, ⋯⟩

def IsInvariant.restrict {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] {S : NonUnitalStarSubalgebra ℂ A} {α : TauCeti.CStarAction G A} (hS : IsInvariant (fun (g : G) (a : A) => (α g) a) ↑S) [IsClosed ↑S] : TauCeti.CStarAction G ↥S

Restrict a C⋆-action to a closed invariant star subalgebra.

@[simp]

theorem IsInvariant.restrict_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] {S : NonUnitalStarSubalgebra ℂ A} {α : TauCeti.CStarAction G A} (hS : IsInvariant (fun (g : G) (a : A) => (α g) a) ↑S) [IsClosed ↑S] (g : G) (a : ↥S) : (hS.restrict g) a = ⟨(α g) ↑a, ⋯⟩

def IsInvariant.subtypeHom {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] {S : NonUnitalStarSubalgebra ℂ A} {α : TauCeti.CStarAction G A} (hS : IsInvariant (fun (g : G) (a : A) => (α g) a) ↑S) [IsClosed ↑S] : hS.restrict.Hom α

The canonical inclusion of a closed invariant star subalgebra is equivariant.

@[simp]

theorem IsInvariant.subtypeHom_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] {S : NonUnitalStarSubalgebra ℂ A} {α : TauCeti.CStarAction G A} (hS : IsInvariant (fun (g : G) (a : A) => (α g) a) ↑S) [IsClosed ↑S] (a : ↥S) : hS.subtypeHom a = ↑a