definition of `equiv`

Stream: general

[Kevin Buzzard]

/-- `α ≃ β` 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]

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

[Kevin Buzzard]

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

[Mario Carneiro]

the second one is defeq to the existing definition

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

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]

the second one is defeq to the existing definition

Right, but it's less obfuscated!

[Kevin Buzzard]

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]

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]

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]

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

[Mario Carneiro]

you put a thing on the left and distribute it

[Mario Carneiro]

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

[Mario Carneiro]

actually it probably originates in group theory

[Mario Carneiro]

category theorists like to call these things monos and sections

[Mario Carneiro]

which is confusing in a completely different way

[Reid Barton]

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]

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]

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]

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]

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]

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]

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]

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]

(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.)