# 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] 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.

Equations
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 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.

Equations
• = let __src := ; { toLinearMap := __src, map_one_eq_zero' := , leibniz' := }
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 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 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.

Equations
• One or more equations did not get rendered due to their size.
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 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 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 I) (x : A) :
( d) x = (d x) + () x
@[simp]
theorem derivationToSquareZeroEquivLift_symm_apply_apply_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 : A →ₐ[R] B // = 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 I { f : A →ₐ[R] B // = 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.

Equations
• One or more equations did not get rendered due to their size.
Instances For