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.instTop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} : Top (CategoryTheory.MonoOver X)

Equations

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

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

Equations

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

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.

Equations

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

@[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) : ⊤.arrow = CategoryTheory.CategoryStruct.id X

def CategoryTheory.MonoOver.mapTop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X 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.

Equations

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

def CategoryTheory.MonoOver.pullbackTop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X 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.

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• CategoryTheory.MonoOver.instBot = { bot := CategoryTheory.MonoOver.mk' (CategoryTheory.Limits.initial.to 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} : ⊥.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.

Equations

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

def CategoryTheory.MonoOver.mapBot {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X 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.

Equations

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

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.

Equations

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

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} : ⊥.arrow = 0

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.

Equations

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

@[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.MonoOver.pullback f.arrow).comp (CategoryTheory.MonoOver.map f.arrow)

@[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.MonoOver.forget A).obj g).hom X✝.arrow) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd ((CategoryTheory.MonoOver.forget A).obj g).hom X✝.arrow) k.left) ⋯) ⋯

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

Equations

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

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

Equations

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

def CategoryTheory.MonoOver.leInf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {A : C} (f g h : CategoryTheory.MonoOver A) : (h ⟶ f) → (h ⟶ g) → (h ⟶ (CategoryTheory.MonoOver.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 ⋯) ⋯

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.

Equations

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

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

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

def CategoryTheory.MonoOver.supLe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A : C} (f g h : CategoryTheory.MonoOver A) : (f ⟶ h) → (g ⟶ h) → ((CategoryTheory.MonoOver.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.

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

Equations

• CategoryTheory.Subobject.orderTop = OrderTop.mk ⋯

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

Equations

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

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 = ⊤.arrow

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

Equations

• ⋯ = ⋯

@[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 ⊤.arrow = CategoryTheory.CategoryStruct.id B

@[simp]

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

@[simp]

theorem CategoryTheory.Subobject.map_top {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X 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 B : C} (f : A ⟶ B) : ⊤.Factors f

theorem CategoryTheory.Subobject.isIso_iff_mk_eq_top {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X 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 P.arrow ↔ P = ⊤

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

Equations

• ⋯ = ⋯

theorem CategoryTheory.Subobject.mk_eq_top_of_isIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X 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 P.arrow] : P = ⊤

theorem CategoryTheory.Subobject.pullback_top {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X 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 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)

Equations

• CategoryTheory.Subobject.orderBot = OrderBot.mk ⋯

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.

Equations

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

theorem CategoryTheory.Subobject.map_bot {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X 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.

Equations

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

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} : ⊥.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 B : C} (f : A ⟶ B) : ⊥.Factors f ↔ f = 0

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

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.

Equations

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

@[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 (Opposite.unop X✝)) : (CategoryTheory.Subobject.functor C).map f a✝ = (CategoryTheory.Subobject.pullback f.unop).obj a✝

@[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 (Opposite.unop X)

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.

Equations

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

theorem CategoryTheory.Subobject.inf_le_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {A : C} (f 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 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 f 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)

Equations

• CategoryTheory.Subobject.semilatticeInf = SemilatticeInf.mk (fun (m n : CategoryTheory.Subobject B) => (CategoryTheory.Subobject.inf.obj m).obj n) ⋯ ⋯ ⋯

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

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

@[simp]

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

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

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

@[simp]

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

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 f₁.arrow).obj ((CategoryTheory.Subobject.pullback f₁.arrow).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 f₁.arrow).obj ((CategoryTheory.Subobject.pullback f₁.arrow).obj f₂)

theorem CategoryTheory.Subobject.prod_eq_inf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {A : C} {f₁ 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 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 Y : C} (g : X ⟶ Y) (f₁ 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 Y : C} (g : Y ⟶ X) [CategoryTheory.Mono g] (f₁ 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.

Equations

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

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)

Equations

• CategoryTheory.Subobject.semilatticeSup = SemilatticeSup.mk (fun (m n : CategoryTheory.Subobject B) => (CategoryTheory.Subobject.sup.obj m).obj n) ⋯ ⋯ ⋯

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 B : C} {X Y : CategoryTheory.Subobject B} {f : A ⟶ B} (P : X.Factors f) : (X ⊔ Y).Factors 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 B : C} {X Y : CategoryTheory.Subobject B} {f : A ⟶ B} (P : Y.Factors f) : (X ⊔ Y).Factors 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 B : C} {s : Finset I} {P : I → CategoryTheory.Subobject B} {f : A ⟶ B} (h : ∃ i ∈ s, (P i).Factors f) : (s.sup P).Factors 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)

Equations

• CategoryTheory.Subobject.boundedOrder = BoundedOrder.mk

instance CategoryTheory.Subobject.instLattice {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)

Equations

• CategoryTheory.Subobject.instLattice = Lattice.mk SemilatticeInf.inf ⋯ ⋯ ⋯

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

Equations

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

@[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) = ((equivShrink (CategoryTheory.Subobject A)).symm ↑j).arrow

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 ∈ s, f ≤ g) : CategoryTheory.Limits.Cone (CategoryTheory.Subobject.wideCospan s)

Auxiliary construction of a cone for le_inf.

Equations

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

@[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 ∈ s, f ≤ g) : (CategoryTheory.Subobject.leInfCone s f k).π.app none = f.arrow

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

Equations

• CategoryTheory.Subobject.widePullback s = CategoryTheory.Limits.limit (CategoryTheory.Subobject.wideCospan s)

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

Equations

• CategoryTheory.Subobject.widePullbackι s = CategoryTheory.Limits.limit.π (CategoryTheory.Subobject.wideCospan s) none

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)

Equations

• ⋯ = ⋯

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.

Equations

• CategoryTheory.Subobject.sInf s = CategoryTheory.Subobject.mk (CategoryTheory.Subobject.widePullbackι s)

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 ∈ 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)

Equations

• CategoryTheory.Subobject.completeSemilatticeInf = CompleteSemilatticeInf.mk ⋯ ⋯

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 : ↑(⇑(equivShrink (CategoryTheory.Subobject A)) '' s)) => 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.

Equations

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

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.

Equations

• CategoryTheory.Subobject.sSup s = CategoryTheory.Subobject.mk (CategoryTheory.Limits.image.ι (CategoryTheory.Subobject.smallCoproductDesc s))

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 ∈ 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)

Equations

• CategoryTheory.Subobject.completeSemilatticeSup = CompleteSemilatticeSup.mk ⋯ ⋯

instance CategoryTheory.Subobject.instCompleteLattice {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)

Equations

• CategoryTheory.Subobject.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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.

Equations

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