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

I ⧸ I ^ 2 as a quotient of I.

@[instance_reducible]

instance Ideal.instInhabitedCotangent {R : Type u_1} [CommRing R] (I : Ideal R) : Inhabited I.Cotangent

@[instance_reducible]

instance Ideal.instModuleCotangentOfAlgebra {R : Type u_2} {S : Type u_1} [CommRing R] [CommSemiring S] [Algebra S R] (I : Ideal R) : Module S I.Cotangent

instance Ideal.instIsScalarTowerCotangent {R : Type u_3} {S : Type u_1} {S' : Type u_2} [CommRing R] [CommSemiring S] [Algebra S R] [CommSemiring S'] [Algebra S' R] [Algebra S S'] [IsScalarTower S S' R] (I : Ideal R) : IsScalarTower S S' I.Cotangent

@[instance_reducible]

instance Ideal.instSMulCotangentOfAlgebra {R : Type u_2} {S : Type u_1} [CommRing R] [CommSemiring S] [Algebra S R] (I : Ideal R) : SMul S I.Cotangent

@[instance_reducible]

instance Ideal.instModuleQuotientCotangent {R : Type u_1} [CommRing R] (I : Ideal R) : Module (R ⧸ I) I.Cotangent

@[instance_reducible]

instance Ideal.instAddCommGroupCotangent {R : Type u_1} [CommRing R] (I : Ideal R) : AddCommGroup I.Cotangent

instance Ideal.instIsScalarTowerQuotientCotangent {R : Type u_1} [CommRing R] (I : Ideal R) : IsScalarTower R (R ⧸ I) I.Cotangent

instance Ideal.instIsNoetherianCotangentOfSubtypeMem {R : Type u_1} [CommRing R] (I : Ideal R) [IsNoetherian R ↥I] : IsNoetherian R I.Cotangent

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

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

theorem Ideal.toCotangent_apply {R : Type u} [CommRing R] (I : Ideal R) (a✝ : ↥I) : I.toCotangent a✝ = Submodule.Quotient.mk a✝

theorem Ideal.map_toCotangent_ker {R : Type u} [CommRing R] (I : Ideal R) : Submodule.map (Submodule.subtype I) I.toCotangent.ker = I ^ 2

theorem Ideal.mem_toCotangent_ker {R : Type u} [CommRing R] (I : Ideal R) {x : ↥I} : x ∈ I.toCotangent.ker ↔ ↑x ∈ I ^ 2

theorem Ideal.toCotangent_eq {R : Type u} [CommRing R] (I : Ideal R) {x y : ↥I} : I.toCotangent x = I.toCotangent y ↔ ↑x - ↑y ∈ I ^ 2

theorem Ideal.toCotangent_eq_zero {R : Type u} [CommRing R] (I : Ideal R) (x : ↥I) : I.toCotangent x = 0 ↔ ↑x ∈ I ^ 2

theorem Ideal.toCotangent_surjective {R : Type u} [CommRing R] (I : Ideal R) : Function.Surjective ⇑I.toCotangent

theorem Ideal.toCotangent_range {R : Type u} [CommRing R] (I : Ideal R) : I.toCotangent.range = ⊤

theorem Ideal.cotangent_subsingleton_iff {R : Type u} [CommRing R] (I : Ideal R) : Subsingleton I.Cotangent ↔ IsIdempotentElem I

def Ideal.cotangentToQuotientSquare {R : Type u} [CommRing R] (I : Ideal R) : I.Cotangent →ₗ[R] R ⧸ I ^ 2

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

theorem Ideal.to_quotient_square_comp_toCotangent {R : Type u} [CommRing R] (I : Ideal R) : I.cotangentToQuotientSquare ∘ₗ I.toCotangent = Submodule.mkQ (I ^ 2) ∘ₗ Submodule.subtype I

@[simp]

theorem Ideal.toCotangent_to_quotient_square {R : Type u} [CommRing R] (I : Ideal R) (x : ↥I) : I.cotangentToQuotientSquare (I.toCotangent x) = (Submodule.mkQ (I ^ 2)) ↑x

theorem Ideal.cotangentToQuotientSquare_injective {R : Type u} [CommRing R] (I : Ideal R) : Function.Injective ⇑I.cotangentToQuotientSquare

theorem Ideal.Cotangent.smul_eq_zero_of_mem {R : Type u} [CommRing R] {I : Ideal R} {x : R} (hx : x ∈ I) (m : I.Cotangent) : x • m = 0

theorem Ideal.isTorsionBySet_cotangent {R : Type u} [CommRing R] (I : Ideal R) : Module.IsTorsionBySet R I.Cotangent ↑I

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.

theorem Ideal.cotangentIdeal_square {R : Type u} [CommRing R] (I : Ideal R) : I.cotangentIdeal ^ 2 = ⊥

theorem Ideal.mk_mem_cotangentIdeal {R : Type u} [CommRing R] {I : Ideal R} {x : R} : (Quotient.mk (I ^ 2)) x ∈ I.cotangentIdeal ↔ x ∈ I

theorem Ideal.comap_cotangentIdeal {R : Type u} [CommRing R] (I : Ideal R) : comap (Quotient.mk (I ^ 2)) I.cotangentIdeal = I

theorem Ideal.range_cotangentToQuotientSquare {R : Type u} [CommRing R] (I : Ideal R) : I.cotangentToQuotientSquare.range = Submodule.restrictScalars R I.cotangentIdeal

noncomputable def Ideal.cotangentEquivIdeal {R : Type u} [CommRing R] (I : Ideal R) : I.Cotangent ≃ₗ[R] ↥I.cotangentIdeal

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

@[simp]

theorem Ideal.cotangentEquivIdeal_apply {R : Type u} [CommRing R] (I : Ideal R) (x : I.Cotangent) : ↑(I.cotangentEquivIdeal x) = I.cotangentToQuotientSquare x

theorem Ideal.cotangentEquivIdeal_symm_apply {R : Type u} [CommRing R] (I : Ideal R) (x : R) (hx : x ∈ I) : I.cotangentEquivIdeal.symm ⟨(Submodule.mkQ (I ^ 2)) x, ⋯⟩ = I.toCotangent ⟨x, hx⟩

@[reducible, inline]

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

theorem AlgHom.kerSquareLift_mk {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) (x : A) : f.kerSquareLift ((Ideal.Quotient.mk (RingHom.ker f.toRingHom ^ 2)) x) = f x

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) : RingHom.ker f.kerSquareLift.toRingHom = (RingHom.ker f.toRingHom).cotangentIdeal

@[instance_reducible]

instance Ideal.Algebra.kerSquareLift {R : Type u} [CommRing R] {A : Type u_1} [CommRing A] [Algebra R A] : Algebra (R ⧸ RingHom.ker (algebraMap R A) ^ 2) A

instance Ideal.instIsScalarTowerQuotientHPowKerRingHomAlgebraMapOfNat {R : Type u} [CommRing R] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] : IsScalarTower R (A ⧸ RingHom.ker (algebraMap A B) ^ 2) B

def Ideal.quotCotangent {R : Type u} [CommRing R] (I : Ideal R) : (R ⧸ I ^ 2) ⧸ I.cotangentIdeal ≃+* R ⧸ I

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

def Ideal.mapCotangent {R : Type u} [CommRing R] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (I₁ : Ideal A) (I₂ : Ideal B) (f : A →ₐ[R] B) (h : I₁ ≤ comap f I₂) : I₁.Cotangent →ₗ[R] I₂.Cotangent

The map I/I² → J/J² if I ≤ f⁻¹(J).

@[simp]

theorem Ideal.mapCotangent_toCotangent {R : Type u} [CommRing R] {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (I₁ : Ideal A) (I₂ : Ideal B) (f : A →ₐ[R] B) (h : I₁ ≤ comap f I₂) (x : ↥I₁) : (I₁.mapCotangent I₂ f h) (I₁.toCotangent x) = I₂.toCotangent ⟨f ↑x, ⋯⟩

def Ideal.Cotangent.lift {R : Type u} [CommRing R] {S : Type u_3} [CommRing S] [Algebra R S] {I : Ideal S} {M : Type u_4} [AddCommGroup M] [Module R M] (f : ↥I →ₗ[R] M) (hf : ∀ (x y : ↥I), f (x * y) = 0) : I.Cotangent →ₗ[R] M

Lift a linear map f : I →ₗ[R] M that vanishes on products to a linear map on the cotangent space I ⧸ I ^ 2.

@[simp]

theorem Ideal.Cotangent.lift_toCotangent {R : Type u} [CommRing R] {S : Type u_3} [CommRing S] [Algebra R S] {I : Ideal S} {M : Type u_4} [AddCommGroup M] [Module R M] (f : ↥I →ₗ[R] M) (hf : ∀ (x y : ↥I), f (x * y) = 0) (x : ↥I) : (lift f hf) (I.toCotangent x) = f x

@[simp]

theorem Ideal.Cotangent.lift_comp_toCotangent {R : Type u} [CommRing R] {S : Type u_3} [CommRing S] [Algebra R S] {I : Ideal S} {M : Type u_4} [AddCommGroup M] [Module R M] (f : ↥I →ₗ[R] M) (hf : ∀ (x y : ↥I), f (x * y) = 0) : lift f hf ∘ₗ ↑R I.toCotangent = f

theorem Ideal.Cotangent.lift_surjective_iff {R : Type u} [CommRing R] {S : Type u_3} [CommRing S] [Algebra R S] {I : Ideal S} {M : Type u_4} [AddCommGroup M] [Module R M] (f : ↥I →ₗ[R] M) (hf : ∀ (x y : ↥I), f (x * y) = 0) : Function.Surjective ⇑(lift f hf) ↔ Function.Surjective ⇑f

def Ideal.Cotangent.equivOfEq {R : Type u} [CommRing R] (I J : Ideal R) (hIJ : I = J) : I.Cotangent ≃ₗ[R] J.Cotangent

A linear isomorphism between cotangent spaces induced by an equality of ideals.

@[simp]

theorem Ideal.Cotangent.equivOfEq_toCotangent {R : Type u} [CommRing R] (I J : Ideal R) (hIJ : I = J) (x : ↥I) : (equivOfEq I J hIJ) (I.toCotangent x) = J.toCotangent ((LinearEquiv.ofEq I J hIJ) x)

@[simp]

theorem Ideal.Cotangent.equivOfEq_symm {R : Type u} [CommRing R] (I J : Ideal R) (hIJ : I = J) : (equivOfEq I J hIJ).symm = equivOfEq J I ⋯

@[reducible, inline]

abbrev IsLocalRing.CotangentSpace (R : Type u_1) [CommRing R] [IsLocalRing R] : Type u_1

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

@[instance_reducible]

instance IsLocalRing.instModuleResidueFieldCotangentSpace (R : Type u_1) [CommRing R] [IsLocalRing R] : Module (ResidueField R) (CotangentSpace R)

instance IsLocalRing.instIsScalarTowerResidueFieldCotangentSpace (R : Type u_1) [CommRing R] [IsLocalRing R] : IsScalarTower R (ResidueField R) (CotangentSpace R)

instance IsLocalRing.instFiniteDimensionalResidueFieldCotangentSpaceOfIsNoetherianRing (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] : FiniteDimensional (ResidueField R) (CotangentSpace R)

theorem IsLocalRing.subsingleton_cotangentSpace_iff {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] : Subsingleton (CotangentSpace R) ↔ IsField R

theorem IsLocalRing.CotangentSpace.map_eq_top_iff {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] {M : Submodule R ↥(maximalIdeal R)} : Submodule.map (maximalIdeal R).toCotangent M = ⊤ ↔ M = ⊤

theorem IsLocalRing.CotangentSpace.span_image_eq_top_iff {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] {s : Set ↥(maximalIdeal R)} : Submodule.span (ResidueField R) (⇑(maximalIdeal R).toCotangent '' s) = ⊤ ↔ Submodule.span R s = ⊤

theorem IsLocalRing.rank_cotangentSpace_eq_spanrank_maximalIdeal_of_fg {R : Type u_1} [CommRing R] [IsLocalRing R] (fg : (maximalIdeal R).FG) : Module.rank (ResidueField R) (CotangentSpace R) = Submodule.spanRank (maximalIdeal R)

In a local ring with its maximal ideal finitely generated, the dimension of the cotangent space is equal to the span rank of the maximal ideal.

theorem IsLocalRing.rank_cotangentSpace_eq_spanrank_maximalIdeal {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] : Module.rank (ResidueField R) (CotangentSpace R) = Submodule.spanRank (maximalIdeal R)

In a Noetherian local ring, the dimension of the cotangent space is equal to the span rank of the maximal ideal.

theorem IsLocalRing.finrank_cotangentSpace_eq_zero_iff {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] : Module.finrank (ResidueField R) (CotangentSpace R) = 0 ↔ IsField R

theorem IsLocalRing.finrank_cotangentSpace_eq_zero (R : Type u_2) [Field R] : Module.finrank (ResidueField R) (CotangentSpace R) = 0

theorem IsLocalRing.finrank_cotangentSpace_le_one_iff {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] : Module.finrank (ResidueField R) (CotangentSpace R) ≤ 1 ↔ Submodule.IsPrincipal (maximalIdeal R)

theorem Ideal.mapCotangent_surjective_of_comap_eq {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (surj : Function.Surjective ⇑(algebraMap A B)) {I : Ideal B} {J : Ideal A} (eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J) : Function.Surjective ⇑(J.mapCotangent I (Algebra.ofId A B) ⋯)

theorem Ideal.mapCotangent_ker_of_surjective {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (surj : Function.Surjective ⇑(algebraMap A B)) {I : Ideal B} {J : Ideal A} (eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J) : (J.mapCotangent I (Algebra.ofId A B) ⋯).ker = Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (RingHom.ker (algebraMap A B) ⊓ J))