Zulip Chat Archive

Stream: new members

Topic: Axiom of choice, quotients, ℚ ⊆ ℝ


view this post on Zulip Pedro Minicz (Jun 17 2020 at 01:10):

The following is an example of an "obvious truth" that feels impossible to prove in Lean. I feel like this is due to my lack of familiarity with AC on Lean.

import data.real.basic
import group_theory.quotient_group

def Q : set  := λ r,  k : , k = r

instance : is_add_subgroup Q :=
{ zero_mem := 0, by push_cast; linarith,
  add_mem := λ _ _ a, _⟩ b, _⟩, a + b, by push_cast; linarith,
  neg_mem := λ _ a, _⟩, ⟨-a, by push_cast; linarith }

def RQ : Type := quotient_add_group.quotient Q
notation `/` := RQ

def RQ.mk :   / := quotient_add_group.mk

noncomputable def rational :  := quot.out (RQ.mk (0 : ))

example : rational  Q := sorry

view this post on Zulip Pedro Minicz (Jun 17 2020 at 01:10):

I guess a proof by contradiction would suffice, but I haven't managed to come up with anything.

view this post on Zulip Bhavik Mehta (Jun 17 2020 at 01:33):

example : rational  Q :=
begin
  have : @setoid.r _ (quotient_add_group.left_rel Q) rational 0,
    apply quotient.mk_out',
  have := quotient.sound' this,
  have := quotient_add_group.eq.1 this.symm,
  simpa,
end

Here's how I did it - I don't think this was at all easy to find though :( Hopefully others can clear it up for you better

view this post on Zulip Pedro Minicz (Jun 17 2020 at 02:04):

It seems I wasn't able to leverage the definition of quotient_add_group.left_rel. Thank you!


Last updated: May 09 2021 at 19:11 UTC