# mathlib3documentation

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

• `def pullback [has_pullbacks C] (f : X ⟶ Y) : subobject Y ⥤ subobject X`
• `def map (f : X ⟶ Y) [mono f] : subobject X ⥤ subobject Y`
• `def «exists» [has_images C] (f : X ⟶ Y) : subobject X ⥤ subobject Y` and prove their basic properties and relationships. These are all easy consequences of the earlier development of the corresponding functors for `mono_over`.

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

• `category_theory.subobject.factor_thru` : an API describing factorization of morphisms through subobjects.
• `category_theory.subobject.lattice` : the lattice structures on subobjects.

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

def category_theory.subobject {C : Type u₁} (X : C) :
Type (max u₁ v₁)

The category of subobjects of `X : C`, defined as isomorphism classes of monomorphisms into `X`.

Equations
Instances for `category_theory.subobject`
@[protected, instance]
def category_theory.subobject.partial_order {C : Type u₁} (X : C) :
@[protected, instance]
def category_theory.subobject.category {C : Type u₁} (X : C) :
@[reducible]
def category_theory.subobject.mk {C : Type u₁} {X A : C} (f : A X)  :

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 : 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 : R) :
x = y x.left = y.left x.right = y.right x.hom == y.hom
@[protected]
theorem category_theory.subobject.ind {C : Type u₁} {X : C} (p : Prop) (h : ⦃A : C⦄ (f : A X) [_inst_3 : , )  :
p P
@[protected]
theorem category_theory.subobject.ind₂ {C : Type u₁} {X : C} (p : ) (h : ⦃A B : C⦄ (f : A X) (g : B X) [_inst_3 : [_inst_4 : , ) (P Q : category_theory.subobject X) :
p P Q
@[protected]
def category_theory.subobject.lift {C : Type u₁} {α : Sort u_1} {X : C} (F : Π ⦃A : C⦄ (f : A X) [_inst_3 : , α) (h : ⦃A B : C⦄ (f : A X) (g : B X) [_inst_4 : [_inst_5 : (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
• = λ (P : , (λ (m : , F m.arrow) _
@[protected, simp]
theorem category_theory.subobject.lift_mk {C : Type u₁} {α : Sort u_1} {X : C} (F : Π ⦃A : C⦄ (f : A X) [_inst_3 : , α) {h : ⦃A B : C⦄ (f : A X) (g : B X) [_inst_4 : [_inst_5 : (i : A B), i.hom g = f F f = F g} {A : C} (f : A X)  :
noncomputable def category_theory.subobject.equiv_mono_over {C : Type u₁} (X : C) :

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
noncomputable def category_theory.subobject.representative {C : Type u₁} {X : C} :

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

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

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
noncomputable def category_theory.subobject.underlying {C : Type u₁} {X : C} :

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
@[protected, instance]
noncomputable def category_theory.subobject.has_coe {C : Type u₁} {X : C} :
Equations
@[simp]
theorem category_theory.subobject.underlying_as_coe {C : Type u₁} {X : C}  :
noncomputable def category_theory.subobject.underlying_iso {C : Type u₁} {X Y : C} (f : X Y)  :

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₁} {X : C}  :
Y X

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

Equations
Instances for `category_theory.subobject.arrow`
@[protected, instance]
def category_theory.subobject.arrow_mono {C : Type u₁} {X : C}  :
@[simp]
theorem category_theory.subobject.arrow_congr {C : Type u₁} {A : C} (X Y : category_theory.subobject A) (h : X = Y) :
@[simp]
theorem category_theory.subobject.representative_coe {C : Type u₁} {X : C}  :
@[simp]
theorem category_theory.subobject.representative_arrow {C : Type u₁} {X : C}  :
@[simp]
theorem category_theory.subobject.underlying_arrow {C : Type u₁} {X : C} {Y Z : category_theory.subobject X} (f : Y Z) :
@[simp]
theorem category_theory.subobject.underlying_arrow_assoc {C : Type u₁} {X : C} {Y Z : category_theory.subobject X} (f : Y Z) {X' : C} (f' : X X') :
= Y.arrow f'
@[simp]
theorem category_theory.subobject.underlying_iso_arrow_apply {C : Type u₁} {X Y : C} (f : X Y) (x : X) :
= f x
@[simp]
theorem category_theory.subobject.underlying_iso_arrow {C : Type u₁} {X Y : C} (f : X Y)  :
@[simp]
theorem category_theory.subobject.underlying_iso_arrow_assoc {C : Type u₁} {X Y : C} (f : X Y) {X' : C} (f' : Y X') :
= f f'
@[simp]
theorem category_theory.subobject.underlying_iso_hom_comp_eq_mk_assoc {C : Type u₁} {X Y : C} (f : X Y) {X' : C} (f' : Y X') :
=
@[simp]
theorem category_theory.subobject.underlying_iso_hom_comp_eq_mk {C : Type u₁} {X Y : C} (f : X Y)  :
@[ext]
theorem category_theory.subobject.eq_of_comp_arrow_eq {C : Type u₁} {X Y : C} {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₁} {B A₁ A₂ : C} {f₁ : A₁ B} {f₂ : A₂ B} (g : A₁ A₂) (w : g f₂ = f₁) :
@[simp]
theorem category_theory.subobject.mk_arrow {C : Type u₁} {X : C}  :
theorem category_theory.subobject.le_of_comm {C : Type u₁} {B : C} {X Y : category_theory.subobject B} (f : X Y) (w : f Y.arrow = X.arrow) :
X Y
theorem category_theory.subobject.le_mk_of_comm {C : Type u₁} {B A : C} {f : A B} (g : X A) (w : g f = X.arrow) :
theorem category_theory.subobject.mk_le_of_comm {C : Type u₁} {B A : C} {f : A B} (g : A X) (w : g X.arrow = f) :
@[ext]
theorem category_theory.subobject.eq_of_comm {C : Type u₁} {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]
theorem category_theory.subobject.eq_mk_of_comm {C : Type u₁} {B A : C} (f : A B) (i : X A) (w : i.hom f = X.arrow) :

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

@[ext]
theorem category_theory.subobject.mk_eq_of_comm {C : Type u₁} {B A : C} (f : A B) (i : A X) (w : i.hom X.arrow = f) :

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₁} {B A₁ A₂ : C} (f : A₁ B) (g : A₂ B) (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₁} {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₁} {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₁} {B : C} {X Y : category_theory.subobject B} (h : X Y) :
X.of_le Y h Y.arrow = X.arrow
@[protected, instance]
theorem category_theory.subobject.of_le_mk_le_mk_of_comm {C : Type u₁} {B A₁ A₂ : C} {f₁ : A₁ B} {f₂ : A₂ B} (g : A₁ A₂) (w : g f₂ = f₁) :
@[protected, instance]
def category_theory.subobject.of_le_mk.mono {C : Type u₁} {B A : C} (f : A B) (h : X ) :
noncomputable def category_theory.subobject.of_le_mk {C : Type u₁} {B A : C} (f : A B) (h : X ) :
X A

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

Equations
Instances for `category_theory.subobject.of_le_mk`
@[simp]
theorem category_theory.subobject.of_le_mk_comp {C : Type u₁} {B A : C} {f : A B} (h : X ) :
X.of_le_mk f h f = X.arrow
@[protected, instance]
def category_theory.subobject.of_mk_le.mono {C : Type u₁} {B A : C} (f : A B) (h : X) :
noncomputable def category_theory.subobject.of_mk_le {C : Type u₁} {B A : C} (f : A B) (h : X) :
A X

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

Equations
Instances for `category_theory.subobject.of_mk_le`
@[simp]
theorem category_theory.subobject.of_mk_le_arrow {C : Type u₁} {B A : C} {f : A B} (h : X) :
= f
@[protected, instance]
def category_theory.subobject.of_mk_le_mk.mono {C : Type u₁} {B A₁ A₂ : C} (f : A₁ B) (g : A₂ B)  :
noncomputable def category_theory.subobject.of_mk_le_mk {C : Type u₁} {B A₁ A₂ : C} (f : A₁ B) (g : A₂ B)  :
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_mk_le_mk_comp {C : Type u₁} {B A₁ A₂ : C} {f : A₁ B} {g : A₂ B}  :
= f
@[simp]
theorem category_theory.subobject.of_le_comp_of_le {C : Type u₁} {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₁} {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₁} {B A : C} (X Y : category_theory.subobject B) (f : A B) (h₁ : X Y) (h₂ : Y ) {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₁} {B A : C} (X Y : category_theory.subobject B) (f : A B) (h₁ : X Y) (h₂ : Y ) :
X.of_le Y h₁ Y.of_le_mk f h₂ = X.of_le_mk f _
@[simp]
theorem category_theory.subobject.of_le_mk_comp_of_mk_le {C : Type u₁} {B A : C} (f : A B) (h₁ : X ) (h₂ : Y) :
X.of_le_mk f h₁ = X.of_le Y _
@[simp]
theorem category_theory.subobject.of_le_mk_comp_of_mk_le_assoc {C : Type u₁} {B A : C} (f : A B) (h₁ : X ) (h₂ : Y) {X' : C} (f' : Y X') :
X.of_le_mk f h₁ f' = X.of_le Y _ f'
@[simp]
theorem category_theory.subobject.of_le_mk_comp_of_mk_le_mk_assoc {C : Type u₁} {B A₁ A₂ : C} (f : A₁ B) (g : A₂ B) (h₁ : X ) {X' : C} (f' : A₂ X') :
X.of_le_mk f h₁ = X.of_le_mk g _ f'
@[simp]
theorem category_theory.subobject.of_le_mk_comp_of_mk_le_mk {C : Type u₁} {B A₁ A₂ : C} (f : A₁ B) (g : A₂ B) (h₁ : X )  :
X.of_le_mk f h₁ = X.of_le_mk g _
@[simp]
theorem category_theory.subobject.of_mk_le_comp_of_le_assoc {C : Type u₁} {B A₁ : C} (f : A₁ B) (X Y : category_theory.subobject B) (h₁ : X) (h₂ : X Y) {X' : C} (f' : Y X') :
X.of_le Y h₂ f' =
@[simp]
theorem category_theory.subobject.of_mk_le_comp_of_le {C : Type u₁} {B A₁ : C} (f : A₁ B) (X Y : category_theory.subobject B) (h₁ : X) (h₂ : X Y) :
X.of_le Y h₂ =
@[simp]
theorem category_theory.subobject.of_mk_le_comp_of_le_mk {C : Type u₁} {B A₁ A₂ : C} (f : A₁ B) (g : A₂ B) (h₁ : X) (h₂ : X ) :
X.of_le_mk g h₂ =
@[simp]
theorem category_theory.subobject.of_mk_le_comp_of_le_mk_assoc {C : Type u₁} {B A₁ A₂ : C} (f : A₁ B) (g : A₂ B) (h₁ : X) (h₂ : X ) {X' : C} (f' : A₂ X') :
X.of_le_mk g h₂ f' =
@[simp]
theorem category_theory.subobject.of_mk_le_mk_comp_of_mk_le {C : Type u₁} {B A₁ A₂ : C} (f : A₁ B) (g : A₂ B) (h₂ : X) :
@[simp]
theorem category_theory.subobject.of_mk_le_mk_comp_of_mk_le_assoc {C : Type u₁} {B A₁ A₂ : C} (f : A₁ B) (g : A₂ B) (h₂ : X) {X' : C} (f' : X X') :
=
@[simp]
theorem category_theory.subobject.of_mk_le_mk_comp_of_mk_le_mk {C : Type u₁} {B A₁ A₂ A₃ : C} (f : A₁ B) (g : A₂ B) (h : A₃ B)  :
@[simp]
theorem category_theory.subobject.of_mk_le_mk_comp_of_mk_le_mk_assoc {C : Type u₁} {B A₁ A₂ A₃ : C} (f : A₁ B) (g : A₂ B) (h : A₃ B) {X' : C} (f' : A₃ X') :
=
@[simp]
theorem category_theory.subobject.of_le_refl {C : Type u₁} {B : C}  :
@[simp]
theorem category_theory.subobject.of_mk_le_mk_refl {C : Type u₁} {B A₁ : C} (f : A₁ B)  :
noncomputable def category_theory.subobject.iso_of_eq {C : Type u₁} {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₁} {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₁} {B : C} (X Y : category_theory.subobject B) (h : X = Y) :
(X.iso_of_eq Y h).hom = X.of_le Y _
noncomputable def category_theory.subobject.iso_of_eq_mk {C : Type u₁} {B A : C} (f : A B) (h : X = ) :
X A

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

Equations
@[simp]
theorem category_theory.subobject.iso_of_eq_mk_hom {C : Type u₁} {B A : C} (f : A B) (h : X = ) :
(X.iso_of_eq_mk f h).hom = X.of_le_mk f _
@[simp]
theorem category_theory.subobject.iso_of_eq_mk_inv {C : Type u₁} {B A : C} (f : A B) (h : X = ) :
(X.iso_of_eq_mk f h).inv =
noncomputable def category_theory.subobject.iso_of_mk_eq {C : Type u₁} {B A : C} (f : A B) (h : = X) :
A X

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

Equations
@[simp]
theorem category_theory.subobject.iso_of_mk_eq_hom {C : Type u₁} {B A : C} (f : A B) (h : = X) :
@[simp]
theorem category_theory.subobject.iso_of_mk_eq_inv {C : Type u₁} {B A : C} (f : A B) (h : = X) :
= X.of_le_mk f _
@[simp]
theorem category_theory.subobject.iso_of_mk_eq_mk_inv {C : Type u₁} {B A₁ A₂ : C} (f : A₁ B) (g : A₂ B)  :
@[simp]
theorem category_theory.subobject.iso_of_mk_eq_mk_hom {C : Type u₁} {B A₁ A₂ : C} (f : A₁ B) (g : A₂ B)  :
noncomputable def category_theory.subobject.iso_of_mk_eq_mk {C : Type u₁} {B A₁ A₂ : C} (f : A₁ B) (g : A₂ B)  :
A₁ A₂

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

Equations
def category_theory.subobject.lower {C : Type u₁} {X : C} {D : Type u₂} {Y : D}  :

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

Equations
theorem category_theory.subobject.lower_iso {C : Type u₁} {X Y : C} (F₁ F₂ : ) (h : F₁ F₂) :

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

def category_theory.subobject.lower₂ {C : Type u₁} {X Y Z : C}  :

A ternary version of `subobject.lower`.

Equations
@[simp]
def category_theory.subobject.lower_adjunction {C : Type u₁} {D : Type u₂} {A : C} {B : D} (h : L R) :

An adjunction between `mono_over A` and `mono_over B` gives an adjunction between `subobject A` and `subobject B`.

Equations
@[simp]
theorem category_theory.subobject.lower_equivalence_counit_iso {C : Type u₁} {D : Type u₂} {A : C} {B : D}  :
@[simp]
theorem category_theory.subobject.lower_equivalence_unit_iso {C : Type u₁} {D : Type u₂} {A : C} {B : D}  :
@[simp]
theorem category_theory.subobject.lower_equivalence_inverse {C : Type u₁} {D : Type u₂} {A : C} {B : D}  :
def category_theory.subobject.lower_equivalence {C : Type u₁} {D : Type u₂} {A : C} {B : D}  :

An equivalence between `mono_over A` and `mono_over B` gives an equivalence between `subobject A` and `subobject B`.

Equations
@[simp]
theorem category_theory.subobject.lower_equivalence_functor {C : Type u₁} {D : Type u₂} {A : C} {B : D}  :
noncomputable def category_theory.subobject.pullback {C : Type u₁} {X Y : C} (f : X Y) :

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`
theorem category_theory.subobject.pullback_id {C : Type u₁} {X : C}  :
= x
theorem category_theory.subobject.pullback_comp {C : Type u₁} {X Y Z : C} (f : X Y) (g : Y Z)  :
@[protected, instance]
def category_theory.subobject.map {C : Type u₁} {X Y : C} (f : X Y)  :

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

Equations
theorem category_theory.subobject.map_id {C : Type u₁} {X : C}  :
x = x
theorem category_theory.subobject.map_comp {C : Type u₁} {X Y Z : C} (f : X Y) (g : Y Z)  :
def category_theory.subobject.map_iso {C : Type u₁} {A B : C} (e : A B) :

Isomorphic objects have equivalent subobject lattices.

Equations
def category_theory.subobject.map_iso_to_order_iso {C : Type u₁} {X Y : C} (e : X Y) :

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

Equations
@[simp]
theorem category_theory.subobject.map_iso_to_order_iso_apply {C : Type u₁} {X Y : C} (e : X Y)  :
@[simp]
theorem category_theory.subobject.map_iso_to_order_iso_symm_apply {C : Type u₁} {X Y : C} (e : X Y)  :
noncomputable def category_theory.subobject.map_pullback_adj {C : Type u₁} {X Y : C} (f : X Y)  :

`map f : subobject X ⥤ subobject Y` is the left adjoint of `pullback f : subobject Y ⥤ subobject X`.

Equations
@[simp]
theorem category_theory.subobject.pullback_map_self {C : Type u₁} {X Y : C} (f : X Y)  :
theorem category_theory.subobject.map_pullback {C : Type u₁} {X Y Z W : C} {f : X Y} {g : X Z} {h : Y W} {k : Z W} (comm : f h = g k)  :
noncomputable def category_theory.subobject.exists {C : Type u₁} {X Y : C} (f : X Y) :

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
theorem category_theory.subobject.exists_iso_map {C : Type u₁} {X Y : C} (f : X Y)  :

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

noncomputable def category_theory.subobject.exists_pullback_adj {C : Type u₁} {X Y : C} (f : X Y)  :

`exists f : subobject X ⥤ subobject Y` is left adjoint to `pullback f : subobject Y ⥤ subobject X`.

Equations