derivationQuotKerSq — Mathlib

English

For a tower of rings S over P over R with I = ker(algebraMap P S), there exists an R-derivation from P/I^2 to S ⊗P Ω[P/R] given by [x] ↦ 1 ⊗ D x. This derivation satisfies the Leibniz rule and maps the product to the sum of Leibniz terms modulo the appropriate quotient.

Русский

Пусть S над P над R, и I = ker(algebraMap P S). Существует R-деривирует от P/I^2 к S ⊗P Ω[P/R], заданный на скобке [x] ↦ 1 ⊗ D x. Этот деривант удовлетворяет правилу Лейбница и ведет произведение к сумме членов Лейбницы в соответствующем факторе.

LaTeX

$$$\\text{Derivation }\\; \\delta: P/(I^2) \\to S \\otimes_P \\Omega[P/R] \\quad\\text{ с }\\; \\delta([x]) = 1 \\otimes D x$$$

Lean4

/-- Given a tower of algebras `S/P/R`, with `I = ker(P → S)`,
this is the `R`-derivative `P/I² → S ⊗[P] Ω[P⁄R]` given by `[x] ↦ 1 ⊗ D x`.
-/
noncomputable def derivationQuotKerSq : Derivation R (P ⧸ (RingHom.ker (algebraMap P S) ^ 2)) (S ⊗[P] Ω[P⁄R]) :=
  by
  letI :=
    Submodule.liftQ ((RingHom.ker (algebraMap P S) ^ 2).restrictScalars R)
      (((mk P S _ 1).restrictScalars R).comp (KaehlerDifferential.D R P).toLinearMap)
  refine ⟨this ?_, ?_, ?_⟩
  · rintro x hx
    simp only [Submodule.restrictScalars_mem, pow_two] at hx
    simp only [LinearMap.mem_ker, LinearMap.coe_comp, LinearMap.coe_restrictScalars, Derivation.coeFn_coe,
      Function.comp_apply, mk_apply]
    refine Submodule.smul_induction_on hx ?_ ?_
    · intro x hx y hy
      simp only [smul_eq_mul, Derivation.leibniz, tmul_add, ← smul_tmul, Algebra.smul_def, mul_one,
        RingHom.mem_ker.mp hx, RingHom.mem_ker.mp hy, zero_tmul, zero_add]
    · intro x y hx hy; simp only [map_add, hx, hy, tmul_add, zero_add]
  · change (1 : S) ⊗ₜ[P] KaehlerDifferential.D R P 1 = 0; simp
  · intro a b
    obtain ⟨a, rfl⟩ := Submodule.Quotient.mk_surjective _ a
    obtain ⟨b, rfl⟩ := Submodule.Quotient.mk_surjective _ b
    change
      (1 : S) ⊗ₜ[P] KaehlerDifferential.D R P (a * b) =
        Ideal.Quotient.mk _ a • ((1 : S) ⊗ₜ[P] KaehlerDifferential.D R P b) +
          Ideal.Quotient.mk _ b • ((1 : S) ⊗ₜ[P] KaehlerDifferential.D R P a)
    simp only [← Ideal.Quotient.algebraMap_eq, IsScalarTower.algebraMap_smul, Derivation.leibniz, tmul_add, tmul_smul]

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