Schlessinger.Categories.Quotient

source

@[reducible, inline]

abbrev maxideal (X : Type u) [CommRing X] [IsLocalRing X] (n : ℕ) :

Ideal X

Equations

maxideal X n = IsLocalRing.maximalIdeal X ^ n.succ

Instances For

source

theorem antitone_maxideal (X : Type u) [CommRing X] [IsLocalRing X] :

Antitone (maxideal X)

source

theorem comap_maxideal_general {R : Type u_1} {S : Type u_2} {F : Type u_3} [CommSemiring R] [IsLocalRing R] [CommSemiring S] [IsLocalRing S] [FunLike F R S] [RingHomClass F R S] (f : F) [IsLocalHom f] :

Ideal.comap f (IsLocalRing.maximalIdeal S) = IsLocalRing.maximalIdeal R

source

theorem map_maxideal_general {R : Type u_1} {S : Type u_2} {F : Type u_3} [CommSemiring R] [IsLocalRing R] [CommSemiring S] [IsLocalRing S] [FunLike F R S] [RingHomClass F R S] (f : F) (h : Function.Surjective ⇑f) [IsLocalHom f] :

IsLocalRing.maximalIdeal S = Ideal.map f (IsLocalRing.maximalIdeal R)

source

theorem comap_maxideal_pow_le_general {R : Type u_1} {S : Type u_2} {F : Type u_3} [CommSemiring R] [IsLocalRing R] [CommSemiring S] [IsLocalRing S] [FunLike F R S] [RingHomClass F R S] (f : F) [IsLocalHom f] (n : ℕ) :

IsLocalRing.maximalIdeal R ^ n ≤ Ideal.comap f (IsLocalRing.maximalIdeal S ^ n)

source

theorem map_maxideal_pow_general {R : Type u_1} {S : Type u_2} {F : Type u_3} [CommSemiring R] [IsLocalRing R] [CommSemiring S] [IsLocalRing S] [FunLike F R S] [RingHomClass F R S] (f : F) (h : Function.Surjective ⇑f) [IsLocalHom f] (n : ℕ) :

IsLocalRing.maximalIdeal S ^ n = Ideal.map f (IsLocalRing.maximalIdeal R ^ n)

source

class QuotInC {X : Type u} [CommRing X] [IsLocalRing X] (J : Ideal X) :

Prop

lt_top : J < ⊤
maxideal_le' : ∃ (n : ℕ), IsLocalRing.maximalIdeal X ^ n ≤ J

Instances

source

instance instNontrivialQuotientIdealOfQuotInC (X : Type u) [CommRing X] [IsLocalRing X] (J : Ideal X) [QuotInC J] :

Nontrivial (X ⧸ J)

source

structure QuotCIdeal (X : Type u) [CommRing X] [IsLocalRing X] :

Type u

ideal : Ideal X
quotinc : QuotInC self.ideal

Instances For

source

theorem QuotInC.maxideal_le {X : Type u} [CommRing X] [IsLocalRing X] (J : Ideal X) [QuotInC J] :

∃ (n : ℕ), IsLocalRing.maximalIdeal X ^ n ≤ J

source

instance quotInC_inf {R : Type u} [CommRing R] [IsLocalRing R] {J K : Ideal R} [QuotInC J] [QuotInC K] :

QuotInC (J ⊓ K)

source

instance quotInC_sup {R : Type u} [CommRing R] [IsLocalRing R] {J K : Ideal R} [QuotInC J] [Nontrivial (R ⧸ K)] :

QuotInC (J ⊔ K)

source

instance quotInC_sup' {R : Type u} [CommRing R] [IsLocalRing R] {J K : Ideal R} [QuotInC J] [Nontrivial (R ⧸ K)] :

QuotInC (K ⊔ J)

source

instance is_artinian_of_quotInC {X : Type u} [CommRing X] [IsLocalRing X] [IsNoetherianRing X] (J : Ideal X) [QuotInC J] :

IsArtinianRing (X ⧸ J)

source

theorem QuotInC.of_nontrivial {X : Type u} [CommRing X] [IsLocalRing X] (J : Ideal X) [Nontrivial (X ⧸ J)] (h : ∃ (n : ℕ), IsLocalRing.maximalIdeal X ^ n ≤ J) :

QuotInC J

source

instance instNontrivialQuotientIdealHPowMaximalIdealHAddOfNat_schlessinger {R : Type u_1} [CommRing R] [IsLocalRing R] (n : ℕ) :

Nontrivial (R ⧸ IsLocalRing.maximalIdeal R ^ (n + 1))

source

instance instQuotInCHPowIdealMaximalIdealHAddOfNat {R : Type u_1} [CommRing R] [IsLocalRing R] (n : ℕ) :

QuotInC (IsLocalRing.maximalIdeal R ^ (n + 1))

source

@[reducible, inline]

abbrev quot_C (Λ : Type u) {X : Type u} [CommRing Λ] [CommRing X] [Algebra Λ X] [IsLocalRing X] [IsNoetherianRing X] [IsResidueAlgebra Λ X] [IsLocalHom (algebraMap Λ X)] (J : Ideal X) [QuotInC J] :

Deformation.ArtinResAlg Λ

X ⧸ J as an ArtinResAlg

Equations

quot_C Λ J = Deformation.ArtinResAlg.of Λ (X ⧸ J)

Instances For

source

@[reducible, inline]

abbrev quot_maxideal_C (Λ X : Type u) [CommRing Λ] [CommRing X] [Algebra Λ X] [IsLocalRing X] [IsNoetherianRing X] [IsResidueAlgebra Λ X] [IsLocalHom (algebraMap Λ X)] (n : ℕ) :

Deformation.ArtinResAlg Λ

note: since we are in a category of local rings, quotient_in_C Λ X n is defined to be $X ⧸ (𝔪 X) ^ (n + 1)

Equations

quot_maxideal_C Λ X n = quot_C Λ (IsLocalRing.maximalIdeal X ^ (n + 1))

Instances For

source

noncomputable def transitionmap {X : Type u} [CommRing X] {I J : Ideal X} (h : I ≤ J) :

X ⧸ I →ₐ[X] X ⧸ J

Equations

transitionmap h = Ideal.Quotient.factorₐ X h

Instances For

source

noncomputable def transitionmap_C (Λ : Type u) {X : Type u} [CommRing Λ] [CommRing X] [Algebra Λ X] [IsLocalRing X] [IsNoetherianRing X] [IsResidueAlgebra Λ X] [IsLocalHom (algebraMap Λ X)] {I J : Ideal X} [QuotInC I] [QuotInC J] (h : I ≤ J) :

quot_C Λ I ⟶ quot_C Λ J

Equations

transitionmap_C Λ h = Deformation.ArtinResAlg.ofHom (AlgHom.restrictScalars Λ (transitionmap h))

Instances For

source

@[simp]

theorem transitionmap_C_hom_apply (Λ : Type u) {X : Type u} [CommRing Λ] [CommRing X] [Algebra Λ X] [IsLocalRing X] [IsNoetherianRing X] [IsResidueAlgebra Λ X] [IsLocalHom (algebraMap Λ X)] {I J : Ideal X} [QuotInC I] [QuotInC J] (h : I ≤ J) (a✝ : X ⧸ I) :

(transitionmap_C Λ h).hom a✝ = (Ideal.Quotient.factorₐ X h) a✝

source

noncomputable def transitionmap_maxideal_C (Λ X : Type u) [CommRing Λ] [CommRing X] [Algebra Λ X] [IsLocalRing X] [IsNoetherianRing X] [IsResidueAlgebra Λ X] [IsLocalHom (algebraMap Λ X)] {n m : ℕ} (hmn : m ≤ n) :

quot_maxideal_C Λ X n ⟶ quot_maxideal_C Λ X m

Equations

transitionmap_maxideal_C Λ X hmn = transitionmap_C Λ ⋯

Instances For

source

@[simp]

theorem transitionmap_maxideal_C_hom_apply (Λ X : Type u) [CommRing Λ] [CommRing X] [Algebra Λ X] [IsLocalRing X] [IsNoetherianRing X] [IsResidueAlgebra Λ X] [IsLocalHom (algebraMap Λ X)] {n m : ℕ} (hmn : m ≤ n) (a✝ : X ⧸ IsLocalRing.maximalIdeal X ^ (n + 1)) :

(transitionmap_maxideal_C Λ X hmn).hom a✝ = (Ideal.Quotient.factorₐ X ⋯) a✝

source

@[simp]

theorem transitionmap_C_self {Λ : Type u} [CommRing Λ] (X : Type u) [CommRing X] [Algebra Λ X] [IsLocalRing X] [IsNoetherianRing X] [IsResidueAlgebra Λ X] [IsLocalHom (algebraMap Λ X)] {I : Ideal X} [QuotInC I] :

transitionmap_C Λ ⋯ = CategoryTheory.CategoryStruct.id (quot_C Λ I)

source

theorem transitionmap_maxideal_C_comp {Λ : Type u} (X : Type u) [CommRing Λ] [CommRing X] [Algebra Λ X] [IsLocalRing X] [IsNoetherianRing X] [IsResidueAlgebra Λ X] [IsLocalHom (algebraMap Λ X)] {n m l : ℕ} (hlm : l ≤ m) (hmn : m ≤ n) :

CategoryTheory.CategoryStruct.comp (transitionmap_maxideal_C Λ X hmn) (transitionmap_maxideal_C Λ X hlm) = transitionmap_maxideal_C Λ X ⋯

source

@[simp]

theorem transitionmap_C_comp (Λ : Type u) {X : Type u} [CommRing Λ] [CommRing X] [Algebra Λ X] [IsLocalRing X] [IsNoetherianRing X] [IsResidueAlgebra Λ X] [IsLocalHom (algebraMap Λ X)] {I J K : Ideal X} [QuotInC I] [QuotInC J] [QuotInC K] (hij : I ≤ J) (hjk : J ≤ K) :

CategoryTheory.CategoryStruct.comp (transitionmap_C Λ hij) (transitionmap_C Λ hjk) = transitionmap_C Λ ⋯

source

theorem transitionmap_C_isiso_of_le_le (Λ : Type u) {X : Type u} [CommRing Λ] [CommRing X] [Algebra Λ X] [IsLocalRing X] [IsNoetherianRing X] [IsResidueAlgebra Λ X] [IsLocalHom (algebraMap Λ X)] {I J : Ideal X} [QuotInC I] [QuotInC J] (hij : I ≤ J) (hji : J ≤ I) :

CategoryTheory.IsIso (transitionmap_C Λ hij)

source

def quot_maxideal_C_map {Λ X : Type u} [CommRing Λ] [CommRing X] [Algebra Λ X] [IsLocalRing X] [IsNoetherianRing X] [IsResidueAlgebra Λ X] [IsLocalHom (algebraMap Λ X)] {Y : Type u} [CommRing Y] [Algebra Λ Y] [IsLocalRing Y] [IsNoetherianRing Y] [IsResidueAlgebra Λ Y] [IsLocalHom (algebraMap Λ Y)] (f : X →ₐ[Λ] Y) [IsLocalHom f] (n : ℕ) :

quot_maxideal_C Λ X n ⟶ quot_maxideal_C Λ Y n

Equations

quot_maxideal_C_map f n = Deformation.ArtinResAlg.ofHom (Ideal.quotientMapₐ (IsLocalRing.maximalIdeal Y ^ (n + 1)) f ⋯)

Instances For

source

theorem quot_maxideal_C_map_commute {Λ X : Type u} [CommRing Λ] [CommRing X] [Algebra Λ X] [IsLocalRing X] [IsNoetherianRing X] [IsResidueAlgebra Λ X] [IsLocalHom (algebraMap Λ X)] {Y : Type u} [CommRing Y] [Algebra Λ Y] [IsLocalRing Y] [IsNoetherianRing Y] [IsResidueAlgebra Λ Y] [IsLocalHom (algebraMap Λ Y)] (f : X →ₐ[Λ] Y) [IsLocalHom f] {n m : ℕ} (hmn : m ≤ n) :

CategoryTheory.CategoryStruct.comp (quot_maxideal_C_map f n) (transitionmap_maxideal_C Λ Y hmn) = CategoryTheory.CategoryStruct.comp (transitionmap_maxideal_C Λ X hmn) (quot_maxideal_C_map f m)

source

def quot_C_iso_of_eq (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Algebra Λ R] [IsResidueAlgebra Λ R] {J K : Ideal R} [QuotInC J] [QuotInC K] (h : J = K) :

quot_C Λ J ≅ quot_C Λ K

Equations

quot_C_iso_of_eq Λ h = Deformation.ArtinResAlg.ofEquiv (Ideal.quotientEquivAlgOfEq Λ h)

Instances For

source

@[simp]

theorem quot_C_iso_of_eq_comp_transition (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Algebra Λ R] [IsResidueAlgebra Λ R] {J K L : Ideal R} [QuotInC J] [QuotInC K] [QuotInC L] (h : J = K) (le : L ≤ J) :

CategoryTheory.CategoryStruct.comp (transitionmap_C Λ le) (quot_C_iso_of_eq Λ h).hom = transitionmap_C Λ ⋯

source

@[simp]

theorem transition_comp_quot_C_iso_of_eq (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Algebra Λ R] [IsResidueAlgebra Λ R] {J K L : Ideal R} [QuotInC J] [QuotInC K] [QuotInC L] (h : J = K) (le : K ≤ L) :

CategoryTheory.CategoryStruct.comp (quot_C_iso_of_eq Λ h).hom (transitionmap_C Λ le) = transitionmap_C Λ ⋯

source

instance quotInC_ker_to_artin {Λ : Type u} [CommRing Λ] {B : Deformation.ArtinResAlg Λ} {C : Deformation.ProArtinResAlg Λ} (q : C ⟶ Deformation.inclusionFunctor.obj B) :

QuotInC (RingHom.ker q.hom)

source

def proartin_quot_mk {Λ : Type u} [CommRing Λ] {C : Deformation.ProArtinResAlg Λ} (I : Ideal ↑C) [QuotInC I] :

C ⟶ Deformation.inclusionFunctor.obj (quot_C Λ I)

Equations

proartin_quot_mk I = Deformation.ProArtinResAlg.ofHom (Ideal.Quotient.mkₐ Λ I)

Instances For

source

theorem proartin_quot_mk_surjective {Λ : Type u} [CommRing Λ] {C : Deformation.ProArtinResAlg Λ} (I : Ideal ↑C) [QuotInC I] :

Function.Surjective ⇑(proartin_quot_mk I).hom

source

theorem proartin_quot_mk_transitionmap_C {Λ : Type u} [CommRing Λ] {C : Deformation.ProArtinResAlg Λ} (I J : Ideal ↑C) [QuotInC I] [QuotInC J] (hIJ : I ≤ J) :

CategoryTheory.CategoryStruct.comp (proartin_quot_mk I) (Deformation.inclusionFunctor.map (transitionmap_C Λ hIJ)) = proartin_quot_mk J

source

def proartin_to_artin_fac {Λ : Type u} [CommRing Λ] {B : Deformation.ArtinResAlg Λ} {C : Deformation.ProArtinResAlg Λ} (q : C ⟶ Deformation.inclusionFunctor.obj B) :

quot_C Λ (RingHom.ker q.hom) ⟶ B

Equations

proartin_to_artin_fac q = Deformation.ArtinResAlg.ofHom (Ideal.kerLiftAlg q.hom)

Instances For

source

theorem proartin_to_artin_fac_comp {Λ : Type u} [CommRing Λ] {B : Deformation.ArtinResAlg Λ} {C : Deformation.ProArtinResAlg Λ} (q : C ⟶ Deformation.inclusionFunctor.obj B) :

CategoryTheory.CategoryStruct.comp (proartin_quot_mk (RingHom.ker q.hom)) (Deformation.inclusionFunctor.map (proartin_to_artin_fac q)) = q