injective scalar actions

Stream: Is there code for X?

[Eric Wieser]

Do we have a typeclass that says ∀ b : β, function.injective ((• b) : α → β) or ∀ b : β, ∀ a1 a2 : α, a1 • b = a2 • b → a1 = a2 or similar?

I found docs#faithful_mul_semiring_action; should I just generalize that to has_faithful_scalar and make it a mixin?

[Reid Barton]

That's not the same as what you're asking about. (Note that for a mul_semiring action, (• 0) is basically never injective.) What you want is more like a free action.

[Damiano Testa]

Is docs#is_smul_regular what you are after, but made into a typeclass? I was the one who introduced is_smul_regular, but I did not make it into a typeclass.

[Anne Baanen]

is_smul_regular states that left-smul is injective, Eric is looking for right-smul, right?

[Damiano Testa]

Ah, I was unsure which injectivity it was that Eric wanted...

[Eric Wieser]

Reid Barton said:

That's not the same as what you're asking about. (Note that for a mul_semiring action, (• 0) is basically never injective.) What you want is more like a free action.

Oh you're right, I got my binders in the wrong places

[Anne Baanen]

BTW: I was thinking about defining something like @Eric Wieser's proposed typeclass, namely a typeclass for algebras where algebra_map is injective.

[Anne Baanen]

So you're looking for function.injective ((•) : α → β → β), then?

[Eric Wieser]

yes, I think I am

[Eric Wieser]

Which is what faithful_mul_semiring_action states after all, I think?

[Anne Baanen]

Looks like it

[Anne Baanen]

So yes, I agree with "just generalize that to has_faithful_scalar and make it a mixin?"

[Eric Wieser]

#8555

[Eric Wieser]

I managed to bump the number of instances from 2 to 8, so this generalization seems pretty justified. I'm sure there are more, but I'm out of motivation to look for them.