hom.op_inv

Stream: Is there code for X?

[Damiano Testa]

Dear All,

is a definition similar to the one below available already?

Thanks!

import algebra.group.opposite

open mul_opposite

@[to_additive]
def hom.op_inv {α : Type*} [group α] : α →* αᵐᵒᵖ :=
⟨λ x, op x⁻¹, by simp, by simp⟩

[Yaël Dillies]

cc @Mantas Baksys

[Yaël Dillies]

You probably want to name it monoid_hom.op_inv and have all other options, like mul_hom.op_inv, monoid_with_zero_hom.op_inv, the additive versions...

[Damiano Testa]

Ok, thanks! At least, it was not simply a matter of adding docs# in front of my name and finding it!

[Damiano Testa]

I think that I would even prefer to have

@[to_additive]
def mul_opposite.op_inv_equiv {α : Type*} [group α] : α ≃* αᵐᵒᵖ :=
{ to_fun    := λ x : α, op x⁻¹,
  inv_fun   := λ x : αᵐᵒᵖ, unop x⁻¹,
  left_inv  := λ x, by simp,
  right_inv := λ x, by simp,
  map_mul'  := λ x y, by simp }

[Mantas Baksys]

I've added some new instances to op in my PR #12931 but your definition was out of scope, so I didn't touch it :smile:

[Mantas Baksys]

Damiano Testa said:

I think that I would even prefer to have

@[to_additive]
def equiv.op_inv {α : Type*} [group α] : α ≃* αᵐᵒᵖ :=
{ to_fun    := λ x : α, op x⁻¹,
  inv_fun   := λ x : αᵐᵒᵖ, unop x⁻¹,
  left_inv  := λ x, by simp,
  right_inv := λ x, by simp,
  map_mul'  := λ x y, by simp }

How about mul_opposite.op_inv_equiv for the name?

[Damiano Testa]

Mantas, thanks for the input! I updated the name!

[Damiano Testa]

While we are at it, where should this definition go?

[Damiano Testa]

(Note: I would like to keep the PR small, simply containing this definition and maybe a couple of simp/rfl lemmas that go with it! I would rather not also do climb the has_mul/mul_one_class/.../field class-ladder!)

[Yaël Dillies]

I would do αᵐᵒᵖ ≃* α to have the more complicated stuff on the LHS.

[Damiano Testa]

Found it! I think that it is docs#mul_equiv.inv'. The direction is the opposite to the one that Yaël suggests.

[Yaël Dillies]

Can you unify docs#mul_equiv.inv and docs#mul_equiv.inv' by working over a div_inv_monoid?

[Eric Wieser]

Probably not, because a div_inv_monoid tells you nothing about how inv behaves

[Eric Wieser]

Yaël Dillies said:

Can you unify docs#mul_equiv.inv and docs#mul_equiv.inv' by working over a div_inv_monoid?

I think you're muddling things, one of these is for group and the other for comm_group. Did you mean docs#mul_equiv.inv₀?

[Eric Wieser]

We seem not to have mul_equiv.inv₀' for group_with_zero

[Yaël Dillies]

Ah it's still the same problem that we have no typeclass stronger than has_involutive_inv and monoid and weaker than group and group_with_zero.

[Damiano Testa]

What would be this intermediate typeclass? Something where the inverse of a product is the (reversed) product of the inverses?

[Yaël Dillies]

Is that enough for inv to be involutive? In any case, it should be stronger than div_inv_monoid.

[Yaël Dillies]

For the record, such a typeclass would allow us to deduplicate docs#set.div_inv_monoid and docs#set.div_inv_monoid'