Zulip Chat Archive

Stream: new members

Topic: Equivalence between subtype and bundled type


view this post on Zulip Nicolò Cavalleri (Aug 29 2020 at 10:19):

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.

view this post on Zulip Kenny Lau (Aug 29 2020 at 10:26):

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

view this post on Zulip Kenny Lau (Aug 29 2020 at 10:27):

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

view this post on Zulip Nicolò Cavalleri (Aug 29 2020 at 10:55):

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

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 16:14):

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.

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 16:16):

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.

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 16:18):

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

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 16:20):

  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,

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 16:22):

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

view this post on Zulip Kevin Buzzard (Aug 29 2020 at 16:24):

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.


Last updated: May 16 2021 at 05:21 UTC