def of IsEssential and lemma 1.4 (ii)

def IsEssential {Λ : Type u} [CommRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) : Prop

A morphism p in ArtinResAlg Λ is essential if for any morphism q such that q ≫ p is surjective, q is surjective

Equations

• IsEssential p = ∀ (C : Deformation.ArtinResAlg Λ) (q : C ⟶ B), Function.Surjective ⇑(CategoryTheory.CategoryStruct.comp q p).hom → Function.Surjective ⇑q.hom

theorem smallext_not_inj {Λ : Type u} [CommRing Λ] {A B : Deformation.ArtinResAlg Λ} {p : B ⟶ A} : IsSmallExtension p → ¬Function.Injective ⇑p.hom

theorem lem14ii {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} {p : B ⟶ A} (h : Function.Surjective ⇑p.hom) [hsmall : IsSmallExtension p] : ¬IsEssential p ↔ CategoryTheory.IsSplitEpi p

theorem proartin_hom_surj {Λ : Type u} [CommRing Λ] {A B : Deformation.ArtinResAlg Λ} {p : B ⟶ A} {C : Deformation.ProArtinResAlg Λ} (essen : IsEssential p) (q : C ⟶ Deformation.inclusionFunctor.obj B) (h : Function.Surjective ⇑(CategoryTheory.CategoryStruct.comp q (Deformation.inclusionFunctor.map p)).hom) : Function.Surjective ⇑q.hom