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].

instance CategoryTheory.MonoOver.instTopMonoOver {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} : Top (CategoryTheory.MonoOver X)

instance CategoryTheory.MonoOver.instInhabitedMonoOver {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} : Inhabited (CategoryTheory.MonoOver X)

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

The morphism to the top object in MonoOver X.

@[simp]

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

@[simp]

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

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

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

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

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

def CategoryTheory.MonoOver.topLEPullbackSelf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {A : C} {B : C} (f : A ⟶ B) [CategoryTheory.Mono f] : ⊤ ⟶ (CategoryTheory.MonoOver.pullback f).obj (CategoryTheory.MonoOver.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.

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

@[simp]

theorem CategoryTheory.MonoOver.inf_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {A : C} (f : CategoryTheory.MonoOver A) : CategoryTheory.MonoOver.inf.obj f = CategoryTheory.Functor.comp (CategoryTheory.MonoOver.pullback (CategoryTheory.MonoOver.arrow f)) (CategoryTheory.MonoOver.map (CategoryTheory.MonoOver.arrow f))

@[simp]

theorem CategoryTheory.MonoOver.inf_map_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {A : C} : ∀ {X Y : CategoryTheory.MonoOver A} (k : X ⟶ Y) (g : CategoryTheory.MonoOver A), (CategoryTheory.MonoOver.inf.map k).app g = CategoryTheory.MonoOver.homMk (CategoryTheory.Limits.pullback.lift CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd k.left) (_ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst ((CategoryTheory.MonoOver.forget A).obj g).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd k.left) (CategoryTheory.MonoOver.arrow Y)))

def CategoryTheory.MonoOver.inf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {A : C} : CategoryTheory.Functor (CategoryTheory.MonoOver A) (CategoryTheory.Functor (CategoryTheory.MonoOver A) (CategoryTheory.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.

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

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

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

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

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

A morphism version of the le_inf axiom.

def CategoryTheory.MonoOver.sup {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A : C} : CategoryTheory.Functor (CategoryTheory.MonoOver A) (CategoryTheory.Functor (CategoryTheory.MonoOver A) (CategoryTheory.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.

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

A morphism version of le_sup_left.

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

A morphism version of le_sup_right.

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

A morphism version of sup_le.

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

instance CategoryTheory.Subobject.instInhabitedSubobject {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} : Inhabited (CategoryTheory.Subobject X)

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

theorem CategoryTheory.Subobject.underlyingIso_top_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {B : C} : (CategoryTheory.Subobject.underlyingIso (CategoryTheory.CategoryStruct.id B)).hom = CategoryTheory.Subobject.arrow ⊤

instance CategoryTheory.Subobject.top_arrow_isIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {B : C} : CategoryTheory.IsIso (CategoryTheory.Subobject.arrow ⊤)

@[simp]

theorem CategoryTheory.Subobject.underlyingIso_inv_top_arrow_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {B : C} {Z : C} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.underlyingIso (CategoryTheory.CategoryStruct.id B)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.arrow ⊤) h) = h

@[simp]

theorem CategoryTheory.Subobject.underlyingIso_inv_top_arrow {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {B : C} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.underlyingIso (CategoryTheory.CategoryStruct.id B)).inv (CategoryTheory.Subobject.arrow ⊤) = CategoryTheory.CategoryStruct.id B

@[simp]

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

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

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

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

instance CategoryTheory.Subobject.isIso_top_arrow {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Y : C} : CategoryTheory.IsIso (CategoryTheory.Subobject.arrow ⊤)

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

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

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

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

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

theorem CategoryTheory.Subobject.bot_eq_initial_to {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.InitialMonoClass C] {B : C} : ⊥ = CategoryTheory.Subobject.mk (CategoryTheory.Limits.initial.to B)

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

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

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

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

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

theorem CategoryTheory.Subobject.functor_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y) (a : CategoryTheory.Subobject X.unop), (CategoryTheory.Subobject.functor C).map f a = (CategoryTheory.Subobject.pullback f.unop).obj a

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

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

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

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

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

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

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

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

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

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

@[simp]

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

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

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

@[simp]

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

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

theorem CategoryTheory.Subobject.inf_eq_map_pullback' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {A : C} (f₁ : CategoryTheory.MonoOver A) (f₂ : CategoryTheory.Subobject A) : (CategoryTheory.Subobject.inf.obj (Quotient.mk'' f₁)).obj f₂ = (CategoryTheory.Subobject.map (CategoryTheory.MonoOver.arrow f₁)).obj ((CategoryTheory.Subobject.pullback (CategoryTheory.MonoOver.arrow f₁)).obj f₂)

theorem CategoryTheory.Subobject.inf_eq_map_pullback {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {A : C} (f₁ : CategoryTheory.MonoOver A) (f₂ : CategoryTheory.Subobject A) : Quotient.mk'' f₁ ⊓ f₂ = (CategoryTheory.Subobject.map (CategoryTheory.MonoOver.arrow f₁)).obj ((CategoryTheory.Subobject.pullback (CategoryTheory.MonoOver.arrow f₁)).obj f₂)

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

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

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

⊓ commutes with pullback.

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

⊓ commutes with map.

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

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

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

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

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

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

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

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

def CategoryTheory.Subobject.wideCospan {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.WellPowered C] {A : C} (s : Set (CategoryTheory.Subobject A)) : CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape ↑(↑(equivShrink (CategoryTheory.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.)

@[simp]

theorem CategoryTheory.Subobject.wideCospan_map_term {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.WellPowered C] {A : C} (s : Set (CategoryTheory.Subobject A)) (j : ↑(↑(equivShrink (CategoryTheory.Subobject A)) '' s)) : (CategoryTheory.Subobject.wideCospan s).map (CategoryTheory.Limits.WidePullbackShape.Hom.term j) = CategoryTheory.Subobject.arrow (↑(equivShrink (CategoryTheory.Subobject A)).symm ↑j)

def CategoryTheory.Subobject.leInfCone {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.WellPowered C] {A : C} (s : Set (CategoryTheory.Subobject A)) (f : CategoryTheory.Subobject A) (k : ∀ (g : CategoryTheory.Subobject A), g ∈ s → f ≤ g) : CategoryTheory.Limits.Cone (CategoryTheory.Subobject.wideCospan s)

Auxiliary construction of a cone for le_inf.

@[simp]

theorem CategoryTheory.Subobject.leInfCone_π_app_none {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.WellPowered C] {A : C} (s : Set (CategoryTheory.Subobject A)) (f : CategoryTheory.Subobject A) (k : ∀ (g : CategoryTheory.Subobject A), g ∈ s → f ≤ g) : (CategoryTheory.Subobject.leInfCone s f k).π.app none = CategoryTheory.Subobject.arrow f

def CategoryTheory.Subobject.widePullback {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.WellPowered C] [CategoryTheory.Limits.HasWidePullbacks C] {A : C} (s : Set (CategoryTheory.Subobject A)) : C

The limit of wideCospan s. (This will be the supremum of the set of subobjects.)

def CategoryTheory.Subobject.widePullbackι {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.WellPowered C] [CategoryTheory.Limits.HasWidePullbacks C] {A : C} (s : Set (CategoryTheory.Subobject A)) : CategoryTheory.Subobject.widePullback s ⟶ A

The inclusion map from widePullback s to A

instance CategoryTheory.Subobject.widePullbackι_mono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.WellPowered C] [CategoryTheory.Limits.HasWidePullbacks C] {A : C} (s : Set (CategoryTheory.Subobject A)) : CategoryTheory.Mono (CategoryTheory.Subobject.widePullbackι s)

def CategoryTheory.Subobject.sInf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.WellPowered C] [CategoryTheory.Limits.HasWidePullbacks C] {A : C} (s : Set (CategoryTheory.Subobject A)) : CategoryTheory.Subobject A

When [WellPowered C] and [HasWidePullbacks C], Subobject A has arbitrary infimums.

theorem CategoryTheory.Subobject.sInf_le {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.WellPowered C] [CategoryTheory.Limits.HasWidePullbacks C] {A : C} (s : Set (CategoryTheory.Subobject A)) (f : CategoryTheory.Subobject A) (hf : f ∈ s) : CategoryTheory.Subobject.sInf s ≤ f

theorem CategoryTheory.Subobject.le_sInf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.WellPowered C] [CategoryTheory.Limits.HasWidePullbacks C] {A : C} (s : Set (CategoryTheory.Subobject A)) (f : CategoryTheory.Subobject A) (k : ∀ (g : CategoryTheory.Subobject A), g ∈ s → f ≤ g) : f ≤ CategoryTheory.Subobject.sInf s

instance CategoryTheory.Subobject.completeSemilatticeInf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.WellPowered C] [CategoryTheory.Limits.HasWidePullbacks C] {B : C} : CompleteSemilatticeInf (CategoryTheory.Subobject B)

def CategoryTheory.Subobject.smallCoproductDesc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.WellPowered C] [CategoryTheory.Limits.HasCoproducts C] {A : C} (s : Set (CategoryTheory.Subobject A)) : (∐ fun j => CategoryTheory.Subobject.underlying.obj (↑(equivShrink (CategoryTheory.Subobject A)).symm ↑j)) ⟶ A

The universal morphism out of the coproduct of a set of subobjects, after using [WellPowered C] to reindex by a small type.

def CategoryTheory.Subobject.sSup {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.WellPowered C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Limits.HasImages C] {A : C} (s : Set (CategoryTheory.Subobject A)) : CategoryTheory.Subobject A

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

theorem CategoryTheory.Subobject.le_sSup {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.WellPowered C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Limits.HasImages C] {A : C} (s : Set (CategoryTheory.Subobject A)) (f : CategoryTheory.Subobject A) (hf : f ∈ s) : f ≤ CategoryTheory.Subobject.sSup s

theorem CategoryTheory.Subobject.symm_apply_mem_iff_mem_image {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set α) (x : β) : ↑e.symm x ∈ s ↔ x ∈ ↑e '' s

theorem CategoryTheory.Subobject.sSup_le {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.WellPowered C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Limits.HasImages C] {A : C} (s : Set (CategoryTheory.Subobject A)) (f : CategoryTheory.Subobject A) (k : ∀ (g : CategoryTheory.Subobject A), g ∈ s → g ≤ f) : CategoryTheory.Subobject.sSup s ≤ f

instance CategoryTheory.Subobject.completeSemilatticeSup {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.WellPowered C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Limits.HasImages C] {B : C} : CompleteSemilatticeSup (CategoryTheory.Subobject B)

instance CategoryTheory.Subobject.instCompleteLatticeSubobject {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.WellPowered C] [CategoryTheory.Limits.HasWidePullbacks C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Limits.InitialMonoClass C] {B : C} : CompleteLattice (CategoryTheory.Subobject B)

theorem CategoryTheory.Subobject.nontrivial_of_not_isZero {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {X : C} (h : ¬CategoryTheory.Limits.IsZero X) : Nontrivial (CategoryTheory.Subobject X)

A nonzero object has nontrivial subobject lattice.

def CategoryTheory.Subobject.subobjectOrderIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (Y : CategoryTheory.Subobject X) : CategoryTheory.Subobject (CategoryTheory.Subobject.underlying.obj Y) ≃o ↑(Set.Iic Y)

The subobject lattice of a subobject Y is order isomorphic to the interval Set.Iic Y.