## Stream: new members

### Topic: mul_action : bihomomorphisms / scalar tower

#### Antoine Chambert-Loir (Apr 24 2022 at 09:59):

Assume M and N are monoids, with actions of M on α and of N on β,
I wish to consider pairs (φ : M →*N , f : α → β) such that φ(m) • f(a) = f(m • a) for all m, a.
Obviously, this can be implemented by a variant of docs#mul_action_hom,
but I guess that a more idiomatic version exists that uses docs#is_scalar_tower and the like.
What do you think?

#### Riccardo Brasca (Apr 24 2022 at 10:01):

Aren't these exactly semilinear maps?

#### Riccardo Brasca (Apr 24 2022 at 10:02):

Except that your monoids are multiplicative

#### Yaël Dillies (Apr 24 2022 at 10:07):

@Anne Baanen, how would such multiplicative semilinear maps fit in the current refactor?

#### Antoine Chambert-Loir (Apr 24 2022 at 10:08):

And there is no law on α, β, so that f: α → β is not required to satisfy anything.

#### Antoine Chambert-Loir (Apr 24 2022 at 10:10):

The interest of such a structure appeared when I had mul_action M α and mul_action N βwhere M and Nhappened (by computation) be equal but I couldn't rwthe equality…

#### Anne Baanen (Apr 24 2022 at 10:10):

Yaël Dillies said:

Anne Baanen, how would such multiplicative semilinear maps fit in the current refactor?

I don't think they would have anything special to them compared with semilinear maps. Those are a bit of an issue since the elaborator isn't always smart enough to work with a completely generic map_smul_sl (map_smul works fine now). I haven't had an opportunity to completely figure out why this is.

#### Anne Baanen (Apr 24 2022 at 10:16):

I guess we could have (up to to_additive) an ancestor of these semi-mul_action_hom and semilinear maps, if we define it along the lines of:

structure semi_mul_action_hom {α β F : Type*} (φ : F) (M N : Type*) [fun_like F α (λ _, β)] extends M →* N :=
(map_smul_sl : ∀ m n, to_fun (m • a) = φ m • to_fun a)


and then restrict the fun_like F parameter to ring_hom_class F in semilinear maps.

#### Anne Baanen (Apr 24 2022 at 10:18):

Or we could even have φ : α → β in the type, and require in the lemma statements that φ = coe_fn (φ' : α →+* β)

#### Riccardo Brasca (Apr 24 2022 at 10:26):

Ah, sorry, I misread the question

#### Eric Wieser (Apr 24 2022 at 10:54):

I would assume the thing to do here is generalize docs#mul_action_hom to take a φ argument, matching how we generalized linear_map

#### Eric Wieser (Apr 24 2022 at 10:55):

Since mul_action_hom only requires has_scalar, probably it should only require φ : M → N not φ : M →* N

#### Antoine Chambert-Loir (May 01 2022 at 23:43):

It's hard to propose a really minimal mwe, so let's me try to state where this story brought me into.
My main goal for the moment was to prove, given a global mul_action G X, a few instances of semi_mul_action_hom relative to appropriate subgroups Hof G which preserve subsets Yof X,
which means that the relevant maps are totally trivial, they map x to x, the only issue is to furnishing the appropriate coercions which, mathematically, are essentially obvious.
The real nightmare begins when I need to prove that these obvious maps have obvious properties such as being injective or surjective. Because for many proofs, I need to reprove the kind of belonging coercions that I had already proven to construct the maps.

I don't know whether these comments will ring a bell, you can have a look in branch#acl-Wielandt (files ad_sub_mul_action, or mul_action_bihom) if you wish.

#### Kevin Buzzard (May 02 2022 at 00:51):

lemma mem_sub_mul_action_of_fixing_subgroup_iff {s : set α} {x : α} :
x ∈ sub_mul_action_of_fixing_subgroup M s ↔ x ∉ s := iff.rfl


#### Kevin Buzzard (May 02 2022 at 00:58):

Is this progress

  { rintro ⟨⟨x, hx1⟩, hx2⟩,
refine ⟨⟨x, _⟩, rfl⟩,
-- ⊢ x ∈ sub_mul_action_of_fixing_subgroup M (insert a (coe '' s))
sorry,
},


with the sorry on line 650 or so of ad_sub_mul_actions.lean?

#### Kevin Buzzard (May 02 2022 at 01:02):

On line 600 or so:

to_fun := λ x,
begin
suffices : ↑x ∈ sub_mul_action_of_stabilizer M α a,
use x,
...


is not good style. You're defining data here so you should not be in tactic mode (your goal is not a Prop, and tactic mode can make lousy definitions).

#### Kevin Buzzard (May 02 2022 at 01:24):

Here's your proof written in this format:

to_fun := λ x, ⟨⟨(x : α), begin
rw mem_sub_mul_action_of_stabilizer_iff,
intro h,
apply (mem_sub_mul_action_of_fixing_subgroup_iff M).mp x.prop,
rw h, apply set.mem_insert,
end⟩,
begin { rw mem_sub_mul_action_of_fixing_subgroup_iff (stabilizer M a),
intro h,
apply (mem_sub_mul_action_of_fixing_subgroup_iff M).mp x.prop,
apply set.mem_insert_of_mem,
refine ⟨⟨(x : α), _⟩, ⟨h, rfl⟩⟩, }
end⟩,


Note that the proof of mem_sub_mul_action_of_fixing_subgroup_iff is refl so can be skipped (try deleting it!), meaning that there is lot of intro, apply, exact stuff which can be hence golfed into term mode. Here's that second proof with all the applys changed to refines:

  begin {
intro h,
refine (mem_sub_mul_action_of_fixing_subgroup_iff M).mp x.prop _,
refine set.mem_insert_of_mem _ _,
refine ⟨⟨(x : α), _⟩, ⟨h, rfl⟩⟩, }
end⟩,


and now we see that this golfs to

to_fun := λ x, ⟨⟨(x : α), begin
rintro (h : (x : α) = a),
apply (mem_sub_mul_action_of_fixing_subgroup_iff M).mp x.prop,
rw h, apply set.mem_insert,
end⟩,
λ h, (mem_sub_mul_action_of_fixing_subgroup_iff M).mp x.prop \$
set.mem_insert_of_mem _ ⟨⟨(x : α), _⟩, ⟨h, rfl⟩⟩⟩,


#### Kevin Buzzard (May 02 2022 at 01:37):

You've made this a def but function.bijective is a Prop so this is a theorem. The def is an equiv presumably, which is often nicer to make in general. I tidied up your other proof. Is this sorry fillable? I don't know what the maths means (your definitions don't have docstrings ;-) ).

def sub_mul_action_of_fixing_subgroup_of_stabilizer_bihom_bijective
(a : α) (s : set (sub_mul_action_of_stabilizer M α a)) :
function.bijective (sub_mul_action_of_fixing_subgroup_of_stabilizer_bihom M a s).to_fun :=
begin
split,
{ rintros ⟨x, hx1⟩ ⟨y, hy1⟩ h,
simpa [sub_mul_action_of_fixing_subgroup_of_stabilizer_bihom] using h },
{ rintro ⟨⟨x, hx1⟩, hx2⟩,
refine ⟨⟨x, _⟩, rfl⟩,
-- ⊢ x ∈ sub_mul_action_of_fixing_subgroup M (insert a (coe '' s))
sorry,
},
end


#### Kevin Buzzard (May 02 2022 at 01:42):

I don't know what the question is in mul_action_bihom. Here's some golfing of the last lemma:

lemma mul_of_preimage_eq (f : mul_action_bihom M X N Y) (B : set Y) (m : M) :
m • f.to_fun ⁻¹' B = f.to_fun ⁻¹' ((f.to_monoid_hom m) • B) :=
begin
ext,
simp only [set.mem_preimage],
split,
{ rintro ⟨y, hy, rfl⟩, -- combine intro and obtain
simp only [set.mem_preimage] at hy,
rw ← f.map_smul',
exact set.smul_mem_smul_set hy },
{ rintro ⟨b, hb, hbx⟩,
refine ⟨m⁻¹ • x, _, _⟩, -- combine use and split
{ simpa [← f.map_smul', ← hbx] using hb }, -- simp, rewrite, simp, just do it all in one go
simp only [smul_inv_smul], }
end


#### Antoine Chambert-Loir (May 02 2022 at 13:48):

Thank you, @Kevin Buzzard , this has been very helpful.

Last updated: Dec 20 2023 at 11:08 UTC