mathlib3 documentation

category_theory.subobject.lattice

The lattice of subobjects #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

The morphism to the top object in mono_over X.

Equations
@[simp]

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

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

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

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

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

Equations