# Zulip Chat Archive

## 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 `N`

happened (by computation) be equal but I couldn't `rw`

the 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 `H`

of `G`

which preserve subsets `Y`

of `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 `apply`

s changed to `refine`

s:

```
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