dual.lean

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