class Deformation.IsProArtinResAlg (Λ : Type u) [CommRing Λ] (X : Type u) [CommRing X] [Algebra Λ X] extends IsLocalRing X, IsNoetherian X X, IsPrecomplete (IsLocalRing.maximalIdeal X) X, 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
• noetherian (s : Submodule X X) : s.FG
• prec' (f : ℕ → X) : (∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD IsLocalRing.maximalIdeal X ^ m • ⊤]) → ∃ (L : X), ∀ (n : ℕ), f n ≡ L [SMOD IsLocalRing.maximalIdeal X ^ n • ⊤]
• isSurjective' : Function.Surjective ⇑(algebraMap Λ (IsLocalRing.ResidueField X))
• map_nonunit (a : Λ) : IsUnit ((algebraMap Λ X) a) → IsUnit a

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

The category of local proartinian algebras over Λ with fixed residue field 𝕜.

• carrier : Type u

  Underlying set of a ProArtinResAlg

• commRing : CommRing ↑self

  ring structure of a ProArtinResAlg

• algebra : Algebra Λ ↑self

  algebra structure of a ProArtinResAlg

• isProArtinResAlg : IsProArtinResAlg Λ ↑self

  local + Artinian + ResidueAlgebra + LocalHom

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

Equations

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

@[reducible, inline]

abbrev Deformation.ProArtinResAlg.of (Λ : Type u) [CommRing Λ] (X : Type u) [CommRing X] [Algebra Λ X] [IsLocalRing X] [IsNoetherianRing X] [IsComplete X] [IsResidueAlgebra Λ X] [IsLocalHom (algebraMap Λ X)] : ProArtinResAlg Λ

Make a ProArtinResAlg from an unbundled algebra.

Equations

• Deformation.ProArtinResAlg.of Λ X = { carrier := X, commRing := inst✝⁶, algebra := inst✝⁵, isProArtinResAlg := ⋯ }

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

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

The type of morphisms in ProArtinResAlg Λ.

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

  The underlying algebra map.

• isLocal : IsLocalHom self.hom

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

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

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

Equations

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

@[reducible, inline]

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

Typecheck an local AlgHom as a morphism in ProArtinResAlg.

Equations

• Deformation.ProArtinResAlg.ofHom f = { hom := f, isLocal := h }

@[simp]

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

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

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

Build a AlgEquiv from an isomorphism in the category ProArtinResAlg R.

Equations

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

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

The residue field 𝕜 as a proartinian local algebra.

Equations

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

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

Equations

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

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

The quotient map of a ProArtinResAlg to the residue field.

Equations

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

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

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

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

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

Equations

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

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

𝕜 is terminal in ProArtinResAlg.

Equations

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

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

Equations

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

@[simp]

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

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

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

theorem Deformation.inclusion (Λ : Type u) [CommRing Λ] (X : Type u) [CommRing X] [Algebra Λ X] : IsArtinResAlg Λ X → IsProArtinResAlg Λ X

def Deformation.inclusionFunctor {Λ : Type u} [CommRing Λ] : CategoryTheory.Functor (ArtinResAlg Λ) (ProArtinResAlg Λ)

Equations

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

@[simp]

theorem Deformation.inclusionFunctor_obj_carrier {Λ : Type u} [CommRing Λ] (X : ArtinResAlg Λ) : ↑(inclusionFunctor.obj X) = ↑X

@[simp]

theorem Deformation.inclusionFunctor_map_hom {Λ : Type u} [CommRing Λ] {X✝ Y✝ : ArtinResAlg Λ} (f : X✝ ⟶ Y✝) : (inclusionFunctor.map f).hom = f.hom

instance Deformation.instIsArtinianRingCarrierObjArtinResAlgProArtinResAlgInclusionFunctor (Λ : Type u) [CommRing Λ] (A : ArtinResAlg Λ) : IsArtinianRing ↑(inclusionFunctor.obj A)

@[simp]

theorem Deformation.inclusion_residueField (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] : inclusionFunctor.obj ArtinResAlg.residueField = ProArtinResAlg.residueField