to_additive mismatch

Stream: maths

[Ashwin Iyengar]

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]

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]

Yep exactly

[Ashwin Iyengar]

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]

If you made a conj a b and add_conj a b API, then the actual definition won't matter any more

[Eric Wieser]

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]

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

[Ashwin Iyengar]

(deleted)

[Ashwin Iyengar]

Sorry ignore that

[Ashwin Iyengar]

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]

Is this a sensible thing to do?

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

[Ashwin Iyengar]

Proving map_mul' and map_one' seems to be a headache

[Anne Baanen]

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]

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]

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]

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]

Perhaps @Gabriel Ebner has a feeling for whether additive.has_coe_to_fun is a reasonable thing to exist

[Gabriel Ebner]

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

[Eric Wieser]

Do you meanf x = (to_mul f) x?

[Eric Wieser]

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

[Eric Wieser]

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]

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

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

Do I need to somehow unfold additive.has_add?

[Eric Wieser]

Where did the @additive.of_mul (add_aut G) line go?

[Ashwin Iyengar]

oh whoops

[Ashwin Iyengar]

Still doesn't simp automatically with that line though

[Eric Wieser]

apply additive.to_mul.injective, seems to get you out of the trouble

[Ashwin Iyengar]

Thanks!

[Gabriel Ebner]

Eric Wieser said:

Do you meanf x = (to_mul f) x?

The parentheses are optional.

[Ashwin Iyengar]

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