Real subX associated to a complex subX

Stream: Is there code for X?

[Heather Macbeth]

I am curious about whether mathlib has the infrastructure needed for one of @Scott Morrison's TODOs on Stone-Weierstrass, or whether it's still missing:

Prove the complex version for self-adjoint subalgebras A, by separately approximating the real and imaginary parts using the real subalgebra of real-valued functions in A (which still separates points, by taking the norm-square of a separating function).

Mathlib does know that a ℂ-vector space E is a ℝ-vector space: docs#module.complex_to_real. Moreover, any ℂ-submodule of E can also be considered as an ℝ-submodule of E: docs#submodule.restrict_scalars.

I don't see the corresponding results for algebras and subalgebras; are these indeed missing?

[Eric Wieser]

Possibly docs#subalgebra.comap?

[Eric Wieser]

But that's not really as good as the submodule def

[Kevin Buzzard]

I'm still kind of reeling from this observation that I should be comapping and not restricting scalars.

[Heather Macbeth]

Ah, thanks! What is this comap business, and why do we do it for algebras but not for modules? (According to docs#subalgebra.comap

comap R S A is a type alias for A, and has an R-algebra structure defined on it when algebra R S and algebra S A. If S is an R-algebra and A is an S-algebra then algebra.comap.algebra R S A can be used to provide A with a structure of an R-algebra. Other than that, algebra.comap is now deprecated and replaced with is_scalar_tower.

[Eric Wieser]

Don't confuse docs#subalgebra.comap with docs#subalgegra.comap'!

[Kevin Buzzard]

docs#subalgebra.comap'

[Heather Macbeth]

So, for example, should I PR

instance algebra.complex_to_real (E : Type*) [ring E] [algebra ℂ E] : algebra ℝ E :=
algebra.comap ℝ ℂ E

by analogy with docs#module.complex_to_real?

[Eric Wieser]

I think comap is just a duplicate of restrict_scalars

[Eric Wieser]

And we should eliminate it

[Heather Macbeth]

Right, and it's frustrating because ideally it would be nice to have comap defeq to restrict_scalars when both exist.

[Eric Wieser]

I'm pretty sure that instance you suggest forms a loop

[Eric Wieser]

Since C is an algebra over anything R is an algebra over

[Heather Macbeth]

Why does docs#module.complex_to_real not form a loop then?

[Eric Wieser]

And usually instances construct typeclasses for big types from small ones

[Eric Wieser]

Nevermind, I misread the argument order

[Heather Macbeth]

Can I just rename comap to restrict_scalars?

[Eric Wieser]

I think that's a good idea

[Eric Wieser]

And I think @Oliver Nash did too but didn't want to take on the work right now

[Heather Macbeth]

Or rather, make comap into restrict_scalars (from the module setting) with a bit of decoration on top.

[Eric Wieser]

I think remove docs#algebra.comap replacing all uses with docs#restrict_scalars, and rename docs#subalgebra.comap to restrict_scalars

[Heather Macbeth]

It seems comap comes from Kenny, #536; restrict_scalars came from Sébastien, #1716, and perhaps no one noticed the duplication.

[Oliver Nash]

Thanks for bringing this up @Heather Macbeth I think it would be awesome good citizenry to eliminate algebra.comapunify subalgebra.comap with restrict_scalars (and I guess ideally, also rename subgalgebra.comap' to subalgebra.comap).

[Oliver Nash]

I have a small dangling PR that is distantly related #7807 but I think you can ignore it since it's mostly just a doc string.

[Oliver Nash]

Oh and also: it would be awesome to have Stone-Weierstrass for ℂ!

[Heather Macbeth]

#7949