Zulip Chat Archive

Stream: maths

Topic: to_additive mismatch


view this post on Zulip 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 -/

view this post on Zulip Kevin Buzzard (Mar 12 2021 at 10:51):

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

view this post on Zulip Ashwin Iyengar (Mar 12 2021 at 10:52):

Yep exactly

view this post on Zulip Ashwin Iyengar (Mar 12 2021 at 10:53):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Mar 12 2021 at 11:12):

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

view this post on Zulip Ashwin Iyengar (Mar 12 2021 at 12:23):

(deleted)

view this post on Zulip Ashwin Iyengar (Mar 12 2021 at 12:30):

Sorry ignore that

view this post on Zulip 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...

view this post on Zulip Ashwin Iyengar (Mar 12 2021 at 13:17):

Is this a sensible thing to do?

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

view this post on Zulip Ashwin Iyengar (Mar 12 2021 at 13:17):

Proving map_mul' and map_one' seems to be a headache

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Gabriel Ebner (Mar 12 2021 at 14:05):

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

view this post on Zulip Eric Wieser (Mar 12 2021 at 14:56):

Do you meanf x = (to_mul f) x?

view this post on Zulip Eric Wieser (Mar 12 2021 at 14:59):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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 }

view this post on Zulip Ashwin Iyengar (Mar 12 2021 at 15:08):

Do I need to somehow unfold additive.has_add?

view this post on Zulip Eric Wieser (Mar 12 2021 at 15:09):

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

view this post on Zulip Ashwin Iyengar (Mar 12 2021 at 15:09):

oh whoops

view this post on Zulip Ashwin Iyengar (Mar 12 2021 at 15:11):

Still doesn't simp automatically with that line though

view this post on Zulip Eric Wieser (Mar 12 2021 at 15:12):

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

view this post on Zulip Ashwin Iyengar (Mar 12 2021 at 15:13):

Thanks!

view this post on Zulip Gabriel Ebner (Mar 12 2021 at 15:41):

Eric Wieser said:

Do you meanf x = (to_mul f) x?

The parentheses are optional.

view this post on Zulip 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