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

Equations

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

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

Equations

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

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 ⋯

@[simp]

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

@[simp]

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

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.

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.

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

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.

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

@[simp]

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

@[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

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

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.

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

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

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.

@[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)

@[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) ⋯) ⋯

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 ⋯

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

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

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.

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.

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.

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.

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

Equations

• CategoryTheory.Subobject.orderTop = OrderTop.mk ⋯

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

Equations

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

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

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

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

@[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

@[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

@[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

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

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

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

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

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

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

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

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) = ⊤

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 = OrderBot.mk ⋯

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)

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)

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 ⊥ = ⊥

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

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

@[simp]

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

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

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

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.

@[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✝

@[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)

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

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

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

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

instance CategoryTheory.Subobject.semilatticeInf {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {B : C} : SemilatticeInf (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₁} [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

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

@[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

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

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

@[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

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

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

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

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₂

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'

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.

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.

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

instance CategoryTheory.Subobject.semilatticeSup {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasImages C] [Limits.HasBinaryCoproducts C] {B : C} : SemilatticeSup (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₁} [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

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

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

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 = BoundedOrder.mk

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

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

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

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

@[simp]

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

def CategoryTheory.Subobject.leInfCone {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] {A : C} (s : Set (Subobject A)) (f : Subobject A) (k : ∀ g ∈ s, f ≤ g) : Limits.Cone (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₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] {A : C} (s : Set (Subobject A)) (f : Subobject A) (k : ∀ g ∈ s, f ≤ g) : (leInfCone s f k).π.app none = f.arrow

def CategoryTheory.Subobject.widePullback {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] [Limits.HasWidePullbacks C] {A : C} (s : Set (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₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] [Limits.HasWidePullbacks C] {A : C} (s : Set (Subobject A)) : 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₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] [Limits.HasWidePullbacks C] {A : C} (s : Set (Subobject A)) : Mono (widePullbackι s)

def CategoryTheory.Subobject.sInf {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] [Limits.HasWidePullbacks C] {A : C} (s : Set (Subobject A)) : 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₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] [Limits.HasWidePullbacks C] {A : C} (s : Set (Subobject A)) (f : Subobject A) (hf : f ∈ s) : sInf s ≤ f

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

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

Equations

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

def CategoryTheory.Subobject.smallCoproductDesc {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] [Limits.HasCoproducts C] {A : C} (s : Set (Subobject A)) : (∐ fun (j : ↑(⇑(equivShrink (Subobject A)) '' s)) => underlying.obj ((equivShrink (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₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] [Limits.HasCoproducts C] [Limits.HasImages C] {A : C} (s : Set (Subobject A)) : 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₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] [Limits.HasCoproducts C] [Limits.HasImages C] {A : C} (s : Set (Subobject A)) (f : Subobject A) (hf : f ∈ s) : f ≤ 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₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] [WellPowered.{w, v₁, u₁} C] [Limits.HasCoproducts C] [Limits.HasImages C] {A : C} (s : Set (Subobject A)) (f : Subobject A) (k : ∀ g ∈ s, g ≤ f) : sSup s ≤ f

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

Equations

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

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

Equations

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

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

A nonzero object has nontrivial subobject lattice.

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