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 = ({ x // x ∈ 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

• @Ideal.Cotangent.isScalarTower = @Ideal.Cotangent.isScalarTower.proof_1

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

Equations

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

@[simp]

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

def Ideal.toCotangent {R : Type u} [CommRing R] (I : Ideal R) : { x // x ∈ 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 : { x // x ∈ I }} : x ∈ LinearMap.ker (Ideal.toCotangent I) ↔ ↑x ∈ I ^ 2

theorem Ideal.toCotangent_eq {R : Type u} [CommRing R] (I : Ideal R) {x : { x // x ∈ I }} {y : { x // x ∈ 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 : { x // 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) (_ : I • ⊤ ≤ Submodule.comap (Submodule.subtype I) (I ^ 2))

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

theorem Ideal.toCotangent_to_quotient_square {R : Type u} [CommRing R] (I : Ideal R) (x : { x // 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] { x // x ∈ 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 := (_ : ↑(Submodule.mkQ (I ^ 2)) x ∈ Submodule.map (Submodule.mkQ (I ^ 2)) I) } = ↑(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 ^ 2 →ₐ[R] B

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

Equations

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

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) = Ideal.cotangentIdeal (RingHom.ker ↑f)

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

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

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

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

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

Equations

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