Skip to content

Instantly share code, notes, and snippets.

@Timeroot
Created October 15, 2021 23:12
Show Gist options
  • Save Timeroot/8fd43e5b58a4f910ad05b098383c788f to your computer and use it in GitHub Desktop.
Save Timeroot/8fd43e5b58a4f910ad05b098383c788f to your computer and use it in GitHub Desktop.
/- Define a "nonzero" type -/
import algebra.group
universe u
variables {M : Type*}
structure nonzero (α : Type u) [C : has_zero α] :=
(val : α)
(not_zero : val ≠ 0)
namespace nonzero
variable [has_zero M]
instance : has_coe (nonzero M) M := ⟨val⟩
@[ext] theorem ext : function.injective (coe : nonzero M → M)
| ⟨v, h₁⟩ ⟨v', h₂⟩ e := by change v = v' at e; subst v'
@[simp] theorem mk_coe (u : nonzero M) (h₁) : mk (u : M) h₁ = u := ext rfl
@[simp] lemma val_eq_coe (a : nonzero M) : a.val = (↑a : M) := rfl
end nonzero
/-- The meat starts here -/
@[reducible, simp] --a new structure where we forcibly add "0"
def with0 (T : Type*) := option T
@[reducible, simp] --a new has_mul where we forcibly remove "0"
def drop0 (T : Type*) [has_zero T] := nonzero T
instance : has_zero (with0 M) := { zero := none }
open classical
local attribute [instance] prop_decidable
noncomputable def iso [sl : has_zero M]: with0 (drop0 M) ≃ M :=
{
to_fun := λ a, option.rec_on a 0 nonzero.val,
inv_fun := λ a, dite (a=0) (λ _, none) (λ h, option.some (nonzero.mk a h)),
left_inv := begin
intro a, cases a; simp, cases a, contradiction,
end,
right_inv := begin
intro a, by_cases a=0,
{
simp [h],
sorry
},{
simp [h],
sorry,
}
end
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment