elements of an action which fix a set

Stream: Is there code for X?

[Eric Wieser]

Do we have a name for the following?

/-- The set of actions that leave elements in `s` unchanged -/
def what_am_i (M) {α} [has_scalar M α] (s : set α) : set M :=
{ m : M | ∀ x ∈ s, m • x = x }

The closest I can find is docs#intermediate_field.fixing_subgroup which is an extremely special case with M = E ≃ₐ[F] E and unused requirements on s

[Reid Barton]

It should be called something like the pointwise stabilizer of s

[Reid Barton]

For a single element, it would be the stabilizer

[Yakov Pechersky]

sUnion of stabilizer?

[Eric Wieser]

#11938 adds the above as fixing_submonoid and fixing_subgroup but only because that matches the one I found already

[Eric Wieser]

Yakov Pechersky said:

sUnion of stabilizer?

More like bInter:

lemma what_am_i_eq (M) {α} [group M] [mul_action M α] (s : set α) :
  ↑(⨅ b ∈ s, mul_action.stabilizer M b) = what_am_i M s :=
begin
  simp,
  ext, simp only [set.mem_Inter],
  refl,
end

[Yakov Pechersky]

Right! Turn that smile upside down.

[Eric Wieser]

Perhaps this doesn't need a name

[Eric Wieser]

The downside of the ⋂ approach is that docs#set.Inter (aka docs#set.has_Inf) is definitionally not as nice as the original

[Yaël Dillies]

That makes me definitionally unhappy.

[Reid Barton]

oh yeah I think I've been caught out by this before--is there a reason we couldn't change the complete_lattice instance or whatever to use the right-hand side of docs#set.mem_Inter as the definition?

[Eric Wieser]

Yes, we get caught up in universe problems if we try to replace the Inf field of complete_lattice with infi

[Reid Barton]

ah

[Eric Wieser]

We could treat set as a special case since it has special notation anyway, but that's probably stillnot worth it

[Eric Wieser]

There might be a middle ground where we have a has_lawful_infi.{u} α typeclass that provides infi in a particular universe and proves it's consistent with Inf

[Eric Wieser]

And then if we end up in a universe mess somewhere we can just conjure an instance built from the Inf.

[Eric Wieser]

But you could also argue that tweaking definitional equality isn't worth that trouble

[Reid Barton]

Wait no I don't understand now--set.Inter is a standalone top-level definition so we could just change it, right?

[Reid Barton]

I see what I said above was wrong but it's a slightly different thing.

[Eric Wieser]

Yes, we could change set.Inter but then ⨅ and ⋂ would no longer be two notations for the same thing

[Eric Wieser]

Which is useful because it encourages us to generalize set lemmas to lattices

[Eric Wieser]

The downside of the ⋂ approach is that docs#set.Inter (aka docs#set.has_Inf) is definitionally not as nice as the original (new Zulip thread)