mathlib documentation

category_theory.subobject.lattice

The lattice of subobjects #

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

The morphism to the top object in mono_over X.

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

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

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

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

Equations

A morphism version of the le_inf axiom.

Equations
theorem category_theory.subobject.top_factors {C : Type u₁} [category_theory.category C] {A B : C} (f : A B) :

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

Equations
@[simp]
theorem category_theory.subobject.finset_inf_factors {C : Type u₁} [category_theory.category C] [category_theory.limits.has_pullbacks C] {I : Type u_1} {A B : C} {s : finset I} {P : I → category_theory.subobject B} (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₁} [category_theory.category C] [category_theory.limits.has_pullbacks C] {I : Type u_1} {B : C} (s : finset I) (P : I → category_theory.subobject B) (i : I) (m : i s) :
(P i).factors (s.inf P).arrow

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