[Merged by Bors] - feat(data/complex/module): define `real_part` and `imaginary_part` #16438

j-loreaux · 2022-09-09T03:02:14Z

In a generic star_module one always has a decomposition of any element into a self_adjoint_part and a skew_self_adjoint part, but in a star module over ℂ we can instead decompose any element into a real_part and an imaginary_part, both of which are self-adjoint. Here we define these as ℝ-linear maps from the star module into the type of its self-adjoint elements and describe the basic relationships between these maps. The decomposition into real and imaginary parts is often useful for reducing arguments about elements of a star module over ℂ to the case when the element is self-adjoint.

dupuisf · 2022-09-10T23:13:44Z

I think it would make more sense for all this to be in the root namespace, no? At the very least skew_adjoint.neg_I_smul and skew_adjoint.I_smul_neg_I.

j-loreaux · 2022-09-11T00:17:10Z

Yes, of course. I meant for that to be the case. Will fix.

dupuisf · 2022-09-13T03:04:11Z

Thanks!

bors r+

…16438) In a generic `star_module` one always has a decomposition of any element into a `self_adjoint_part` and a `skew_self_adjoint` part, but in a star module over `ℂ` we can instead decompose any element into a `real_part` and an `imaginary_part`, both of which are self-adjoint. Here we define these as `ℝ`-linear maps from the star module into the type of its self-adjoint elements and describe the basic relationships between these maps. The decomposition into real and imaginary parts is often useful for reducing arguments about elements of a star module over `ℂ` to the case when the element is self-adjoint.

bors · 2022-09-13T04:22:47Z

Pull request successfully merged into master.

Build succeeded:

…16438) In a generic `star_module` one always has a decomposition of any element into a `self_adjoint_part` and a `skew_self_adjoint` part, but in a star module over `ℂ` we can instead decompose any element into a `real_part` and an `imaginary_part`, both of which are self-adjoint. Here we define these as `ℝ`-linear maps from the star module into the type of its self-adjoint elements and describe the basic relationships between these maps. The decomposition into real and imaginary parts is often useful for reducing arguments about elements of a star module over `ℂ` to the case when the element is self-adjoint.

…tar/spectrum): define the Gelfand transform as an `alg_hom` (#16451) This defines the `gelfand_transform` as an algebra homomorphism from a `𝕜`-algebra `A` into the continuous functions from the `character_space 𝕜 A` into the base field `𝕜`, where the map is given by evaluation. For this definition it is only supposed that `𝕜` is a topological ring and `A` is a topological space. When the algebra `A` is a C⋆-algebra over `ℂ`, algebra homomorphisms of `A` into `ℂ` (hence also terms of `character_space ℂ A`) are automatically star-preserving. Therefore, in this setting the Gelfand transform may be upgraded to a `star_alg_hom`. However, we do not implement that here because, with more work, one may show that this is actually an equivalence. - [x] depends on: #16438

…ansform is a bijective isometry for C⋆-algebras over ℂ (#16488) - [x] depends on: #16451 - [x] depends on: #16438 - [x] depends on: #16368 - [x] depends on: #16303 - [x] depends on: #16446 - [x] depends on: #16448

…16438) In a generic `star_module` one always has a decomposition of any element into a `self_adjoint_part` and a `skew_self_adjoint` part, but in a star module over `ℂ` we can instead decompose any element into a `real_part` and an `imaginary_part`, both of which are self-adjoint. Here we define these as `ℝ`-linear maps from the star module into the type of its self-adjoint elements and describe the basic relationships between these maps. The decomposition into real and imaginary parts is often useful for reducing arguments about elements of a star module over `ℂ` to the case when the element is self-adjoint.

…tar/spectrum): define the Gelfand transform as an `alg_hom` (#16451) This defines the `gelfand_transform` as an algebra homomorphism from a `𝕜`-algebra `A` into the continuous functions from the `character_space 𝕜 A` into the base field `𝕜`, where the map is given by evaluation. For this definition it is only supposed that `𝕜` is a topological ring and `A` is a topological space. When the algebra `A` is a C⋆-algebra over `ℂ`, algebra homomorphisms of `A` into `ℂ` (hence also terms of `character_space ℂ A`) are automatically star-preserving. Therefore, in this setting the Gelfand transform may be upgraded to a `star_alg_hom`. However, we do not implement that here because, with more work, one may show that this is actually an equivalence. - [x] depends on: #16438

…ansform is a bijective isometry for C⋆-algebras over ℂ (#16488) - [x] depends on: #16451 - [x] depends on: #16438 - [x] depends on: #16368 - [x] depends on: #16303 - [x] depends on: #16446 - [x] depends on: #16448

j-loreaux added 2 commits September 8, 2022 21:52

add real and imaginary parts

fa138a8

fix over 100 chars

b72f988

j-loreaux added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. t-algebra Algebra (groups, rings, fields etc) labels Sep 9, 2022

github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Sep 9, 2022

j-loreaux mentioned this pull request Sep 9, 2022

[Merged by Bors] - feat(topology/algebra/module/character_space, analysis/normed_space/star/spectrum): define the Gelfand transform as an alg_hom #16451

Closed

1 task

dupuisf added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Sep 12, 2022

j-loreaux mentioned this pull request Sep 12, 2022

[Merged by Bors] - feat(analysis/normed_space/star/gelfand_duality): Show the Gelfand transform is a bijective isometry for C⋆-algebras over ℂ #16488

Closed

6 tasks

move material into the root namespace

09317f4

j-loreaux added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Sep 13, 2022

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Sep 13, 2022

bors bot changed the title ~~feat(data/complex/module): define real_part and imaginary_part~~ [Merged by Bors] - feat(data/complex/module): define real_part and imaginary_part Sep 13, 2022

bors bot closed this Sep 13, 2022

bors bot deleted the j-loreaux/real-imaginary-parts branch September 13, 2022 04:22

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(data/complex/module): define `real_part` and `imaginary_part` #16438

[Merged by Bors] - feat(data/complex/module): define `real_part` and `imaginary_part` #16438

j-loreaux commented Sep 9, 2022

dupuisf commented Sep 10, 2022

j-loreaux commented Sep 11, 2022

dupuisf commented Sep 13, 2022

bors bot commented Sep 13, 2022

[Merged by Bors] - feat(data/complex/module): define real_part and imaginary_part #16438

[Merged by Bors] - feat(data/complex/module): define real_part and imaginary_part #16438

Conversation

j-loreaux commented Sep 9, 2022

dupuisf commented Sep 10, 2022

j-loreaux commented Sep 11, 2022

dupuisf commented Sep 13, 2022

bors bot commented Sep 13, 2022

[Merged by Bors] - feat(data/complex/module): define `real_part` and `imaginary_part` #16438

[Merged by Bors] - feat(data/complex/module): define `real_part` and `imaginary_part` #16438