mul_action : bihomomorphisms / scalar tower

Stream: new members

[Antoine Chambert-Loir]

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]

Aren't these exactly semilinear maps?

[Riccardo Brasca]

Except that your monoids are multiplicative

[Yaël Dillies]

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

[Antoine Chambert-Loir]

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

[Antoine Chambert-Loir]

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]

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]

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]

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

[Riccardo Brasca]

Ah, sorry, I misread the question

[Eric Wieser]

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]

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

[Antoine Chambert-Loir]

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]

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]

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]

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]

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]

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]

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]

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