Dual-number points and derivations

An R-algebra homomorphism A →ₐ[R] B[ε] into the dual numbers lifting a fixed point A →ₐ[R] B is the same data as an R-derivation of A valued in B. This is the infinitesimal-lifting dictionary specialised to the square-zero extension B[ε] → B, and it is the engine identifying the tangent space of a functor of points with a module of derivations (reductive-groups roadmap, Layer 2): tangent vectors at a point are exactly the dual-number points lying over it.

The fixed point is carried by the algebra-tower hypotheses [Algebra A B] [IsScalarTower R A B], as in Mathlib.RingTheory.Derivation.ToSquareZero. For an arbitrary point φ : A →ₐ[R] B, instantiate the tower locally with letI := φ.toRingHom.toAlgebra and IsScalarTower.of_algHom φ — in a fresh scope only: installing the instance where an SMul A B already exists creates a diamond, and derivations elaborated before it refer to the old point.

The construction is direct (send d to a ↦ inl (algebraMap A B a) + inr (d a)), which keeps B an arbitrary semiring — the image of A is central by Algebra.commutes — where the ideal-general route through Mathlib.RingTheory.Derivation.ToSquareZero would force a CommRing.

Main declarations

• derivationToDualNumberEquivLift: R-derivations A → B are equivalent to lifts A →ₐ[R] B[ε] of the structure point along TrivSqZeroExt.fstHom.

noncomputable def TauCeti.derivationToDualNumberEquivLift (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] : Derivation R A B ≃ { ψ : A →ₐ[R] DualNumber B // (TrivSqZeroExt.fstHom R B B).comp ψ = IsScalarTower.toAlgHom R A B }

Lifting the structure point of an algebra to the dual numbers is the same as giving a derivation: the equivalence between R-derivations A → B and dual-number points A →ₐ[R] B[ε] lying over the point A →ₐ[R] B of the tower.

Equations

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

@[simp]

theorem TauCeti.derivationToDualNumberEquivLift_apply_fst {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] (d : Derivation R A B) (a : A) : TrivSqZeroExt.fst (↑((derivationToDualNumberEquivLift R A B) d) a) = (algebraMap A B) a

@[simp]

theorem TauCeti.derivationToDualNumberEquivLift_apply_snd {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] (d : Derivation R A B) (a : A) : TrivSqZeroExt.snd (↑((derivationToDualNumberEquivLift R A B) d) a) = d a

@[simp]

theorem TauCeti.derivationToDualNumberEquivLift_symm_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] (ψ : { ψ : A →ₐ[R] DualNumber B // (TrivSqZeroExt.fstHom R B B).comp ψ = IsScalarTower.toAlgHom R A B }) (a : A) : ((derivationToDualNumberEquivLift R A B).symm ψ) a = TrivSqZeroExt.snd (↑ψ a)