Zulip Chat Archive

Stream: general

Topic: definition of `equiv`


view this post on Zulip Kevin Buzzard (Aug 21 2019 at 11:48):

/-- `α ≃ β` is the type of functions from `α → β` with a two-sided inverse. -/
structure equiv (α : Sort*) (β : Sort*) :=
(to_fun    : α  β)
(inv_fun   : β  α)
(left_inv  : left_inverse inv_fun to_fun)
(right_inv : right_inverse inv_fun to_fun)

Why was it decided to use left_inverse and right_inverse, rather than the other possibilities inv_fun \circ to_fun = id or \forall x, inv_fun (to_fun x) = x? Both of my suggestions seem more natural to me.

view this post on Zulip Chris Hughes (Aug 21 2019 at 11:59):

The first thing you'd do when defining an equiv using your definition is apply funext. This definition saves you that trouble.

view this post on Zulip Kevin Buzzard (Aug 21 2019 at 12:00):

I thought I was offering both a pre-funext and a post-funext suggestion?

view this post on Zulip Mario Carneiro (Aug 21 2019 at 12:01):

the second one is defeq to the existing definition

view this post on Zulip Mario Carneiro (Aug 21 2019 at 12:01):

I guess the reasoning is, if you have a definition for something why not use it when it's obviously applicable

view this post on Zulip Mario Carneiro (Aug 21 2019 at 12:02):

If you don't think that left_inverse is appropriate here, when would it ever be appropriate?

view this post on Zulip Patrick Massot (Aug 21 2019 at 12:03):

The "pre-funext" vs "post-funext" dilemma is unfortunately unfixable. In my experience, you will always want both, depending on what you are proving.

view this post on Zulip Kevin Buzzard (Aug 21 2019 at 12:04):

the second one is defeq to the existing definition

Right, but it's less obfuscated!

view this post on Zulip Kevin Buzzard (Aug 21 2019 at 12:05):

If you don't think that left_inverse is appropriate here, when would it ever be appropriate?

I don't think I've ever used it...(and that's not only because I can never remember whether it says fg=id or gf=id)

view this post on Zulip Mario Carneiro (Aug 21 2019 at 12:07):

that's actually a totally reasonable response too. I'm not sure I would have ever defined left_inverse and right_inverse; they aren't abbreviating enough to be worth it, plus they are easily confused and differ only in argument order

view this post on Zulip Kevin Buzzard (Aug 21 2019 at 12:17):

So this "left" and "right" stuff comes up sometimes, and I can never remember which way round things are. If MM is a left RR-module then that means RR acts on the left, so r \bub m. This one I remember because I have to in my day job. left_distrib I have no idea what this means, I just use mul_add or add_mul as appropriate, because I know what these mean. left_inverse I have no idea what this means, but it seems to be actually longer than its definition, whatever the definition is. Is there some rule of thumb? Left associative I think I understand -- that means that abc=(ab)cabc=(ab)c, right? That is maybe a more sensible use of left?

view this post on Zulip Mario Carneiro (Aug 21 2019 at 12:22):

left distrib is the same as left assoc - a * (b + c) = ...

view this post on Zulip Mario Carneiro (Aug 21 2019 at 12:24):

you put a thing on the left and distribute it

view this post on Zulip Mario Carneiro (Aug 21 2019 at 12:25):

as for left inverse, your guess is as good as mine. Blame the category theorists

view this post on Zulip Mario Carneiro (Aug 21 2019 at 12:26):

actually it probably originates in group theory

view this post on Zulip Mario Carneiro (Aug 21 2019 at 12:26):

category theorists like to call these things monos and sections

view this post on Zulip Mario Carneiro (Aug 21 2019 at 12:26):

which is confusing in a completely different way

view this post on Zulip Reid Barton (Aug 21 2019 at 12:55):

I just remember that the first law (left_inv) wants an argument which is the same type as the first function (to_fun) and then the same for the second law/function

view this post on Zulip Kevin Buzzard (Aug 21 2019 at 14:06):

In data.equiv.basic there is

@[trans] protected def trans (e₁ : α  β) (e₂ : β  γ) : α  γ :=
e₂.to_fun  e₁.to_fun, e₁.inv_fun  e₂.inv_fun,
  e₂.left_inv.comp e₁.left_inv, e₂.right_inv.comp e₁.right_inv

and the proofs would not typecheck if one used the more low-level definitions. Here it seems to work because there is a function called function.left_inverse.comp

view this post on Zulip Simon Hudon (Aug 21 2019 at 14:14):

There's an attribute higher_order if, from the post-ext formulation, you want to create the pre-ext formulation of a lemma

view this post on Zulip Floris van Doorn (Aug 21 2019 at 14:37):

I remember left-inverse/right-inverse as follows: if you have g ∘ f = id in the equation g is on the left, so it is a left-inverse of f, and f is on the right, so it is a right-inverse of g.

view this post on Zulip Kevin Buzzard (Aug 21 2019 at 14:38):

Yeah, this is just the sort of idea that I find really hard to remember like that. Because on other days I might figure that g is on the left, so f is a left-inverse of g.

view this post on Zulip Kevin Buzzard (Aug 21 2019 at 14:39):

The only reason I can remember what a left RR-module is ("RR goes on the left" as opposed to "the module goes on the left") is that this comes up time and time again in the stuff I read.

view this post on Zulip Floris van Doorn (Aug 21 2019 at 14:46):

Makes sense. I get confused myself about most other left/right distinctions (in left_distrib and add_le_add_left, or the direction of assoc), just not this one.

view this post on Zulip Scott Morrison (Aug 21 2019 at 21:46):

The corresponding fields in iso (which works fine for Type, as long as you don't mind a fixed universe) are called hom_inv_id and inv_hom_id, which are a little easier to remember.

view this post on Zulip Scott Morrison (Aug 21 2019 at 21:47):

(Except that they are actually called hom_inv_id' and inv_hom_id', because they have auto_params which hopefully mean you don't even need to write them.)


Last updated: May 08 2021 at 04:14 UTC