Derivations into Square-Zero Ideals

Main statements

• 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} [CommSemiring R] [CommSemiring A] [CommRing 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₂) : 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

• diffToIdealOfQuotientCompEq I f₁ f₂ e = LinearMap.codRestrict (Submodule.restrictScalars R I) (f₁.toLinearMap - f₂.toLinearMap) ⋯

@[simp]

theorem diffToIdealOfQuotientCompEq_apply {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [CommSemiring A] [CommRing 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) : ↑((diffToIdealOfQuotientCompEq I f₁ f₂ e) x) = f₁ x - f₂ x

def derivationToSquareZeroOfLift {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [CommSemiring A] [CommRing B] [Algebra R A] [Algebra R B] (I : Ideal B) [Algebra A B] [IsScalarTower R A B] (hI : I ^ 2 = ⊥) (f : A →ₐ[R] B) (e : (Ideal.Quotient.mkₐ R I).comp f = 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

• derivationToSquareZeroOfLift I hI f e = { toLinearMap := diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯, map_one_eq_zero' := ⋯, leibniz' := ⋯ }

theorem derivationToSquareZeroOfLift_apply {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [CommSemiring A] [CommRing B] [Algebra R A] [Algebra R B] (I : Ideal B) [Algebra A B] (hI : I ^ 2 = ⊥) [IsScalarTower R A B] (f : A →ₐ[R] B) (e : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)) (x : A) : ↑((derivationToSquareZeroOfLift I hI f e) x) = f x - (algebraMap A B) x

def liftOfDerivationToSquareZero {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [CommSemiring A] [CommRing B] [Algebra R A] [Algebra R B] (I : Ideal B) [Algebra A B] [IsScalarTower R A B] (hI : I ^ 2 = ⊥) (f : Derivation R A ↥I) : A →ₐ[R] B

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

• liftOfDerivationToSquareZero I hI f = { toFun := fun (x : A) => ↑(f x) + (algebraMap A B) x, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

theorem liftOfDerivationToSquareZero_apply {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [CommSemiring A] [CommRing B] [Algebra R A] [Algebra R B] (I : Ideal B) [Algebra A B] [IsScalarTower R A B] (hI : I ^ 2 = ⊥) (f : Derivation R A ↥I) (x : A) : (liftOfDerivationToSquareZero I hI f) x = ↑(f x) + (algebraMap A B) x

theorem liftOfDerivationToSquareZero_mk_apply {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [CommSemiring A] [CommRing B] [Algebra R A] [Algebra R B] (I : Ideal B) [Algebra A B] (hI : I ^ 2 = ⊥) [IsScalarTower R A B] (d : Derivation R A ↥I) (x : A) : (Ideal.Quotient.mk I) ((liftOfDerivationToSquareZero I hI d) x) = (algebraMap A (B ⧸ I)) x

@[simp]

theorem liftOfDerivationToSquareZero_mk_apply' {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [CommSemiring A] [CommRing B] [Algebra R A] [Algebra R B] (I : Ideal B) [Algebra A B] (d : Derivation R A ↥I) (x : A) : (Ideal.Quotient.mk I) ↑(d x) + (algebraMap A (B ⧸ I)) x = (algebraMap A (B ⧸ I)) x

def derivationToSquareZeroEquivLift {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [CommSemiring A] [CommRing B] [Algebra R A] [Algebra R B] (I : Ideal B) [Algebra A B] (hI : I ^ 2 = ⊥) [IsScalarTower R A B] : Derivation R A ↥I ≃ { f : A →ₐ[R] B // (Ideal.Quotient.mkₐ R I).comp 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.

Equations

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

@[simp]

theorem derivationToSquareZeroEquivLift_apply_coe_apply {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [CommSemiring A] [CommRing B] [Algebra R A] [Algebra R B] (I : Ideal B) [Algebra A B] (hI : I ^ 2 = ⊥) [IsScalarTower R A B] (d : Derivation R A ↥I) (x : A) : ↑((derivationToSquareZeroEquivLift I hI) d) x = ↑(d x) + (algebraMap A B) x

@[simp]

theorem derivationToSquareZeroEquivLift_symm_apply_apply_coe {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [CommSemiring A] [CommRing B] [Algebra R A] [Algebra R B] (I : Ideal B) [Algebra A B] (hI : I ^ 2 = ⊥) [IsScalarTower R A B] (f : { f : A →ₐ[R] B // (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I) }) (c : A) : ↑(((derivationToSquareZeroEquivLift I hI).symm f) c) = ↑f c - (algebraMap A B) c