Equivalence between subtype and bundled type

Stream: new members

[Nicolò Cavalleri]

In the file algebra.group.units, how can I fill up the sorries of the following definition, placed after is_unit.unit?

noncomputable def is_unit.equiv [monoid M] : equiv {a : M | is_unit a} (units M) :=
{ to_fun := λ a, a.prop.unit,
  inv_fun := λ a, ⟨a.val, a, rfl⟩,
  left_inv := begin intros x, ext, simp only [subtype.coe_mk], sorry end,
  right_inv := begin intro x, dsimp only, sorry end }

I would expect refl to work, but it is as if Lean is replacing things with underscores and cannot look back in to them.

[Kenny Lau]

import algebra.group.units
import data.equiv.basic

variables (M : Type*)

noncomputable def is_unit.equiv [monoid M] : equiv {a : M | is_unit a} (units M) :=
equiv.symm $ equiv.of_injective _ units.ext

[Kenny Lau]

{ a | is_unit a } is defeq to set.range (coe : units M -> M)

[Nicolò Cavalleri]

Ok thanks a lot! This looks smart, I'll try to understand the proof

[Kevin Buzzard]

refl doesn't work because "eta isn't refl" I think. For example if z is a complex number, then \<z.re, z.im\> = z but the proof isn't refl, it's cases z, refl. You need to case on x more in your first sorry. That's what the underscores are -- they're parts of x which don't have names yet.

[Kevin Buzzard]

No, I tell a lie, the issue is that is_unit is an existence statement, and to get the unit there's some classical.some, so your underscore is something which needs to be reasoned about with classical.some_spec. I think Kenny's approach is better.

[Kevin Buzzard]

/-- The element of the group of units, corresponding to an element of a monoid which is a unit. -/
noncomputable def is_unit.unit [monoid M] {a : M} (h : is_unit a) : units M :=
classical.some h

lemma is_unit.unit_spec [monoid M] {a : M} (h : is_unit a) : ↑h.unit = a :=
classical.some_spec h

If you look at the definition of is_unit.unit in mathlib then immediately afterwards we see the API, i.e. the function you need.

[Kevin Buzzard]

  left_inv := begin
    change ∀ _, _, -- so rintro? works, but you can comment this line out
    rintro ⟨_, ⟨val, inv, h1, h2⟩, rfl⟩, -- using rintro and changing names to shorter ones
    ext,
    -- dsimp, -- I wrote this line so I could see what the heck was going on, but it's not needed
    exact is_unit.unit_spec _,
  end,

[Kevin Buzzard]

  right_inv := begin
    rintro ⟨val, inv, h1, h2⟩,
    ext,
    exact is_unit.unit_spec _,
  end }

[Kevin Buzzard]

here is the list of the greek letters involved in "computation" in lambda calculus, and here is the list of the ones which are built into Lean's definition of definitional equality, i.e. the ones which refl works for. The one which is missing is "eta reduction for structures" I think, but I'm certainly not an expert. But in this case the problem was something else anyway, namely the classical issue involved in getting from the existence statement to the actual object.