mathlib3 documentation

ring_theory.derivation.to_square_zero

Results #

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

def diff_to_ideal_of_quotient_comp_eq {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [comm_semiring A] [comm_ring B] [algebra R A] [algebra R B] (I : ideal B) (f₁ f₂ : A →ₐ[R] B) (e : (ideal.quotient.mkₐ R I).comp f₁ = (ideal.quotient.mkₐ R 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
@[simp]
theorem diff_to_ideal_of_quotient_comp_eq_apply {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [comm_semiring A] [comm_ring B] [algebra R A] [algebra R B] (I : ideal B) (f₁ f₂ : A →ₐ[R] B) (e : (ideal.quotient.mkₐ R I).comp f₁ = (ideal.quotient.mkₐ R I).comp f₂) (x : A) :
((diff_to_ideal_of_quotient_comp_eq I f₁ f₂ e) x) = f₁ x - f₂ x
def derivation_to_square_zero_of_lift {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [comm_semiring A] [comm_ring B] [algebra R A] [algebra R B] (I : ideal B) (hI : I ^ 2 = ) [algebra A B] [is_scalar_tower R A B] (f : A →ₐ[R] B) (e : (ideal.quotient.mkₐ R I).comp f = is_scalar_tower.to_alg_hom R A (B 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_semiring R] [comm_semiring A] [comm_ring B] [algebra R A] [algebra R B] (I : ideal B) (hI : I ^ 2 = ) [algebra A B] [is_scalar_tower R A B] (f : A →ₐ[R] B) (e : (ideal.quotient.mkₐ R I).comp f = is_scalar_tower.to_alg_hom R A (B I)) (x : A) :
theorem lift_of_derivation_to_square_zero_apply {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [comm_semiring A] [comm_ring B] [algebra R A] [algebra R B] (I : ideal B) (hI : I ^ 2 = ) [algebra A B] [is_scalar_tower R A B] (f : derivation R A I) (x : A) :
def lift_of_derivation_to_square_zero {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [comm_semiring A] [comm_ring B] [algebra R A] [algebra R B] (I : ideal B) (hI : I ^ 2 = ) [algebra A B] [is_scalar_tower R 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
@[simp]
theorem lift_of_derivation_to_square_zero_mk_apply {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [comm_semiring A] [comm_ring B] [algebra R A] [algebra R B] (I : ideal B) (hI : I ^ 2 = ) [algebra A B] [is_scalar_tower R A B] (d : derivation R A I) (x : A) :
def derivation_to_square_zero_equiv_lift {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [comm_semiring A] [comm_ring B] [algebra R A] [algebra R B] (I : ideal B) (hI : I ^ 2 = ) [algebra A B] [is_scalar_tower R A B] :

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