The degree-two grading on the dual numbers

This file gives the dual numbers their standard nonnegative grading: scalars have degree zero and the infinitesimal generator has degree two. Thus only degrees zero and two are nonzero. The grading is internal to DualNumber R, so the graded algebra supplied here compares directly with the usual ungraded dual-number algebra.

Main definitions

• TauCeti.dualNumberGrade: the degree pieces of the dual numbers.
• TauCeti.dualNumberGradedAlgebra: the corresponding graded-algebra structure.

Main results

• TauCeti.isInternal_dualNumberGrade: the dual numbers are the internal direct sum of their scalar and infinitesimal pieces.
• TauCeti.dualNumberGrade_zero_eq_ker_snd and TauCeti.dualNumberGrade_two_eq_ker_fst: the two nonzero pieces in coordinates.
• TauCeti.dualNumberGrade_eq_bot: every degree other than zero and two vanishes.
• TauCeti.dualNumberGradeZeroEquiv and TauCeti.dualNumberGradeTwoEquiv: the two nonzero pieces are linearly equivalent to the base ring.

Implementation notes

In this grading the dual numbers R[ε] model the ring R[x]/(x²) with deg x = 2, which is the zigzag algebra of a single vertex with no edges.

noncomputable def TauCeti.dualNumberGrade (R : Type u) [CommSemiring R] (n : ℕ) : Submodule R (DualNumber R)

The standard nonnegative grading on the dual numbers: degree zero consists of scalars, degree two consists of scalar multiples of DualNumber.eps, and every other degree is zero.

Equations

• TauCeti.dualNumberGrade R n = if n = 0 then (TrivSqZeroExt.sndHom R R).ker else if n = 2 then (TrivSqZeroExt.fstHom R R R).toLinearMap.ker else ⊥

theorem TauCeti.dualNumberGrade_zero_eq_ker_snd (R : Type u) [CommSemiring R] : dualNumberGrade R 0 = (TrivSqZeroExt.sndHom R R).ker

The degree-zero piece consists exactly of dual numbers with zero infinitesimal coordinate.

theorem TauCeti.dualNumberGrade_two_eq_ker_fst (R : Type u) [CommSemiring R] : dualNumberGrade R 2 = (TrivSqZeroExt.fstHom R R R).toLinearMap.ker

The degree-two piece consists exactly of dual numbers with zero scalar coordinate.

theorem TauCeti.dualNumberGrade_eq_bot (R : Type u) [CommSemiring R] {n : ℕ} (h0 : n ≠ 0) (h2 : n ≠ 2) : dualNumberGrade R n = ⊥

All pieces other than degrees zero and two vanish.

@[simp]

theorem TauCeti.mem_dualNumberGrade_zero (R : Type u) [CommSemiring R] {x : DualNumber R} : x ∈ dualNumberGrade R 0 ↔ TrivSqZeroExt.snd x = 0

Membership in degree zero is detected by the infinitesimal coordinate.

@[simp]

theorem TauCeti.mem_dualNumberGrade_two (R : Type u) [CommSemiring R] {x : DualNumber R} : x ∈ dualNumberGrade R 2 ↔ TrivSqZeroExt.fst x = 0

Membership in degree two is detected by the scalar coordinate.

theorem TauCeti.inl_mem_dualNumberGrade_zero (R : Type u) [CommSemiring R] (r : R) : TrivSqZeroExt.inl r ∈ dualNumberGrade R 0

The scalar inclusion lands in degree zero.

theorem TauCeti.algebraMap_mem_dualNumberGrade_zero (R : Type u) [CommSemiring R] (r : R) : (algebraMap R (DualNumber R)) r ∈ dualNumberGrade R 0

The algebra map lands in degree zero.

theorem TauCeti.inr_mem_dualNumberGrade_two (R : Type u) [CommSemiring R] (r : R) : TrivSqZeroExt.inr r ∈ dualNumberGrade R 2

The infinitesimal inclusion lands in degree two.

theorem TauCeti.eps_mem_dualNumberGrade_two (R : Type u) [CommSemiring R] : DualNumber.eps ∈ dualNumberGrade R 2

The dual-number generator has degree two.

noncomputable def TauCeti.dualNumberGradeZeroEquiv (R : Type u) [CommSemiring R] : ↥(dualNumberGrade R 0) ≃ₗ[R] R

The degree-zero piece of the dual numbers is linearly equivalent to the base ring.

Equations

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

@[simp]

theorem TauCeti.dualNumberGradeZeroEquiv_apply (R : Type u) [CommSemiring R] (x : ↥(dualNumberGrade R 0)) : (dualNumberGradeZeroEquiv R) x = TrivSqZeroExt.fst ↑x

The degree-zero equivalence reads the scalar coordinate.

@[simp]

theorem TauCeti.dualNumberGradeZeroEquiv_symm_apply (R : Type u) [CommSemiring R] (r : R) : (dualNumberGradeZeroEquiv R).symm r = ⟨TrivSqZeroExt.inl r, ⋯⟩

The inverse degree-zero equivalence inserts a scalar dual number.

noncomputable def TauCeti.dualNumberGradeTwoEquiv (R : Type u) [CommSemiring R] : ↥(dualNumberGrade R 2) ≃ₗ[R] R

The degree-two piece of the dual numbers is linearly equivalent to the base ring.

Equations

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

@[simp]

theorem TauCeti.dualNumberGradeTwoEquiv_apply (R : Type u) [CommSemiring R] (x : ↥(dualNumberGrade R 2)) : (dualNumberGradeTwoEquiv R) x = TrivSqZeroExt.snd ↑x

The degree-two equivalence reads the infinitesimal coordinate.

@[simp]

theorem TauCeti.dualNumberGradeTwoEquiv_symm_apply (R : Type u) [CommSemiring R] (r : R) : (dualNumberGradeTwoEquiv R).symm r = ⟨TrivSqZeroExt.inr r, ⋯⟩

The inverse degree-two equivalence inserts an infinitesimal dual number.

theorem TauCeti.mul_mem_dualNumberGrade (R : Type u) [CommSemiring R] {m n : ℕ} {x y : DualNumber R} (hx : x ∈ dualNumberGrade R m) (hy : y ∈ dualNumberGrade R n) : x * y ∈ dualNumberGrade R (m + n)

Multiplication adds degrees in the standard grading of the dual numbers.

theorem TauCeti.dualNumberGradedMonoid (R : Type u) [CommSemiring R] : SetLike.GradedMonoid (dualNumberGrade R)

The standard grading makes the dual numbers a graded monoid. This is a theorem rather than a global instance so callers choose when to install the grading.

theorem TauCeti.isInternal_dualNumberGrade (R : Type u) [CommSemiring R] : DirectSum.IsInternal (dualNumberGrade R)

The dual numbers are the internal direct sum of the scalar piece in degree zero and the infinitesimal piece in degree two.

@[instance_reducible]

noncomputable def TauCeti.dualNumberGradedAlgebra (R : Type u) [CommSemiring R] : GradedAlgebra (dualNumberGrade R)

The standard degree-two grading makes DualNumber R a graded algebra. This is a definition rather than a global instance so callers choose when to install it locally.

Equations

• TauCeti.dualNumberGradedAlgebra R = ⋯.gradedAlgebra