mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard
verified publisher icon leanprover-community

feat(analysis/normed_space/category/CStarAlg): categories of C⋆-algebras

Open j-loreaux opened this issue 3 years ago • 1 comments

This introduces three categories of C⋆-algebras (over ℂ), namely:

  • CStarAlg: not necessarily unital C⋆-algebras with non_unital_star_alg_homs
  • CStarAlg₁: unital C⋆-algebras with star_alg_homs
  • CommCStarAlg₁: commutative unital C⋆-algebras with star_alg_homs

We currently have to avoid the natural CommCStarAlg because we don't have non_unital_normed_comm_ring since #13719 is blocked by timeouts.

  • [ ] depends on: #16784

This is my first foray into category theory in mathlib, so please don't hesitate to tell me I've done something horribly wrong! :smile:

Open in Gitpod

j-loreaux avatar Oct 10 '22 23:10 j-loreaux

This PR/issue depends on:

  • ~~leanprover-community/mathlib#16784~~ By Dependent Issues (🤖). Happy coding!

mathlib-dependent-issues-bot avatar Oct 25 '22 14:10 mathlib-dependent-issues-bot

Closed to wait for Lean 4. This isn't urgent and probably needs to be implemented slightly differently anyway (to take a star_ordered_ring field).

j-loreaux avatar Nov 09 '22 15:11 j-loreaux