# Zulip Chat Archive

## Stream: maths

### Topic: to_additive mismatch

#### Ashwin Iyengar (Mar 12 2021 at 10:24):

This is a little annoying: `to_additive`

fails because it can't unify `x - y`

with `x + -y`

. If I change the definition of `conj`

in `add_group_filter_basis`

to `x₀+x+-x₀`

then it works, but that seems ugly. Does anyone know a cleaner way of handling this?

```
import topology.algebra.group
/-- An alternative characterization of a `topological_add_group`, given by
axiomatizing properties of a filter basis for the neighborhood filter at `0`. -/
class add_group_filter_basis (G : Type*) [add_group G] extends filter_basis G :=
(zero : ∀ {U}, U ∈ sets → (0 : G) ∈ U)
(add : ∀ {U}, U ∈ sets → ∃ V ∈ sets, V + V ⊆ U)
(neg : ∀ {U}, U ∈ sets → ∃ V ∈ sets, V ⊆ (λ x, -x) ⁻¹' U)
(conj : ∀ x₀, ∀ U ∈ sets, ∃ V ∈ sets, V ⊆ (λ x, x₀+x-x₀) ⁻¹' U)
/-- An alternative characterization of a `topological_group` structure, given by
axiomatizing properties of a filter basis for the neighborhood filter at `1`. -/
@[to_additive]
class group_filter_basis (G : Type*) [group G] extends filter_basis G :=
(one : ∀ {U}, U ∈ sets → (1 : G) ∈ U)
(mul : ∀ {U}, U ∈ sets → ∃ V ∈ sets, V * V ⊆ U)
(inv : ∀ {U}, U ∈ sets → ∃ V ∈ sets, V ⊆ (λ x, x⁻¹) ⁻¹' U)
(conj : ∀ x₀, ∀ U ∈ sets, ∃ V ∈ sets, V ⊆ (λ x, x₀*x*x₀⁻¹) ⁻¹' U)
instance group_filter_basis.has_mem {α : Type*} [group α] :
has_mem (set α) (group_filter_basis α) := ⟨λ s f, s ∈ f.sets⟩
instance add_group_filter_basis.has_mem {α : Type*} [add_group α] :
has_mem (set α) (add_group_filter_basis α) := ⟨λ s f, s ∈ f.sets⟩
@[to_additive]
lemma mul_blah {G : Type*} [group G] (basis: group_filter_basis G) (g : G) {W}
(hW : W ∈ basis) : true :=
begin
rcases group_filter_basis.conj g W hW,
trivial
end
/--
type mismatch at application
(add_group_filter_basis.conj g W hW).dcases_on
term
add_group_filter_basis.conj g W hW
has type
∃ (V : set G) (H : V ∈ add_group_filter_basis.to_filter_basis.sets), V ⊆ (λ (x : G), g + x - g) ⁻¹' W
but is expected to have type
∃ (V : set G) (H : V ∈ add_group_filter_basis.to_filter_basis.sets), V ⊆ (λ (x : G), g + x + -g) ⁻¹' W -/
```

#### Kevin Buzzard (Mar 12 2021 at 10:51):

So your issue is that multiplicatively $ghg^{-1}$ looks nice but $gh/g$ looks odd because who does division in groups -- they're not in general commutative. Conversely $a+b-a$ looks nice but $a+b+(-a)$ looks odd because addition is always commutative so subtraction is far more natural and useful than the weird negation function.

#### Ashwin Iyengar (Mar 12 2021 at 10:52):

Yep exactly

#### Ashwin Iyengar (Mar 12 2021 at 10:53):

I guess I could just change it to $a + b + (-a)$, but I hope this won't cause weird errors down the line

#### Eric Wieser (Mar 12 2021 at 11:11):

If you made a `conj a b`

and `add_conj a b`

API, then the actual definition won't matter any more

#### Eric Wieser (Mar 12 2021 at 11:12):

Then you can have `conj`

defined with `inv`

and `add_conj`

defined with `neg`

, but as long as you don't unfold it once you've made the API then `to_additive`

won't care

#### Eric Wieser (Mar 12 2021 at 11:12):

We have docs#mul_aut.conj but no add_aut.conj right now

#### Ashwin Iyengar (Mar 12 2021 at 12:23):

(deleted)

#### Ashwin Iyengar (Mar 12 2021 at 12:30):

Sorry ignore that

#### Ashwin Iyengar (Mar 12 2021 at 12:55):

Eric Wieser said:

We have docs#mul_aut.conj but no add_aut.conj right now

Ah right. I tried adding `add_aut.conj`

but it's a bit awkward because `add_aut A`

is a `group`

and not an `add_group`

...

#### Ashwin Iyengar (Mar 12 2021 at 13:17):

Is this a sensible thing to do?

```
def conj [group G] : G →* add_aut (additive G) :=
```

#### Ashwin Iyengar (Mar 12 2021 at 13:17):

Proving `map_mul'`

and `map_one'`

seems to be a headache

#### Anne Baanen (Mar 12 2021 at 13:21):

Eric Wieser said:

If you made a

`conj a b`

and`add_conj a b`

API, then the actual definition won't matter any more

I would even go as far as putting `@[to_additive]`

on `def conj (a b) := a * b * a⁻¹`

, and a pair of lemmas `conj_eq_mul_mul_inv`

and `conj_eq_mul_div`

. Just let the user choose between the two ways to write it.

#### Anne Baanen (Mar 12 2021 at 13:22):

Perhaps even simp lemmas rewriting `a * b * a\-1 = conj a b`

and `a * b / a = conj a b`

(with the caveat that you would need to copy the whole `group`

simp API as well).

#### Eric Wieser (Mar 12 2021 at 13:42):

Ashwin Iyengar said:

Is this a sensible thing to do?

`def conj [group G] : G →* add_aut (additive G) :=`

I think you'd have a better time with

```
def add_aut.conj {G : Type*} [add_group G] : multiplicative G →* add_aut G
```

or

```
def add_aut.conj {G : Type*} [add_group G] : G →+ additive (add_aut G)
```

#### Eric Wieser (Mar 12 2021 at 13:55):

This seems to work out alright:

```
instance additive.has_coe_to_fun {α : Type*} [has_coe_to_fun α] : has_coe_to_fun (additive α) := ⟨
λ a,
has_coe_to_fun.F a.to_mul, λ a, has_coe_to_fun.coe a.to_mul⟩
variables {G : Type*} [add_group G]
def add_aut.conj : G →+ additive (add_aut G) :=
{ to_fun := λ x, @additive.of_mul (add_aut G)
{ to_fun := λ y, x + y - x,
inv_fun := λ y, -x + y + x,
left_inv := sorry,
right_inv := sorry,
map_add' := sorry, },
map_zero' := sorry,
map_add' := sorry,}
variables (x y : G)
example : add_aut.conj x y = x + y - x := rfl
```

#### Eric Wieser (Mar 12 2021 at 13:55):

Perhaps @Gabriel Ebner has a feeling for whether `additive.has_coe_to_fun`

is a reasonable thing to exist

#### Gabriel Ebner (Mar 12 2021 at 14:05):

Which way should the simp lemma go? `f x = to_mul f x`

?

#### Eric Wieser (Mar 12 2021 at 14:56):

Do you mean`f x = (to_mul f) x`

?

#### Eric Wieser (Mar 12 2021 at 14:59):

I can't even work out how to state that lemma

#### Eric Wieser (Mar 12 2021 at 15:03):

This seems to work:

```
def has_coe_to_fun.simps.coe {α : Sort*} [has_coe_to_fun α] : Π a : α, has_coe_to_fun.F a :=
coe_fn
@[simps]
instance additive.has_coe_to_fun {α : Type*} [has_coe_to_fun α] : has_coe_to_fun (additive α) := ⟨
λ a,
has_coe_to_fun.F a.to_mul, λ a, coe_fn a.to_mul⟩
#check additive.has_coe_to_fun_coe
-- additive.has_coe_to_fun_coe : ∀ (a : additive ?M_1), ⇑a = ⇑(⇑additive.to_mul a)
```

#### Ashwin Iyengar (Mar 12 2021 at 15:07):

@Eric Wieser I'm having trouble proving the last `map_add'`

in your suggestion, it's having trouble figuring out that it needs to use `add_aut.mul_apply`

with the additive notation

#### Ashwin Iyengar (Mar 12 2021 at 15:08):

```
/-- group conjugation as a group homomorphism into the automorphism group.
`conj g h = g + h - g` -/
def conj [add_group G] : G →+ additive (add_aut G) :=
{ to_fun := λ g, @additive.of_mul (add_aut G)
{ to_fun := λ h, g + h - g,
inv_fun := λ h, -g + h + g,
left_inv := λ _, by simp [add_assoc],
right_inv := λ _, by simp [add_assoc],
map_add' := by simp [add_assoc, sub_eq_add_neg] },
map_add' := begin
intros x y,
ext,
simp [add_assoc, sub_eq_add_neg],
end, -- }λ _ _, by ext; simp [add_assoc, sub_eq_add_neg] }
map_zero' := by ext; simpa }
```

#### Ashwin Iyengar (Mar 12 2021 at 15:08):

Do I need to somehow unfold `additive.has_add`

?

#### Eric Wieser (Mar 12 2021 at 15:09):

Where did the `@additive.of_mul (add_aut G)`

line go?

#### Ashwin Iyengar (Mar 12 2021 at 15:09):

oh whoops

#### Ashwin Iyengar (Mar 12 2021 at 15:11):

Still doesn't simp automatically with that line though

#### Eric Wieser (Mar 12 2021 at 15:12):

`apply additive.to_mul.injective,`

seems to get you out of the trouble

#### Ashwin Iyengar (Mar 12 2021 at 15:13):

Thanks!

#### Gabriel Ebner (Mar 12 2021 at 15:41):

Eric Wieser said:

Do you mean

`f x = (to_mul f) x`

?

The parentheses are optional.

#### Ashwin Iyengar (Mar 12 2021 at 17:12):

I added @Eric Wieser's coercion in #6657, but was made aware that #6045 exists and might conflict

Last updated: May 09 2021 at 10:11 UTC