Unit interval, ℝ/ℚ and ℝ/ℤ

unit_interval.lean

import data.real.basic
import group_theory.quotient_group

-- https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Defining.20the.20unit.20interval
-- https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/About.20measures

namespace set

@[simp] def I : Type := set.Icc (0 : ℝ) (1 : ℝ)

instance : has_zero I := ⟨⟨0, by simp [zero_le_one]⟩⟩
instance : has_one I  := ⟨⟨1, by simp [zero_le_one]⟩⟩

end set

namespace quot

def RQ_setoid : setoid ℝ :=
{ r := λ a b, ∃ k : ℚ, ↑k = b - a,
  iseqv := by {
    split, exact λ _, ⟨0, by push_cast; linarith⟩,
    split, exact λ _ _ ⟨a, _⟩, ⟨-a, by push_cast; linarith⟩,
    exact λ _ _ _ ⟨a, _⟩ ⟨b, _⟩, ⟨a + b, by push_cast; linarith⟩ } }

def RQ : Type := quotient RQ_setoid
notation `ℝ/ℚ` := RQ

def RQ.mk : ℝ → ℝ/ℚ := @quotient.mk _ RQ_setoid

end quot

namespace group_theory

instance : is_add_submonoid (set.range (coe : ℤ → ℝ)) :=
begin
  refine is_add_submonoid.mk ⟨0, rfl⟩ _,
  rintros a b ⟨ka, hka⟩ ⟨kb, hkb⟩,
  exact ⟨ka + kb, by push_cast; linarith⟩
end

instance : is_add_subgroup (set.range (coe : ℤ → ℝ)) :=
is_add_subgroup.mk (by rintros a ⟨k, hk⟩; exact ⟨-k, by push_cast; linarith⟩)

@[derive add_group]
def I : Type := quotient_add_group.quotient (set.range (coe : ℤ → ℝ))

def I.mk : ℝ → I := quotient_add_group.mk

instance : has_zero I := ⟨I.mk 0⟩
instance : has_one I  := ⟨I.mk 1⟩

example : (0 : I) = 1 := quot.sound ⟨1, by simp⟩
example (a b : ℤ) : I.mk a = I.mk b := quot.sound ⟨-a + b, by push_cast⟩

end group_theory