semi-mul_action_hom

Stream: maths

[Antoine Chambert-Loir]

For my work on group actions (proving a theorem of Jordan), I have introduced something which I called mul_action_bihom and is to mul_action_homof what the semilinear maps introduced in mathlib by @Rob Lewis , @Frédéric Dupuis and @Heather Macbeth are to linear maps.
Now that I will start tidying up my work, it might be interesting to refactor the mul_action_homin this direction.

One motivation is to diminish the numbers of explicit coercions/decoercions that my naïve approach often required…

A reasonable definition for these equivariant maps is:

structure equivariant_map {M N : Type*} (φ : M → N)
  (α : Type*) (β : Type*) [has_scalar M α] [has_scalar N β] :=
(to_fun : α → β)
(map_smul' : ∀ (m : M) (a : α), to_fun (m • a) = φ(m) • to_fun (a))

notation α ` →ₑ[`:25 φ:25 `] `:0 β:0 := equivariant_map φ α β
notation α ` →[`:25 M:25 `] `:0 β:0 := equivariant_map (@id M) α β

There are two issues for the moment:

• I don't really understand how to build this into a fun_like class.

• Composition of semilinear maps relies on ring_hom_comp_triple which expresses for three ring morphisms are in composition, and I wonder whether I have to introduce such a class. (The reasons explained in Formalized functional analysis with semilinear maps, by Frédéric Dupuis, Robert Y. Lewis, Heather Macbeth are not completely clear to me.

What I did is in branch#acl-Wielandt/acl-sandbox/group_theory/jordan/equivariant_map.lean

[Notification Bot]

This topic was moved here from #new members > semi-mul_action_hom by Heather Macbeth.

[Heather Macbeth]

@Antoine Chambert-Loir Something that's interesting to me is that this has less structure than Frédéric, Rob and I needed. We required the φ (in your notation) to be a ring homomorphism. Yours, as implemented here, is a bare function, but what kind of thing would it be in your use case?

It matters because the kind of object φ is appears in the type signature of equivariant_map.

[Heather Macbeth]

As you observe, the ring_home_comp_triple mechanism matters if you expect to be doing nontrivial compositions of equivariant maps. Do you?

[Antoine Chambert-Loir]

Eventually, in the case I'm interested in,Mand Nwill be groups and φ will be a group morphism.

[Antoine Chambert-Loir]

And yes, the group will move in the composition. (Although I did not really use the composition as an equivariant map itself, and applied the equivariant maps one by one.)

[Heather Macbeth]

This might be a case where the ring_hom_comp_triple mechanism is not useful. It's useful for us (for linear maps) because we work in settings where M and N (rings for us) are given quite explicitly ($\mathbb{R}$, $\mathbb{C}$, etc), there is a finite list of homomorphisms φ of interest (id, conj), and the ring_hom_comp_triple mechanism silently records all of the relationships among these homomorphisms (like conj.comp conj = id, etc). If you're in a more general setting where the M, N and φ are not known explicitly, this trick might not be useful.

[Heather Macbeth]

For now, you could try just defining the composition naively, so the composition of a equivariant_map Φ₁₂ α₁ α₂ and a equivariant_map Φ₂₃ α₂ α₃ is a equivariant_map (Φ₂₃.comp Φ₁₂) α₁ α₃. Also write a "homomorphism-switching" constructor which takes a equivariant_map φ α β and a hypothesis (h : Φ = Ψ) and produces an equivariant_map Ψ α β.

[Heather Macbeth]

Or, it may be that your unbundled version is_equivariant_map is more convenient (with otherwise the same notes as in my previous message).

[Antoine Chambert-Loir]

OK, so I'll just define it naïvely and see whether it suffices!

[Antoine Chambert-Loir]

A naïve question : why does function.comp ψ φ work, and not ψ.comp φ as you wrote?

[Yaël Dillies]

That's because dot notation doesn't work on f : α → β (but it does on f : α →* β). I believe this could be fixed.

[Antoine Chambert-Loir]

Can you give me a hint on where to look?

[Yaël Dillies]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/function.20namespace/near/256048388

[Heather Macbeth]

You can just write Ψ ∘ Φ; in my head I had already upgraded them to group homomorphisms (for which you would indeed write Ψ.comp Φ), but maybe there's no advantage.

[Eric Wieser]

I think there's a danger here that if σ is a bare function, higher order unification will kick in and ruin your day, which it can't do for bundled morphisms

[Heather Macbeth]

If Antoine uses his unbundled version is_equivariant_map, this won't be an issue, right? Because it won't appear in a type signature?

[Oliver Nash]

This reminds me that I previously wondered if we definitely needed a new structure to handle semi-linear: after all they are just plain old __linear__ maps, it's just that we need a good setup for extension / restriction of scalars to make this all work.

[Oliver Nash]

In the case of equivariant maps here, one could try to force mul_action_hom to do the work like this:

import algebra.hom.group_action

local notation α ` →ₑ[`:25 M,φ:25 `] `:0 β:0 := @mul_action_hom M α _ β ⟨λ m b, (φ m) • b⟩

variables {M N α β : Type*} [has_scalar M α] [has_scalar N β] (φ : M → N)

-- Let `f` be one of these equivariant maps
variables (f : α →ₑ[M,φ] β)

-- Indeed it is equivariant!
example (x : α) (m : M) : f (m • x) = (φ m) • f x :=
@mul_action_hom.map_smul M α _ β ⟨λ m b, (φ m) • b⟩ _ _ _

[Oliver Nash]

I guess one would need some sort of type synonym for the pair β, φ and that would carry the M action as an instance. It's not clear to me that this would work well but it might be worth a few minutes' thought.

[Heather Macbeth]

You're suggesting to encode semilinear as "linear with respect to a twisted scalar structure on the codomain"? For example, in the conjugate-linear case this amounts to encoding conjugate-linear as "linear with respect to the complex conjugate vector space"?

[Heather Macbeth]

Frédéric did try this out at some point in one extended example, the Riesz representation theorem, and found the type synonyms behaved a bit unpredictably. Here's some of the code from that experiment: #5830.

[Heather Macbeth]

For what it's worth, this is how semilinear maps are encoded in Coq, and we had some discussion of the relative merits back in March: https://machinemath.zulipchat.com/#narrow/stream/316927-presentations/topic/Semi-linear.20maps.20in.20Lean

[Antoine Chambert-Loir]

One additional question that I have is about equivariant_map that woud both extend equiv and equivariant_map.
I am not sure that it is mathematically so interesting, but they appear occasionnally. One issue when $f : X \to Y$ is a bijective equivariant map, its inverse is not always equivariant because the important case is that where the map $\phi$ on scalars is only surjective.

But my true question lies in the proper way to do it in mathlib: one can start from a function, add map_mul, and then add the rest to make an equiv. And one should have .to_equiv, and .to_equivariant_map. (All of this as fun_like?)

[Eric Wieser]

If you use old_structure_cmd then you can justextend all the weaker notions

[Eric Wieser]

(and create a parallel fun_like class for each structure you create)

[Oliver Nash]

Heather Macbeth said:

Frédéric did try this out [...] Here's some of the code from that experiment: #5830.

Interesting! It's good to have this PR as a record of what was explored.

[Eric Wieser]

That branch seems to take the approach of putting the type synonym on the module; was putting the synonym on the ring also tried?