Skip to content

Instantly share code, notes, and snippets.

@kesinger
Created October 16, 2020 21:30
Show Gist options
  • Save kesinger/ed7fb84bdcc78abce09db9c710527cb4 to your computer and use it in GitHub Desktop.
Save kesinger/ed7fb84bdcc78abce09db9c710527cb4 to your computer and use it in GitHub Desktop.
import data.real.basic
import tactic.simps
import algebra.algebra.basic
structure dualno : Type :=
(re : ℝ) (im : ℝ)
@[ext]
structure dual_algebra (R : Type*)[comm_ring R] (jj: R) :=
mk {} :: (re : R) (im : R)
notation `DUAL[` R`,` jj`]` := dual_algebra R jj
def split_complex (R : Type*) [comm_ring R] := dual_algebra R (1)
def dual_number (R : Type*) [comm_ring R] := dual_algebra R (0)
namespace dual_algebra
variables {R:Type*} [comm_ring R] (x y jj : R)
instance : has_coe R DUAL[R,jj] := ⟨λ r, ⟨r, 0⟩⟩
instance : has_coe_t R (DUAL[R,jj]) := ⟨λ x, ⟨x, 0⟩⟩
@[simp] lemma coe_re : (x : DUAL[R,jj]).re = x := rfl
@[simp] lemma coe_im : (x : DUAL[R,jj]).im = 0 := rfl
lemma coe_injective : function.injective (coe : R → DUAL[R,jj]) :=
λ x y h, congr_arg re h
@[simps {short_name:= tt}] def ε : DUAL[R,jj]:= ⟨0, 1⟩
@[simps {short_name:= tt}] instance : has_one DUAL[R, jj] := ⟨⟨1, 0⟩⟩
@[simps {short_name:= tt}] instance : has_zero DUAL[R, jj] := ⟨⟨0, 0⟩⟩
@[simps {short_name:= tt}] instance : has_add DUAL[R,jj] := ⟨λ z w, ⟨z.re + w.re, z.im + w.im⟩⟩
@[simps {short_name:= tt}] instance : has_neg DUAL[R,jj] := ⟨λ z, ⟨-z.re, -z.im⟩⟩
@[simps {short_name:= tt}] instance : has_mul DUAL[R,jj] := ⟨λ z w, ⟨z.re * w.re + jj * z.im * w.im, z.re * w.im + z.im * w.re⟩⟩
instance : comm_ring DUAL[R,jj] :=
by refine { zero := 0, add := (+), neg := has_neg.neg, one := 1, mul := (*), ..};
{ intros, ext; simp; ring }
theorem ext' : ∀ {z w : DUAL[R,jj]}, z.re = w.re → z.im = w.im → z = w
| ⟨zr, zi⟩ ⟨_, _⟩ rfl rfl := rfl
@[ext]
theorem pext { z w : DUAL[R,jj]} (hre : z.re = w.re) (him : z.im = w.im) : z=w :=
begin
cases z with zr zi,
cases w with wr wi,
simp *,
cc
end
@[ext]
theorem rext { z w : DUAL[R,jj]} (hyp : z = w) : (z.re = w.re) ∧(z.im = w.im) :=
begin
cases z with zr zi,
cases w with wr wi,
simp *,
cc
end
@[simp] lemma incl_one : ((1 : R) : DUAL[R,jj]) = 1 := rfl
@[simp] lemma incl_zero : ((0 : R) : DUAL[R,jj]) = 0 := rfl
@[simp] lemma incl_add (r s : R) : ((r + s : R) : DUAL[R,jj]) =
r + s :=
begin
ext,
refl,
simp at *,
end
@[simp, norm_cast] lemma coe_one : ((1 : R) : DUAL[R,jj]) = 1 := rfl
@[simp] lemma incl_neg (r : R) : ((-r : R) : DUAL[R,jj]) = -r :=
begin
ext, refl, simp at *
end
@[simp] lemma incl_mul (jj r s : R) : ((r * s : R) : DUAL[R,jj]) = r * s :=
begin
ext,
simp at *,
simp at *,
end
def incl : R →+* DUAL[R,jj] := ⟨coe, coe_one jj,
incl_mul jj, incl_zero jj, incl_add jj ⟩
def conj : DUAL[R,jj] →+* DUAL[R,jj] :=
begin
refine_struct { to_fun := λ z : DUAL[R,jj], (⟨z.re, -z.im⟩ : DUAL[R,jj]), .. };
{ intros, ext; simp [add_comm], },
end
instance : algebra R DUAL[R,jj] := by ring_hom.to_algebra incl
#check conj
end dual_algebra
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment