The lattice of subobjects #

We provide the SemilatticeInf with OrderTop (Subobject X) instance when [HasPullback C], and the SemilatticeSup (Subobject X) instance when [HasImages C] [HasBinaryCoproducts C].

source

instance CategoryTheory.MonoOver.instTop {C : Type u₁} [Category.{v₁, u₁} C] {X : C} :

Top (MonoOver X)

Equations

CategoryTheory.MonoOver.instTop = { top := CategoryTheory.MonoOver.mk' (CategoryTheory.CategoryStruct.id X) }

source

instance CategoryTheory.MonoOver.instInhabited {C : Type u₁} [Category.{v₁, u₁} C] {X : C} :

Inhabited (MonoOver X)

Equations

CategoryTheory.MonoOver.instInhabited = { default := ⊤ }

source

def CategoryTheory.MonoOver.leTop {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (f : MonoOver X) :

f ⟶ ⊤

The morphism to the top object in MonoOver X.

Equations

f.leTop = CategoryTheory.MonoOver.homMk f.arrow ⋯

source

@[simp]

theorem CategoryTheory.MonoOver.top_left {C : Type u₁} [Category.{v₁, u₁} C] (X : C) :

⊤.obj.left = X

source

@[simp]

theorem CategoryTheory.MonoOver.top_arrow {C : Type u₁} [Category.{v₁, u₁} C] (X : C) :

⊤.arrow = CategoryStruct.id X

source

def CategoryTheory.MonoOver.mapTop {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [Mono f] :

(map f).obj ⊤ ≅ mk' f

map f sends ⊤ : MonoOver X to ⟨X, f⟩ : MonoOver Y.

Equations

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

source

def CategoryTheory.MonoOver.pullbackTop {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Limits.HasPullbacks C] (f : X ⟶ Y) :

(pullback f).obj ⊤ ≅ ⊤

The pullback of the top object in MonoOver Y is (isomorphic to) the top object in MonoOver X.

Equations

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

source

def CategoryTheory.MonoOver.topLEPullbackSelf {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A B : C} (f : A ⟶ B) [Mono f] :

⊤ ⟶ (pullback f).obj (mk' f)

There is a morphism from ⊤ : MonoOver A to the pullback of a monomorphism along itself; as the category is thin this is an isomorphism.

Equations

CategoryTheory.MonoOver.topLEPullbackSelf f = CategoryTheory.MonoOver.homMk (CategoryTheory.Limits.pullback.lift ⊤.arrow ⊤.arrow ⋯) ⋯

source

def CategoryTheory.MonoOver.pullbackSelf {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A B : C} (f : A ⟶ B) [Mono f] :

(pullback f).obj (mk' f) ≅ ⊤

The pullback of a monomorphism along itself is isomorphic to the top object.

Equations

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

source

instance CategoryTheory.MonoOver.instBot {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasInitial C] [Limits.InitialMonoClass C] {X : C} :

Bot (MonoOver X)

Equations

CategoryTheory.MonoOver.instBot = { bot := CategoryTheory.MonoOver.mk' (CategoryTheory.Limits.initial.to X) }

source

@[simp]

theorem CategoryTheory.MonoOver.bot_left {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasInitial C] [Limits.InitialMonoClass C] (X : C) :

⊥.obj.left = ⊥_ C

source

@[simp]

theorem CategoryTheory.MonoOver.bot_arrow {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasInitial C] [Limits.InitialMonoClass C] {X : C} :

⊥.arrow = Limits.initial.to X

source

def CategoryTheory.MonoOver.botLE {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasInitial C] [Limits.InitialMonoClass C] {X : C} (f : MonoOver X) :

⊥ ⟶ f

The (unique) morphism from ⊥ : MonoOver X to any other f : MonoOver X.

Equations

f.botLE = CategoryTheory.MonoOver.homMk (CategoryTheory.Limits.initial.to f.obj.left) ⋯

source

def CategoryTheory.MonoOver.mapBot {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Limits.HasInitial C] [Limits.InitialMonoClass C] (f : X ⟶ Y) [Mono f] :

(map f).obj ⊥ ≅ ⊥

map f sends ⊥ : MonoOver X to ⊥ : MonoOver Y.

Equations

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

source

def CategoryTheory.MonoOver.botCoeIsoZero {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] {B : C} :

⊥.obj.left ≅ 0

The object underlying ⊥ : Subobject B is (up to isomorphism) the zero object.

Equations

CategoryTheory.MonoOver.botCoeIsoZero = CategoryTheory.Limits.initialIsInitial.uniqueUpToIso CategoryTheory.Limits.HasZeroObject.zeroIsInitial

source

theorem CategoryTheory.MonoOver.bot_arrow_eq_zero {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {B : C} :

⊥.arrow = 0

source

def CategoryTheory.MonoOver.inf {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} :

Functor (MonoOver A) (Functor (MonoOver A) (MonoOver A))

When [HasPullbacks C], MonoOver A has "intersections", functorial in both arguments.

As MonoOver A is only a preorder, this doesn't satisfy the axioms of SemilatticeInf, but we reuse all the names from SemilatticeInf because they will be used to construct SemilatticeInf (subobject A) shortly.

Equations

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

source

@[simp]

theorem CategoryTheory.MonoOver.inf_obj {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} (f : MonoOver A) :

inf.obj f = (pullback f.arrow).comp (map f.arrow)

source

@[simp]

theorem CategoryTheory.MonoOver.inf_map_app {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} {X✝ Y✝ : MonoOver A} (k : X✝ ⟶ Y✝) (g : MonoOver A) :

(inf.map k).app g = homMk (Limits.pullback.lift (Limits.pullback.fst ((forget A).obj g).hom X✝.arrow) (CategoryStruct.comp (Limits.pullback.snd ((forget A).obj g).hom X✝.arrow) k.left) ⋯) ⋯

source

def CategoryTheory.MonoOver.infLELeft {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} (f g : MonoOver A) :

(inf.obj f).obj g ⟶ f

A morphism from the "infimum" of two objects in MonoOver A to the first object.

Equations

f.infLELeft g = CategoryTheory.MonoOver.homMk ((CategoryTheory.MonoOver.forget f.obj.left).obj ((CategoryTheory.MonoOver.pullback f.arrow).obj g)).hom ⋯

source

def CategoryTheory.MonoOver.infLERight {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} (f g : MonoOver A) :

(inf.obj f).obj g ⟶ g

A morphism from the "infimum" of two objects in MonoOver A to the second object.

Equations

f.infLERight g = CategoryTheory.MonoOver.homMk (CategoryTheory.Limits.pullback.fst ((CategoryTheory.MonoOver.forget A).obj g).hom f.arrow) ⋯

source

def CategoryTheory.MonoOver.leInf {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} (f g h : MonoOver A) :

(h ⟶ f) → (h ⟶ g) → (h ⟶ (inf.obj f).obj g)

A morphism version of the le_inf axiom.

Equations

f.leInf g h k₁ k₂ = CategoryTheory.MonoOver.homMk (CategoryTheory.Limits.pullback.lift k₂.left k₁.left ⋯) ⋯

source

def CategoryTheory.MonoOver.sup {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasImages C] [Limits.HasBinaryCoproducts C] {A : C} :

Functor (MonoOver A) (Functor (MonoOver A) (MonoOver A))

When [HasImages C] [HasBinaryCoproducts C], MonoOver A has a sup construction, which is functorial in both arguments, and which on Subobject A will induce a SemilatticeSup.

Equations

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

source

def CategoryTheory.MonoOver.leSupLeft {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasImages C] [Limits.HasBinaryCoproducts C] {A : C} (f g : MonoOver A) :

f ⟶ (sup.obj f).obj g

A morphism version of le_sup_left.

Equations

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

source

def CategoryTheory.MonoOver.leSupRight {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasImages C] [Limits.HasBinaryCoproducts C] {A : C} (f g : MonoOver A) :

g ⟶ (sup.obj f).obj g

A morphism version of le_sup_right.

Equations

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

source

def CategoryTheory.MonoOver.supLe {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasImages C] [Limits.HasBinaryCoproducts C] {A : C} (f g h : MonoOver A) :

(f ⟶ h) → (g ⟶ h) → ((sup.obj f).obj g ⟶ h)

A morphism version of sup_le.

Equations

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

source

instance CategoryTheory.Subobject.orderTop {C : Type u₁} [Category.{v₁, u₁} C] {X : C} :

OrderTop (Subobject X)

Equations

CategoryTheory.Subobject.orderTop = { top := Quotient.mk'' ⊤, le_top := ⋯ }

source

instance CategoryTheory.Subobject.instInhabited {C : Type u₁} [Category.{v₁, u₁} C] {X : C} :

Inhabited (Subobject X)

Equations

CategoryTheory.Subobject.instInhabited = { default := ⊤ }

source

theorem CategoryTheory.Subobject.top_eq_id {C : Type u₁} [Category.{v₁, u₁} C] (B : C) :

⊤ = mk (CategoryStruct.id B)

source

theorem CategoryTheory.Subobject.underlyingIso_top_hom {C : Type u₁} [Category.{v₁, u₁} C] {B : C} :

(underlyingIso (CategoryStruct.id B)).hom = ⊤.arrow

source

instance CategoryTheory.Subobject.top_arrow_isIso {C : Type u₁} [Category.{v₁, u₁} C] {B : C} :

IsIso ⊤.arrow

source

@[simp]

theorem CategoryTheory.Subobject.underlyingIso_inv_top_arrow {C : Type u₁} [Category.{v₁, u₁} C] {B : C} :

CategoryStruct.comp (underlyingIso (CategoryStruct.id B)).inv ⊤.arrow = CategoryStruct.id B

source

@[simp]

theorem CategoryTheory.Subobject.underlyingIso_inv_top_arrow_assoc {C : Type u₁} [Category.{v₁, u₁} C] {B Z : C} (h : B ⟶ Z) :

CategoryStruct.comp (underlyingIso (CategoryStruct.id B)).inv (CategoryStruct.comp ⊤.arrow h) = h

source

@[simp]

theorem CategoryTheory.Subobject.map_top {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [Mono f] :

(map f).obj ⊤ = mk f

source

theorem CategoryTheory.Subobject.top_factors {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} (f : A ⟶ B) :

⊤.Factors f

source

theorem CategoryTheory.Subobject.isIso_iff_mk_eq_top {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [Mono f] :

IsIso f ↔ mk f = ⊤

source

theorem CategoryTheory.Subobject.isIso_arrow_iff_eq_top {C : Type u₁} [Category.{v₁, u₁} C] {Y : C} (P : Subobject Y) :

IsIso P.arrow ↔ P = ⊤

source

instance CategoryTheory.Subobject.isIso_top_arrow {C : Type u₁} [Category.{v₁, u₁} C] {Y : C} :

IsIso ⊤.arrow

source

theorem CategoryTheory.Subobject.mk_eq_top_of_isIso {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [IsIso f] :

mk f = ⊤

source

theorem CategoryTheory.Subobject.eq_top_of_isIso_arrow {C : Type u₁} [Category.{v₁, u₁} C] {Y : C} (P : Subobject Y) [IsIso P.arrow] :

P = ⊤

source

theorem CategoryTheory.Subobject.epi_iff_mk_eq_top {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Balanced C] (f : X ⟶ Y) [Mono f] :

Epi f ↔ mk f = ⊤

source

theorem CategoryTheory.Subobject.pullback_top {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Limits.HasPullbacks C] (f : X ⟶ Y) :

(pullback f).obj ⊤ = ⊤

source

theorem CategoryTheory.Subobject.pullback_self {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A B : C} (f : A ⟶ B) [Mono f] :

(pullback f).obj (mk f) = ⊤

source

instance CategoryTheory.Subobject.orderBot {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasInitial C] [Limits.InitialMonoClass C] {X : C} :

OrderBot (Subobject X)

Equations

CategoryTheory.Subobject.orderBot = { bot := Quotient.mk'' ⊥, bot_le := ⋯ }

source

theorem CategoryTheory.Subobject.bot_eq_initial_to {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasInitial C] [Limits.InitialMonoClass C] {B : C} :

⊥ = mk (Limits.initial.to B)

source

def CategoryTheory.Subobject.botCoeIsoInitial {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasInitial C] [Limits.InitialMonoClass C] {B : C} :

underlying.obj ⊥ ≅ ⊥_ C

The object underlying ⊥ : Subobject B is (up to isomorphism) the initial object.

Equations

CategoryTheory.Subobject.botCoeIsoInitial = CategoryTheory.Subobject.underlyingIso (CategoryTheory.Limits.initial.to B)

source

theorem CategoryTheory.Subobject.map_bot {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Limits.HasInitial C] [Limits.InitialMonoClass C] (f : X ⟶ Y) [Mono f] :

(map f).obj ⊥ = ⊥

source

def CategoryTheory.Subobject.botCoeIsoZero {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] {B : C} :

underlying.obj ⊥ ≅ 0

The object underlying ⊥ : Subobject B is (up to isomorphism) the zero object.

Equations

CategoryTheory.Subobject.botCoeIsoZero = CategoryTheory.Subobject.botCoeIsoInitial ≪≫ CategoryTheory.Limits.initialIsInitial.uniqueUpToIso CategoryTheory.Limits.HasZeroObject.zeroIsInitial

source

theorem CategoryTheory.Subobject.bot_eq_zero {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {B : C} :

⊥ = mk 0

source

@[simp]

theorem CategoryTheory.Subobject.bot_arrow {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {B : C} :

⊥.arrow = 0

source

theorem CategoryTheory.Subobject.bot_factors_iff_zero {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {A B : C} (f : A ⟶ B) :

⊥.Factors f ↔ f = 0

source

theorem CategoryTheory.Subobject.mk_eq_bot_iff_zero {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] {f : X ⟶ Y} [Mono f] :

mk f = ⊥ ↔ f = 0

source

def CategoryTheory.Subobject.functor (C : Type u₁) [Category.{v₁, u₁} C] [Limits.HasPullbacks C] :

Functor Cᵒᵖ (Type (max u₁ v₁))

Sending X : C to Subobject X is a contravariant functor Cᵒᵖ ⥤ Type.

Equations

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

source

@[simp]

theorem CategoryTheory.Subobject.functor_obj (C : Type u₁) [Category.{v₁, u₁} C] [Limits.HasPullbacks C] (X : Cᵒᵖ) :

(functor C).obj X = Subobject (Opposite.unop X)

source

@[simp]

theorem CategoryTheory.Subobject.functor_map (C : Type u₁) [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) (a✝ : Subobject (Opposite.unop X✝)) :

(functor C).map f a✝ = (pullback f.unop).obj a✝

source

def CategoryTheory.Subobject.inf {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} :

Functor (Subobject A) (Functor (Subobject A) (Subobject A))

The functorial infimum on MonoOver A descends to an infimum on Subobject A.

Equations

CategoryTheory.Subobject.inf = CategoryTheory.ThinSkeleton.map₂ CategoryTheory.MonoOver.inf

source

theorem CategoryTheory.Subobject.inf_le_left {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} (f g : Subobject A) :

(inf.obj f).obj g ≤ f

source

theorem CategoryTheory.Subobject.inf_le_right {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} (f g : Subobject A) :

(inf.obj f).obj g ≤ g

source

theorem CategoryTheory.Subobject.le_inf {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} (h f g : Subobject A) :

h ≤ f → h ≤ g → h ≤ (inf.obj f).obj g

source

instance CategoryTheory.Subobject.semilatticeInf {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {B : C} :

SemilatticeInf (Subobject B)

Equations

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

source

theorem CategoryTheory.Subobject.factors_left_of_inf_factors {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A B : C} {X Y : Subobject B} {f : A ⟶ B} (h : (X ⊓ Y).Factors f) :

X.Factors f

source

theorem CategoryTheory.Subobject.factors_right_of_inf_factors {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A B : C} {X Y : Subobject B} {f : A ⟶ B} (h : (X ⊓ Y).Factors f) :

Y.Factors f

source

@[simp]

theorem CategoryTheory.Subobject.inf_factors {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A B : C} {X Y : Subobject B} (f : A ⟶ B) :

(X ⊓ Y).Factors f ↔ X.Factors f ∧ Y.Factors f

source

theorem CategoryTheory.Subobject.inf_arrow_factors_left {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {B : C} (X Y : Subobject B) :

X.Factors (X ⊓ Y).arrow

source

theorem CategoryTheory.Subobject.inf_arrow_factors_right {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {B : C} (X Y : Subobject B) :

Y.Factors (X ⊓ Y).arrow

source

@[simp]

theorem CategoryTheory.Subobject.finset_inf_factors {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {I : Type u_1} {A B : C} {s : Finset I} {P : I → Subobject B} (f : A ⟶ B) :

(s.inf P).Factors f ↔ ∀ i ∈ s, (P i).Factors f

source

theorem CategoryTheory.Subobject.finset_inf_arrow_factors {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {I : Type u_1} {B : C} (s : Finset I) (P : I → Subobject B) (i : I) (m : i ∈ s) :

(P i).Factors (s.inf P).arrow

source

theorem CategoryTheory.Subobject.inf_eq_map_pullback' {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} (f₁ : MonoOver A) (f₂ : Subobject A) :

(inf.obj (Quotient.mk'' f₁)).obj f₂ = (map f₁.arrow).obj ((pullback f₁.arrow).obj f₂)

source

theorem CategoryTheory.Subobject.inf_eq_map_pullback {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} (f₁ : MonoOver A) (f₂ : Subobject A) :

Quotient.mk'' f₁ ⊓ f₂ = (map f₁.arrow).obj ((pullback f₁.arrow).obj f₂)

source

theorem CategoryTheory.Subobject.prod_eq_inf {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {A : C} {f₁ f₂ : Subobject A} [Limits.HasBinaryProduct f₁ f₂] :

(f₁ ⨯ f₂) = f₁ ⊓ f₂

source

theorem CategoryTheory.Subobject.inf_def {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {B : C} (m m' : Subobject B) :

m ⊓ m' = (inf.obj m).obj m'

source

theorem CategoryTheory.Subobject.inf_pullback {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {X Y : C} (g : X ⟶ Y) (f₁ f₂ : Subobject Y) :

(pullback g).obj (f₁ ⊓ f₂) = (pullback g).obj f₁ ⊓ (pullback g).obj f₂

⊓ commutes with pullback.

source

theorem CategoryTheory.Subobject.inf_map {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {X Y : C} (g : Y ⟶ X) [Mono g] (f₁ f₂ : Subobject Y) :

(map g).obj (f₁ ⊓ f₂) = (map g).obj f₁ ⊓ (map g).obj f₂

⊓ commutes with map.

source

def CategoryTheory.Subobject.sup {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasImages C] [Limits.HasBinaryCoproducts C] {A : C} :

Functor (Subobject A) (Functor (Subobject A) (Subobject A))

The functorial supremum on MonoOver A descends to a supremum on Subobject A.

Equations

CategoryTheory.Subobject.sup = CategoryTheory.ThinSkeleton.map₂ CategoryTheory.MonoOver.sup

source

instance CategoryTheory.Subobject.semilatticeSup {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasImages C] [Limits.HasBinaryCoproducts C] {B : C} :

SemilatticeSup (Subobject B)

Equations

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

source

theorem CategoryTheory.Subobject.sup_factors_of_factors_left {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasImages C] [Limits.HasBinaryCoproducts C] {A B : C} {X Y : Subobject B} {f : A ⟶ B} (P : X.Factors f) :

(X ⊔ Y).Factors f

source

theorem CategoryTheory.Subobject.sup_factors_of_factors_right {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasImages C] [Limits.HasBinaryCoproducts C] {A B : C} {X Y : Subobject B} {f : A ⟶ B} (P : Y.Factors f) :

(X ⊔ Y).Factors f

source

theorem CategoryTheory.Subobject.finset_sup_factors {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasImages C] [Limits.HasBinaryCoproducts C] [Limits.HasInitial C] [Limits.InitialMonoClass C] {I : Type u_1} {A B : C} {s : Finset I} {P : I → Subobject B} {f : A ⟶ B} (h : ∃ i ∈ s, (P i).Factors f) :

(s.sup P).Factors f

source

instance CategoryTheory.Subobject.boundedOrder {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasInitial C] [Limits.InitialMonoClass C] {B : C} :

BoundedOrder (Subobject B)

Equations

CategoryTheory.Subobject.boundedOrder = { toOrderTop := CategoryTheory.Subobject.orderTop, toOrderBot := CategoryTheory.Subobject.orderBot }

source

instance CategoryTheory.Subobject.instLattice {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] [Limits.HasImages C] [Limits.HasBinaryCoproducts C] {B : C} :

Lattice (Subobject B)

Equations

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

source

def CategoryTheory.Subobject.wideCospan {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] {A : C} (s : Set (Subobject A)) :

Functor (Limits.WidePullbackShape ↑(⇑(equivShrink (Subobject A)) '' s)) C

The "wide cospan" diagram, with a small indexing type, constructed from a set of subobjects. (This is just the diagram of all the subobjects pasted together, but using WellPowered C to make the diagram small.)

Equations