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) :

module (R ⧸ I) I.cotangent

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

I.cotangent = (↥I ⧸ I • ⊤)

Instances for ideal.cotangent

@[protected, instance]

def ideal.cotangent.add_comm_group {R : Type u_1} [comm_ring R] (I : ideal R) :

add_comm_group I.cotangent

@[protected, instance]

def ideal.cotangent.inhabited {R : Type u_1} [comm_ring R] (I : ideal R) :

inhabited I.cotangent

Equations

ideal.cotangent.inhabited I = {default := 0}

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

module S I.cotangent

Equations

ideal.cotangent.module_of_tower I = submodule.quotient.module' (I • ⊤)

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

is_scalar_tower S S' I.cotangent

@[protected, instance]

def ideal.cotangent.is_noetherian {R : Type u_1} [comm_ring R] (I : ideal R) [is_noetherian R ↥I] :

is_noetherian R I.cotangent

theorem ideal.to_cotangent_apply {R : Type u_1} [comm_ring R] (I : ideal R) (ᾰ : ↥I) :

⇑(I.to_cotangent) ᾰ = submodule.quotient.mk ᾰ

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

↥I →ₗ[R] I.cotangent

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

Equations

I.to_cotangent = (I • ⊤).mkq

theorem ideal.map_to_cotangent_ker {R : Type u_1} [comm_ring R] (I : ideal R) :

submodule.map (submodule.subtype I) (linear_map.ker I.to_cotangent) = I ^ 2

theorem ideal.mem_to_cotangent_ker {R : Type u_1} [comm_ring R] (I : ideal R) {x : ↥I} :

x ∈ linear_map.ker I.to_cotangent ↔ ↑x ∈ I ^ 2

theorem ideal.to_cotangent_eq {R : Type u_1} [comm_ring R] (I : ideal R) {x y : ↥I} :

⇑(I.to_cotangent) x = ⇑(I.to_cotangent) y ↔ ↑x - ↑y ∈ I ^ 2

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) :

function.surjective ⇑(I.to_cotangent)

theorem ideal.to_cotangent_range {R : Type u_1} [comm_ring R] (I : ideal R) :

linear_map.range I.to_cotangent = ⊤

theorem ideal.cotangent_subsingleton_iff {R : Type u_1} [comm_ring R] (I : ideal R) :

subsingleton I.cotangent ↔ is_idempotent_elem I

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

I.cotangent →ₗ[R] R ⧸ I ^ 2

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

Equations

I.cotangent_to_quotient_square = (I • ⊤).mapq (I ^ 2) (submodule.subtype I) _

theorem ideal.to_quotient_square_comp_to_cotangent {R : Type u_1} [comm_ring R] (I : ideal R) :

I.cotangent_to_quotient_square.comp I.to_cotangent = (submodule.mkq (I ^ 2)).comp (submodule.subtype I)

@[simp]

theorem ideal.to_cotangent_to_quotient_square {R : Type u_1} [comm_ring R] (I : ideal R) (x : ↥I) :

⇑(I.cotangent_to_quotient_square) (⇑(I.to_cotangent) x) = ⇑(submodule.mkq (I ^ 2)) ↑x

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

I.cotangent_ideal = let rq : R →+* R ⧸ I ^ 2 := ideal.quotient.mk (I ^ 2) in submodule.map rq.to_semilinear_map I

theorem ideal.cotangent_ideal_square {R : Type u_1} [comm_ring R] (I : ideal R) :

I.cotangent_ideal ^ 2 = ⊥

theorem ideal.to_quotient_square_range {R : Type u_1} [comm_ring R] (I : ideal R) :

linear_map.range I.cotangent_to_quotient_square = submodule.restrict_scalars R I.cotangent_ideal

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

I.cotangent ≃ₗ[R] ↥(I.cotangent_ideal)

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

Equations

I.cotangent_equiv_ideal = {to_fun := (linear_map.cod_restrict (submodule.restrict_scalars R I.cotangent_ideal) I.cotangent_to_quotient_square _).to_fun, map_add' := _, map_smul' := _, inv_fun := (equiv.of_bijective (λ (c : I.cotangent), ⟨⇑(I.cotangent_to_quotient_square) c, _⟩) _).inv_fun, left_inv := _, right_inv := _}

@[simp, nolint]

theorem ideal.cotangent_equiv_ideal_apply {R : Type u_1} [comm_ring R] (I : ideal R) (x : I.cotangent) :

↑(⇑(I.cotangent_equiv_ideal) x) = ⇑(I.cotangent_to_quotient_square) x

theorem ideal.cotangent_equiv_ideal_symm_apply {R : Type u_1} [comm_ring R] (I : ideal R) (x : R) (hx : x ∈ I) :

⇑(I.cotangent_equiv_ideal.symm) ⟨⇑(submodule.mkq (I ^ 2)) x, _⟩ = ⇑(I.to_cotangent) ⟨x, hx⟩

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) :

A ⧸ ring_hom.ker f.to_ring_hom ^ 2 →ₐ[R] B

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

Equations

f.ker_square_lift = {to_fun := (ideal.quotient.lift (ring_hom.ker f.to_ring_hom ^ 2) f.to_ring_hom _).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

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] [algebra R A] [algebra R B] (f : A →ₐ[R] B) :

ring_hom.ker f.ker_square_lift.to_ring_hom = (ring_hom.ker f.to_ring_hom).cotangent_ideal

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

(R ⧸ I ^ 2) ⧸ I.cotangent_ideal ≃+* R ⧸ I

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

Equations

I.quot_cotangent = (ideal.quot_equiv_of_eq _).trans ((double_quot.quot_quot_equiv_quot_sup (I ^ 2) I).trans (ideal.quot_equiv_of_eq _))

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

local_ring.cotangent_space R = (local_ring.maximal_ideal R).cotangent

@[protected, instance]

def local_ring.cotangent_space.module (R : Type u_1) [comm_ring R] [local_ring R] :

module (local_ring.residue_field R) (local_ring.cotangent_space R)

Equations

local_ring.cotangent_space.module R = ideal.cotangent.module (local_ring.maximal_ideal R)

@[protected, instance]

def local_ring.cotangent_space.is_scalar_tower (R : Type u_1) [comm_ring R] [local_ring R] :

is_scalar_tower R (local_ring.residue_field R) (local_ring.cotangent_space R)

@[protected, instance]

def local_ring.cotangent_space.finite_dimensional (R : Type u_1) [comm_ring R] [local_ring R] [is_noetherian_ring R] :

finite_dimensional (local_ring.residue_field R) (local_ring.cotangent_space R)