Class of Artinian local Λ-algebras having same residue field as Λ.

class Deformation.IsArtinResAlg (Λ : Type u) [CommRing Λ] (X : Type u) [CommRing X] [Algebra Λ X] extends IsLocalRing X, IsWellFounded (Submodule X X) fun (x1 x2 : Submodule X X) => x1 < x2, IsResidueAlgebra Λ X, IsLocalHom (algebraMap Λ X) : Prop

• exists_pair_ne : ∃ (x : X) (y : X), x ≠ y
• isUnit_or_isUnit_of_add_one {a b : X} (h : a + b = 1) : IsUnit a ∨ IsUnit b
• wf : WellFounded fun (x1 x2 : Submodule X X) => x1 < x2
• isSurjective' : Function.Surjective ⇑(algebraMap Λ (IsLocalRing.ResidueField X))
• map_nonunit (a : Λ) : IsUnit ((algebraMap Λ X) a) → IsUnit a

structure Deformation.ArtinResAlg (Λ : Type u) [CommRing Λ] : Type (u + 1)

The category of local Artinian algebras over Λ having same residue field as Λ.

• carrier : Type u

  Underlying set of a ArtinResAlg

• commRing : CommRing ↑self

  The commutative ring structure of a ArtinResAlg

• algebra : Algebra Λ ↑self

  The algebra structure of a ArtinResAlg

• isArtinResAlg : IsArtinResAlg Λ ↑self

  local + Artinian + ResidueAlgebra + LocalHom

instance Deformation.ArtinResAlg.instCoeSortType (Λ : Type u) [CommRing Λ] : CoeSort (ArtinResAlg Λ) (Type u)

Equations

• Deformation.ArtinResAlg.instCoeSortType Λ = { coe := Deformation.ArtinResAlg.carrier }

@[reducible, inline]

abbrev Deformation.ArtinResAlg.of (Λ : Type u) [CommRing Λ] (X : Type u) [CommRing X] [Algebra Λ X] [IsLocalRing X] [IsArtinianRing X] [IsResidueAlgebra Λ X] [IsLocalHom (algebraMap Λ X)] : ArtinResAlg Λ

Make a ArtinResAlg from an unbundled algebra.

Equations

• Deformation.ArtinResAlg.of Λ X = { carrier := X, commRing := inst✝⁵, algebra := inst✝⁴, isArtinResAlg := ⋯ }

theorem Deformation.ArtinResAlg.coe_of (Λ : Type u) [CommRing Λ] (X : Type u) [CommRing X] [Algebra Λ X] [IsLocalRing X] [IsArtinianRing X] [IsResidueAlgebra Λ X] [IsLocalHom (algebraMap Λ X)] : ↑(of Λ X) = X

structure Deformation.ArtinResAlg.Hom {Λ : Type u} [CommRing Λ] (A B : ArtinResAlg Λ) : Type u

The type of morphisms in ArtinResAlg Λ.

• hom : ↑A →ₐ[Λ] ↑B

  The underlying algebra map.

theorem Deformation.ArtinResAlg.Hom.ext {Λ : Type u} {inst✝ : CommRing Λ} {A B : ArtinResAlg Λ} {x y : A.Hom B} (hom : x.hom = y.hom) : x = y

theorem Deformation.ArtinResAlg.Hom.ext_iff {Λ : Type u} {inst✝ : CommRing Λ} {A B : ArtinResAlg Λ} {x y : A.Hom B} : x = y ↔ x.hom = y.hom

instance Deformation.ArtinResAlg.instCategory (Λ : Type u) [CommRing Λ] : CategoryTheory.Category.{u, u + 1} (ArtinResAlg Λ)

Equations

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

@[reducible, inline]

abbrev Deformation.ArtinResAlg.ofHom {Λ : Type u} [CommRing Λ] {A B : Type u} [CommRing A] [Algebra Λ A] [IsLocalRing A] [IsArtinianRing A] [IsResidueAlgebra Λ A] [IsLocalHom (algebraMap Λ A)] [CommRing B] [Algebra Λ B] [IsLocalRing B] [IsArtinianRing B] [IsResidueAlgebra Λ B] [IsLocalHom (algebraMap Λ B)] (f : A →ₐ[Λ] B) : of Λ A ⟶ of Λ B

Typecheck an AlgHom as a morphism in ArtinResAlg.

Equations

• Deformation.ArtinResAlg.ofHom f = { hom := f }

@[simp]

theorem Deformation.ArtinResAlg.hom_id {Λ : Type u} [CommRing Λ] {A : ArtinResAlg Λ} : (CategoryTheory.CategoryStruct.id A).hom = AlgHom.id Λ ↑A

theorem Deformation.ArtinResAlg.id_apply {Λ : Type u} [CommRing Λ] {A : ArtinResAlg Λ} (x : ↑A) : (CategoryTheory.CategoryStruct.id A).hom x = x

@[simp]

theorem Deformation.ArtinResAlg.hom_comp {Λ : Type u} [CommRing Λ] {A B C : ArtinResAlg Λ} (f : A ⟶ B) (g : B ⟶ C) : (CategoryTheory.CategoryStruct.comp f g).hom = g.hom.comp f.hom

theorem Deformation.ArtinResAlg.comp_apply {Λ : Type u} [CommRing Λ] {A B C : ArtinResAlg Λ} (f : A ⟶ B) (g : B ⟶ C) (x : ↑A) : (CategoryTheory.CategoryStruct.comp f g).hom x = g.hom (f.hom x)

theorem Deformation.ArtinResAlg.hom_ext {Λ : Type u} [CommRing Λ] {A B : ArtinResAlg Λ} {f g : A ⟶ B} (hf : f.hom = g.hom) : f = g

theorem Deformation.ArtinResAlg.hom_ext_iff {Λ : Type u} [CommRing Λ] {A B : ArtinResAlg Λ} {f g : A ⟶ B} : f = g ↔ f.hom = g.hom

theorem Deformation.ArtinResAlg.hom_ofHom {Λ : Type u} [CommRing Λ] {X Y : Type u} [CommRing X] [Algebra Λ X] [IsLocalRing X] [IsArtinianRing X] [IsResidueAlgebra Λ X] [IsLocalHom (algebraMap Λ X)] [CommRing Y] [Algebra Λ Y] [IsLocalRing Y] [IsArtinianRing Y] [IsResidueAlgebra Λ Y] [IsLocalHom (algebraMap Λ Y)] (f : X →ₐ[Λ] Y) : (ofHom f).hom = f

@[simp]

theorem Deformation.ArtinResAlg.ofHom_hom {Λ : Type u} [CommRing Λ] {A B : ArtinResAlg Λ} (f : A ⟶ B) : ofHom f.hom = f

@[simp]

theorem Deformation.ArtinResAlg.ofHom_id {Λ : Type u} [CommRing Λ] {X : Type u} [CommRing X] [Algebra Λ X] [IsLocalRing X] [IsArtinianRing X] [IsResidueAlgebra Λ X] [IsLocalHom (algebraMap Λ X)] : ofHom (AlgHom.id Λ X) = CategoryTheory.CategoryStruct.id (of Λ X)

@[simp]

theorem Deformation.ArtinResAlg.ofHom_comp {Λ : Type u} [CommRing Λ] {X Y Z : Type u} [CommRing X] [Algebra Λ X] [IsLocalRing X] [IsArtinianRing X] [IsResidueAlgebra Λ X] [IsLocalHom (algebraMap Λ X)] [CommRing Y] [Algebra Λ Y] [IsLocalRing Y] [IsArtinianRing Y] [IsResidueAlgebra Λ Y] [IsLocalHom (algebraMap Λ Y)] [CommRing Z] [Algebra Λ Z] [IsLocalRing Z] [IsArtinianRing Z] [IsResidueAlgebra Λ Z] [IsLocalHom (algebraMap Λ Z)] (f : X →ₐ[Λ] Y) (g : Y →ₐ[Λ] Z) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

def Deformation.ArtinResAlg.ofEquiv {Λ : Type u} [CommRing Λ] {X Y : Type u} [CommRing X] [Algebra Λ X] [IsLocalRing X] [IsArtinianRing X] [IsResidueAlgebra Λ X] [IsLocalHom (algebraMap Λ X)] [CommRing Y] [Algebra Λ Y] [IsLocalRing Y] [IsArtinianRing Y] [IsResidueAlgebra Λ Y] [IsLocalHom (algebraMap Λ Y)] (e : X ≃ₐ[Λ] Y) : of Λ X ≅ of Λ Y

Build an isomorphism in the category ArtinResAlg R from a ContinuousAlgEquiv between Algebras.

Equations

• Deformation.ArtinResAlg.ofEquiv e = { hom := Deformation.ArtinResAlg.ofHom ↑e, inv := Deformation.ArtinResAlg.ofHom ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem Deformation.ArtinResAlg.ofEquiv_inv_hom {Λ : Type u} [CommRing Λ] {X Y : Type u} [CommRing X] [Algebra Λ X] [IsLocalRing X] [IsArtinianRing X] [IsResidueAlgebra Λ X] [IsLocalHom (algebraMap Λ X)] [CommRing Y] [Algebra Λ Y] [IsLocalRing Y] [IsArtinianRing Y] [IsResidueAlgebra Λ Y] [IsLocalHom (algebraMap Λ Y)] (e : X ≃ₐ[Λ] Y) : (ofEquiv e).inv.hom = ↑e.symm

@[simp]

theorem Deformation.ArtinResAlg.ofEquiv_hom_hom {Λ : Type u} [CommRing Λ] {X Y : Type u} [CommRing X] [Algebra Λ X] [IsLocalRing X] [IsArtinianRing X] [IsResidueAlgebra Λ X] [IsLocalHom (algebraMap Λ X)] [CommRing Y] [Algebra Λ Y] [IsLocalRing Y] [IsArtinianRing Y] [IsResidueAlgebra Λ Y] [IsLocalHom (algebraMap Λ Y)] (e : X ≃ₐ[Λ] Y) : (ofEquiv e).hom.hom = ↑e

def CategoryTheory.Iso.ArtintoAlgEquiv {Λ : Type u} [CommRing Λ] {A B : Deformation.ArtinResAlg Λ} (i : A ≅ B) : ↑A ≃ₐ[Λ] ↑B

Build a ContinuousAlgEquiv from an isomorphism in the category ArtinResAlg R.

Equations

• i.ArtintoAlgEquiv = { toFun := (↑↑i.hom.hom.toRingHom).toFun, invFun := ⇑i.inv.hom, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

def Deformation.ArtinResAlg.residueField {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] : ArtinResAlg Λ

The residue field 𝕜 as a proartinian local algebra.

Equations

• Deformation.ArtinResAlg.residueField = Deformation.ArtinResAlg.of Λ (IsLocalRing.ResidueField Λ)

noncomputable instance Deformation.ArtinResAlg.instFieldCarrierResidueField {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] : Field ↑residueField

Equations

• Deformation.ArtinResAlg.instFieldCarrierResidueField = inferInstanceAs (Field (IsLocalRing.ResidueField Λ))

noncomputable def Deformation.ArtinResAlg.toResidueField {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (R : ArtinResAlg Λ) : R ⟶ residueField

The quotient map of a ArtinResAlg to the residue field.

Equations

• R.toResidueField = { hom := (↑(IsResidueAlgebra.algEquiv Λ ↑R).symm).comp (IsScalarTower.toAlgHom Λ (↑R) (IsLocalRing.ResidueField ↑R)) }

theorem Deformation.ArtinResAlg.toResidueField_surjective {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (R : ArtinResAlg Λ) : Function.Surjective ⇑R.toResidueField.hom

theorem Deformation.ArtinResAlg.ker_toResidueField {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (R : ArtinResAlg Λ) : RingHom.ker R.toResidueField.hom = IsLocalRing.maximalIdeal ↑R

theorem Deformation.ArtinResAlg.to_residueField_apply {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {R : ArtinResAlg Λ} (f : R ⟶ residueField) (r : ↑R) : f.hom r = (IsLocalRing.residue Λ) (IsResidueAlgebra.preimage Λ r)

noncomputable instance Deformation.ArtinResAlg.instUniqueHomResidueField {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (R : ArtinResAlg Λ) : Unique (R ⟶ residueField)

Equations

• R.instUniqueHomResidueField = { default := R.toResidueField, uniq := ⋯ }

noncomputable def Deformation.ArtinResAlg.isTerminalResidueField {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] : CategoryTheory.Limits.IsTerminal residueField

𝕜 is terminal in ArtinResAlg.

Equations

• Deformation.ArtinResAlg.isTerminalResidueField = CategoryTheory.Limits.IsTerminal.ofUnique Deformation.ArtinResAlg.residueField

A bijective morphism defines an isomorphism.

noncomputable def Deformation.ArtinResAlg.iso_of_bijective {Λ : Type u} [CommRing Λ] {X Y : ArtinResAlg Λ} (f : X ⟶ Y) (h : Function.Bijective ⇑f.hom) : X ≅ Y

Equations

• Deformation.ArtinResAlg.iso_of_bijective f h = Deformation.ArtinResAlg.ofEquiv (AlgEquiv.ofBijective f.hom h)

@[simp]

theorem Deformation.ArtinResAlg.iso_of_bijective_hom {Λ : Type u} [CommRing Λ] {X Y : ArtinResAlg Λ} (f : X ⟶ Y) (h : Function.Bijective ⇑f.hom) : (iso_of_bijective f h).hom = f

theorem Deformation.ArtinResAlg.isIso_of_bijective {Λ : Type u} [CommRing Λ] {X Y : ArtinResAlg Λ} (f : X ⟶ Y) (h : Function.Bijective ⇑f.hom) : CategoryTheory.IsIso f

theorem Deformation.ArtinResAlg.isIso_iff_bijective {Λ : Type u} [CommRing Λ] {X Y : ArtinResAlg Λ} (f : X ⟶ Y) : CategoryTheory.IsIso f ↔ Function.Bijective ⇑f.hom

theorem Deformation.ArtinResAlg.isArtinianNoethrianModule {Λ : Type u} [CommRing Λ] {X : Type u} [CommRing X] [Algebra Λ X] [IsLocalRing X] [IsArtinianRing X] [IsResidueAlgebra Λ X] [IsLocalRing Λ] : IsNoetherian Λ X ∧ IsArtinian Λ X

instance Deformation.ArtinResAlg.instIsArtinianOfIsLocalRing {Λ : Type u} [CommRing Λ] {X : Type u} [CommRing X] [Algebra Λ X] [IsLocalRing X] [IsArtinianRing X] [IsResidueAlgebra Λ X] [IsLocalRing Λ] : IsArtinian Λ X

instance Deformation.ArtinResAlg.instIsNoetherianOfIsLocalRing {Λ : Type u} [CommRing Λ] {X : Type u} [CommRing X] [Algebra Λ X] [IsLocalRing X] [IsArtinianRing X] [IsResidueAlgebra Λ X] [IsLocalRing Λ] : IsNoetherian Λ X