## Stream: maths

#### 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. -/
(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. -/
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⟩
has_mem (set α) (add_group_filter_basis α) := ⟨λ s f, s ∈ f.sets⟩

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
term
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.

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

(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]

{ to_fun := λ y, x + y - x,
inv_fun := λ y, -x + y + x,
left_inv := sorry,
right_inv := sorry,
map_zero' := 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 meanf 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⟩



#### 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 -/
{ to_fun := λ h, g + h - g,
inv_fun := λ h, -g + h + g,
left_inv := λ _, by simp [add_assoc],
right_inv := λ _, by simp [add_assoc],
intros x y,
ext,
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?

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

Thanks!

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

Eric Wieser said:

Do you meanf 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