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

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

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

Equations

• Ideal.instAddCommGroupCotangent I = id inferInstance

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

Equations

• Ideal.cotangentModule I = id inferInstance

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

Equations

• Ideal.instInhabitedCotangent I = { default := 0 }

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

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' (Ideal.Cotangent I)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[simp]

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

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

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

Equations

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

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

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

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

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

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

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

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

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

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

Equations

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

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

theorem Ideal.toCotangent_to_quotient_square {R : Type u} [CommRing R] (I : Ideal R) (x : ↥I) : (Ideal.cotangentToQuotientSquare I) ((Ideal.toCotangent I) 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

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

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

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

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

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 : Ideal.Cotangent I) : ↑((Ideal.cotangentEquivIdeal I) x) = (Ideal.cotangentToQuotientSquare I) x

theorem Ideal.cotangentEquivIdeal_symm_apply {R : Type u} [CommRing R] (I : Ideal R) (x : R) (hx : x ∈ I) : (LinearEquiv.symm (Ideal.cotangentEquivIdeal I)) { val := (Submodule.mkQ (I ^ 2)) x, property := ⋯ } = (Ideal.toCotangent I) { val := x, property := 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

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

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

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

Equations

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

@[reducible]

def 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 = Ideal.Cotangent (LocalRing.maximalIdeal R)

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

Equations

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

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

Equations

• ⋯ = ⋯

instance LocalRing.instFiniteDimensionalResidueFieldCotangentSpaceToDivisionRingFieldInstAddCommGroupCotangentMaximalIdealToCommSemiringInstModuleResidueFieldCotangentSpaceToSemiringToDivisionSemiringToSemifieldFieldToAddCommMonoidInstAddCommGroupCotangentMaximalIdealToCommSemiring (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 (Ideal.toCotangent (LocalRing.maximalIdeal R)) 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) (⇑(Ideal.toCotangent (LocalRing.maximalIdeal R)) '' 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)