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.

Equations

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

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

Equations

• I.instAddCommGroupCotangent = id inferInstance

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

Equations

• I.cotangentModule = id inferInstance

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

Equations

• I.instInhabitedCotangent = { default := 0 }

instance Ideal.Cotangent.moduleOfTower {R : Type u} {S : Type v} [CommRing R] [CommSemiring S] [Algebra S R] (I : Ideal R) : Module S I.Cotangent

Equations

• Ideal.Cotangent.moduleOfTower I = Submodule.Quotient.module' (I • ⊤)

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) : IsScalarTower S S' I.Cotangent

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

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

Equations

• I.toCotangent = (I • ⊤).mkQ

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

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

theorem Ideal.toCotangent_eq {R : Type u} [CommRing R] (I : Ideal R) {x : ↥I} {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) : LinearMap.range I.toCotangent = ⊤

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.

Equations

• I.cotangentToQuotientSquare = (I • ⊤).mapQ (I ^ 2) (Submodule.subtype I) ⋯

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

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

• I.cotangentIdeal = Submodule.map (Ideal.Quotient.mk (I ^ 2)).toSemilinearMap I

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

theorem Ideal.to_quotient_square_range {R : Type u} [CommRing R] (I : Ideal R) : LinearMap.range I.cotangentToQuotientSquare = 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.

Equations

• One or more equations did not get rendered due to their size.

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

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

• f.kerSquareLift = let __src := Ideal.Quotient.lift (RingHom.ker f.toRingHom ^ 2) f.toRingHom ⋯; { toRingHom := __src, commutes' := ⋯ }

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

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.

Equations

• I.quotCotangent = (Ideal.quotEquivOfEq ⋯).trans ((DoubleQuot.quotQuotEquivQuotSup (I ^ 2) I).trans (Ideal.quotEquivOfEq ⋯))

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₁ ≤ Ideal.comap f I₂) : I₁.Cotangent →ₗ[R] I₂.Cotangent

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

Equations

• I₁.mapCotangent I₂ f h = (Submodule.restrictScalars R (I₁ • ⊤)).mapQ (Submodule.restrictScalars R (I₂ • ⊤)) (f.toLinearMap.restrict h) ⋯

@[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₁ ≤ Ideal.comap f I₂) (x : ↥I₁) : (I₁.mapCotangent I₂ f h) (I₁.toCotangent x) = I₂.toCotangent ⟨f ↑x, ⋯⟩

@[reducible, inline]

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

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

Equations

• LocalRing.CotangentSpace R = (LocalRing.maximalIdeal R).Cotangent

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

Equations

• LocalRing.instModuleResidueFieldCotangentSpace R = (LocalRing.maximalIdeal R).cotangentModule

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

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

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

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

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