Documentation

Mathlib.RingTheory.Derivation.ToSquareZero

Results #

source
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
    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₁ 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
      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) [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
        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) [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
          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) [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
            Instances For
              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) [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
              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) [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
              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 ↥I) (x : A) :
              (Ideal.Quotient.mk I) ↑(d x) + (algebraMap A (B ⧸ I)) x = (algebraMap A (B ⧸ I)) x
              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) [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
                Instances For
                  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) [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
                  source
                  @[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