# mathlibdocumentation

ring_theory.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.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) :
def ideal.cotangent {R : Type u_1} [comm_ring R] (I : ideal R) :
Type u_1

I ⧸ I ^ 2 as a quotient of I.

Equations
Instances for ideal.cotangent
@[protected, instance]
def ideal.cotangent.add_comm_group {R : Type u_1} [comm_ring R] (I : ideal R) :
@[protected, instance]
def ideal.cotangent.inhabited {R : Type u_1} [comm_ring R] (I : ideal R) :
Equations
@[protected, instance]
def ideal.cotangent.module_of_tower {R : Type u_1} {S : Type u_2} [comm_ring R] [ 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] [ R] [comm_semiring S'] [algebra S' R] [ S'] [ S' R] (I : ideal R) :
S' I.cotangent
@[protected, instance]
def ideal.cotangent.is_noetherian {R : Type u_1} [comm_ring R] (I : ideal R) [ I] :
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.map_to_cotangent_ker {R : Type u_1} [comm_ring R] (I : ideal R) :
= I ^ 2
theorem ideal.mem_to_cotangent_ker {R : Type u_1} [comm_ring R] (I : ideal R) {x : I} :
x I ^ 2
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
theorem ideal.to_cotangent_surjective {R : Type u_1} [comm_ring R] (I : ideal R) :
theorem ideal.to_cotangent_range {R : Type u_1} [comm_ring R] (I : ideal R) :
theorem ideal.cotangent_subsingleton_iff {R : Type u_1} [comm_ring R] (I : ideal R) :
def ideal.cotangent_to_quotient_square {R : Type u_1} [comm_ring R] (I : ideal R) :

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

Equations
theorem ideal.to_quotient_square_comp_to_cotangent {R : Type u_1} [comm_ring R] (I : ideal R) :
= (submodule.mkq (I ^ 2)).comp
@[simp]
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
theorem ideal.cotangent_ideal_square {R : Type u_1} [comm_ring R] (I : ideal R) :
theorem ideal.to_quotient_square_range {R : Type u_1} [comm_ring R] (I : ideal R) :
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
@[simp, nolint]
theorem ideal.cotangent_equiv_ideal_apply {R : Type u_1} [comm_ring R] (I : ideal R) (x : I.cotangent) :
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] [ A] [ 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
theorem alg_hom.ker_ker_sqare_lift {R : Type u_1} [comm_ring R] {A : Type u_4} {B : Type u_5} [comm_ring A] [comm_ring B] [ A] [ B] (f : A →ₐ[R] B) :
@[reducible]
def local_ring.cotangent_space (R : Type u_1) [comm_ring R] [local_ring R] :
Type u_1

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

Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]