# Documentation

Mathlib.RingTheory.Derivation.ToSquareZero

# Results #

• derivationToSquareZeroOfLift: The R-derivations from A into a square-zero ideal I of B corresponds to the lifts A →ₐ[R] B of the map A →ₐ[R] B ⧸ I.
def diffToIdealOfQuotientCompEq {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (I : ) (f₁ : A →ₐ[R] B) (f₂ : A →ₐ[R] B) (e : AlgHom.comp () f₁ = AlgHom.comp () f₂) :
A →ₗ[R] { x // x I }

If f₁ f₂ : A →ₐ[R] B are two lifts of the same A →ₐ[R] B ⧸ I, we may define a map f₁ - f₂ : A →ₗ[R] I.

Instances For
@[simp]
theorem diffToIdealOfQuotientCompEq_apply {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (I : ) (f₁ : A →ₐ[R] B) (f₂ : A →ₐ[R] B) (e : AlgHom.comp () f₁ = AlgHom.comp () f₂) (x : A) :
↑(↑() x) = f₁ x - f₂ x
def derivationToSquareZeroOfLift {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (I : ) (hI : I ^ 2 = ) [Algebra A B] [] (f : A →ₐ[R] B) (e : = IsScalarTower.toAlgHom R A (B I)) :
Derivation R A { x // x I }

Given a tower of algebras R → A → B, and a square-zero I : Ideal B, each lift A →ₐ[R] B of the canonical map A →ₐ[R] B ⧸ I corresponds to an R-derivation from A to I.

Instances For
theorem derivationToSquareZeroOfLift_apply {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (I : ) (hI : I ^ 2 = ) [Algebra A B] [] (f : A →ₐ[R] B) (e : = IsScalarTower.toAlgHom R A (B I)) (x : A) :
↑(↑() x) = f x - ↑() x
theorem liftOfDerivationToSquareZero_apply {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (I : ) (hI : I ^ 2 = ) [Algebra A B] [] (f : Derivation R A { x // x I }) (x : A) :
↑() x = ↑(f x) + ↑() x
def liftOfDerivationToSquareZero {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (I : ) (hI : I ^ 2 = ) [Algebra A B] [] (f : Derivation R A { x // x I }) :

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.

Instances For
theorem liftOfDerivationToSquareZero_mk_apply {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (I : ) (hI : I ^ 2 = ) [Algebra A B] [] (d : Derivation R A { x // x I }) (x : A) :
↑() (↑() x) = ↑(algebraMap A (B I)) x
@[simp]
theorem liftOfDerivationToSquareZero_mk_apply' {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (I : ) [Algebra A B] (d : Derivation R A { x // x I }) (x : A) :
↑() ↑(d x) + ↑(algebraMap A (B I)) x = ↑(algebraMap A (B I)) x
@[simp]
theorem derivationToSquareZeroEquivLift_apply_coe_apply {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (I : ) (hI : I ^ 2 = ) [Algebra A B] [] (d : Derivation R A { x // x I }) (x : A) :
↑(↑() d) x = ↑(d x) + ↑() x
@[simp]
theorem derivationToSquareZeroEquivLift_symm_apply_toFun_coe {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (I : ) (hI : I ^ 2 = ) [Algebra A B] [] (f : { f // = IsScalarTower.toAlgHom R A (B I) }) (c : A) :
↑(↑(().symm f) c) = f c - ↑() c
def derivationToSquareZeroEquivLift {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (I : ) (hI : I ^ 2 = ) [Algebra A B] [] :
Derivation R A { x // x I } { f // = IsScalarTower.toAlgHom R A (B I) }

Given a tower of algebras R → A → B, and a square-zero I : ideal B, there is a 1-1 correspondence between R-derivations from A to I and lifts A →ₐ[R] B of the canonical map A →ₐ[R] B ⧸ I.

Instances For