Star-semilinear maps are semilinear when star is trivial

Stream: Is there code for X?

[Eric Wieser]

In #19038 (for #Is there code for X? > Derivative commutes with conjugation), I need docs#starL as a linear equivalence (in the presense of has_trivial_star R), not as a semi-linear equivalence. Do we have any existing machinery to do this conversion? Perhaps a semi-linear version of restrict_scalars?

[Eric Wieser]

Currently I have

@[simps]
def starL' (R : Type*) {A : Type*}
  [comm_semiring R] [star_ring R] [has_trivial_star R] [add_comm_monoid A] [star_add_monoid A]
  [module R A] [star_module R A] [topological_space A] [has_continuous_star A] :
    A ≃L[R] A :=
(starL R : A ≃L⋆[R] A).trans
  ({ map_smul' := λ r a, by simp [star_ring_end_apply],
    continuous_to_fun := continuous_id,
    continuous_inv_fun := continuous_id,
    ..add_equiv.refl A, } : A ≃L⋆[R] A)

but that seems ugly

[Heather Macbeth]

Can you explain what has_trivial_star is and why you aren't using $\mathbb{R}$?

[Eric Wieser]

has_trivial_star says star x = x for all x. Using it instead of $\mathbb{R}$ means that $\mathbb{Q}$ is covered too.

[Heather Macbeth]

Hmm, but why do you need a star at all?

[Eric Wieser]

Because we don't have a typeclass that says star (c • x) = c • star x

[Eric Wieser]

We only have one that says star (c • x) = star c • star x (docs#star_module)

[Heather Macbeth]

I think I don't understand why you're not just working with a general division ring? What's the setting?

[Eric Wieser]

do you mean for R or A?

[Heather Macbeth]

$R$, I guess, the thing you are describing as a "ring with trivial star"

[Eric Wieser]

So in practice yes,R is a nontrivially_normed_field for everything that comes later in the PR

[Eric Wieser]

But I still need the non-semilinear linear map in order to state the fderiv results

[Heather Macbeth]

Eric Wieser said:

So in practice yes,R is a nontrivially_normed_field for everything that comes later in the PR

So not the quaternions.

[Eric Wieser]

No, but A can be the quaternions

[Eric Wieser]

(and indeed, that's one of the motivations for #19038)

[Eric Wieser]

So to answer your original question again; using $\mathbb{R}$ would be sufficient for what I'm actually doing, but I would still need starL' in some form

[Heather Macbeth]

I think I am missing some context here, I just don't understand why you are considering this "has trivial star" typeclass at all enough to need its derivative.

[Eric Wieser]

The result I want to state is:

theorem has_fderiv_at.star (h : has_fderiv_at f f' x) :
  has_fderiv_at (λ x, star (f x)) (((starL' 𝕜 : F ≃L[𝕜] F) : F →L[𝕜] F) ∘L f') x :=
h.star

[Heather Macbeth]

For what typeclasses?

[Eric Wieser]

(note this is in the PR, if that helps)

[Eric Wieser]

variables {𝕜 : Type*} [nontrivially_normed_field 𝕜] [star_ring 𝕜] [has_trivial_star 𝕜]
variables {E : Type*} [normed_add_comm_group E] [normed_space 𝕜 E]
variables {F : Type*} [normed_add_comm_group F] [star_add_monoid F] [normed_space 𝕜 F]
  [star_module 𝕜 F] [has_continuous_star F]

variables {f : E → F}
variables {f' : E →L[𝕜] F}

[Heather Macbeth]

OK, it's just not clear to me that this is a useful generalization. Why don't you just take $\mathbb{k}$ to be a commutative ring? Or even to be $\mathbb{R}$ itself?

[Eric Wieser]

Because if you try it, you'll need star as a $\R$-linear map, and we don't have a typeclass that lets us do that; docs#star_smul doesn't exist

[Eric Wieser]

(I agree that the generalization to arbitrary 𝕜 for has_fderiv_at.star is pretty useless and ℝ would suffice for all the cases I can think of; but I think it's orthogonal to my question)

[Heather Macbeth]

So your situation is that you want to uniformly consider $\mathbb{C}$ and $\mathbb{H}$ as $\mathbb{R}$-modules, and have a generic way of referring to the conjugation as a $\mathbb{R}$-linear map?

[Kevin Buzzard]

(deleted)

[Eric Wieser]

Yes; and the reason I need it as a linear map is because It needs to be usable in the second argument of docs#has_fderiv_at, which does not accept semilinear maps (which I assume is because that wouldn't be mathematically meaningful, but I don't really know for sure)

[Eric Wieser]

and have a generic way of referring to the conjugation as a $R$-linear map?

Or a general way to change the σ in a linear map, such as

variables {R₁ R₂ R₁' R₂' M N : Type*}
  [semiring R₁] [semiring R₂] [add_comm_monoid M] [add_comm_monoid N]
  [module R₁ M] [module R₂ N] {σ σ' : R₁ →+* R₂}

/-- Replace the ring morphism in a semilinear map with an equal one.
This has better defeq than `h ▸  f`  and is easier to elaborate. -/
def linear_map.change_scalarsₛₗ (h : σ = σ') (f : M →ₛₗ[σ] N) : M →ₛₗ[σ'] N :=
{ map_smul' := λ c x, h▸ map_smulₛₗ f c x,
  ..f }

-- repeat for `linear_equiv`, `continuous_linear_equiv`, etc

then the answer would be (starL ℝ).change_scalarsₛₗ (star_end_eq_ring_hom_id) or something

[Heather Macbeth]

Eric Wieser said:

Perhaps a semi-linear version of restrict_scalars?

It seems like this would do it. If you have $M_i$ a module over $R_i$ and $R_i$ an algebra over $S_i$, and ring homomorphisms $\rho:R_1\to R_2$ and $\sigma:S_1\to S_2$, and a typeclass saying that $\sigma \circ \operatorname{alg\_hom}_1=\operatorname{alg\_hom}_2\circ \rho$, then maybe you can restrict-scalars a $\rho$-linear map to a $\sigma$-linear map.

[Heather Macbeth]

Specialize to $R_1=R_2\in\{\mathbb{C},\mathbb{H}\}$ and $S_1=S_2=\mathbb{R}$ and $\rho=\operatorname{conj}$ and $\sigma=\operatorname{id}$.

[Heather Macbeth]

I've thought vaguely about this before, the lack of such a construction prevented @Floris van Doorn and I from doing the $\operatorname{Hom}$ of smooth vector bundles in the right generality.

[Heather Macbeth]

(You want the bundle of conjugate-linear maps between two holomorphic vector bundles to be a real-smooth vector bundle.)

[Eric Wieser]

Here's an adapted version of your suggestion that doesn't need a full algebra:

import algebra.module.linear_map

variables {R₁ R₂ R₁' R₂' M N : Type*}
  [semiring R₁] [semiring R₂] [semiring R₁'] [semiring R₂']
  [add_comm_monoid M] [add_comm_monoid N]
  [module R₁ M] [module R₂ N] [module R₁' M] [module R₂' N]
  [mul_action R₁' R₁] [mul_action R₂' R₂]
  [is_scalar_tower R₁' R₁ M] [is_scalar_tower R₂' R₂ N]
   {σ : R₁ →+* R₂} (σ' : R₁' →+* R₂')

def linear_map.restrict_scalarsₛₗ (f : M →ₛₗ[σ] N) (h : ∀ c, σ (c • 1) = σ' c • 1) :
  M →ₛₗ[σ'] N :=
{ to_fun := f,
  map_smul' := λ c x, by rw [←smul_one_smul R₁ c x, ←smul_one_smul R₂ (σ' c) (f x),
    map_smulₛₗ f (c • 1 : _) x, h],
  ..f }

[Eric Wieser]

(apologies for the different variable names, I'd already started writing it when you posted your comment)

[Eric Wieser]

But restricting semilinear maps might be an #xy problem; perhaps a star_invariant_module typeclass would be the easy way out here

[Heather Macbeth]

Hmm, don't you then have to identify the invariant submodule with $\mathbb{R}$ itself? That seems ugly. I think restricting semilinear maps is the right choice, at least in my application which I've though about more than yours ....

[Eric Wieser]

I'm happy to take your word for it; I think my application doesn't care

[Eric Wieser]

Though maybe we need both; we could unify docs#clifford_algebra.star_smul and docs#quaternion.star_smul with a star_invariant_module typeclass

[Heather Macbeth]

Actually, maybe Floris and I need something slightly different -- not the fact that the conjugate-linear maps are real-linear themselves, but that the collection they form is a real vector space.

[Eric Wieser]

Doesn't docs#linear_map.module already provide that?

[Heather Macbeth]

Indeed, looks like it!

[Eric Wieser]

Unwinding the stack briefly; is starL' an acceptable hack for the purpose of #19038? It has the advantage of being above the porting tide, while adding a semilinear restrict_scalars would not be

[Heather Macbeth]

Eric Wieser said:

Doesn't docs#linear_map.module already provide that?

Looked at it briefly, this seems correct but the path is then littered with other tasks: a continuous-linear version of this construction, a vector bundle version of is_scalar_tower, and more ...

[Eric Wieser]

docs#continuous_linear_map.module already provides the next task I think?

[Eric Wieser]

It's hard to say for sure without actually asking Lean of course!

[Heather Macbeth]

Ah, very good!

[Eric Wieser]

And maybe docs#continuous_linear_map.is_scalar_tower (added in #10494) is your last task?

[Heather Macbeth]

The latter task should really be a vector bundle construction, so I don't think so. And I think there's also more to do on docs#continuous_linear_map.module: one needs to topologize this and normify it :(

[Eric Wieser]

docs#continuous_linear_map.to_normed_space also already exists

[Eric Wieser]

Heather Macbeth said:

at least in my application which I've though about more than yours ....

Did we conclude then that your application wouldn't benefit from restricting semilinear maps after all?

[Heather Macbeth]

Actually, I just came to the conclusion that it needs that too! But I don't think I will believe it until I've slept on it.

[Heather Macbeth]

Anyway, that has to happen after the port.

[Eric Wieser]

I would claim that #19038 can safely happen during the port :)

[Eric Wieser]

I can add a todo comment referencing the ideas here next to starL'