mathlib3 documentation

ring_theory.ideal.cotangent

The module I ⧸ I ^ 2 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.cotangent_equiv_ideal.

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

@[protected, instance]
def ideal.cotangent.module {R : Type u_1} [comm_ring R] (I : ideal R) :
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
def ideal.cotangent.module_of_tower {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_semiring S] [algebra S R] (I : ideal R) :
Equations
@[protected, instance]
def ideal.cotangent.is_scalar_tower {R : Type u_1} {S : Type u_2} {S' : Type u_3} [comm_ring R] [comm_semiring S] [algebra S R] [comm_semiring S'] [algebra S' R] [algebra S S'] [is_scalar_tower S S' R] (I : ideal R) :
@[protected, instance]
theorem ideal.to_cotangent_apply {R : Type u_1} [comm_ring R] (I : ideal R) (ᾰ : I) :
def ideal.to_cotangent {R : Type u_1} [comm_ring R] (I : ideal R) :

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

Equations
theorem ideal.mem_to_cotangent_ker {R : Type u_1} [comm_ring R] (I : ideal R) {x : I} :
theorem ideal.to_cotangent_eq {R : Type u_1} [comm_ring R] (I : ideal R) {x y : I} :
theorem ideal.to_cotangent_eq_zero {R : Type u_1} [comm_ring R] (I : ideal R) (x : I) :
(I.to_cotangent) x = 0 x I ^ 2

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

Equations
def ideal.cotangent_ideal {R : Type u_1} [comm_ring R] (I : ideal R) :
ideal (R I ^ 2)

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

Equations
noncomputable def ideal.cotangent_equiv_ideal {R : Type u_1} [comm_ring R] (I : ideal R) :

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

Equations
theorem ideal.cotangent_equiv_ideal_symm_apply {R : Type u_1} [comm_ring R] (I : ideal R) (x : R) (hx : x I) :
def alg_hom.ker_square_lift {R : Type u_1} [comm_ring R] {A : Type u_4} {B : Type u_5} [comm_ring A] [comm_ring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) :

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

Equations
def ideal.quot_cotangent {R : Type u_1} [comm_ring R] (I : ideal R) :

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

Equations
@[reducible]

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

Equations