Theorems · Definition · category theory

CategoryTheory.Subobject.sSup

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] →
      [CategoryTheory.WellPowered.{w, v₁, u₁} C] →
        [CategoryTheory.Limits.HasCoproducts C] →
          [CategoryTheory.Limits.HasImages C] → {A : C} → Set (CategoryTheory.Subobject A) → CategoryTheory.Subobject A

When [WellPowered C] [HasImages C] [HasCoproducts C], Subobject A has arbitrary supremums.

Defined in: Mathlib.CategoryTheory.Subobject.Lattice
Cited by: 2 results in Mathlib
Foundations: Depth 41 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category CategoryTheory.LocallySmall CategoryTheory.WellPowered CategoryTheory.Limits.HasCoproducts CategoryTheory.Limits.HasImages

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
CategoryTheory.Categorystatement and proof · cited by 32,673
CategoryTheory.Subobjectstatement and proof · cited by 385
CategoryTheory.LocallySmallstatement and proof · cited by 242
CategoryTheory.Limits.HasCoproductsstatement and proof · cited by 119
CategoryTheory.Subobject.mkproof · cited by 109
CategoryTheory.Limits.image.ιproof · cited by 104
CategoryTheory.Limits.HasImagesstatement and proof · cited by 37
CategoryTheory.WellPoweredstatement and proof · cited by 22
CategoryTheory.Subobject.smallCoproductDescproof · cited by 2

Cited by2

Results whose statement or proof uses this declaration.

CategoryTheory.Subobject.le_sSupstatement · cited by 0
CategoryTheory.Subobject.sSup_lestatement · cited by 0