Documentation

Schlessinger.TrivSqZeroExt

source
instance instIsLocalRingTrivSqZeroExt_schlessinger (Λ : Type u_1) (M : Type u_3) [CommRing Λ] [IsLocalRing Λ] [AddCommGroup M] [Module Λ M] [Module Λᵐᵒᵖ M] [IsCentralScalar Λ M] :
IsLocalRing (TrivSqZeroExt Λ M)
source
instance instIsResidueAlgebraTrivSqZeroExt (Λ : Type u_1) (M : Type u_3) [CommRing Λ] [IsLocalRing Λ] [AddCommGroup M] [Module Λ M] (X : Type u_4) [CommRing X] [Algebra Λ X] [IsLocalRing X] [IsResidueAlgebra Λ X] [Module X M] [Module Xᵐᵒᵖ M] [IsCentralScalar X M] [IsScalarTower Λ X M] :
IsResidueAlgebra Λ (TrivSqZeroExt X M)
source
theorem tsze_maxideal_sq (k : Type u_2) (M : Type u_3) [AddCommGroup M] [Field k] [Module k M] [Module kᵐᵒᵖ M] [IsCentralScalar k M] :
IsLocalRing.maximalIdeal (TrivSqZeroExt k M) ^ 2 = 0
source
instance instIsNoetherianRingTrivSqZeroExtOfFinite_schlessinger (Λ : Type u_1) (M : Type u_3) [CommRing Λ] [AddCommGroup M] [Module Λ M] [Module Λᵐᵒᵖ M] [IsCentralScalar Λ M] [IsNoetherianRing Λ] [Module.Finite Λ M] :
IsNoetherianRing (TrivSqZeroExt Λ M)
source
instance instIsArtinianRingTrivSqZeroExtOfFinite_schlessinger (k : Type u_2) (M : Type u_3) [AddCommGroup M] [Field k] [Module k M] [Module kᵐᵒᵖ M] [IsCentralScalar k M] [Module.Finite k M] :
IsArtinianRing (TrivSqZeroExt k M)
source
instance instIsArtinianRingTrivSqZeroExtResidueFieldOfFinite_schlessinger (Λ : Type u_1) (M : Type u_3) [CommRing Λ] [IsLocalRing Λ] [AddCommGroup M] [Module Λ M] [Module (IsLocalRing.ResidueField Λ) M] [Module (IsLocalRing.ResidueField Λ)ᵐᵒᵖ M] [IsCentralScalar (IsLocalRing.ResidueField Λ) M] [IsScalarTower Λ (IsLocalRing.ResidueField Λ) M] [h : Module.Finite Λ M] :
IsArtinianRing (TrivSqZeroExt (IsLocalRing.ResidueField Λ) M)