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✝¹)

Equations

• instDecidableEqQuadraticAlgebra.decEq { re := a, im := a_1 } { re := b, im := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

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

Equations

• instDecidableEqQuadraticAlgebra = instDecidableEqQuadraticAlgebra.decEq

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.

Equations

• QuadraticAlgebra.equivProd a b = { toFun := fun (z : QuadraticAlgebra R a b) => (z.re, z.im), invFun := fun (p : R × R) => { re := p.1, im := p.2 }, left_inv := ⋯, right_inv := ⋯ }

@[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.coe {R : Type u_1} {a b : R} [Zero R] (x : R) : QuadraticAlgebra R a b

Coercion R → QuadraticAlgebra R a b.

Equations

• ↑x = { re := x, im := 0 }

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

Equations

• QuadraticAlgebra.instCoe = { coe := QuadraticAlgebra.coe }

@[simp]

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

@[simp]

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

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

@[simp]

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

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

Equations

• QuadraticAlgebra.instZero = { zero := { re := 0, im := 0 } }

@[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.coe_zero {R : Type u_1} {a b : R} [Zero R] : ↑0 = 0

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

Equations

• QuadraticAlgebra.instInhabited = { default := 0 }

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

Equations

• QuadraticAlgebra.instOne = { one := { re := 1, im := 0 } }

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.coe_one {R : Type u_1} {a b : R} [Zero R] [One R] : ↑1 = 1

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

Equations

• QuadraticAlgebra.instAdd = { add := fun (z w : QuadraticAlgebra R a b) => { re := z.re + w.re, im := z.im + w.im } }

@[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.coe_add {R : Type u_1} {a b : R} [AddZeroClass R] (x y : R) : ↑(x + y) = ↑x + ↑y

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

Equations

• QuadraticAlgebra.instNeg = { neg := fun (z : QuadraticAlgebra R a b) => { re := -z.re, im := -z.im } }

@[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.coe_neg {R : Type u_1} {a b : R} [NegZeroClass R] (x : R) : ↑(-x) = -↑x

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

Equations

• QuadraticAlgebra.instSub = { sub := fun (z w : QuadraticAlgebra R a b) => { re := z.re - w.re, im := z.im - w.im } }

@[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.coe_sub {R : Type u_1} {a b : R} (r1 r2 : R) [SubNegZeroMonoid R] : ↑(r1 - r2) = ↑r1 - ↑r2

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

Equations

• QuadraticAlgebra.instMul = { mul := fun (z w : QuadraticAlgebra R a b) => { re := z.re * w.re + a * z.im * w.im, im := z.re * w.im + z.im * w.re + b * z.im * w.im } }

@[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 QuadraticAlgebra.instSMul {R : Type u_1} {S : Type u_2} {a b : R} [SMul S R] : SMul S (QuadraticAlgebra R a b)

Equations

• QuadraticAlgebra.instSMul = { smul := fun (s : S) (z : QuadraticAlgebra R a b) => { re := s • z.re, im := s • z.im } }

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 QuadraticAlgebra.instMulAction {R : Type u_1} {S : Type u_2} {a b : R} [Monoid S] [MulAction S R] : MulAction S (QuadraticAlgebra R a b)

Equations

• QuadraticAlgebra.instMulAction = { toSMul := QuadraticAlgebra.instSMul, one_smul := ⋯, mul_smul := ⋯ }

@[simp]

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

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

Equations

• One or more equations did not get rendered due to their size.

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)

Equations

• QuadraticAlgebra.instDistribMulAction = { toMulAction := QuadraticAlgebra.instMulAction, smul_zero := ⋯, smul_add := ⋯ }

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

Equations

• QuadraticAlgebra.instAddCommMonoid = { toAddMonoid := QuadraticAlgebra.instAddMonoid, add_comm := ⋯ }

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)

Equations

• QuadraticAlgebra.instModule = { toDistribMulAction := QuadraticAlgebra.instDistribMulAction, add_smul := ⋯, zero_smul := ⋯ }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• QuadraticAlgebra.instAddCommGroup = { toAddGroup := QuadraticAlgebra.instAddGroup, add_comm := ⋯ }

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem QuadraticAlgebra.coe_ofNat {R : Type u_1} {a b : R} [AddCommMonoidWithOne R] (n : ℕ) [n.AtLeastTwo] : ↑(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.coe_natCast {R : Type u_1} {a b : R} [AddCommMonoidWithOne R] (n : ℕ) : ↑↑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 QuadraticAlgebra.instAddCommGroupWithOne {R : Type u_1} {a b : R} [AddCommGroupWithOne R] : AddCommGroupWithOne (QuadraticAlgebra R a b)

Equations

• One or more equations did not get rendered due to their size.

@[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.coe_intCast {R : Type u_1} {a b : R} [AddCommGroupWithOne R] (n : ℤ) : ↑↑n = ↑n

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

Equations

• One or more equations did not get rendered due to their size.

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

@[simp]

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

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

Equations

• One or more equations did not get rendered due to their size.

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

QuadraticAlgebra.re as a LinearMap

Equations

• QuadraticAlgebra.reₗ a b = { toFun := QuadraticAlgebra.re, map_add' := ⋯, map_smul' := ⋯ }

@[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

Equations

• QuadraticAlgebra.imₗ a b = { toFun := QuadraticAlgebra.im, map_add' := ⋯, map_smul' := ⋯ }

@[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

Equations

• One or more equations did not get rendered due to their size.

@[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

Equations

• QuadraticAlgebra.basis a b = Module.Basis.ofEquivFun (QuadraticAlgebra.linearEquivTuple a b)

@[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]

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 QuadraticAlgebra.instCommSemiring {R : Type u_1} {a b : R} [CommSemiring R] : CommSemiring (QuadraticAlgebra R a b)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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))

instance QuadraticAlgebra.instNoZeroSMulDivisors {R : Type u_1} {S : Type u_2} {a b : R} [CommSemiring R] [Zero S] [SMulWithZero S R] [NoZeroSMulDivisors S R] : NoZeroSMulDivisors S (QuadraticAlgebra R a b)

@[simp]

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

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

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.