mathlib3 documentation

category_theory.subobject.basic

Subobjects #

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

We define subobject X as the quotient (by isomorphisms) of mono_over X := {f : over X // mono f.hom}.

Here mono_over X is a thin category (a pair of objects has at most one morphism between them), so we can think of it as a preorder. However as it is not skeletal, it is not a partial order.

There is a coercion from subobject X back to the ambient category C (using choice to pick a representative), and for P : subobject X, P.arrow : (P : C) ⟶ X is the inclusion morphism.

We provide

The subobjects of X form a preorder making them into a category. We have X ≤ Y if and only if X.arrow factors through Y.arrow: see of_le/of_le_mk/of_mk_le/of_mk_le_mk and le_of_comm. Similarly, to show that two subobjects are equal, we can supply an isomorphism between the underlying objects that commutes with the arrows (eq_of_comm).

See also

Notes #

This development originally appeared in Bhavik Mehta's "Topos theory for Lean" repository, and was ported to mathlib by Scott Morrison.

Implementation note #

Currently we describe pullback, map, etc., as functors. It may be better to just say that they are monotone functions, and even avoid using categorical language entirely when describing subobject X. (It's worth keeping this in mind in future use; it should be a relatively easy change here if it looks preferable.)

Relation to pseudoelements #

There is a separate development of pseudoelements in category_theory.abelian.pseudoelements, as a quotient (but not by isomorphism) of over X.

When a morphism f has an image, the image represents the same pseudoelement. In a category with images pseudoelements X could be constructed as a quotient of mono_over X. In fact, in an abelian category (I'm not sure in what generality beyond that), pseudoelements X agrees with subobject X, but we haven't developed this in mathlib yet.

We now construct the subobject lattice for X : C, as the quotient by isomorphisms of mono_over X.

Since mono_over X is a thin category, we use thin_skeleton to take the quotient.

Essentially all the structure defined above on mono_over X descends to subobject X, with morphisms becoming inequalities, and isomorphisms becoming equations.

@[reducible]

Convenience constructor for a subobject.

theorem category_theory.comma.ext {A : Type u₁} {_inst_1 : category_theory.category A} {B : Type u₂} {_inst_2 : category_theory.category B} {T : Type u₃} {_inst_3 : category_theory.category T} {L : A T} {R : B T} (x y : category_theory.comma L R) (h : x.left = y.left) (h_1 : x.right = y.right) (h_2 : x.hom == y.hom) :
x = y
theorem category_theory.comma.ext_iff {A : Type u₁} {_inst_1 : category_theory.category A} {B : Type u₂} {_inst_2 : category_theory.category B} {T : Type u₃} {_inst_3 : category_theory.category T} {L : A T} {R : B T} (x y : category_theory.comma L R) :
x = y x.left = y.left x.right = y.right x.hom == y.hom
@[protected]
theorem category_theory.subobject.ind {C : Type u₁} [category_theory.category C] {X : C} (p : category_theory.subobject X Prop) (h : ⦃A : C⦄ (f : A X) [_inst_3 : category_theory.mono f], p (category_theory.subobject.mk f)) (P : category_theory.subobject X) :
p P
@[protected]
@[protected]
def category_theory.subobject.lift {C : Type u₁} [category_theory.category C] {α : Sort u_1} {X : C} (F : Π ⦃A : C⦄ (f : A X) [_inst_3 : category_theory.mono f], α) (h : ⦃A B : C⦄ (f : A X) (g : B X) [_inst_4 : category_theory.mono f] [_inst_5 : category_theory.mono g] (i : A B), i.hom g = f F f = F g) :

Declare a function on subobjects of X by specifying a function on monomorphisms with codomain X.

Equations
@[protected, simp]
theorem category_theory.subobject.lift_mk {C : Type u₁} [category_theory.category C] {α : Sort u_1} {X : C} (F : Π ⦃A : C⦄ (f : A X) [_inst_3 : category_theory.mono f], α) {h : ⦃A B : C⦄ (f : A X) (g : B X) [_inst_4 : category_theory.mono f] [_inst_5 : category_theory.mono g] (i : A B), i.hom g = f F f = F g} {A : C} (f : A X) [category_theory.mono f] :

The category of subobjects is equivalent to the mono_over category. It is more convenient to use the former due to the partial order instance, but oftentimes it is easier to define structures on the latter.

Equations

Use choice to pick a representative mono_over X for each subobject X.

Equations

Starting with A : mono_over X, we can take its equivalence class in subobject X then pick an arbitrary representative using representative.obj. This is isomorphic (in mono_over X) to the original A.

Equations

Use choice to pick a representative underlying object in C for any subobject X.

Prefer to use the coercion P : C rather than explicitly writing underlying.obj P.

Equations

If we construct a subobject Y from an explicit f : X ⟶ Y with [mono f], then pick an arbitrary choice of underlying object (subobject.mk f : C) back in C, it is isomorphic (in C) to the original X.

Equations
noncomputable def category_theory.subobject.arrow {C : Type u₁} [category_theory.category C] {X : C} (Y : category_theory.subobject X) :
Y X

The morphism in C from the arbitrarily chosen underlying object to the ambient object.

Equations
Instances for category_theory.subobject.arrow
@[ext]
theorem category_theory.subobject.eq_of_comp_arrow_eq {C : Type u₁} [category_theory.category C] {X Y : C} {P : category_theory.subobject Y} {f g : X P} (h : f P.arrow = g P.arrow) :
f = g

Two morphisms into a subobject are equal exactly if the morphisms into the ambient object are equal

theorem category_theory.subobject.mk_le_mk_of_comm {C : Type u₁} [category_theory.category C] {B A₁ A₂ : C} {f₁ : A₁ B} {f₂ : A₂ B} [category_theory.mono f₁] [category_theory.mono f₂] (g : A₁ A₂) (w : g f₂ = f₁) :
theorem category_theory.subobject.le_of_comm {C : Type u₁} [category_theory.category C] {B : C} {X Y : category_theory.subobject B} (f : X Y) (w : f Y.arrow = X.arrow) :
X Y
@[ext]
theorem category_theory.subobject.eq_of_comm {C : Type u₁} [category_theory.category C] {B : C} {X Y : category_theory.subobject B} (f : X Y) (w : f.hom Y.arrow = X.arrow) :
X = Y

To show that two subobjects are equal, it suffices to exhibit an isomorphism commuting with the arrows.

@[ext]

To show that two subobjects are equal, it suffices to exhibit an isomorphism commuting with the arrows.

@[ext]

To show that two subobjects are equal, it suffices to exhibit an isomorphism commuting with the arrows.

@[ext]
theorem category_theory.subobject.mk_eq_mk_of_comm {C : Type u₁} [category_theory.category C] {B A₁ A₂ : C} (f : A₁ B) (g : A₂ B) [category_theory.mono f] [category_theory.mono g] (i : A₁ A₂) (w : i.hom g = f) :

To show that two subobjects are equal, it suffices to exhibit an isomorphism commuting with the arrows.

noncomputable def category_theory.subobject.of_le {C : Type u₁} [category_theory.category C] {B : C} (X Y : category_theory.subobject B) (h : X Y) :

An inequality of subobjects is witnessed by some morphism between the corresponding objects.

Equations
Instances for category_theory.subobject.of_le
@[simp]
theorem category_theory.subobject.of_le_arrow_assoc {C : Type u₁} [category_theory.category C] {B : C} {X Y : category_theory.subobject B} (h : X Y) {X' : C} (f' : B X') :
X.of_le Y h Y.arrow f' = X.arrow f'
@[simp]
theorem category_theory.subobject.of_le_arrow {C : Type u₁} [category_theory.category C] {B : C} {X Y : category_theory.subobject B} (h : X Y) :
X.of_le Y h Y.arrow = X.arrow

An inequality of subobjects is witnessed by some morphism between the corresponding objects.

Equations
Instances for category_theory.subobject.of_le_mk

An inequality of subobjects is witnessed by some morphism between the corresponding objects.

Equations
Instances for category_theory.subobject.of_mk_le
noncomputable def category_theory.subobject.of_mk_le_mk {C : Type u₁} [category_theory.category C] {B A₁ A₂ : C} (f : A₁ B) (g : A₂ B) [category_theory.mono f] [category_theory.mono g] (h : category_theory.subobject.mk f category_theory.subobject.mk g) :
A₁ A₂

An inequality of subobjects is witnessed by some morphism between the corresponding objects.

Equations
Instances for category_theory.subobject.of_mk_le_mk
@[simp]
theorem category_theory.subobject.of_le_comp_of_le {C : Type u₁} [category_theory.category C] {B : C} (X Y Z : category_theory.subobject B) (h₁ : X Y) (h₂ : Y Z) :
X.of_le Y h₁ Y.of_le Z h₂ = X.of_le Z _
@[simp]
theorem category_theory.subobject.of_le_comp_of_le_assoc {C : Type u₁} [category_theory.category C] {B : C} (X Y Z : category_theory.subobject B) (h₁ : X Y) (h₂ : Y Z) {X' : C} (f' : Z X') :
X.of_le Y h₁ Y.of_le Z h₂ f' = X.of_le Z _ f'
@[simp]
theorem category_theory.subobject.of_le_comp_of_le_mk_assoc {C : Type u₁} [category_theory.category C] {B A : C} (X Y : category_theory.subobject B) (f : A B) [category_theory.mono f] (h₁ : X Y) (h₂ : Y category_theory.subobject.mk f) {X' : C} (f' : A X') :
X.of_le Y h₁ Y.of_le_mk f h₂ f' = X.of_le_mk f _ f'
@[simp]
theorem category_theory.subobject.of_le_comp_of_le_mk {C : Type u₁} [category_theory.category C] {B A : C} (X Y : category_theory.subobject B) (f : A B) [category_theory.mono f] (h₁ : X Y) (h₂ : Y category_theory.subobject.mk f) :
X.of_le Y h₁ Y.of_le_mk f h₂ = X.of_le_mk f _
noncomputable def category_theory.subobject.iso_of_eq {C : Type u₁} [category_theory.category C] {B : C} (X Y : category_theory.subobject B) (h : X = Y) :

An equality of subobjects gives an isomorphism of the corresponding objects. (One could use underlying.map_iso (eq_to_iso h)) here, but this is more readable.)

Equations
@[simp]
theorem category_theory.subobject.iso_of_eq_inv {C : Type u₁} [category_theory.category C] {B : C} (X Y : category_theory.subobject B) (h : X = Y) :
(X.iso_of_eq Y h).inv = Y.of_le X _
@[simp]
theorem category_theory.subobject.iso_of_eq_hom {C : Type u₁} [category_theory.category C] {B : C} (X Y : category_theory.subobject B) (h : X = Y) :
(X.iso_of_eq Y h).hom = X.of_le Y _

An equality of subobjects gives an isomorphism of the corresponding objects.

Equations

An equality of subobjects gives an isomorphism of the corresponding objects.

Equations
noncomputable def category_theory.subobject.iso_of_mk_eq_mk {C : Type u₁} [category_theory.category C] {B A₁ A₂ : C} (f : A₁ B) (g : A₂ B) [category_theory.mono f] [category_theory.mono g] (h : category_theory.subobject.mk f = category_theory.subobject.mk g) :
A₁ A₂

An equality of subobjects gives an isomorphism of the corresponding objects.

Equations

Any functor mono_over X ⥤ mono_over Y descends to a functor subobject X ⥤ subobject Y, because mono_over Y is thin.

Equations

Isomorphic functors become equal when lowered to subobject. (It's not as evil as usual to talk about equality between functors because the categories are thin and skeletal.)

When C has pullbacks, a morphism f : X ⟶ Y induces a functor subobject Y ⥤ subobject X, by pulling back a monomorphism along f.

Equations
Instances for category_theory.subobject.pullback

We can map subobjects of X to subobjects of Y by post-composition with a monomorphism f : X ⟶ Y.

Equations

In fact, there's a type level bijection between the subobjects of isomorphic objects, which preserves the order.

Equations

The functor from subobjects of X to subobjects of Y given by sending the subobject S to its "image" under f, usually denoted $\exists_f$. For instance, when C is the category of types, viewing subobject X as set X this is just set.image f.

This functor is left adjoint to the pullback f functor (shown in exists_pullback_adj) provided both are defined, and generalises the map f functor, again provided it is defined.

Equations

When f : X ⟶ Y is a monomorphism, exists f agrees with map f.