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

A small extension is a (surjective) morphism p : B ⟶ A in ArtinResAlg Λ such that its kernel I is a principal non-zero ideal with maximalIdeal B * I = 0

• principal : Submodule.IsPrincipal (RingHom.ker p.hom)
• nonZero : RingHom.ker p.hom ≠ ⊥
• small : IsLocalRing.maximalIdeal ↑B * RingHom.ker p.hom = ⊥

theorem IsSmallExtension.lem {Λ : Type u} [CommRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) : IsSmallExtension p → IsAtom (RingHom.ker p.hom)

theorem IsSmallExtension.lem' {Λ : Type u} [CommRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) : IsAtom (RingHom.ker p.hom) → IsSmallExtension p

theorem IsSmallExtension.isSmallExtension_iff {Λ : Type u} [CommRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) : IsSmallExtension p ↔ IsAtom (RingHom.ker p.hom)

A morphism is a small extension if and only if its kernel is a minimal nonzero ideal.

theorem IsSmallExtension.isSmallExtension_iff_length_ker {Λ : Type u} [CommRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsLocalRing Λ] : IsSmallExtension p ↔ Module.length Λ ↥(RingHom.ker p.hom) = 1

A morphism in ArtinResAlg Λ is a small extension if and only if its kernel has length 1 over Λ.

theorem IsSmallExtension.isSmallExtension_iff_length {Λ : Type u} [CommRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsLocalRing Λ] (h : Function.Surjective ⇑p.hom) : IsSmallExtension p ↔ Module.length Λ ↑B = Module.length Λ ↑A + 1

A surjective morphism is a small extension if and only if it reduces length by 1.

theorem IsSmallExtension.hom_induction {Λ : Type u} [CommRing Λ] {A B : Deformation.ArtinResAlg Λ} [IsLocalRing Λ] {C : {A₁ A₂ : Deformation.ArtinResAlg Λ} → (A₁ ⟶ A₂) → Prop} (p : B ⟶ A) (h : Function.Surjective ⇑p.hom) (h0 : ∀ {A₁ A₂ : Deformation.ArtinResAlg Λ} (q : A₁ ⟶ A₂), CategoryTheory.IsIso q → C q) (ih : ∀ {A₁ A₂ A₃ : Deformation.ArtinResAlg Λ} (q₁ : A₁ ⟶ A₂) (q₂ : A₂ ⟶ A₃), Function.Surjective ⇑q₁.hom → IsSmallExtension q₁ → Function.Surjective ⇑q₂.hom → C q₂ → C (CategoryTheory.CategoryStruct.comp q₁ q₂)) : C p

If a property is true for isomorphisms and stable by composing on the (categorical) left by small extensions, then it is true for any surjective morphism.

theorem IsSmallExtension.obj_induction {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {C : Deformation.ArtinResAlg Λ → Prop} (X : Deformation.ArtinResAlg Λ) (hk : C Deformation.ArtinResAlg.residueField) (hiso : ∀ {A B : Deformation.ArtinResAlg Λ} (x : A ≅ B), C B → C A) (ih : ∀ {A B : Deformation.ArtinResAlg Λ} (p : A ⟶ B), IsSmallExtension p → C B → C A) : C X

induction principle on objects using small extension

theorem IsSmallExtension.istorsion {Λ : Type u} [CommRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] : Module.IsTorsionBySet ↑B ↥(RingHom.ker p.hom) ↑(IsLocalRing.maximalIdeal ↑B)

theorem IsSmallExtension.istorsion' {Λ : Type u} [CommRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] [IsLocalRing Λ] : Module.IsTorsionBySet Λ ↥(RingHom.ker p.hom) ↑(IsLocalRing.maximalIdeal Λ)