# Zulip Chat Archive

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

s which hopefully mean you don't even need to write them.)

Last updated: May 08 2021 at 04:14 UTC