The colon construction on preradicals

Given preradicals Φ and Ψ on an abelian category C, this file defines their colon Φ : Ψ in the sense of Stenström. Following Stenström, one can realize the colon object r : s evaluated at X : C as the pullback of X ⟶ X / r X along s (X / r X) ⟶ X / r X. We encode this categorically by constructing Φ : Ψ as a pullback in the category of endofunctors of the canonical projection Φ.π : 𝟭 C ⟶ Φ.quotient along Φ.quotient.whiskerLeft Ψ.ι ≫ Φ.quotient.rightUnitor.hom : Φ.quotient ⋙ Ψ.r ⟶ Φ.quotient.

Main definitions

• Preradical.colon Φ Ψ : Preradical C : The colon preradical Φ : Ψ of Stenström.
• toColon Φ Ψ : Φ ⟶ Φ.colon Ψ : The canonical inclusion of the left preradical into the colon.

Main results

• isIso_toColon_iff : The morphism toColon Φ Ψ is an isomorphism if and only if Ψ kills quotients in the sense that Φ.quotient ⋙ Ψ.r is the zero object.

References

• Bo Stenström, Rings and Modules of Quotients
• Bo Stenström, Rings of Quotients

Tags

category_theory, preradical, colon, pullback, torsion theory

@[reducible, inline]

noncomputable abbrev CategoryTheory.Abelian.Preradical.quotient {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ : Preradical C) : Functor C C

The cokernel of Φ.ι : Φ.r ⟶ 𝟭 C.

Equations

• Φ.quotient = CategoryTheory.Limits.cokernel Φ.ι

noncomputable def CategoryTheory.Abelian.Preradical.π {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ : Preradical C) : Functor.id C ⟶ Φ.quotient

The canonical projection 𝟭 C ⥤ Φ.quotient where Φ.quotient is the cokernel of Φ.ι : Φ.r ⟶ 𝟭 C.

Equations

• Φ.π = CategoryTheory.Limits.cokernel.π Φ.ι

@[implicit_reducible]

instance CategoryTheory.Abelian.Preradical.instEpiFunctorπ {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ : Preradical C) : Epi Φ.π

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.Abelian.Preradical.ι_π {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ : Preradical C) : CategoryStruct.comp Φ.ι Φ.π = 0

@[simp]

theorem CategoryTheory.Abelian.Preradical.ι_π_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ : Preradical C) {Z : Functor C C} (h : Φ.quotient ⟶ Z) : CategoryStruct.comp Φ.ι (CategoryStruct.comp Φ.π h) = CategoryStruct.comp 0 h

noncomputable def CategoryTheory.Abelian.Preradical.isColimitCokernelCofork {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ : Preradical C) : Limits.IsColimit (Limits.CokernelCofork.ofπ Φ.π ⋯)

The canonical cofork CokernelCofork.ofπ Φ.π Φ.ι_π exhibits Φ.π : 𝟭 C ⟶ Φ.quotient as the cokernel of Φ.ι : Φ.r ⟶ 𝟭 C.

Equations

• Φ.isColimitCokernelCofork = CategoryTheory.Limits.cokernelIsCokernel Φ.ι

noncomputable def CategoryTheory.Abelian.Preradical.shortComplex {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ : Preradical C) : ShortComplex (Functor C C)

The short complex Φ.r ⟶ 𝟭 C ⟶ Φ.quotient in the functor category associated to a preradical Φ.

Equations

• Φ.shortComplex = { X₁ := Φ.r, X₂ := CategoryTheory.Functor.id C, X₃ := Φ.quotient, f := Φ.ι, g := Φ.π, zero := ⋯ }

@[simp]

theorem CategoryTheory.Abelian.Preradical.shortComplex_f {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ : Preradical C) : Φ.shortComplex.f = Φ.ι

@[simp]

theorem CategoryTheory.Abelian.Preradical.shortComplex_g {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ : Preradical C) : Φ.shortComplex.g = Φ.π

@[simp]

theorem CategoryTheory.Abelian.Preradical.shortComplex_X₁ {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ : Preradical C) : Φ.shortComplex.X₁ = Φ.r

@[simp]

theorem CategoryTheory.Abelian.Preradical.shortComplex_X₃ {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ : Preradical C) : Φ.shortComplex.X₃ = Φ.quotient

@[simp]

theorem CategoryTheory.Abelian.Preradical.shortComplex_X₂ {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ : Preradical C) : Φ.shortComplex.X₂ = Functor.id C

instance CategoryTheory.Abelian.Preradical.instMonoFunctorFShortComplex {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ : Preradical C) : Mono Φ.shortComplex.f

instance CategoryTheory.Abelian.Preradical.instEpiFunctorGShortComplex {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ : Preradical C) : Epi Φ.shortComplex.g

theorem CategoryTheory.Abelian.Preradical.shortExact_shortComplex {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ : Preradical C) : Φ.shortComplex.ShortExact

noncomputable def CategoryTheory.Abelian.Preradical.isLimitKernelFork {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ : Preradical C) : Limits.IsLimit (Limits.KernelFork.ofι Φ.ι ⋯)

The kernel fork KernelFork.ofι Φ.ι Φ.ι_π exhibits Φ.ι : Φ.r ⟶ 𝟭 C as the kernel of the canonical projection Φ.π : 𝟭 C ⟶ Φ.quotient.

Equations

• Φ.isLimitKernelFork = ⋯.fIsKernel

@[simp]

theorem CategoryTheory.Abelian.Preradical.ι_π_app {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ : Preradical C) (X : C) : CategoryStruct.comp (Φ.ι.app X) (Φ.π.app X) = 0

@[simp]

theorem CategoryTheory.Abelian.Preradical.ι_π_app_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ : Preradical C) (X : C) {Z : C} (h : Φ.quotient.obj X ⟶ Z) : CategoryStruct.comp (Φ.ι.app X) (CategoryStruct.comp (Φ.π.app X) h) = CategoryStruct.comp 0 h

noncomputable def CategoryTheory.Abelian.Preradical.shortComplexObj {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ : Preradical C) (X : C) : ShortComplex C

For X : C, the short complex Φ.r.obj X ⟶ X ⟶ Φ.quotient.obj X obtained by evaluating Φ.shortComplex at X.

Equations

• Φ.shortComplexObj X = { X₁ := Φ.r.obj X, X₂ := (CategoryTheory.Functor.id C).obj X, X₃ := Φ.quotient.obj X, f := Φ.ι.app X, g := Φ.π.app X, zero := ⋯ }

@[simp]

theorem CategoryTheory.Abelian.Preradical.shortComplexObj_g {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ : Preradical C) (X : C) : (Φ.shortComplexObj X).g = Φ.π.app X

@[simp]

theorem CategoryTheory.Abelian.Preradical.shortComplexObj_X₃ {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ : Preradical C) (X : C) : (Φ.shortComplexObj X).X₃ = Φ.quotient.obj X

@[simp]

theorem CategoryTheory.Abelian.Preradical.shortComplexObj_f {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ : Preradical C) (X : C) : (Φ.shortComplexObj X).f = Φ.ι.app X

@[simp]

theorem CategoryTheory.Abelian.Preradical.shortComplexObj_X₁ {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ : Preradical C) (X : C) : (Φ.shortComplexObj X).X₁ = Φ.r.obj X

@[simp]

theorem CategoryTheory.Abelian.Preradical.shortComplexObj_X₂ {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ : Preradical C) (X : C) : (Φ.shortComplexObj X).X₂ = (Functor.id C).obj X

instance CategoryTheory.Abelian.Preradical.instMonoFShortComplexObj {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ : Preradical C) (X : C) : Mono (Φ.shortComplexObj X).f

instance CategoryTheory.Abelian.Preradical.instEpiGShortComplexObj {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ : Preradical C) (X : C) : Epi (Φ.shortComplexObj X).g

theorem CategoryTheory.Abelian.Preradical.shortExact_shortComplexObj {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ : Preradical C) (X : C) : (Φ.shortComplexObj X).ShortExact

noncomputable def CategoryTheory.Abelian.Preradical.isLimitKernelForkObj {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ : Preradical C) (X : C) : Limits.IsLimit (Limits.KernelFork.ofι (Φ.ι.app X) ⋯)

For X : C, the kernel fork KernelFork.ofι (Φ.ι.app X) (Φ.ι_π_app X) exhibits Φ.ι.app X : Φ.r.obj X ⟶ X as the kernel of the projection Φ.π.app X : X ⟶ Φ.quotient.obj X.

Equations

• Φ.isLimitKernelForkObj X = ⋯.fIsKernel

noncomputable def CategoryTheory.Abelian.Preradical.isColimitCokernelCoforkObj {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ : Preradical C) (X : C) : Limits.IsColimit (Limits.CokernelCofork.ofπ (Φ.π.app X) ⋯)

For X : C, the cokernel cofork CokernelCofork.ofπ (Φ.π.app X) (Φ.ι_π_app X) exhibits Φ.π.app X : X ⟶ Φ.quotient.obj X as the cokernel of Φ.ι.app X : Φ.r.obj X ⟶ X.

Equations

• Φ.isColimitCokernelCoforkObj X = ⋯.gIsCokernel

noncomputable def CategoryTheory.Abelian.Preradical.colon {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ Ψ : Preradical C) : Preradical C

The colon preradical from Stenström, defined as the pullback of Φ.π : 𝟭 C ⟶ Φ.quotient along Φ.quotient.whiskerLeft Ψ.ι ≫ Φ.quotient.rightUnitor.hom : Φ.quotient ⋙ Ψ.r ⟶ Φ.quotient

Equations

• Φ.colon Ψ = CategoryTheory.MonoOver.mk (CategoryTheory.Limits.pullback.fst Φ.π (CategoryTheory.CategoryStruct.comp (Φ.quotient.whiskerLeft Ψ.ι) Φ.quotient.rightUnitor.hom))

noncomputable def CategoryTheory.Abelian.Preradical.colonπ {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ Ψ : Preradical C) : (Φ.colon Ψ).r ⟶ Φ.quotient.comp Ψ.r

The second projection of the pullback defining the colon preradical.

Equations

• Φ.colonπ Ψ = CategoryTheory.Limits.pullback.snd Φ.π (CategoryTheory.CategoryStruct.comp (Φ.quotient.whiskerLeft Ψ.ι) Φ.quotient.rightUnitor.hom)

instance CategoryTheory.Abelian.Preradical.instEpiFunctorColonπ {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ Ψ : Preradical C) : Epi (Φ.colonπ Ψ)

instance CategoryTheory.Abelian.Preradical.instEpiAppColonπ {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ Ψ : Preradical C) (X : C) : Epi ((Φ.colonπ Ψ).app X)

theorem CategoryTheory.Abelian.Preradical.isPullback_colon {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ Ψ : Preradical C) : IsPullback (Φ.colon Ψ).ι (Φ.colonπ Ψ) Φ.π (CategoryStruct.comp (Φ.quotient.whiskerLeft Ψ.ι) Φ.quotient.rightUnitor.hom)

theorem CategoryTheory.Abelian.Preradical.isPullback_colon_obj {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ Ψ : Preradical C) (X : C) : IsPullback ((Φ.colon Ψ).ι.app X) ((Φ.colonπ Ψ).app X) (Φ.π.app X) (Ψ.ι.app (Φ.quotient.obj X))

theorem CategoryTheory.Abelian.Preradical.colon_ι_app_π_app {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ Ψ : Preradical C) (X : C) : CategoryStruct.comp ((Φ.colon Ψ).ι.app X) (Φ.π.app X) = CategoryStruct.comp ((Φ.colonπ Ψ).app X) (Ψ.ι.app (Φ.quotient.obj X))

theorem CategoryTheory.Abelian.Preradical.colon_ι_app_π_app_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ Ψ : Preradical C) (X : C) {Z : C} (h : Φ.quotient.obj X ⟶ Z) : CategoryStruct.comp ((Φ.colon Ψ).ι.app X) (CategoryStruct.comp (Φ.π.app X) h) = CategoryStruct.comp ((Φ.colonπ Ψ).app X) (CategoryStruct.comp (Ψ.ι.app (Φ.quotient.obj X)) h)

noncomputable def CategoryTheory.Abelian.Preradical.toColon {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ Ψ : Preradical C) : Φ ⟶ Φ.colon Ψ

There is a morphism Φ ⟶ (Φ.colon Ψ) induced by the universal property for the pullback via Φ.ι : Φ.r X ⟶ 𝟭 C and the zero morphism Φ.r ⟶ Φ.quotient ⋙ Ψ.r.

Equations

• Φ.toColon Ψ = CategoryTheory.MonoOver.homMk (⋯.lift Φ.ι 0 ⋯) ⋯

@[simp]

theorem CategoryTheory.Abelian.Preradical.toColon_hom_left_colonπ {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ Ψ : Preradical C) : CategoryStruct.comp (Φ.toColon Ψ).hom.left (Φ.colonπ Ψ) = 0

@[simp]

theorem CategoryTheory.Abelian.Preradical.toColon_hom_left_colonπ_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ Ψ : Preradical C) {Z : Functor C C} (h : Φ.quotient.comp Ψ.r ⟶ Z) : CategoryStruct.comp (Φ.toColon Ψ).hom.left (CategoryStruct.comp (Φ.colonπ Ψ) h) = CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.Abelian.Preradical.toColon_hom_left_app_colonπ_app {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ Ψ : Preradical C) (X : C) : CategoryStruct.comp ((Φ.toColon Ψ).hom.left.app X) ((Φ.colonπ Ψ).app X) = 0

@[simp]

theorem CategoryTheory.Abelian.Preradical.toColon_hom_left_app_colonπ_app_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ Ψ : Preradical C) (X : C) {Z : C} (h : Ψ.r.obj (Φ.quotient.obj X) ⟶ Z) : CategoryStruct.comp ((Φ.toColon Ψ).hom.left.app X) (CategoryStruct.comp ((Φ.colonπ Ψ).app X) h) = CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.Abelian.Preradical.toColon_hom_left_app_colon_ι_app {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ Ψ : Preradical C) (X : C) : CategoryStruct.comp ((Φ.toColon Ψ).hom.left.app X) ((Φ.colon Ψ).ι.app X) = Φ.ι.app X

@[simp]

theorem CategoryTheory.Abelian.Preradical.toColon_hom_left_app_colon_ι_app_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] (Φ Ψ : Preradical C) (X : C) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp ((Φ.toColon Ψ).hom.left.app X) (CategoryStruct.comp ((Φ.colon Ψ).ι.app X) h) = CategoryStruct.comp (Φ.ι.app X) h

theorem CategoryTheory.Abelian.Preradical.isIso_toColon_hom_left_app_iff {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] {Φ Ψ : Preradical C} {X : C} : IsIso ((Φ.toColon Ψ).hom.left.app X) ↔ Limits.IsZero (Ψ.r.obj (Φ.quotient.obj X))

For X : C, the morphism (toColon Φ Ψ) is an isomorphism if and only if (Ψ.r.obj (Φ.quotient.obj X)) is the zero object.

theorem CategoryTheory.Abelian.Preradical.isIso_toColon_iff {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] {Φ Ψ : Preradical C} : IsIso (Φ.toColon Ψ) ↔ Limits.IsZero (Φ.quotient.comp Ψ.r)

The morphism (toColon Φ Ψ) is an isomorphism if and only if Φ.quotient ⋙ Ψ.r is the zero object.