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} [CommSemiring R] [CommSemiring A] [CommRing B] [Algebra R A] [Algebra R B] (I : Ideal B) (f₁ : A →ₐ[R] B) (f₂ : A →ₐ[R] B) (e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) 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

source

@[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₁ : A →ₐ[R] B) (f₂ : A →ₐ[R] B) (e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂) (x : A) :

↑(↑(diffToIdealOfQuotientCompEq I f₁ f₂ e) x) = ↑f₁ x - ↑f₂ x

source

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) (hI : I ^ 2 = ⊥) [Algebra A B] [IsScalarTower R A B] (f : A →ₐ[R] B) (e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = 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

source

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) (hI : I ^ 2 = ⊥) [Algebra A B] [IsScalarTower R A B] (f : A →ₐ[R] B) (e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f = IsScalarTower.toAlgHom R A (B ⧸ I)) (x : A) :

↑(↑(derivationToSquareZeroOfLift I hI f e) x) = ↑f x - ↑(algebraMap A B) x

source

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) (hI : I ^ 2 = ⊥) [Algebra A B] [IsScalarTower R A B] (f : Derivation R A { x // x ∈ I }) (x : A) :

↑(liftOfDerivationToSquareZero I hI f) x = ↑(↑f x) + ↑(algebraMap A B) x

source

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) (hI : I ^ 2 = ⊥) [Algebra A B] [IsScalarTower R A B] (f : Derivation R A { x // x ∈ 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.

Instances For

source

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) (hI : I ^ 2 = ⊥) [Algebra A B] [IsScalarTower R A B] (d : Derivation R A { x // x ∈ I }) (x : A) :

↑(Ideal.Quotient.mk I) (↑(liftOfDerivationToSquareZero I hI d) x) = ↑(algebraMap A (B ⧸ I)) x

source

@[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 { x // x ∈ I }) (x : A) :

↑(Ideal.Quotient.mk I) ↑(↑d x) + ↑(algebraMap A (B ⧸ I)) x = ↑(algebraMap A (B ⧸ I)) x

source

@[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) (hI : I ^ 2 = ⊥) [Algebra A B] [IsScalarTower R A B] (d : Derivation R A { x // x ∈ I }) (x : A) :

↑↑(↑(derivationToSquareZeroEquivLift I hI) d) x = ↑(↑d x) + ↑(algebraMap A B) x

source

@[simp]

theorem derivationToSquareZeroEquivLift_symm_apply_toFun_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) (hI : I ^ 2 = ⊥) [Algebra A B] [IsScalarTower R A B] (f : { f // AlgHom.comp (Ideal.Quotient.mkₐ R I) f = IsScalarTower.toAlgHom R A (B ⧸ I) }) (c : A) :

↑(↑(↑(derivationToSquareZeroEquivLift I hI).symm f) c) = ↑↑f c - ↑(algebraMap A B) c

source

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) (hI : I ^ 2 = ⊥) [Algebra A B] [IsScalarTower R A B] :

Derivation R A { x // x ∈ I } ≃ { f // AlgHom.comp (Ideal.Quotient.mkₐ R 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