# mathlibdocumentation

category_theory.subobject.lattice

# The lattice of subobjects #

We provide the semilattice_inf with order_top (subobject X) instance when [has_pullback C], and the semilattice_sup (subobject X) instance when [has_images C] [has_binary_coproducts C].

@[protected, instance]
def category_theory.mono_over.has_top {C : Type u₁} {X : C} :
Equations
@[protected, instance]
def category_theory.mono_over.inhabited {C : Type u₁} {X : C} :
Equations
def category_theory.mono_over.le_top {C : Type u₁} {X : C}  :

The morphism to the top object in mono_over X.

Equations
@[simp]
theorem category_theory.mono_over.top_left {C : Type u₁} (X : C) :
@[simp]
theorem category_theory.mono_over.top_arrow {C : Type u₁} (X : C) :
def category_theory.mono_over.map_top {C : Type u₁} {X Y : C} (f : X Y)  :

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

Equations
noncomputable def category_theory.mono_over.pullback_top {C : Type u₁} {X Y : C} (f : X Y) :

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

Equations
noncomputable def category_theory.mono_over.top_le_pullback_self {C : Type u₁} {A B : C} (f : A B)  :

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

Equations
noncomputable def category_theory.mono_over.pullback_self {C : Type u₁} {A B : C} (f : A B)  :

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

Equations
@[protected, instance]
noncomputable def category_theory.mono_over.has_bot {C : Type u₁} {X : C} :
Equations
@[simp]
theorem category_theory.mono_over.bot_left {C : Type u₁} (X : C) :
@[simp]
theorem category_theory.mono_over.bot_arrow {C : Type u₁} {X : C} :
noncomputable def category_theory.mono_over.bot_le {C : Type u₁} {X : C}  :

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

Equations
noncomputable def category_theory.mono_over.map_bot {C : Type u₁} {X Y : C} (f : X Y)  :

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

Equations
noncomputable def category_theory.mono_over.bot_coe_iso_zero {C : Type u₁} {B : C} :

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

Equations
@[simp]
theorem category_theory.mono_over.bot_arrow_eq_zero {C : Type u₁} {B : C} :
@[simp]
theorem category_theory.mono_over.inf_map_app {C : Type u₁} {A : C} (f₁ f₂ : category_theory.mono_over A) (k : f₁ f₂)  :
@[simp]
theorem category_theory.mono_over.inf_obj {C : Type u₁} {A : C}  :
noncomputable def category_theory.mono_over.inf {C : Type u₁} {A : C} :

When [has_pullbacks C], mono_over A has "intersections", functorial in both arguments.

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

Equations
noncomputable def category_theory.mono_over.inf_le_left {C : Type u₁} {A : C} (f g : category_theory.mono_over A) :
f

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

Equations
noncomputable def category_theory.mono_over.inf_le_right {C : Type u₁} {A : C} (f g : category_theory.mono_over A) :
g

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

Equations
noncomputable def category_theory.mono_over.le_inf {C : Type u₁} {A : C} (f g h : category_theory.mono_over A) :
(h f)(h g)(h

A morphism version of the le_inf axiom.

Equations
noncomputable def category_theory.mono_over.sup {C : Type u₁} {A : C} :

When [has_images C] [has_binary_coproducts C], mono_over A has a sup construction, which is functorial in both arguments, and which on subobject A will induce a semilattice_sup.

Equations
noncomputable def category_theory.mono_over.le_sup_left {C : Type u₁} {A : C} (f g : category_theory.mono_over A) :
f

A morphism version of le_sup_left.

Equations
noncomputable def category_theory.mono_over.le_sup_right {C : Type u₁} {A : C} (f g : category_theory.mono_over A) :
g

A morphism version of le_sup_right.

Equations
noncomputable def category_theory.mono_over.sup_le {C : Type u₁} {A : C} (f g h : category_theory.mono_over A) :
(f h)(g h) h)

A morphism version of sup_le.

Equations
@[protected, instance]
def category_theory.subobject.order_top {C : Type u₁} {X : C} :
Equations
@[protected, instance]
def category_theory.subobject.inhabited {C : Type u₁} {X : C} :
Equations
theorem category_theory.subobject.top_eq_id {C : Type u₁} (B : C) :
theorem category_theory.subobject.underlying_iso_top_hom {C : Type u₁} {B : C} :
@[protected, instance]
def category_theory.subobject.top_arrow_is_iso {C : Type u₁} {B : C} :
@[simp]
theorem category_theory.subobject.underlying_iso_inv_top_arrow_assoc {C : Type u₁} {B X' : C} (f' : B X') :
.arrow f' = f'
@[simp]
theorem category_theory.subobject.underlying_iso_inv_top_arrow {C : Type u₁} {B : C} :
@[simp]
theorem category_theory.subobject.map_top {C : Type u₁} {X Y : C} (f : X Y)  :
theorem category_theory.subobject.top_factors {C : Type u₁} {A B : C} (f : A B) :
theorem category_theory.subobject.is_iso_iff_mk_eq_top {C : Type u₁} {X Y : C} (f : X Y)  :
theorem category_theory.subobject.is_iso_arrow_iff_eq_top {C : Type u₁} {Y : C}  :
@[protected, instance]
def category_theory.subobject.is_iso_top_arrow {C : Type u₁} {Y : C} :
theorem category_theory.subobject.mk_eq_top_of_is_iso {C : Type u₁} {X Y : C} (f : X Y)  :
theorem category_theory.subobject.eq_top_of_is_iso_arrow {C : Type u₁} {Y : C}  :
P =
theorem category_theory.subobject.pullback_top {C : Type u₁} {X Y : C} (f : X Y) :
theorem category_theory.subobject.pullback_self {C : Type u₁} {A B : C} (f : A B)  :
@[protected, instance]
noncomputable def category_theory.subobject.order_bot {C : Type u₁} {X : C} :
Equations
noncomputable def category_theory.subobject.bot_coe_iso_initial {C : Type u₁} {B : C} :

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

Equations
theorem category_theory.subobject.map_bot {C : Type u₁} {X Y : C} (f : X Y)  :
noncomputable def category_theory.subobject.bot_coe_iso_zero {C : Type u₁} {B : C} :

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

Equations
theorem category_theory.subobject.bot_eq_zero {C : Type u₁} {B : C} :
@[simp]
theorem category_theory.subobject.bot_arrow {C : Type u₁} {B : C} :
theorem category_theory.subobject.bot_factors_iff_zero {C : Type u₁} {A B : C} (f : A B) :
theorem category_theory.subobject.mk_eq_bot_iff_zero {C : Type u₁} {X Y : C} {f : X Y}  :
f = 0
@[simp]
theorem category_theory.subobject.functor_obj (C : Type u₁) (X : Cᵒᵖ) :
noncomputable def category_theory.subobject.functor (C : Type u₁)  :
Cᵒᵖ Type (max u₁ v₁)

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

Equations
@[simp]
theorem category_theory.subobject.functor_map (C : Type u₁) (X Y : Cᵒᵖ) (f : X Y)  :
noncomputable def category_theory.subobject.inf {C : Type u₁} {A : C} :

The functorial infimum on mono_over A descends to an infimum on subobject A.

Equations
theorem category_theory.subobject.inf_le_left {C : Type u₁} {A : C} (f g : category_theory.subobject A) :
f
theorem category_theory.subobject.inf_le_right {C : Type u₁} {A : C} (f g : category_theory.subobject A) :
g
theorem category_theory.subobject.le_inf {C : Type u₁} {A : C} (h f g : category_theory.subobject A) :
h fh gh
@[protected, instance]
noncomputable def category_theory.subobject.semilattice_inf {C : Type u₁} {B : C} :
Equations
theorem category_theory.subobject.factors_left_of_inf_factors {C : Type u₁} {A B : C} {X Y : category_theory.subobject B} {f : A B} (h : (X Y).factors f) :
theorem category_theory.subobject.factors_right_of_inf_factors {C : Type u₁} {A B : C} {X Y : category_theory.subobject B} {f : A B} (h : (X Y).factors f) :
@[simp]
theorem category_theory.subobject.inf_factors {C : Type u₁} {A B : C} {X Y : category_theory.subobject B} (f : A B) :
(X Y).factors f X.factors f Y.factors f
@[simp]
theorem category_theory.subobject.finset_inf_factors {C : Type u₁} {I : Type u_1} {A B : C} {s : finset I} {P : I → } (f : A B) :
(s.inf P).factors f ∀ (i : I), i s(P i).factors f
theorem category_theory.subobject.finset_inf_arrow_factors {C : Type u₁} {I : Type u_1} {B : C} (s : finset I) (P : I → ) (i : I) (m : i s) :
(P i).factors (s.inf P).arrow
theorem category_theory.subobject.prod_eq_inf {C : Type u₁} {A : C} {f₁ f₂ : category_theory.subobject A}  :
(f₁ f₂) = f₁ f₂
theorem category_theory.subobject.inf_def {C : Type u₁} {B : C} (m m' : category_theory.subobject B) :
m m' =
theorem category_theory.subobject.inf_pullback {C : Type u₁} {X Y : C} (g : X Y) (f₁ f₂ : category_theory.subobject Y) :
(f₁ f₂) =

⊓ commutes with pullback.

theorem category_theory.subobject.inf_map {C : Type u₁} {X Y : C} (g : Y X) (f₁ f₂ : category_theory.subobject Y) :
(f₁ f₂) =

⊓ commutes with map.

noncomputable def category_theory.subobject.sup {C : Type u₁} {A : C} :

The functorial supremum on mono_over A descends to an supremum on subobject A.

Equations
@[protected, instance]
noncomputable def category_theory.subobject.semilattice_sup {C : Type u₁} {B : C} :
Equations
theorem category_theory.subobject.sup_factors_of_factors_left {C : Type u₁} {A B : C} {X Y : category_theory.subobject B} {f : A B} (P : X.factors f) :
(X Y).factors f
theorem category_theory.subobject.sup_factors_of_factors_right {C : Type u₁} {A B : C} {X Y : category_theory.subobject B} {f : A B} (P : Y.factors f) :
(X Y).factors f
theorem category_theory.subobject.finset_sup_factors {C : Type u₁} {I : Type u_1} {A B : C} {s : finset I} {P : I → } {f : A B} (h : ∃ (i : I) (H : i s), (P i).factors f) :
(s.sup P).factors f
@[protected, instance]
noncomputable def category_theory.subobject.bounded_order {C : Type u₁} {B : C} :
Equations
@[protected, instance]
noncomputable def category_theory.subobject.lattice {C : Type u₁} {B : C} :
Equations
noncomputable def category_theory.subobject.wide_cospan {C : Type u₁} {A : C} (s : set ) :

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 well_powered C to make the diagram small.)

Equations
@[simp]
theorem category_theory.subobject.wide_cospan_map_term {C : Type u₁} {A : C} (s : set ) (j : '' s)) :
noncomputable def category_theory.subobject.le_Inf_cone {C : Type u₁} {A : C} (s : set ) (k : ∀ (g : , g sf g) :

Auxiliary construction of a cone for le_Inf.

Equations
@[simp]
theorem category_theory.subobject.le_Inf_cone_π_app_none {C : Type u₁} {A : C} (s : set ) (k : ∀ (g : , g sf g) :
noncomputable def category_theory.subobject.wide_pullback {C : Type u₁} {A : C} (s : set ) :
C

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

Equations
noncomputable def category_theory.subobject.wide_pullback_ι {C : Type u₁} {A : C} (s : set ) :

The inclusion map from wide_pullback s to A

Equations
Instances for category_theory.subobject.wide_pullback_ι
@[protected, instance]
noncomputable def category_theory.subobject.Inf {C : Type u₁} {A : C} (s : set ) :

When [well_powered C] and [has_wide_pullbacks C], subobject A has arbitrary infimums.

Equations
theorem category_theory.subobject.Inf_le {C : Type u₁} {A : C} (s : set ) (H : f s) :
theorem category_theory.subobject.le_Inf {C : Type u₁} {A : C} (s : set ) (k : ∀ (g : , g sf g) :
@[protected, instance]
noncomputable def category_theory.subobject.complete_semilattice_Inf {C : Type u₁} {B : C} :
Equations
noncomputable def category_theory.subobject.small_coproduct_desc {C : Type u₁} {A : C} (s : set ) :
( λ (j : '' s)), ( j)) A

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

Equations
noncomputable def category_theory.subobject.Sup {C : Type u₁} {A : C} (s : set ) :

When [well_powered C] [has_images C] [has_coproducts C], subobject A has arbitrary supremums.

Equations
theorem category_theory.subobject.le_Sup {C : Type u₁} {A : C} (s : set ) (H : f s) :
theorem category_theory.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 category_theory.subobject.Sup_le {C : Type u₁} {A : C} (s : set ) (k : ∀ (g : , g sg f) :
@[protected, instance]
noncomputable def category_theory.subobject.complete_semilattice_Sup {C : Type u₁} {B : C} :
Equations
@[protected, instance]
Equations

A nonzero object has nontrivial subobject lattice.

noncomputable def category_theory.subobject.subobject_order_iso {C : Type u₁} {X : C}  :

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

Equations