Documentation

Mathlib.RingTheory.Ideal.Cotangent

The module I ⧸ I ^ 2 #

In this file, we provide special API support for the module I ⧸ I ^ 2. The official definition is a quotient module of I, but the alternative definition as an ideal of R ⧸ I ^ 2 is also given, and the two are R-equivalent as in Ideal.cotangentEquivIdeal.

Additional support is also given to the cotangent space m ⧸ m ^ 2 of a local ring.

def Ideal.Cotangent {R : Type u} [CommRing R] (I : Ideal R) :

I ⧸ I ^ 2 as a quotient of I.

Equations
Instances For
    instance Ideal.cotangentModule {R : Type u} [CommRing R] (I : Ideal R) :
    Equations
    instance Ideal.Cotangent.isScalarTower {R : Type u} {S : Type v} {S' : Type w} [CommRing R] [CommSemiring S] [Algebra S R] [CommSemiring S'] [Algebra S' R] [Algebra S S'] [IsScalarTower S S' R] (I : Ideal R) :
    Equations
    • =
    @[simp]
    theorem Ideal.toCotangent_apply {R : Type u} [CommRing R] (I : Ideal R) :
    ∀ (a : I), (Ideal.toCotangent I) a = Submodule.Quotient.mk a
    def Ideal.toCotangent {R : Type u} [CommRing R] (I : Ideal R) :

    The quotient map from I to I ⧸ I ^ 2.

    Equations
    Instances For
      theorem Ideal.mem_toCotangent_ker {R : Type u} [CommRing R] (I : Ideal R) {x : I} :
      theorem Ideal.toCotangent_eq {R : Type u} [CommRing R] (I : Ideal R) {x : I} {y : I} :
      (Ideal.toCotangent I) x = (Ideal.toCotangent I) y x - y I ^ 2
      theorem Ideal.toCotangent_eq_zero {R : Type u} [CommRing R] (I : Ideal R) (x : I) :
      (Ideal.toCotangent I) x = 0 x I ^ 2

      The inclusion map I ⧸ I ^ 2 to R ⧸ I ^ 2.

      Equations
      Instances For
        def Ideal.cotangentIdeal {R : Type u} [CommRing R] (I : Ideal R) :
        Ideal (R I ^ 2)

        I ⧸ I ^ 2 as an ideal of R ⧸ I ^ 2.

        Equations
        Instances For

          The equivalence of the two definitions of I / I ^ 2, either as the quotient of I or the ideal of R / I ^ 2.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem Ideal.cotangentEquivIdeal_symm_apply {R : Type u} [CommRing R] (I : Ideal R) (x : R) (hx : x I) :
            (LinearEquiv.symm (Ideal.cotangentEquivIdeal I)) { val := (Submodule.mkQ (I ^ 2)) x, property := } = (Ideal.toCotangent I) { val := x, property := hx }
            def AlgHom.kerSquareLift {R : Type u} [CommRing R] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
            A RingHom.ker f.toRingHom ^ 2 →ₐ[R] B

            The lift of f : A →ₐ[R] B to A ⧸ J ^ 2 →ₐ[R] B with J being the kernel of f.

            Equations
            Instances For
              theorem AlgHom.ker_kerSquareLift {R : Type u} [CommRing R] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
              def Ideal.quotCotangent {R : Type u} [CommRing R] (I : Ideal R) :

              The quotient ring of I ⧸ I ^ 2 is R ⧸ I.

              Equations
              Instances For
                @[reducible]

                The A ⧸ I-vector space I ⧸ I ^ 2.

                Equations
                Instances For