## Stream: maths

### Topic: homeo equiv etc.

#### Patrick Massot (Apr 03 2018 at 21:08):

A more specific version of https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/structure.20vs.20class/near/124574243 (it may be easier to understand my problem by looking at code) is https://github.com/PatrickMassot/lean-scratchpad/blob/master/src/support.lean#L188 where I'm clearly very stupidly trying to Lean some trivial lemma. I'm completely tangled in coercions and type classes

#### Patrick Massot (Apr 03 2018 at 21:09):

I need two version of supp because I don't know how to have only one

#### Patrick Massot (Apr 03 2018 at 21:10):

Then we have a classical rw failure on line 193 (always the same thing, rw itself doesn't do some kind of elaboration or reduction that is needed, and I still can't quite point out what)

#### Patrick Massot (Apr 03 2018 at 21:11):

Then I would like line 196 to be unnecessary (with the ugly  (g.to_equiv).inv_fun never appearing)

#### Patrick Massot (Apr 03 2018 at 21:12):

And finally the computation which should be easy (but still the core of the proof) and cannot do it

#### Patrick Massot (Apr 03 2018 at 21:13):

I'd like to know whether the full setup is broken from the beginning or I only need a couple a carefully crafted simp lemmas to hide this mess (and prove stuff).

#### Chris Hughes (Apr 03 2018 at 21:20):

cons_inj tells me about the lists being equal. Oops wrong topic.

#### Patrick Massot (Apr 05 2018 at 20:23):

I can see this topic has not much success. Maybe the context is too complicated because of topology. But I really think this will come up in other places. The question is: how to do group theory with groups of transformations? As long as you don't need to use the inverse of a transformation, you can easily functions and composition of function. But what about inverses? Say I'm working with permutations of a type (not necessarily encoded as perm in current mathlib). I define the support of a permutation f as the complement supp f of the fixed point set (no topology here). I want to prove supp gfg⁻¹ = g(supp f). And ideally I would really like f, g and g⁻¹ to live in a type endowed with a group structure, because I have other group theoretic stuff to do. What encoding should I use? How to then talk about the image of a subset as in g(supp f)?

#### Kevin Buzzard (Apr 05 2018 at 20:28):

I got as far as cutting and pasting a 230 line file and then realising I didn't have the imports

#### Kevin Buzzard (Apr 05 2018 at 20:29):

You define suppp f to be supp f?

#### Patrick Massot (Apr 05 2018 at 20:30):

If you want to directly play with code it's much faster to git clone

#### Patrick Massot (Apr 05 2018 at 20:30):

Yes, that definition is part of the problem

#### Patrick Massot (Apr 05 2018 at 20:30):

I couldn't avoid it

#### Patrick Massot (Apr 05 2018 at 20:33):

It's part of coercion/extension hell

#### Patrick Massot (Apr 05 2018 at 20:33):

supp is defined on functions from X to X

#### Patrick Massot (Apr 05 2018 at 20:34):

homeos have coercions to functions

#### Patrick Massot (Apr 05 2018 at 20:34):

but it's not enough

#### Patrick Massot (Apr 05 2018 at 20:34):

try to replace suppp by supp in the statement following that def and it won't type check

#### Patrick Massot (Apr 05 2018 at 20:35):

But it's probably easier to solve the problem as I described it today than to add the topology layer

#### Kevin Buzzard (Apr 05 2018 at 20:36):

It's just too hard to make it work.

#### Kevin Buzzard (Apr 05 2018 at 20:36):

I have mathlib not compiling.

make what work?

#### Patrick Massot (Apr 05 2018 at 20:36):

I just pushed a version compatible with latest Lean nightly and mathlib head

#### Patrick Massot (Apr 05 2018 at 20:37):

(only handling a renamed lemma)

#### Kevin Buzzard (Apr 05 2018 at 20:40):

Now I have errors in commutators.lean and groups.lean

#### Patrick Massot (Apr 05 2018 at 20:40):

those are old stuff irrelevant here

#### Patrick Massot (Apr 05 2018 at 20:40):

they are not updated

#### Patrick Massot (Apr 05 2018 at 20:40):

(this repo is my garbage repo, I'm sorry)

#### Patrick Massot (Apr 05 2018 at 20:40):

Everything imported in support.lean is ok

#### Kevin Buzzard (Apr 05 2018 at 20:41):

OK it now compiles. What's the question?

#### Kevin Buzzard (Apr 05 2018 at 20:41):

Not that I'm likely to be able to answer it...

#### Patrick Massot (Apr 05 2018 at 20:42):

How do you sort out the mess with supp vs suppp, fundamental vs fundamental'', how to remove the sorries in the proof of supp_conj

#### Chris Hughes (Apr 05 2018 at 20:44):

open equiv
variables {α : Type*}

lemma mul_apply (a b : perm α) (x : α) : (a * b) x = (a (b x)) := rfl

@[simp] lemma one_apply (x : α) : (1 : perm α) x = x := rfl

def support (a : perm α) : set α := {x : α | a x ≠ x}

example (f g : perm α) : support (g * f * g⁻¹) = set.image g (support f) :=


#### Mario Carneiro (Apr 06 2018 at 04:40):

This works for supp_conj:

lemma supp_conj (f g : homeo X X) : supp (conj g f : homeo X X) = g '' supp f :=


#### Mario Carneiro (Apr 06 2018 at 05:23):

Here's a proof of supp_conj:

-- should be in equiv.lean
theorem equiv.left_inverse (f : α ≃ β) : left_inverse f.symm f := f.left_inv

theorem equiv.right_inverse (f : α ≃ β) : function.right_inverse f.symm f := f.right_inv

-- should be in homeos.lean
theorem homeo.left_inverse (f : homeo α β) : left_inverse f.symm f := f.left_inv

theorem homeo.right_inverse (f : homeo α β) : function.right_inverse f.symm f := f.right_inv

theorem homeo.bijective (f : homeo α β) : bijective f := f.to_equiv.bijective

@[simp] theorem aut_mul_val (f g : homeo α α) (x) : (f * g) x = f (g x) :=
homeo.comp_val _ _ _

@[simp] theorem aut_one_val (x) : (1 : homeo α α) x = x := rfl

@[simp] theorem aut_inv (f : homeo α α) : f⁻¹ = f.symm := rfl

lemma supp_conj (f g : homeo X X) : supp (conj g f : homeo X X) = g '' supp f :=
begin
unfold supp,
rw homeo.image_closure,
congr_n 1,
apply set.ext (λ x, _),
rw mem_image_iff_of_inverse g.left_inverse g.right_inverse,
apply not_congr,
dsimp [conj],
exact calc
(g * f * g⁻¹) x = x
↔ g⁻¹ (g (f (g⁻¹ x))) = g⁻¹ x : by simp [(g⁻¹).bijective.1.eq_iff]
... ↔ (f (g⁻¹ x)) = g⁻¹ x : by rw [← aut_mul_val, mul_left_inv]; simp
end


#### Patrick Massot (Apr 06 2018 at 05:36):

A million thanks!

#### Patrick Massot (Apr 06 2018 at 05:36):

This looks very nice

#### Patrick Massot (Apr 06 2018 at 05:37):

Right now I'm at the train station typing on my phone but I'll try this on the train

#### Patrick Massot (Apr 06 2018 at 05:40):

Question about stuff you indicated as belonging to homeos.lean: are those restatements needed because of modeling mistakes I made or is it normal? I don't mind having them but I try to understand how to do things right.

#### Mario Carneiro (Apr 06 2018 at 05:43):

It is normal. Since you have a coe_fn instance for homeo, the coercion there is not written by composing other coercions so you have to restate theorems about the underlying function if you want them as simp lemmas or projections

#### Mario Carneiro (Apr 06 2018 at 05:45):

I put all the stuff together and PR'd it to your repo: https://github.com/PatrickMassot/lean-scratchpad/pull/1

#### Patrick Massot (Apr 06 2018 at 05:48):

Should I remove this coercion and have a coercion to equiv?

#### Mario Carneiro (Apr 06 2018 at 05:49):

I think it is okay, especially if you expect it will get a lot of use. Otherwise the arrows can pile up

#### Patrick Massot (Apr 06 2018 at 05:55):

Ok. Thank you very much

#### Patrick Massot (Apr 06 2018 at 05:55):

I even managed to merge using the crappy train station wifi

#### Mario Carneiro (Apr 06 2018 at 05:58):

let me know if you want an explanation on something I did there

#### Kevin Buzzard (Apr 06 2018 at 10:37):

I tried to describe my problems in https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/structure.20vs.20class/near/124574243 without code, and then I posted link to my actual code. Then I tried to describe a simplified problem. I don't what I could do better to ask for help

Write a MWE. I am much more inclined to look at code if I can just cut and paste it and it works first time. Git cloning and then downloading a new mathlib and building everything was a PITA and I couldn't possibly answer a question of the form "why does line 193 not work" without doing all that.

#### Kevin Buzzard (Apr 06 2018 at 10:39):

I even managed to merge using the crappy train station wifi

git is great for that isn't it.

#### Kevin Buzzard (Apr 06 2018 at 10:42):

Should I remove this coercion and have a coercion to equiv?

It seemed to me that one problem was you had coes from homeo to perm, from perm to fun and from homeo to fun. You had set it up so that the two maps from homeo to fun were definitionally equal (and if they weren't it would surely have been a nightmare) but even with definitional equality this didn't help with rw. @Mario Carneiro Can there be some version of rw which takes definitonal equality into account? i.e. "the user said rw (proof of X = Y) and I can't find X in the goal so I'll now start trying to find some term in the goal which is definitionally equal to X"?

#### Chris Hughes (Apr 06 2018 at 10:46):

I've read erw does that, but I've never managed to use it.

Last updated: May 11 2021 at 16:22 UTC