derivationOfSectionOfKerSqZero — Mathlib

English

Given a surjective map f: P → S with square-zero kernel and a section g: S → P, the map x ↦ x − g(fx) defines an R-derivation P → ker(f).

Русский

Пусть есть сюръекция f: P → S с ядром квадратно нулевого свойства и секция g: S → P; отображение x ↦ x − g(fx) задаёт R-дифференциацию P → ker(f).

LaTeX

$$$\text{Derivation}(R,P,\ker f)$ with $\mathrm{toFun}(x) = x - g(fx)$ and Leibniz property$$

Lean4

/-- Given a surjective algebra homomorphism `f : P →ₐ[R] S` with square-zero kernel `I`,
and a section `g : S →ₐ[R] P` (as an algebra homomorphism),
we get an `R`-derivation `P → I` via `x ↦ x - g (f x)`.
-/
@[simps]
def derivationOfSectionOfKerSqZero (f : P →ₐ[R] S) (hf' : (RingHom.ker f) ^ 2 = ⊥) (g : S →ₐ[R] P)
    (hg : f.comp g = AlgHom.id R S) : Derivation R P (RingHom.ker f)
    where
  toFun x := ⟨x - g (f x), by simpa [RingHom.mem_ker, sub_eq_zero] using AlgHom.congr_fun hg.symm (f x)⟩
  map_add' x y := by simp only [map_add, AddMemClass.mk_add_mk, Subtype.mk.injEq]; ring
  map_smul' x
    y := by
    ext
    simp only [Algebra.smul_def, map_mul, AlgHom.commutes, RingHom.id_apply, Submodule.coe_smul_of_tower]
    ring
  map_one_eq_zero' := by simp only [LinearMap.coe_mk, AddHom.coe_mk, map_one, sub_self, Submodule.mk_eq_zero]
  leibniz' a
    b :=
    by
    have : (a - g (f a)) * (b - g (f b)) = 0 :=
      by
      rw [← Ideal.mem_bot, ← hf', pow_two]
      apply Ideal.mul_mem_mul
      · simpa [RingHom.mem_ker, sub_eq_zero] using AlgHom.congr_fun hg.symm (f a)
      · simpa [RingHom.mem_ker, sub_eq_zero] using AlgHom.congr_fun hg.symm (f b)
    ext
    rw [← sub_eq_zero]
    conv_rhs => rw [← neg_zero, ← this]
    simp only [LinearMap.coe_mk, AddHom.coe_mk, map_mul, SetLike.mk_smul_mk, smul_eq_mul, mul_sub,
      AddMemClass.mk_add_mk, sub_mul, neg_sub]
    ring

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