Quadratic Algebra

In this file we define the quadratic algebra QuadraticAlgebra R a b over a commutative ring R, and define some algebraic structures on it.

Main definitions

• QuadraticAlgebra R a b: [Bourbaki, Algebra I][bourbaki1989] with coefficients a, b in R.

Tags

Quadratic algebra, quadratic extension

structure QuadraticAlgebra (R : Type u) (a b : R) : Type u

Quadratic algebra over a type with fixed coefficient where $i^2 = a + bi$, implemented as a structure with two fields, re and im. When R is a commutative ring, this is isomorphic to R[X]/(X^2-b*X-a).

• re : R

  Real part of an element in quadratic algebra

• im : R

  Imaginary part of an element in quadratic algebra

theorem QuadraticAlgebra.ext_iff {R : Type u} {a b : R} {x y : QuadraticAlgebra R a b} : x = y ↔ x.re = y.re ∧ x.im = y.im

theorem QuadraticAlgebra.ext {R : Type u} {a b : R} {x y : QuadraticAlgebra R a b} (re : x.re = y.re) (im : x.im = y.im) : x = y

def instDecidableEqQuadraticAlgebra.decEq {R✝ : Type u_1} {a✝ b✝ : R✝} [DecidableEq R✝] (x✝ x✝¹ : QuadraticAlgebra R✝ a✝ b✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance instDecidableEqQuadraticAlgebra {R✝ : Type u_1} {a✝ b✝ : R✝} [DecidableEq R✝] : DecidableEq (QuadraticAlgebra R✝ a✝ b✝)

def QuadraticAlgebra.equivProd {R : Type u_1} (a b : R) : QuadraticAlgebra R a b ≃ R × R

The equivalence between quadratic algebra over R and R × R.

@[simp]

theorem QuadraticAlgebra.equivProd_symm_apply {R : Type u_1} (a b : R) (p : R × R) : (equivProd a b).symm p = { re := p.1, im := p.2 }

@[simp]

theorem QuadraticAlgebra.mk_eta {R : Type u_1} {a b : R} (z : QuadraticAlgebra R a b) : { re := z.re, im := z.im } = z

instance QuadraticAlgebra.instSubsingleton {R : Type u_1} {a b : R} [Subsingleton R] : Subsingleton (QuadraticAlgebra R a b)

instance QuadraticAlgebra.instNontrivial {R : Type u_1} {a b : R} [Nontrivial R] : Nontrivial (QuadraticAlgebra R a b)

def QuadraticAlgebra.C {R : Type u_1} {a b : R} [Zero R] (x : R) : QuadraticAlgebra R a b

The natural function R → QuadraticAlgebra R a b.

Note that, if R is a ring, you should use algebraMap instead of C.

@[simp]

theorem QuadraticAlgebra.re_C {R : Type u_1} {a b : R} (r : R) [Zero R] : (QuadraticAlgebra.C r).re = r

@[simp]

theorem QuadraticAlgebra.im_C {R : Type u_1} {a b : R} (r : R) [Zero R] : (QuadraticAlgebra.C r).im = 0

theorem QuadraticAlgebra.C_injective {R : Type u_1} {a b : R} [Zero R] : Function.Injective QuadraticAlgebra.C

@[simp]

theorem QuadraticAlgebra.C_inj {R : Type u_1} {a b : R} [Zero R] {x y : R} : QuadraticAlgebra.C x = QuadraticAlgebra.C y ↔ x = y

@[instance_reducible]

instance QuadraticAlgebra.instZero {R : Type u_1} {a b : R} [Zero R] : Zero (QuadraticAlgebra R a b)

@[simp]

theorem QuadraticAlgebra.re_zero {R : Type u_1} {a b : R} [Zero R] : re 0 = 0

@[simp]

theorem QuadraticAlgebra.im_zero {R : Type u_1} {a b : R} [Zero R] : im 0 = 0

@[simp]

theorem QuadraticAlgebra.C_zero {R : Type u_1} {a b : R} [Zero R] : QuadraticAlgebra.C 0 = 0

@[simp]

theorem QuadraticAlgebra.C_eq_zero_iff {R : Type u_1} {a b : R} [Zero R] {r : R} : QuadraticAlgebra.C r = 0 ↔ r = 0

@[instance_reducible]

instance QuadraticAlgebra.instInhabited {R : Type u_1} {a b : R} [Zero R] : Inhabited (QuadraticAlgebra R a b)

@[instance_reducible]

instance QuadraticAlgebra.instOne {R : Type u_1} {a b : R} [Zero R] [One R] : One (QuadraticAlgebra R a b)

theorem QuadraticAlgebra.re_one {R : Type u_1} {a b : R} [Zero R] [One R] : re 1 = 1

theorem QuadraticAlgebra.im_one {R : Type u_1} {a b : R} [Zero R] [One R] : im 1 = 0

@[simp]

theorem QuadraticAlgebra.C_one {R : Type u_1} {a b : R} [Zero R] [One R] : QuadraticAlgebra.C 1 = 1

@[simp]

theorem QuadraticAlgebra.C_eq_one_iff {R : Type u_1} {a b : R} [Zero R] [One R] {r : R} : QuadraticAlgebra.C r = 1 ↔ r = 1

@[instance_reducible]

instance QuadraticAlgebra.instAdd {R : Type u_1} {a b : R} [Add R] : Add (QuadraticAlgebra R a b)

@[simp]

theorem QuadraticAlgebra.re_add {R : Type u_1} {a b : R} [Add R] (z w : QuadraticAlgebra R a b) : (z + w).re = z.re + w.re

@[simp]

theorem QuadraticAlgebra.im_add {R : Type u_1} {a b : R} [Add R] (z w : QuadraticAlgebra R a b) : (z + w).im = z.im + w.im

@[simp]

theorem QuadraticAlgebra.mk_add_mk {R : Type u_1} {a b : R} [Add R] (z w : QuadraticAlgebra R a b) : { re := z.re, im := z.im } + { re := w.re, im := w.im } = { re := z.re + w.re, im := z.im + w.im }

@[simp]

theorem QuadraticAlgebra.C_add {R : Type u_1} {a b : R} [AddZeroClass R] (x y : R) : QuadraticAlgebra.C (x + y) = QuadraticAlgebra.C x + QuadraticAlgebra.C y

@[instance_reducible]

instance QuadraticAlgebra.instNeg {R : Type u_1} {a b : R} [Neg R] : Neg (QuadraticAlgebra R a b)

@[simp]

theorem QuadraticAlgebra.re_neg {R : Type u_1} {a b : R} [Neg R] (z : QuadraticAlgebra R a b) : (-z).re = -z.re

@[simp]

theorem QuadraticAlgebra.im_neg {R : Type u_1} {a b : R} [Neg R] (z : QuadraticAlgebra R a b) : (-z).im = -z.im

@[simp]

theorem QuadraticAlgebra.neg_mk {R : Type u_1} {a b : R} [Neg R] (x y : R) : -{ re := x, im := y } = { re := -x, im := -y }

@[simp]

theorem QuadraticAlgebra.C_neg {R : Type u_1} {a b : R} [NegZeroClass R] (x : R) : QuadraticAlgebra.C (-x) = -QuadraticAlgebra.C x

@[instance_reducible]

instance QuadraticAlgebra.instSub {R : Type u_1} {a b : R} [Sub R] : Sub (QuadraticAlgebra R a b)

@[simp]

theorem QuadraticAlgebra.re_sub {R : Type u_1} {a b : R} [Sub R] (z w : QuadraticAlgebra R a b) : (z - w).re = z.re - w.re

@[simp]

theorem QuadraticAlgebra.im_sub {R : Type u_1} {a b : R} [Sub R] (z w : QuadraticAlgebra R a b) : (z - w).im = z.im - w.im

@[simp]

theorem QuadraticAlgebra.mk_sub_mk {R : Type u_1} {a b : R} [Sub R] (x1 y1 x2 y2 : R) : { re := x1, im := y1 } - { re := x2, im := y2 } = { re := x1 - x2, im := y1 - y2 }

@[simp]

theorem QuadraticAlgebra.C_sub {R : Type u_1} {a b : R} (r1 r2 : R) [SubNegZeroMonoid R] : QuadraticAlgebra.C (r1 - r2) = QuadraticAlgebra.C r1 - QuadraticAlgebra.C r2

@[instance_reducible]

instance QuadraticAlgebra.instMul {R : Type u_1} {a b : R} [Mul R] [Add R] : Mul (QuadraticAlgebra R a b)

@[simp]

theorem QuadraticAlgebra.re_mul {R : Type u_1} {a b : R} [Mul R] [Add R] (z w : QuadraticAlgebra R a b) : (z * w).re = z.re * w.re + a * z.im * w.im

@[simp]

theorem QuadraticAlgebra.im_mul {R : Type u_1} {a b : R} [Mul R] [Add R] (z w : QuadraticAlgebra R a b) : (z * w).im = z.re * w.im + z.im * w.re + b * z.im * w.im

@[simp]

theorem QuadraticAlgebra.mk_mul_mk {R : Type u_1} {a b : R} [Mul R] [Add R] (x1 y1 x2 y2 : R) : { re := x1, im := y1 } * { re := x2, im := y2 } = { re := x1 * x2 + a * y1 * y2, im := x1 * y2 + y1 * x2 + b * y1 * y2 }

@[instance_reducible]

instance QuadraticAlgebra.instSMul {R : Type u_1} {S : Type u_2} {a b : R} [SMul S R] : SMul S (QuadraticAlgebra R a b)

instance QuadraticAlgebra.instIsScalarTower {R : Type u_1} {S : Type u_2} {T : Type u_3} {a b : R} [SMul S R] [SMul T R] [SMul S T] [IsScalarTower S T R] : IsScalarTower S T (QuadraticAlgebra R a b)

instance QuadraticAlgebra.instSMulCommClass {R : Type u_1} {S : Type u_2} {T : Type u_3} {a b : R} [SMul S R] [SMul T R] [SMulCommClass S T R] : SMulCommClass S T (QuadraticAlgebra R a b)

instance QuadraticAlgebra.instIsCentralScalar {R : Type u_1} {S : Type u_2} {a b : R} [SMul S R] [SMul Sᵐᵒᵖ R] [IsCentralScalar S R] : IsCentralScalar S (QuadraticAlgebra R a b)

@[simp]

theorem QuadraticAlgebra.re_smul {R : Type u_1} {S : Type u_2} {a b : R} [SMul S R] (s : S) (z : QuadraticAlgebra R a b) : (s • z).re = s • z.re

@[simp]

theorem QuadraticAlgebra.im_smul {R : Type u_1} {S : Type u_2} {a b : R} [SMul S R] (s : S) (z : QuadraticAlgebra R a b) : (s • z).im = s • z.im

@[simp]

theorem QuadraticAlgebra.smul_mk {R : Type u_1} {S : Type u_2} {a b : R} [SMul S R] (s : S) (x y : R) : s • { re := x, im := y } = { re := s • x, im := s • y }

@[instance_reducible]

instance QuadraticAlgebra.instMulAction {R : Type u_1} {S : Type u_2} {a b : R} [Monoid S] [MulAction S R] : MulAction S (QuadraticAlgebra R a b)

@[simp]

theorem QuadraticAlgebra.C_smul {R : Type u_1} {S : Type u_2} {a b : R} [Zero R] [SMulZeroClass S R] (s : S) (r : R) : QuadraticAlgebra.C (s • r) = s • QuadraticAlgebra.C r

@[instance_reducible]

instance QuadraticAlgebra.instAddMonoid {R : Type u_1} {a b : R} [AddMonoid R] : AddMonoid (QuadraticAlgebra R a b)

@[instance_reducible]

instance QuadraticAlgebra.instDistribMulAction {R : Type u_1} {S : Type u_2} {a b : R} [Monoid S] [AddMonoid R] [DistribMulAction S R] : DistribMulAction S (QuadraticAlgebra R a b)

@[instance_reducible]

instance QuadraticAlgebra.instAddCommMonoid {R : Type u_1} {a b : R} [AddCommMonoid R] : AddCommMonoid (QuadraticAlgebra R a b)

@[instance_reducible]

instance QuadraticAlgebra.instModule {R : Type u_1} {S : Type u_2} {a b : R} [Semiring S] [AddCommMonoid R] [Module S R] : Module S (QuadraticAlgebra R a b)

@[instance_reducible]

instance QuadraticAlgebra.instAddGroup {R : Type u_1} {a b : R} [AddGroup R] : AddGroup (QuadraticAlgebra R a b)

@[instance_reducible]

instance QuadraticAlgebra.instAddCommGroup {R : Type u_1} {a b : R} [AddCommGroup R] : AddCommGroup (QuadraticAlgebra R a b)

@[instance_reducible]

instance QuadraticAlgebra.instAddCommMonoidWithOne {R : Type u_1} {a b : R} [AddCommMonoidWithOne R] : AddCommMonoidWithOne (QuadraticAlgebra R a b)

@[simp]

theorem QuadraticAlgebra.C_ofNat {R : Type u_1} {a b : R} [AddCommMonoidWithOne R] (n : ℕ) [n.AtLeastTwo] : QuadraticAlgebra.C (OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem QuadraticAlgebra.re_natCast {R : Type u_1} {a b : R} [AddCommMonoidWithOne R] (n : ℕ) : (↑n).re = ↑n

@[simp]

theorem QuadraticAlgebra.im_natCast {R : Type u_1} {a b : R} [AddCommMonoidWithOne R] (n : ℕ) : (↑n).im = 0

theorem QuadraticAlgebra.C_natCast {R : Type u_1} {a b : R} [AddCommMonoidWithOne R] (n : ℕ) : QuadraticAlgebra.C ↑n = ↑n

theorem QuadraticAlgebra.re_ofNat {R : Type u_1} {a b : R} [AddCommMonoidWithOne R] (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).re = OfNat.ofNat n

theorem QuadraticAlgebra.im_ofNat {R : Type u_1} {a b : R} [AddCommMonoidWithOne R] (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).im = 0

@[instance_reducible]

instance QuadraticAlgebra.instAddCommGroupWithOne {R : Type u_1} {a b : R} [AddCommGroupWithOne R] : AddCommGroupWithOne (QuadraticAlgebra R a b)

@[simp]

theorem QuadraticAlgebra.re_intCast {R : Type u_1} {a b : R} [AddCommGroupWithOne R] (n : ℤ) : (↑n).re = ↑n

@[simp]

theorem QuadraticAlgebra.im_intCast {R : Type u_1} {a b : R} [AddCommGroupWithOne R] (n : ℤ) : (↑n).im = 0

theorem QuadraticAlgebra.C_intCast {R : Type u_1} {a b : R} [AddCommGroupWithOne R] (n : ℤ) : QuadraticAlgebra.C ↑n = ↑n

@[instance_reducible]

instance QuadraticAlgebra.instNonUnitalNonAssocSemiring {R : Type u_1} {a b : R} [NonUnitalNonAssocSemiring R] : NonUnitalNonAssocSemiring (QuadraticAlgebra R a b)

theorem QuadraticAlgebra.C_mul_eq_smul {R : Type u_1} {a b : R} [NonUnitalNonAssocSemiring R] (r : R) (x : QuadraticAlgebra R a b) : QuadraticAlgebra.C r * x = r • x

@[simp]

theorem QuadraticAlgebra.C_mul {R : Type u_1} {a b : R} [NonUnitalNonAssocSemiring R] (x y : R) : QuadraticAlgebra.C (x * y) = QuadraticAlgebra.C x * QuadraticAlgebra.C y

@[instance_reducible]

instance QuadraticAlgebra.instNonAssocSemiring {R : Type u_1} {a b : R} [NonAssocSemiring R] : NonAssocSemiring (QuadraticAlgebra R a b)

@[simp]

theorem QuadraticAlgebra.nsmul_mk {R : Type u_1} {a b : R} [NonAssocSemiring R] (n : ℕ) (x y : R) : ↑n * { re := x, im := y } = { re := ↑n * x, im := ↑n * y }

def QuadraticAlgebra.reₗ {R : Type u_1} (a b : R) [Semiring R] : QuadraticAlgebra R a b →ₗ[R] R

QuadraticAlgebra.re as a LinearMap

@[simp]

theorem QuadraticAlgebra.reₗ_apply {R : Type u_1} (a b : R) [Semiring R] (self : QuadraticAlgebra R a b) : (reₗ a b) self = self.re

def QuadraticAlgebra.imₗ {R : Type u_1} (a b : R) [Semiring R] : QuadraticAlgebra R a b →ₗ[R] R

QuadraticAlgebra.im as a LinearMap

@[simp]

theorem QuadraticAlgebra.imₗ_apply {R : Type u_1} (a b : R) [Semiring R] (self : QuadraticAlgebra R a b) : (imₗ a b) self = self.im

def QuadraticAlgebra.linearEquivTuple {R : Type u_1} (a b : R) [Semiring R] : QuadraticAlgebra R a b ≃ₗ[R] Fin 2 → R

QuadraticAlgebra.equivTuple as a LinearEquiv

@[simp]

theorem QuadraticAlgebra.linearEquivTuple_apply {R : Type u_1} (a b : R) [Semiring R] (z : QuadraticAlgebra R a b) : (linearEquivTuple a b) z = ![z.re, z.im]

@[simp]

theorem QuadraticAlgebra.linearEquivTuple_symm_apply {R : Type u_1} (a b : R) [Semiring R] (x : Fin 2 → R) : (linearEquivTuple a b).symm x = { re := x 0, im := x 1 }

noncomputable def QuadraticAlgebra.basis {R : Type u_1} (a b : R) [Semiring R] : Module.Basis (Fin 2) R (QuadraticAlgebra R a b)

QuadraticAlgebra R a b has a basis over R given by 1 and i

@[simp]

theorem QuadraticAlgebra.basis_repr_apply {R : Type u_1} (a b : R) [Semiring R] (x : QuadraticAlgebra R a b) : ⇑((basis a b).repr x) = ![x.re, x.im]

@[simp]

theorem QuadraticAlgebra.basis_apply_zero {R : Type u_1} (a b : R) [Semiring R] : (basis a b) 0 = 1

instance QuadraticAlgebra.instFinite {R : Type u_1} (a b : R) [Semiring R] : Module.Finite R (QuadraticAlgebra R a b)

instance QuadraticAlgebra.instFree {R : Type u_1} (a b : R) [Semiring R] : Module.Free R (QuadraticAlgebra R a b)

theorem QuadraticAlgebra.rank_eq_two {R : Type u_1} (a b : R) [Semiring R] [StrongRankCondition R] : Module.rank R (QuadraticAlgebra R a b) = 2

theorem QuadraticAlgebra.finrank_eq_two {R : Type u_1} (a b : R) [Semiring R] [StrongRankCondition R] : Module.finrank R (QuadraticAlgebra R a b) = 2

@[instance_reducible]

instance QuadraticAlgebra.instCommSemiring {R : Type u_1} {a b : R} [CommSemiring R] : CommSemiring (QuadraticAlgebra R a b)

@[instance_reducible]

instance QuadraticAlgebra.instAlgebra {R : Type u_1} {S : Type u_2} {a b : R} [CommSemiring R] [CommSemiring S] [Algebra S R] : Algebra S (QuadraticAlgebra R a b)

theorem QuadraticAlgebra.algebraMap_eq {R : Type u_1} {a b : R} [CommSemiring R] (r : R) : (algebraMap R (QuadraticAlgebra R a b)) r = { re := r, im := 0 }

theorem QuadraticAlgebra.algebraMap_injective {R : Type u_1} {a b : R} [CommSemiring R] : Function.Injective ⇑(algebraMap R (QuadraticAlgebra R a b))

@[simp]

theorem QuadraticAlgebra.algebraMap_inj {R : Type u_1} {a b : R} [CommSemiring R] {x y : R} : (algebraMap R (QuadraticAlgebra R a b)) x = (algebraMap R (QuadraticAlgebra R a b)) y ↔ x = y

@[simp]

theorem QuadraticAlgebra.algebraMap_re {R : Type u_1} {a b : R} (r : R) [CommSemiring R] : ((algebraMap R (QuadraticAlgebra R a b)) r).re = r

@[simp]

theorem QuadraticAlgebra.algebraMap_im {R : Type u_1} {a b : R} (r : R) [CommSemiring R] : ((algebraMap R (QuadraticAlgebra R a b)) r).im = 0

instance QuadraticAlgebra.instIsTorsionFree {R : Type u_1} {S : Type u_2} {a b : R} [CommSemiring R] [Semiring S] [Module S R] [Module.IsTorsionFree S R] : Module.IsTorsionFree S (QuadraticAlgebra R a b)

@[simp]

theorem QuadraticAlgebra.C_pow {R : Type u_1} {a b : R} [CommSemiring R] (n : ℕ) (r : R) : QuadraticAlgebra.C (r ^ n) = QuadraticAlgebra.C r ^ n

theorem QuadraticAlgebra.mul_C_eq_smul {R : Type u_1} {a b : R} [CommSemiring R] (r : R) (x : QuadraticAlgebra R a b) : x * QuadraticAlgebra.C r = r • x

@[simp]

theorem QuadraticAlgebra.C_eq_algebraMap {R : Type u_1} {a b : R} [CommSemiring R] : QuadraticAlgebra.C = ⇑(algebraMap R (QuadraticAlgebra R a b))

theorem QuadraticAlgebra.smul_C {R : Type u_1} {a b : R} [CommSemiring R] (r1 r2 : R) : r1 • QuadraticAlgebra.C r2 = QuadraticAlgebra.C (r1 * r2)

theorem QuadraticAlgebra.algebraMap_dvd_iff {R : Type u_1} {a b : R} [CommSemiring R] {r : R} {z : QuadraticAlgebra R a b} : (algebraMap R (QuadraticAlgebra R a b)) r ∣ z ↔ r ∣ z.re ∧ r ∣ z.im

@[simp]

theorem QuadraticAlgebra.algebraMap_dvd_iff_dvd {R : Type u_1} {a b : R} [CommSemiring R] {z w : R} : (algebraMap R (QuadraticAlgebra R a b)) z ∣ (algebraMap R (QuadraticAlgebra R a b)) w ↔ z ∣ w

@[instance_reducible]

instance QuadraticAlgebra.instCommRing {R : Type u_1} {a b : R} [CommRing R] : CommRing (QuadraticAlgebra R a b)

instance QuadraticAlgebra.instCharZero {R : Type u_1} {a b : R} [CommRing R] [CharZero R] : CharZero (QuadraticAlgebra R a b)

@[simp]

theorem QuadraticAlgebra.zsmul_val {R : Type u_1} {a b : R} [CommRing R] (n : ℤ) (x y : R) : ↑n * { re := x, im := y } = { re := ↑n * x, im := ↑n * y }