lift — Mathlib

English

Let R be a commutative semiring, and A,B be semirings with R-algebra structures. For every R-algebra map f: A →ₐ[R] B and a chosen element e ∈ B with e^2 = 0 that commutes with the image of f, there is a unique R-algebra homomorphism A[ε] →ₐ[R] B corresponding to the data (f, e). In other words, the dual-number extension A[ε] represents exactly those pairs (f, e) consisting of an A→ₐ[R] B map and a square-zero, centralizing perturbation.

Русский

Пусть R — коммутативная полукольца, A и B — полугруппы с R-алгебрами. Для каждого алгебро-отображения f: A →ₐ[R] B и выбранного элемента e ∈ B, удовлетворяющего e^2 = 0 и коммутирующего с образами f(A), существует уникальный R-алгебр-хомоморфизм A[ε] →ₐ[R] B, соответствующий данным (f, e). Другими словами, A[ε] представляет ровно такие пары (f, e).

LaTeX

$$$\operatorname{lift} : \{ fe : (A \toₐ[R] B) \times B \;|\; fe.2^2 = 0 \wedge \forall a!,\; Commute fe.2 (fe.1 a) \} \ \simeq\ (A[\varepsilon] \toₐ[R] B).$$$

Lean4

/-- A universal property of the dual numbers, providing a unique `A[ε] →ₐ[R] B` for every map
`f : A →ₐ[R] B` and a choice of element `e : B` which squares to `0` and commutes with the range of
`f`.

This isomorphism is named to match the similar `Complex.lift`.
Note that when `f : R →ₐ[R] B := Algebra.ofId R B`, the commutativity assumption is automatic, and
we are free to choose any element `e : B`. -/
def lift : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ a, Commute fe.2 (fe.1 a) } ≃ (A[ε] →ₐ[R] B) :=
  by
  refine Equiv.trans ?_ TrivSqZeroExt.liftEquiv
  exact
    { toFun := fun fe =>
        ⟨(fe.val.1, MulOpposite.op fe.val.2 • fe.val.1.toLinearMap), fun x y =>
          show (fe.val.1 x * fe.val.2) * (fe.val.1 y * fe.val.2) = 0 by
            rw [(fe.prop.2 _).mul_mul_mul_comm, fe.prop.1, mul_zero],
          fun r x => show fe.val.1 (r * x) * fe.val.2 = fe.val.1 r * (fe.val.1 x * fe.val.2) by rw [map_mul, mul_assoc],
          fun r x =>
          show fe.val.1 (x * r) * fe.val.2 = (fe.val.1 x * fe.val.2) * fe.val.1 r by
            rw [map_mul, (fe.prop.2 _).right_comm]⟩
      invFun := fun fg =>
        ⟨(fg.val.1, fg.val.2 1), fg.prop.1 _ _, fun a =>
          show fg.val.2 1 * fg.val.1 a = fg.val.1 a * fg.val.2 1 by
            rw [← fg.prop.2.1, ← fg.prop.2.2, smul_eq_mul, op_smul_eq_mul, mul_one, one_mul]⟩
      left_inv := fun fe =>
        Subtype.ext <| Prod.ext rfl <| show fe.val.1 1 * fe.val.2 = fe.val.2 by rw [map_one, one_mul]
      right_inv := fun fg =>
        Subtype.ext <|
          Prod.ext rfl <|
            LinearMap.ext fun x =>
              show fg.val.1 x * fg.val.2 1 = fg.val.2 x by rw [← fg.prop.2.1, smul_eq_mul, mul_one] }

Похожие утверждения