mathlib3documentation

ring_theory.derivation.to_square_zero

Results #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

• derivation_to_square_zero_equiv_lift: 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 diff_to_ideal_of_quotient_comp_eq {R : Type u} {A : Type v} {B : Type w} [comm_ring B] [ A] [ B] (I : ideal B) (f₁ f₂ : A →ₐ[R] B) (e : I).comp f₁ = I).comp f₂) :

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
• e = _
@[simp]
theorem diff_to_ideal_of_quotient_comp_eq_apply {R : Type u} {A : Type v} {B : Type w} [comm_ring B] [ A] [ B] (I : ideal B) (f₁ f₂ : A →ₐ[R] B) (e : I).comp f₁ = I).comp f₂) (x : A) :
( e) x) = f₁ x - f₂ x
def derivation_to_square_zero_of_lift {R : Type u} {A : Type v} {B : Type w} [comm_ring B] [ A] [ B] (I : ideal B) (hI : I ^ 2 = ) [ B] [ B] (f : A →ₐ[R] B) (e : I).comp f = (B I)) :
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 a R-derivation from A to I.

Equations
theorem derivation_to_square_zero_of_lift_apply {R : Type u} {A : Type v} {B : Type w} [comm_ring B] [ A] [ B] (I : ideal B) (hI : I ^ 2 = ) [ B] [ B] (f : A →ₐ[R] B) (e : I).comp f = (B I)) (x : A) :
( e) x) = f x - B) x
theorem lift_of_derivation_to_square_zero_apply {R : Type u} {A : Type v} {B : Type w} [comm_ring B] [ A] [ B] (I : ideal B) (hI : I ^ 2 = ) [ B] [ B] (f : A I) (x : A) :
x = (f x) + B) x
def lift_of_derivation_to_square_zero {R : Type u} {A : Type v} {B : Type w} [comm_ring B] [ A] [ B] (I : ideal B) (hI : I ^ 2 = ) [ B] [ B] (f : 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
@[simp]
theorem lift_of_derivation_to_square_zero_mk_apply {R : Type u} {A : Type v} {B : Type w} [comm_ring B] [ A] [ B] (I : ideal B) (hI : I ^ 2 = ) [ B] [ B] (d : A I) (x : A) :
( x) = (B I)) x
def derivation_to_square_zero_equiv_lift {R : Type u} {A : Type v} {B : Type w} [comm_ring B] [ A] [ B] (I : ideal B) (hI : I ^ 2 = ) [ B] [ B] :
A I {f // I).comp f = (B I)}

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

Equations
@[simp]
theorem derivation_to_square_zero_equiv_lift_symm_apply {R : Type u} {A : Type v} {B : Type w} [comm_ring B] [ A] [ B] (I : ideal B) (hI : I ^ 2 = ) [ B] [ B] (f : {f // I).comp f = (B I)}) :
f = _
@[simp]
theorem derivation_to_square_zero_equiv_lift_apply_coe {R : Type u} {A : Type v} {B : Type w} [comm_ring B] [ A] [ B] (I : ideal B) (hI : I ^ 2 = ) [ B] [ B] (d : A I) :
d) =