Documentation

TauCeti.Algebra.DualNumber.TensorProduct

Base change of the dual numbers #

For a commutative R-algebra S, the dual numbers commute with base change: S ⊗[R] R[ε] ≃ₐ[S] S[ε], sending s ⊗ (a + b ε) to s • (a + b ε) with a and b mapped into S.

The statement and naming are modelled on Mathlib's MvPolynomial.algebraTensorAlgEquiv (in Mathlib/RingTheory/TensorProduct/MvPolynomial.lean); the construction here instead assembles the two directions from Algebra.TensorProduct.lift and DualNumber.lift.

source
noncomputable def TauCeti.dualNumberAlgebraTensorAlgEquiv (R : Type u_1) (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] :
TensorProduct R S (DualNumber R) ≃ₐ[S] DualNumber S

The base change S ⊗[R] R[ε] ≃ₐ[S] S[ε] of the dual numbers.

Instances For
    source
    @[simp]
    theorem TauCeti.dualNumberAlgebraTensorAlgEquiv_tmul_fst {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] (s : S) (x : DualNumber R) :
    TrivSqZeroExt.fst ((dualNumberAlgebraTensorAlgEquiv R S) (s ⊗ₜ[R] x)) = s * (algebraMap R S) (TrivSqZeroExt.fst x)

    The scalar part of the base change of s ⊗ x.

    source
    @[simp]
    theorem TauCeti.dualNumberAlgebraTensorAlgEquiv_tmul_snd {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] (s : S) (x : DualNumber R) :
    TrivSqZeroExt.snd ((dualNumberAlgebraTensorAlgEquiv R S) (s ⊗ₜ[R] x)) = s * (algebraMap R S) (TrivSqZeroExt.snd x)

    The infinitesimal part of the base change of s ⊗ x.

    source
    @[simp]
    theorem TauCeti.dualNumberAlgebraTensorAlgEquiv_tmul_one {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] (s : S) :
    (dualNumberAlgebraTensorAlgEquiv R S) (s ⊗ₜ[R] 1) = (algebraMap S (DualNumber S)) s

    Base change sends s ⊗ 1 to the constant s.

    source
    @[simp]
    theorem TauCeti.dualNumberAlgebraTensorAlgEquiv_tmul_eps {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] (s : S) :
    (dualNumberAlgebraTensorAlgEquiv R S) (s ⊗ₜ[R] DualNumber.eps) = s • DualNumber.eps

    Base change sends s ⊗ ε to s • ε.

    source
    @[simp]
    theorem TauCeti.dualNumberAlgebraTensorAlgEquiv_symm_eps {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] :
    (dualNumberAlgebraTensorAlgEquiv R S).symm DualNumber.eps = 1 ⊗ₜ[R] DualNumber.eps

    The inverse of base change sends ε to 1 ⊗ ε.