Simple quotients of commutative algebras in the ind-completion

Every nonzero commutative algebra object of Ind C has a quotient algebra which is simple as an algebra: its only ideals are ⊥ and ⊤.

Well-poweredness of the ind-completion

instance RS.wellPoweredInd {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] : CategoryTheory.WellPowered.{v, v, v + 1} (CategoryTheory.Ind C)

The ind-completion is well powered. The embedded objects form a separating family, hence a detecting one, and a category with a small detecting family is well powered.

Factoring through a subobject

theorem RS.factors_of_comm {C : Type v} [CategoryTheory.SmallCategory C] {X Y : CategoryTheory.Ind C} {P : CategoryTheory.Subobject Y} {f : X ⟶ Y} (g : X ⟶ CategoryTheory.Subobject.underlying.obj P) (h : CategoryTheory.CategoryStruct.comp g P.arrow = f) : P.Factors f

A commuting triangle exhibits a factorisation through a subobject.

theorem RS.exists_factor {C : Type v} [CategoryTheory.SmallCategory C] {X Y : CategoryTheory.Ind C} {P : CategoryTheory.Subobject Y} {f : X ⟶ Y} (h : P.Factors f) : ∃ (g : X ⟶ CategoryTheory.Subobject.underlying.obj P), CategoryTheory.CategoryStruct.comp g P.arrow = f

The factorisation named by Subobject.Factors, read back as an explicit commuting triangle.

theorem RS.factors_iff_comp_cokernel {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] {X Y : CategoryTheory.Ind C} (P : CategoryTheory.Subobject Y) (f : X ⟶ Y) : P.Factors f ↔ CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.cokernel.π P.arrow) = 0

Factoring through a subobject is being killed by its cokernel. A monomorphism of an abelian category is the kernel of its own cokernel, so a morphism factors through a subobject exactly when it dies against the cokernel of the subobject's arrow.

theorem RS.factors_of_isColimit {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J (CategoryTheory.Ind C)} (c : CategoryTheory.Limits.Cocone F) (hc : CategoryTheory.Limits.IsColimit c) {W : CategoryTheory.Ind C} (P : CategoryTheory.Subobject W) (f : c.pt ⟶ W) (h : ∀ (j : J), P.Factors (CategoryTheory.CategoryStruct.comp (c.ι.app j) f)) : P.Factors f

Factoring is detected on a colimit cocone: a morphism out of a colimit factors through a subobject as soon as each of its restrictions to the stages does.

Ideals

def RS.IsIdeal {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] (I : CategoryTheory.Subobject 𝔸) : Prop

An ideal of an algebra object: a subobject that absorbs multiplication by the algebra.

Equations

• RS.IsIdeal 𝔸 I = I.Factors (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft 𝔸 I.arrow) CategoryTheory.MonObj.mul)

theorem RS.isIdeal_bot {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] : IsIdeal 𝔸 ⊥

The zero subobject is an ideal.

Proper ideals

def RS.IsProper {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] (I : CategoryTheory.Subobject 𝔸) : Prop

A proper subobject: one through which the unit of the algebra does not factor.

Equations

• RS.IsProper 𝔸 I = ¬I.Factors CategoryTheory.MonObj.one

theorem RS.isProper_iff_ne_top {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] {I : CategoryTheory.Subobject 𝔸} (hI : IsIdeal 𝔸 I) : IsProper 𝔸 I ↔ I ≠ ⊤

For an ideal, properness is exactly being different from the whole algebra. If the unit factors through an ideal then the arrow of the ideal is a split epimorphism, hence an isomorphism.

theorem RS.isProper_bot {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] (hne : CategoryTheory.MonObj.one ≠ 0) : IsProper 𝔸 ⊥

The zero ideal is proper as soon as the unit is nonzero.

Suprema of ideals

@[instance_reducible]

noncomputable instance RS.completeSemilatticeSupSubobject {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] (A : CategoryTheory.Ind C) : CompleteSemilatticeSup (CategoryTheory.Subobject A)

Arbitrary suprema of subobjects of an ind-object, from well-poweredness, images and coproducts.

Equations

• RS.completeSemilatticeSupSubobject A = CategoryTheory.Subobject.completeSemilatticeSup

Compactness of the unit

theorem RS.IndCompactObj.of_iso {C : Type v} [CategoryTheory.SmallCategory C] {X Y : CategoryTheory.Ind C} (e : X ≅ Y) (h : IndCompactObj X) : IndCompactObj Y

Compactness transports along an isomorphism.

theorem RS.indCompactObj_tensorUnit {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] : IndCompactObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C))

The unit object of the ind-completion is compact: it is the embedded unit of the small category.

The union of a directed family of subobjects

instance RS.small_subobject_subset {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] {A : CategoryTheory.Ind C} (s : Set (CategoryTheory.Subobject A)) : Small.{v, v + 1} ↑s

A family of subobjects of an ind-object is v-small.

def RS.SubIndex {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] {A : CategoryTheory.Ind C} (s : Set (CategoryTheory.Subobject A)) : Type v

A v-small copy of a family of subobjects of an ind-object, serving as the index of the diagram of its members.

Equations

• RS.SubIndex s = Shrink.{?u.1, ?u.1 + 1} ↑s

noncomputable def RS.SubIndex.val {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] {A : CategoryTheory.Ind C} {s : Set (CategoryTheory.Subobject A)} (j : SubIndex s) : CategoryTheory.Subobject A

The subobject named by an index.

Equations

• j.val = ↑((equivShrink ↑s).symm j)

theorem RS.SubIndex.val_mem {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] {A : CategoryTheory.Ind C} {s : Set (CategoryTheory.Subobject A)} (j : SubIndex s) : j.val ∈ s

The subobject named by an index belongs to the family.

theorem RS.SubIndex.val_index {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] {A : CategoryTheory.Ind C} {s : Set (CategoryTheory.Subobject A)} {I : CategoryTheory.Subobject A} (hI : I ∈ s) : val ((equivShrink ↑s) ⟨I, hI⟩) = I

Every member of the family is named by an index.

@[instance_reducible]

noncomputable instance RS.subIndexPreorder {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] {A : CategoryTheory.Ind C} (s : Set (CategoryTheory.Subobject A)) : Preorder (SubIndex s)

The index of a family of subobjects, ordered by inclusion of the subobjects it names.

Equations

• RS.subIndexPreorder s = Preorder.lift RS.SubIndex.val

theorem RS.SubIndex.le_of_hom {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] {A : CategoryTheory.Ind C} {s : Set (CategoryTheory.Subobject A)} {j k : SubIndex s} (h : j ⟶ k) : j.val ≤ k.val

A morphism of the index category is an inclusion of the subobjects it names.

theorem RS.isFiltered_subIndex {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] {A : CategoryTheory.Ind C} {s : Set (CategoryTheory.Subobject A)} (hne : s.Nonempty) (hdir : DirectedOn (fun (x1 x2 : CategoryTheory.Subobject A) => x1 ≤ x2) s) : CategoryTheory.IsFiltered (SubIndex s)

The index of a nonempty directed family is filtered.

noncomputable def RS.subDiagram {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] {A : CategoryTheory.Ind C} (s : Set (CategoryTheory.Subobject A)) : CategoryTheory.Functor (SubIndex s) (CategoryTheory.Ind C)

The diagram of the members of a family of subobjects.

Equations

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

noncomputable def RS.subCocone {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] {A : CategoryTheory.Ind C} (s : Set (CategoryTheory.Subobject A)) : CategoryTheory.Limits.Cocone (subDiagram s)

The tautological cocone of RS.subDiagram on the ambient ind-object, given by the arrows of the members.

Equations

• RS.subCocone s = { pt := A, ι := { app := fun (j : RS.SubIndex s) => j.val.arrow, naturality := ⋯ } }

noncomputable def RS.subUnionHom {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] {A : CategoryTheory.Ind C} (s : Set (CategoryTheory.Subobject A)) : CategoryTheory.Limits.colimit (subDiagram s) ⟶ A

The comparison morphism from the colimit of a family of subobjects to the ambient ind-object.

Equations

• RS.subUnionHom s = CategoryTheory.Limits.colimit.desc (RS.subDiagram s) (RS.subCocone s)

theorem RS.ι_subUnionHom {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] {A : CategoryTheory.Ind C} (s : Set (CategoryTheory.Subobject A)) (j : SubIndex s) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (subDiagram s) j) (subUnionHom s) = j.val.arrow

The colimit injections composed with the comparison morphism are the arrows of the members.

noncomputable def RS.constColimitIso {C : Type v} [CategoryTheory.SmallCategory C] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (A : CategoryTheory.Ind C) : CategoryTheory.Limits.colimit ((CategoryTheory.Functor.const J).obj A) ≅ A

The colimit of a constant diagram over a filtered index is the constant value.

Equations

• RS.constColimitIso A = (CategoryTheory.Limits.colimit.isColimit ((CategoryTheory.Functor.const J).obj A)).coconePointUniqueUpToIso (CategoryTheory.Limits.isColimitConstCocone J A)

theorem RS.ι_constColimitIso {C : Type v} [CategoryTheory.SmallCategory C] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (A : CategoryTheory.Ind C) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.const J).obj A) j) (constColimitIso A).hom = CategoryTheory.CategoryStruct.id A

Each injection of the constant colimit is undone by RS.constColimitIso.

instance RS.mono_subUnionHom {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] {A : CategoryTheory.Ind C} (s : Set (CategoryTheory.Subobject A)) [CategoryTheory.IsFiltered (SubIndex s)] : CategoryTheory.Mono (subUnionHom s)

The union of a filtered family of subobjects is a subobject: filtered colimits are exact in the ind-completion, so the comparison morphism of RS.subUnionHom is a monomorphism.

The chain condition

theorem RS.exists_ub_of_directed {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] {c : Set (CategoryTheory.Subobject 𝔸)} (hne : c.Nonempty) (hdir : DirectedOn (fun (x1 x2 : CategoryTheory.Subobject 𝔸) => x1 ≤ x2) c) (hid : ∀ I ∈ c, IsIdeal 𝔸 I) (hpr : ∀ I ∈ c, IsProper 𝔸 I) : ∃ (ub : CategoryTheory.Subobject 𝔸), IsIdeal 𝔸 ub ∧ IsProper 𝔸 ub ∧ ∀ I ∈ c, I ≤ ub

A nonempty directed family of proper ideals is bounded above by a proper ideal. The bound is the union of the family: it is an ideal because tensoring preserves the colimit of the members, and it is proper because the unit is compact, so a factorisation of the unit through the union already factors through a member.

Maximal proper ideals

theorem RS.exists_maximal_ideal {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] (hne : CategoryTheory.MonObj.one ≠ 0) : ∃ (𝔪 : CategoryTheory.Subobject 𝔸), IsIdeal 𝔸 𝔪 ∧ IsProper 𝔸 𝔪 ∧ ∀ (J : CategoryTheory.Subobject 𝔸), IsIdeal 𝔸 J → IsProper 𝔸 J → 𝔪 ≤ J → J ≤ 𝔪

Every algebra with a nonzero unit has a maximal proper ideal.

Transport of an algebra structure along an epimorphism

@[reducible]

noncomputable def RS.monObjOfEpi {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] {A B : CategoryTheory.Ind C} [CategoryTheory.MonObj A] (p : A ⟶ B) [CategoryTheory.Epi p] (o : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C) ⟶ B) (m : CategoryTheory.MonoidalCategoryStruct.tensorObj B B ⟶ B) (ho : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one p = o) (hm : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom p p) m = CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul p) : CategoryTheory.MonObj B

An epimorphism transports an algebra structure. If a unit and a multiplication on the target are compatible with those of the source along an epimorphism, they satisfy the algebra laws.

Equations

• RS.monObjOfEpi p o m ho hm = { one := o, mul := m, one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }

theorem RS.isCommMonObj_of_epi {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] {A B : CategoryTheory.Ind C} [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] [CategoryTheory.MonObj B] (p : A ⟶ B) [CategoryTheory.Epi p] (hm : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom p p) CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul p) : CategoryTheory.IsCommMonObj B

An epimorphism transports commutativity.

The quotient of an algebra by an ideal

theorem RS.whiskerLeft_arrow_mul_π {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] (𝔪 : CategoryTheory.Subobject 𝔸) (h𝔪 : IsIdeal 𝔸 𝔪) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft 𝔸 𝔪.arrow) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (CategoryTheory.Limits.cokernel.π 𝔪.arrow)) = 0

The multiplication of the algebra against an ideal dies in the quotient by that ideal.

theorem RS.whiskerRight_arrow_mul_π {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] [CategoryTheory.IsCommMonObj 𝔸] (𝔪 : CategoryTheory.Subobject 𝔸) (h𝔪 : IsIdeal 𝔸 𝔪) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight 𝔪.arrow 𝔸) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (CategoryTheory.Limits.cokernel.π 𝔪.arrow)) = 0

The same on the other side, by commutativity.

noncomputable def RS.quotMulAux {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] (𝔪 : CategoryTheory.Subobject 𝔸) (h𝔪 : IsIdeal 𝔸 𝔪) : CategoryTheory.MonoidalCategoryStruct.tensorObj 𝔸 (CategoryTheory.Limits.cokernel 𝔪.arrow) ⟶ CategoryTheory.Limits.cokernel 𝔪.arrow

The multiplication of the algebra, descended in its second variable to the quotient by an ideal.

Equations

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

theorem RS.whiskerLeft_π_quotMulAux {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] (𝔪 : CategoryTheory.Subobject 𝔸) (h𝔪 : IsIdeal 𝔸 𝔪) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft 𝔸 (CategoryTheory.Limits.cokernel.π 𝔪.arrow)) (quotMulAux 𝔸 𝔪 h𝔪) = CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (CategoryTheory.Limits.cokernel.π 𝔪.arrow)

The defining property of RS.quotMulAux.

theorem RS.whiskerRight_quotMulAux {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] [CategoryTheory.IsCommMonObj 𝔸] (𝔪 : CategoryTheory.Subobject 𝔸) (h𝔪 : IsIdeal 𝔸 𝔪) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight 𝔪.arrow (CategoryTheory.Limits.cokernel 𝔪.arrow)) (quotMulAux 𝔸 𝔪 h𝔪) = 0

The half-descended multiplication kills the ideal in its first variable as well.

noncomputable def RS.quotMul {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] [CategoryTheory.IsCommMonObj 𝔸] (𝔪 : CategoryTheory.Subobject 𝔸) (h𝔪 : IsIdeal 𝔸 𝔪) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.Limits.cokernel 𝔪.arrow) (CategoryTheory.Limits.cokernel 𝔪.arrow) ⟶ CategoryTheory.Limits.cokernel 𝔪.arrow

The multiplication of the quotient algebra.

Equations

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

theorem RS.whiskerRight_π_quotMul {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] [CategoryTheory.IsCommMonObj 𝔸] (𝔪 : CategoryTheory.Subobject 𝔸) (h𝔪 : IsIdeal 𝔸 𝔪) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.cokernel.π 𝔪.arrow) (CategoryTheory.Limits.cokernel 𝔪.arrow)) (quotMul 𝔸 𝔪 h𝔪) = quotMulAux 𝔸 𝔪 h𝔪

The defining property of RS.quotMul.

theorem RS.tensorHom_π_quotMul {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] [CategoryTheory.IsCommMonObj 𝔸] (𝔪 : CategoryTheory.Subobject 𝔸) (h𝔪 : IsIdeal 𝔸 𝔪) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.Limits.cokernel.π 𝔪.arrow) (CategoryTheory.Limits.cokernel.π 𝔪.arrow)) (quotMul 𝔸 𝔪 h𝔪) = CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (CategoryTheory.Limits.cokernel.π 𝔪.arrow)

The projection is multiplicative.

@[reducible]

noncomputable def RS.quotMonObj {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] [CategoryTheory.IsCommMonObj 𝔸] (𝔪 : CategoryTheory.Subobject 𝔸) (h𝔪 : IsIdeal 𝔸 𝔪) : CategoryTheory.MonObj (CategoryTheory.Limits.cokernel 𝔪.arrow)

The quotient of an algebra by an ideal is an algebra.

Equations

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

Pulling ideals back along the projection

theorem RS.factors_pullback_iff {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] {A B W : CategoryTheory.Ind C} (I : CategoryTheory.Subobject B) (p : A ⟶ B) (h : W ⟶ A) : (CategoryTheory.Subobject.mk (CategoryTheory.Limits.pullback.snd I.arrow p)).Factors h ↔ I.Factors (CategoryTheory.CategoryStruct.comp h p)

Pulling a subobject back: a morphism factors through the pullback of a subobject exactly when its composite factors through the subobject.

The simple quotient

theorem RS.exists_simple_quotient {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] (𝔸 : CategoryTheory.Ind C) [CategoryTheory.MonObj 𝔸] [CategoryTheory.IsCommMonObj 𝔸] (hne : CategoryTheory.MonObj.one ≠ 0) : ∃ (𝔹 : CategoryTheory.Ind C) (x : CategoryTheory.MonObj 𝔹) (_ : CategoryTheory.IsCommMonObj 𝔹) (π : 𝔸 ⟶ 𝔹), CategoryTheory.MonObj.one ≠ 0 ∧ CategoryTheory.Epi π ∧ CategoryTheory.IsMonHom π ∧ ∀ (I : CategoryTheory.Subobject 𝔹), IsIdeal 𝔹 I → I = ⊥ ∨ I = ⊤

Every commutative algebra object of the ind-completion with a nonzero unit has a simple quotient: a quotient algebra whose only ideals are the zero subobject and the whole object. The quotient is by a maximal proper ideal, and ideals of the quotient correspond to ideals of the algebra containing that maximal ideal.