# Documentation

Mathlib.CategoryTheory.Subobject.Lattice

# 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₁} [] {X : C} :
def CategoryTheory.MonoOver.leTop {C : Type u₁} [] {X : C} (f : ) :

The morphism to the top object in MonoOver X.

Instances For
@[simp]
theorem CategoryTheory.MonoOver.top_left {C : Type u₁} [] (X : C) :
.obj.left = X
@[simp]
theorem CategoryTheory.MonoOver.top_arrow {C : Type u₁} [] (X : C) :
def CategoryTheory.MonoOver.mapTop {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

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

Instances For
def CategoryTheory.MonoOver.pullbackTop {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

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

Instances For
def CategoryTheory.MonoOver.topLEPullbackSelf {C : Type u₁} [] {A : C} {B : C} (f : A B) :

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

Instances For
def CategoryTheory.MonoOver.pullbackSelf {C : Type u₁} [] {A : C} {B : C} (f : A B) :

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

Instances For
instance CategoryTheory.MonoOver.instBotMonoOver {C : Type u₁} [] {X : C} :
@[simp]
theorem CategoryTheory.MonoOver.bot_left {C : Type u₁} [] (X : C) :
.obj.left = ⊥_ C
@[simp]
def CategoryTheory.MonoOver.botLE {C : Type u₁} [] {X : C} (f : ) :

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

Instances For
def CategoryTheory.MonoOver.mapBot {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
().obj

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

Instances For
def CategoryTheory.MonoOver.botCoeIsoZero {C : Type u₁} [] {B : C} :
.obj.left 0

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

Instances For
@[simp]
theorem CategoryTheory.MonoOver.inf_obj {C : Type u₁} [] {A : C} (f : ) :
CategoryTheory.MonoOver.inf.obj f =
@[simp]
theorem CategoryTheory.MonoOver.inf_map_app {C : Type u₁} [] {A : C} :
∀ {X Y : } (k : X Y) (g : ), (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 (().obj g).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd k.left) ()))

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.

Instances For
def CategoryTheory.MonoOver.infLELeft {C : Type u₁} [] {A : C} (f : ) (g : ) :
(CategoryTheory.MonoOver.inf.obj f).obj g f

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

Instances For
def CategoryTheory.MonoOver.infLERight {C : Type u₁} [] {A : C} (f : ) (g : ) :
(CategoryTheory.MonoOver.inf.obj f).obj g g

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

Instances For
def CategoryTheory.MonoOver.leInf {C : Type u₁} [] {A : C} (f : ) (g : ) (h : ) :
(h f) → (h g) → (h (CategoryTheory.MonoOver.inf.obj f).obj g)

A morphism version of the le_inf axiom.

Instances For

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.

Instances For
def CategoryTheory.MonoOver.leSupLeft {C : Type u₁} [] {A : C} (f : ) (g : ) :
f (CategoryTheory.MonoOver.sup.obj f).obj g

A morphism version of le_sup_left.

Instances For
def CategoryTheory.MonoOver.leSupRight {C : Type u₁} [] {A : C} (f : ) (g : ) :
g (CategoryTheory.MonoOver.sup.obj f).obj g

A morphism version of le_sup_right.

Instances For
def CategoryTheory.MonoOver.supLe {C : Type u₁} [] {A : C} (f : ) (g : ) (h : ) :
(f h) → (g h) → ((CategoryTheory.MonoOver.sup.obj f).obj g h)

A morphism version of sup_le.

Instances For
instance CategoryTheory.Subobject.orderTop {C : Type u₁} [] {X : C} :
theorem CategoryTheory.Subobject.top_eq_id {C : Type u₁} [] (B : C) :
instance CategoryTheory.Subobject.top_arrow_isIso {C : Type u₁} [] {B : C} :
@[simp]
theorem CategoryTheory.Subobject.underlyingIso_inv_top_arrow_assoc {C : Type u₁} [] {B : C} {Z : C} (h : B Z) :
@[simp]
@[simp]
theorem CategoryTheory.Subobject.map_top {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.Subobject.top_factors {C : Type u₁} [] {A : C} {B : C} (f : A B) :
theorem CategoryTheory.Subobject.isIso_iff_mk_eq_top {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.Subobject.isIso_arrow_iff_eq_top {C : Type u₁} [] {Y : C} (P : ) :
instance CategoryTheory.Subobject.isIso_top_arrow {C : Type u₁} [] {Y : C} :
theorem CategoryTheory.Subobject.mk_eq_top_of_isIso {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.Subobject.eq_top_of_isIso_arrow {C : Type u₁} [] {Y : C} (P : ) :
P =
theorem CategoryTheory.Subobject.pullback_top {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.Subobject.pullback_self {C : Type u₁} [] {A : C} {B : C} (f : A B) :
instance CategoryTheory.Subobject.orderBot {C : Type u₁} [] {X : C} :
def CategoryTheory.Subobject.botCoeIsoInitial {C : Type u₁} [] {B : C} :
CategoryTheory.Subobject.underlying.obj ⊥_ C

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

Instances For
theorem CategoryTheory.Subobject.map_bot {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
().obj =
def CategoryTheory.Subobject.botCoeIsoZero {C : Type u₁} [] {B : C} :
CategoryTheory.Subobject.underlying.obj 0

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

Instances For
theorem CategoryTheory.Subobject.bot_eq_zero {C : Type u₁} [] {B : C} :
@[simp]
theorem CategoryTheory.Subobject.bot_arrow {C : Type u₁} [] {B : C} :
theorem CategoryTheory.Subobject.bot_factors_iff_zero {C : Type u₁} [] {A : C} {B : C} (f : A B) :
theorem CategoryTheory.Subobject.mk_eq_bot_iff_zero {C : Type u₁} [] {X : C} {Y : C} {f : X Y} :
f = 0
@[simp]
theorem CategoryTheory.Subobject.functor_obj (C : Type u₁) [] (X : Cᵒᵖ) :
().obj X = CategoryTheory.Subobject X.unop
@[simp]
theorem CategoryTheory.Subobject.functor_map (C : Type u₁) [] :
∀ {X Y : Cᵒᵖ} (f : X Y) (a : CategoryTheory.Subobject X.unop), ().map f a = ().obj a

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

Instances For

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

Instances For
theorem CategoryTheory.Subobject.inf_le_left {C : Type u₁} [] {A : C} (f : ) (g : ) :
(CategoryTheory.Subobject.inf.obj f).obj g f
theorem CategoryTheory.Subobject.inf_le_right {C : Type u₁} [] {A : C} (f : ) (g : ) :
(CategoryTheory.Subobject.inf.obj f).obj g g
theorem CategoryTheory.Subobject.le_inf {C : Type u₁} [] {A : C} (h : ) (f : ) (g : ) :
h fh gh (CategoryTheory.Subobject.inf.obj f).obj g
instance CategoryTheory.Subobject.semilatticeInf {C : Type u₁} [] {B : C} :
theorem CategoryTheory.Subobject.factors_left_of_inf_factors {C : Type u₁} [] {A : C} {B : C} {X : } {Y : } {f : A B} (h : ) :
theorem CategoryTheory.Subobject.factors_right_of_inf_factors {C : Type u₁} [] {A : C} {B : C} {X : } {Y : } {f : A B} (h : ) :
@[simp]
theorem CategoryTheory.Subobject.inf_factors {C : Type u₁} [] {A : C} {B : C} {X : } {Y : } (f : A B) :
theorem CategoryTheory.Subobject.inf_arrow_factors_left {C : Type u₁} [] {B : C} (X : ) (Y : ) :
theorem CategoryTheory.Subobject.inf_arrow_factors_right {C : Type u₁} [] {B : C} (X : ) (Y : ) :
@[simp]
theorem CategoryTheory.Subobject.finset_inf_factors {C : Type u₁} [] {I : Type u_1} {A : C} {B : C} {s : } {P : } (f : A B) :
∀ (i : I), i s
theorem CategoryTheory.Subobject.finset_inf_arrow_factors {C : Type u₁} [] {I : Type u_1} {B : C} (s : ) (P : ) (i : I) (m : i s) :
theorem CategoryTheory.Subobject.inf_eq_map_pullback' {C : Type u₁} [] {A : C} (f₁ : ) (f₂ : ) :
(CategoryTheory.Subobject.inf.obj ()).obj f₂ = ().obj ()
theorem CategoryTheory.Subobject.inf_eq_map_pullback {C : Type u₁} [] {A : C} (f₁ : ) (f₂ : ) :
f₂ = ().obj ()
theorem CategoryTheory.Subobject.prod_eq_inf {C : Type u₁} [] {A : C} {f₁ : } {f₂ : } :
(f₁ f₂) = f₁ f₂
theorem CategoryTheory.Subobject.inf_def {C : Type u₁} [] {B : C} (m : ) (m' : ) :
m m' = (CategoryTheory.Subobject.inf.obj m).obj m'
theorem CategoryTheory.Subobject.inf_pullback {C : Type u₁} [] {X : C} {Y : C} (g : X Y) (f₁ : ) (f₂ : ) :
().obj (f₁ f₂) = ().obj f₁ ().obj f₂

⊓ commutes with pullback.

theorem CategoryTheory.Subobject.inf_map {C : Type u₁} [] {X : C} {Y : C} (g : Y X) (f₁ : ) (f₂ : ) :
().obj (f₁ f₂) = ().obj f₁ ().obj f₂

⊓ commutes with map.

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

Instances For
theorem CategoryTheory.Subobject.sup_factors_of_factors_left {C : Type u₁} [] {A : C} {B : C} {X : } {Y : } {f : A B} (P : ) :
theorem CategoryTheory.Subobject.sup_factors_of_factors_right {C : Type u₁} [] {A : C} {B : C} {X : } {Y : } {f : A B} (P : ) :
theorem CategoryTheory.Subobject.finset_sup_factors {C : Type u₁} [] {I : Type u_1} {A : C} {B : C} {s : } {P : } {f : A B} (h : i, i s ) :
instance CategoryTheory.Subobject.boundedOrder {C : Type u₁} [] {B : C} :
def CategoryTheory.Subobject.wideCospan {C : Type u₁} [] {A : C} (s : ) :

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

Instances For
@[simp]
theorem CategoryTheory.Subobject.wideCospan_map_term {C : Type u₁} [] {A : C} (s : ) (j : ↑()) :
def CategoryTheory.Subobject.leInfCone {C : Type u₁} [] {A : C} (s : ) (f : ) (k : ∀ (g : ), g sf g) :

Auxiliary construction of a cone for le_inf.

Instances For
@[simp]
theorem CategoryTheory.Subobject.leInfCone_π_app_none {C : Type u₁} [] {A : C} (s : ) (f : ) (k : ∀ (g : ), g sf g) :
().π.app none =
def CategoryTheory.Subobject.widePullback {C : Type u₁} [] {A : C} (s : ) :
C

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

Instances For
def CategoryTheory.Subobject.widePullbackι {C : Type u₁} [] {A : C} (s : ) :

The inclusion map from widePullback s to A

Instances For
instance CategoryTheory.Subobject.widePullbackι_mono {C : Type u₁} [] {A : C} (s : ) :
def CategoryTheory.Subobject.sInf {C : Type u₁} [] {A : C} (s : ) :

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

Instances For
theorem CategoryTheory.Subobject.sInf_le {C : Type u₁} [] {A : C} (s : ) (f : ) (hf : f s) :
theorem CategoryTheory.Subobject.le_sInf {C : Type u₁} [] {A : C} (s : ) (f : ) (k : ∀ (g : ), g sf g) :
def CategoryTheory.Subobject.smallCoproductDesc {C : Type u₁} [] {A : C} (s : ) :
( fun j => CategoryTheory.Subobject.underlying.obj (().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.

Instances For
def CategoryTheory.Subobject.sSup {C : Type u₁} [] {A : C} (s : ) :

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

Instances For
theorem CategoryTheory.Subobject.le_sSup {C : Type u₁} [] {A : C} (s : ) (f : ) (hf : f 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₁} [] {A : C} (s : ) (f : ) (k : ∀ (g : ), g sg f) :

A nonzero object has nontrivial subobject lattice.

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

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

Instances For