## Stream: general

### Topic: definition of equiv

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

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

#### Kevin Buzzard (Aug 21 2019 at 12:00):

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

#### Mario Carneiro (Aug 21 2019 at 12:01):

the second one is defeq to the existing definition

#### 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

#### 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?

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

#### Kevin Buzzard (Aug 21 2019 at 12:04):

the second one is defeq to the existing definition

Right, but it's less obfuscated!

#### 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)

#### 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

#### 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 $M$ is a left $R$-module then that means $R$ 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)c$, right? That is maybe a more sensible use of left?

#### Mario Carneiro (Aug 21 2019 at 12:22):

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

#### Mario Carneiro (Aug 21 2019 at 12:24):

you put a thing on the left and distribute it

#### Mario Carneiro (Aug 21 2019 at 12:25):

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

#### Mario Carneiro (Aug 21 2019 at 12:26):

actually it probably originates in group theory

#### Mario Carneiro (Aug 21 2019 at 12:26):

category theorists like to call these things monos and sections

#### Mario Carneiro (Aug 21 2019 at 12:26):

which is confusing in a completely different way

#### 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

#### 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

#### 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

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

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

#### Kevin Buzzard (Aug 21 2019 at 14:39):

The only reason I can remember what a left $R$-module is ("$R$ 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.

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

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

#### 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