Documentation

Mathlib.RingTheory.Derivation.ToSquareZero

Results #

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
    @[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
    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
      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
      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
      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 }) :

      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
        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
        @[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
        @[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
        @[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
        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