Documentation

Schlessinger.Categories.Lemma

theorem Deformation.length_tower (Λ : Type u_1) (A : Type u_2) [CommRing Λ] [CommRing A] [Algebra Λ A] [IsLocalRing A] (M : Type u_3) [AddCommGroup M] [Module A M] [Module Λ M] [IsScalarTower Λ A M] :

Module.length A M * Module.length Λ (IsLocalRing.ResidueField A) = Module.length Λ M

Stacks Tag 06GG

@[simp]

theorem Deformation.length_residue (Λ : Type u_1) (A : Type u_2) [CommRing Λ] [CommRing A] [Algebra Λ A] [IsLocalRing A] [IsLocalRing Λ] [IsResidueAlgebra Λ A] :

Module.length Λ (IsLocalRing.ResidueField A) = 1

theorem Deformation.length_eq (Λ : Type u_1) (A : Type u_2) [CommRing Λ] [CommRing A] [Algebra Λ A] [IsLocalRing A] (M : Type u_3) [AddCommGroup M] [Module A M] [Module Λ M] [IsScalarTower Λ A M] [IsLocalRing Λ] [IsResidueAlgebra Λ A] :

Module.length A M = Module.length Λ M

theorem Deformation.decomposition (Λ : Type u_1) {A : Type u_2} [CommRing Λ] [CommRing A] [Algebra Λ A] [IsLocalRing A] [IsResidueAlgebra Λ A] (a : A) :

∃ (a₁ : Λ), ∃ a₂ ∈ IsLocalRing.maximalIdeal A, (algebraMap Λ A) a₁ + a₂ = a

theorem Deformation.isNilpotent_maximalIdeal (A : Type u_2) [CommRing A] [IsLocalRing A] [IsArtinianRing A] :

IsNilpotent (IsLocalRing.maximalIdeal A)

theorem Deformation.isNilpotent_mem_maximalIdeal {A : Type u_2} [CommRing A] [IsLocalRing A] [IsArtinianRing A] {x : A} (h : x ∈ IsLocalRing.maximalIdeal A) :

instance Deformation.instIsLocalHomAlgHomOfIsArtinianRing_schlessinger {Λ : Type u_1} {A : Type u_2} [CommRing Λ] [CommRing A] [Algebra Λ A] [IsLocalRing A] {B : Type u_3} [CommRing B] [Algebra Λ B] [IsLocalRing B] (f : A →ₐ[Λ] B) [IsArtinianRing A] :

theorem Deformation.comap_maximalIdeal {Λ : Type u_1} {A : Type u_2} [CommRing Λ] [CommRing A] [Algebra Λ A] [IsLocalRing A] {B : Type u_3} [CommRing B] [Algebra Λ B] [IsLocalRing B] (f : A →ₐ[Λ] B) [IsLocalHom f] :

IsLocalRing.maximalIdeal A ≤ Ideal.comap f (IsLocalRing.maximalIdeal B)

If f is a local homomorphism, then f (𝔪 X) ≤ 𝔪 Y.

def Deformation.maximalIdeal_map {Λ : Type u_1} {A : Type u_2} [CommRing Λ] [CommRing A] [Algebra Λ A] [IsLocalRing A] {B : Type u_3} [CommRing B] [Algebra Λ B] [IsLocalRing B] (f : A →ₐ[Λ] B) [IsLocalHom f] :

↥(IsLocalRing.maximalIdeal A) →ₗ[Λ] ↥(IsLocalRing.maximalIdeal B)

Equations

Deformation.maximalIdeal_map f = f.toLinearMap.restrict ⋯

Instances For

@[simp]

theorem Deformation.maximalIdeal_map_apply {Λ : Type u_1} {A : Type u_2} [CommRing Λ] [CommRing A] [Algebra Λ A] [IsLocalRing A] {B : Type u_3} [CommRing B] [Algebra Λ B] [IsLocalRing B] (f : A →ₐ[Λ] B) [IsLocalHom f] (x : ↥(IsLocalRing.maximalIdeal A)) :

↑((maximalIdeal_map f) x) = f ↑x

theorem Deformation.comap_maximalIdeal_pow {Λ : Type u_1} {A : Type u_2} [CommRing Λ] [CommRing A] [Algebra Λ A] [IsLocalRing A] {B : Type u_3} [CommRing B] [Algebra Λ B] [IsLocalRing B] (f : A →ₐ[Λ] B) [IsLocalHom f] (n : ℕ) :

IsLocalRing.maximalIdeal A ^ n ≤ Ideal.comap f (IsLocalRing.maximalIdeal B ^ n)

If f is a local homomorphism, then f (𝔪 X ^ n) ≤ 𝔪 Y ^ n.

theorem Deformation.maxideal_pow_le_ker_of_artinian {Λ : Type u_1} {A : Type u_2} [CommRing Λ] [CommRing A] [Algebra Λ A] [IsLocalRing A] {B : Type u_3} [CommRing B] [Algebra Λ B] [IsLocalRing B] (f : A →ₐ[Λ] B) [IsLocalHom f] [IsArtinianRing B] :

∃ (n : ℕ), IsLocalRing.maximalIdeal A ^ n ≤ RingHom.ker f

if needed n is such that (maximalIdeal B ^ n = 0)

def Deformation.relIsoQuotient {R : Type u_1} [Ring R] (I : Ideal R) [I.IsTwoSided] :

Ideal (R ⧸ I) ≃o { J : Ideal R // I ≤ J }

Equations

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

Instances For

theorem Deformation.isartinianring_quotient_iff_wellfounded_subtype (R : Type u_1) [Ring R] (I : Ideal R) [I.IsTwoSided] :

IsArtinianRing (R ⧸ I) ↔ WellFoundedLT { p : Ideal R // I ≤ p }

instance Deformation.instWellFoundedLTSubtypeIdealLeOfIsArtinianRingQuotient_schlessinger (R : Type u_1) [Ring R] (I : Ideal R) [I.IsTwoSided] [IsArtinianRing (R ⧸ I)] :

WellFoundedLT { p : Ideal R // I ≤ p }

theorem Deformation.isArtinian_of_noetherian_nilpotent (X : Type u_1) [CommRing X] [IsLocalRing X] [IsNoetherianRing X] (h : IsNilpotent (IsLocalRing.maximalIdeal X)) :

IsArtinianRing X