unbundled equiv

Stream: general

[David Wärn]

Is there no typeclass saying that a specified function has a two-sided inverse? Like bijective f but carrying data for the inverse. I tried to define this but noticed that simp doesn't like the lemma f (inv f y) = y

[Kenny Lau]

you can create your own structure.

[Mario Carneiro]

That's equiv

[Mario Carneiro]

however it bundles both functions inside the structure

[Mario Carneiro]

which plays better with simp lemmas like the one you gave

[Kenny Lau]

this new structure would be a subsingleton, which might have some advantage

[Scott Morrison]

is_iso

[Scott Morrison]

You might have to make sure category_theory.types is also imported, to hook in the right instance.

[David Wärn]

I like this idea

[David Wärn]

How do I tell Lean to think of my function as a hom?

import category_theory.types
open category_theory
variables (α β : Type) (f : α → β)
#check is_iso (f : α ⟶ β)

Here Lean complains that f is a \r arrow and not an \h arrow (unless I declare it as an \h arrow to begin with)

[Johan Commelin]

@David Wärn Weird... that shouldn't happen

[Johan Commelin]

The problem is that it doesn't find the category instance...

import category_theory.types
open category_theory
variables (α β : Type) (f : α → β)

instance foo : category Type := by apply_instance

#check @is_iso Type _ α β _

[Johan Commelin]

Don't ask me why it doesn't...

[Johan Commelin]

This works:

#check @is_iso Type category_theory.types α β f

[Kevin Buzzard]

include the instance? Isn't this often what we have to do?

[David Wärn]

include category_theory.types is invalid as types is not a parameter/variable

[David Wärn]

#print instances category shows that the instance is in scope anyway

[Kevin Buzzard]

Even though it's in scope, it is sometimes not picked up because of universe issues.

[Johan Commelin]

Even

#check is_iso.{0} (f : α ⟶ β)

doesn't work

[Scott Morrison]

Hmm... that's a pity.

[Scott Morrison]

@Johan Commelin -- could you explain to me the difference between { } brackets and the double braces I've seen you use?

[Scott Morrison]

I never learnt this.

[Scott Morrison]

def bar := @is_iso.{0} _ _ _ β f

[Scott Morrison]

works, but you can't replace the \beta with an _, even if you supply the additional universe level @is_iso.{0 1}.

[Mario Carneiro]

a double brace argument is implicit but it doesn't get applied unless some argument coming after it also gets applied. For example if f : \all {{x y : A}}, A -> A then f results in just @f, while f z is elaborated to @f _ _ z

[Johan Commelin]

@Scott Morrison I think function.injective is a good example.

def function.injective (f : X → Y) :=
\forall {{x y}}, f x = f y → x = y

without the double braces hf : function.injective f would have type f ?1 = f ?2 → ?1 = ?2. And you would get two crazy meta-variable goals. But with the double braces, hf : function.injective f has type \forall {x y}, f x = f y → x = y. Does that make sense?

[Mario Carneiro]

It is good for definitions that are hiding a forall, like set.subset and function.injective

[Johan Commelin]

Scott Morrison said:

works, but you can't replace the \beta with an _, even if you supply the additional universe level @is_iso.{0 1}.

This is really annoying and sad....

[Scott Morrison]

This is the best I can do so far:

import category_theory.types
import category_theory.epi_mono
open category_theory

universe u
variables (α β γ : Type) (f : α → β) (g : β → γ)

-- We can define an `abbreviation` wrapper that
-- lifts honest functions to morphisms in the category `Type`.

abbreviation as_hom {α β : Type u} (f : α → β) : α ⟶ β := f

example : α → γ := (as_hom f) ≫ (as_hom g)
example [is_iso (as_hom f)] : mono (as_hom f) := by apply_instance
example [is_iso (as_hom f)] : (as_hom f) ≫ inv (as_hom f) = 𝟙 α := by simp

-- If you don't mind some notation you can use fewer keystrokes:

notation  `↾` f : 200 := as_hom f

example : α → γ := ↾f ≫ ↾g
example [is_iso ↾f] : mono ↾f := by apply_instance
example [is_iso ↾f] : ↾f ≫ inv ↾f = 𝟙 α := by simp