liftOfDerivationToSquareZero — Mathlib

English

There is an IsScalarTower-compatible equivalence between derivations A → I and lifts A → B making the canonical diagram commute; i.e., a natural bijection between derivations and lifts.

Русский

Существуют эквивалентности между деривациями A → I и лифтами A → B, сохраняющими диаграмму канонического отображения; тождественная биекция.

LaTeX

$$$\text{Equiv } Derivation(R,A,I) \simeq \{ f: A \to_{R} B \mid (Ideal.Quotient.mk) \circ f = IsScalarTower.toAlgHom R A (B/I) \}$$$

Lean4

/-- Given a tower of algebras `R → A → B`, and a square-zero `I : Ideal B`, each `R`-derivation
from `A` to `I` corresponds to a lift `A →ₐ[R] B` of the canonical map `A →ₐ[R] B ⧸ I`. -/
@[simps -isSimp]
def liftOfDerivationToSquareZero [IsScalarTower R A B] (hI : I ^ 2 = ⊥) (f : Derivation R A I) : A →ₐ[R] B :=
  {
    ((I.restrictScalars R).subtype.comp f.toLinearMap + (IsScalarTower.toAlgHom R A B).toLinearMap :
      A →ₗ[R] B) with
    toFun := fun x => f x + algebraMap A B x
    map_one' := by
      -- Note: added the `(algebraMap _ _)` hint because otherwise it would match `f 1`
      rw [map_one (algebraMap _ _), f.map_one_eq_zero, Submodule.coe_zero, zero_add]
    map_mul' := fun x y =>
      by
      have : (f x : B) * f y = 0 := by
        rw [← Ideal.mem_bot, ← hI, pow_two]
        convert Ideal.mul_mem_mul (f x).2 (f y).2 using 1
      simp only [map_mul, f.leibniz, add_mul, mul_add, Submodule.coe_add, Submodule.coe_smul_of_tower, Algebra.smul_def,
        this]
      ring
    commutes' := fun r => by
      simp only [Derivation.map_algebraMap, zero_add, Submodule.coe_zero, ← IsScalarTower.algebraMap_apply R A B r]
    map_zero' :=
      ((I.restrictScalars R).subtype.comp f.toLinearMap + (IsScalarTower.toAlgHom R A B).toLinearMap).map_zero }
    -- simp normal form is `liftOfDerivationToSquareZero_mk_apply'`

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