# mathlib3documentation

category_theory.subobject.mono_over

# Monomorphisms over a fixed object #

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

As preparation for defining subobject X, we set up the theory for 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 yet a partial order.

subobject X will be defined as the skeletalization of mono_over X.

We provide

• def pullback [has_pullbacks C] (f : X ⟶ Y) : mono_over Y ⥤ mono_over X
• def map (f : X ⟶ Y) [mono f] : mono_over X ⥤ mono_over Y
• def «exists» [has_images C] (f : X ⟶ Y) : mono_over X ⥤ mono_over Y and prove their basic properties and relationships.

## Notes #

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

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

The category of monomorphisms into X as a full subcategory of the over category. This isn't skeletal, so it's not a partial order.

Later we define subobject X as the quotient of this by isomorphisms.

Equations
Instances for category_theory.mono_over
@[protected, instance]
def category_theory.mono_over.category {C : Type u₁} (X : C) :
def category_theory.mono_over.mk' {C : Type u₁} {X A : C} (f : A X) [hf : category_theory.mono f] :

Construct a mono_over X.

Equations
@[simp]
theorem category_theory.mono_over.mk'_obj {C : Type u₁} {X A : C} (f : A X) [hf : category_theory.mono f] :
def category_theory.mono_over.forget {C : Type u₁} (X : C) :

The inclusion from monomorphisms over X to morphisms over X.

Equations
Instances for category_theory.mono_over.forget
@[protected, instance]
def category_theory.mono_over.has_coe {C : Type u₁} {X : C} :
Equations
@[simp]
theorem category_theory.mono_over.forget_obj_left {C : Type u₁} {X : C}  :
@[simp]
theorem category_theory.mono_over.mk'_coe' {C : Type u₁} {X A : C} (f : A X) [hf : category_theory.mono f] :
@[reducible]
def category_theory.mono_over.arrow {C : Type u₁} {X : C}  :
f X

Convenience notation for the underlying arrow of a monomorphism over X.

@[simp]
theorem category_theory.mono_over.mk'_arrow {C : Type u₁} {X A : C} (f : A X) [hf : category_theory.mono f] :
@[simp]
theorem category_theory.mono_over.forget_obj_hom {C : Type u₁} {X : C}  :
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
def category_theory.mono_over.mono {C : Type u₁} {X : C}  :
@[protected, instance]
def category_theory.mono_over.is_thin {C : Type u₁} {X : C} :

The category of monomorphisms over X is a thin category, which makes defining its skeleton easy.

theorem category_theory.mono_over.w {C : Type u₁} {X : C} {f g : category_theory.mono_over X} (k : f g) :
theorem category_theory.mono_over.w_assoc {C : Type u₁} {X : C} {f g : category_theory.mono_over X} (k : f g) {X' : C} (f' : X X') :
k.left g.arrow f' = f.arrow f'
@[reducible]
def category_theory.mono_over.hom_mk {C : Type u₁} {X : C} {f g : category_theory.mono_over X} (h : f.obj.left g.obj.left) (w : h g.arrow = f.arrow) :
f g

Convenience constructor for a morphism in monomorphisms over X.

@[simp]
theorem category_theory.mono_over.iso_mk_hom {C : Type u₁} {X : C} {f g : category_theory.mono_over X} (h : f.obj.left g.obj.left) (w : h.hom g.arrow = f.arrow) :
def category_theory.mono_over.iso_mk {C : Type u₁} {X : C} {f g : category_theory.mono_over X} (h : f.obj.left g.obj.left) (w : h.hom g.arrow = f.arrow) :
f g

Convenience constructor for an isomorphism in monomorphisms over X.

Equations
@[simp]
theorem category_theory.mono_over.iso_mk_inv {C : Type u₁} {X : C} {f g : category_theory.mono_over X} (h : f.obj.left g.obj.left) (w : h.hom g.arrow = f.arrow) :
@[simp]
def category_theory.mono_over.mk'_arrow_iso {C : Type u₁} {X : C}  :

If f : mono_over X, then mk' f.arrow is of course just f, but not definitionally, so we package it as an isomorphism.

Equations
def category_theory.mono_over.lift {C : Type u₁} {X : C} {D : Type u₂} {Y : D} (h : (f : , ) :

Lift a functor between over categories to a functor between mono_over categories, given suitable evidence that morphisms are taken to monomorphisms.

Equations
@[simp]
theorem category_theory.mono_over.lift_map {C : Type u₁} {X : C} {D : Type u₂} {Y : D} (h : (f : , ) (_x _x_1 : category_theory.mono_over Y) (k : _x _x_1) :
@[simp]
theorem category_theory.mono_over.lift_obj_obj {C : Type u₁} {X : C} {D : Type u₂} {Y : D} (h : (f : , )  :
f).obj = F.obj
def category_theory.mono_over.lift_iso {C : Type u₁} {X : C} {D : Type u₂} {Y : D} {F₁ F₂ : } (h₁ : (f : , category_theory.mono (F₁.obj f)).hom) (h₂ : (f : , category_theory.mono (F₂.obj f)).hom) (i : F₁ F₂) :

Isomorphic functors over Y ⥤ over X lift to isomorphic functors mono_over Y ⥤ mono_over X.

Equations
def category_theory.mono_over.lift_comp {C : Type u₁} {D : Type u₂} {X Z : C} {Y : D} (h₁ : (f : , ) (h₂ : (f : , ) :

mono_over.lift commutes with composition of functors.

Equations
def category_theory.mono_over.lift_id {C : Type u₁} {X : C} :
category_theory.mono_over.lift_id._proof_1

mono_over.lift preserves the identity functor.

Equations
@[simp]
theorem category_theory.mono_over.lift_comm {C : Type u₁} {X Y : C} (h : (f : , ) :
@[simp]
theorem category_theory.mono_over.lift_obj_arrow {C : Type u₁} {X : C} {D : Type u₂} {Y : D} (h : (f : , )  :
f).arrow = (F.obj f)).hom
def category_theory.mono_over.slice {C : Type u₁} {A : C} {f : category_theory.over A} (h₁ : (f_1 : , ) (h₂ : (f_1 : , ) :

Monomorphisms over an object f : over A in an over category are equivalent to monomorphisms over the source of f.

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

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

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

pullback commutes with composition (up to a natural isomorphism)

Equations
noncomputable def category_theory.mono_over.pullback_id {C : Type u₁} {X : C}  :

pullback preserves the identity (up to a natural isomorphism)

Equations
@[simp]
theorem category_theory.mono_over.pullback_obj_left {C : Type u₁} {X Y : C} (f : X Y)  :
@[simp]
theorem category_theory.mono_over.pullback_obj_arrow {C : Type u₁} {X Y : C} (f : X Y)  :
def category_theory.mono_over.map {C : Type u₁} {X Y : C} (f : X Y)  :

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

Equations
Instances for category_theory.mono_over.map
def category_theory.mono_over.map_comp {C : Type u₁} {X Y Z : C} (f : X Y) (g : Y Z)  :

mono_over.map commutes with composition (up to a natural isomorphism).

Equations
def category_theory.mono_over.map_id {C : Type u₁} {X : C} :

mono_over.map preserves the identity (up to a natural isomorphism).

Equations
@[simp]
theorem category_theory.mono_over.map_obj_left {C : Type u₁} {X Y : C} (f : X Y)  :
g) = g.obj.left
@[simp]
theorem category_theory.mono_over.map_obj_arrow {C : Type u₁} {X Y : C} (f : X Y)  :
g).arrow = g.arrow f
@[protected, instance]
def category_theory.mono_over.full_map {C : Type u₁} {X Y : C} (f : X Y)  :
Equations
@[protected, instance]
def category_theory.mono_over.faithful_map {C : Type u₁} {X Y : C} (f : X Y)  :
@[simp]
theorem category_theory.mono_over.map_iso_functor {C : Type u₁} {A B : C} (e : A B) :
def category_theory.mono_over.map_iso {C : Type u₁} {A B : C} (e : A B) :

Isomorphic objects have equivalent mono_over categories.

Equations
@[simp]
theorem category_theory.mono_over.map_iso_unit_iso {C : Type u₁} {A B : C} (e : A B) :
@[simp]
theorem category_theory.mono_over.map_iso_inverse {C : Type u₁} {A B : C} (e : A B) :
@[simp]
theorem category_theory.mono_over.map_iso_counit_iso {C : Type u₁} {A B : C} (e : A B) :
@[simp]
theorem category_theory.mono_over.congr_functor {C : Type u₁} (X : C) {D : Type u₂} (e : C D) :
@[simp]
theorem category_theory.mono_over.congr_inverse {C : Type u₁} (X : C) {D : Type u₂} (e : C D) :
@[simp]
theorem category_theory.mono_over.congr_unit_iso {C : Type u₁} (X : C) {D : Type u₂} (e : C D) :
@[simp]
theorem category_theory.mono_over.congr_counit_iso {C : Type u₁} (X : C) {D : Type u₂} (e : C D) :
def category_theory.mono_over.congr {C : Type u₁} (X : C) {D : Type u₂} (e : C D) :

An equivalence of categories e between C and D induces an equivalence between mono_over X and mono_over (e.functor.obj X) whenever X is an object of C.

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

map f is left adjoint to pullback f when f is a monomorphism

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

mono_over.map f followed by mono_over.pullback f is the identity.

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

The mono_over Y for the image inclusion for a morphism f : X ⟶ Y.

Equations
@[simp]
theorem category_theory.mono_over.image_mono_over_arrow {C : Type u₁} {X Y : C} (f : X Y)  :
@[simp]
noncomputable def category_theory.mono_over.image {C : Type u₁} {X : C}  :

Taking the image of a morphism gives a functor over X ⥤ mono_over X.

Equations
@[simp]
theorem category_theory.mono_over.image_map {C : Type u₁} {X : C} (f g : category_theory.over X) (k : f g) :
noncomputable def category_theory.mono_over.image_forget_adj {C : Type u₁} {X : C}  :

mono_over.image : over X ⥤ mono_over X is left adjoint to mono_over.forget : mono_over X ⥤ over X

Equations
@[protected, instance]
Equations
@[protected, instance]
noncomputable def category_theory.mono_over.reflective {C : Type u₁} {X : C}  :
Equations
noncomputable def category_theory.mono_over.forget_image {C : Type u₁} {X : C}  :

Forgetting that a monomorphism over X is a monomorphism, then taking its image, is the identity functor.

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

In the case where f is not a monomorphism but C has images, we can still take the "forward map" under it, which agrees with mono_over.map f.

Equations
Instances for category_theory.mono_over.exists
@[protected, instance]
def category_theory.mono_over.faithful_exists {C : Type u₁} {X Y : C} (f : X Y) :
noncomputable def category_theory.mono_over.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.

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

exists is adjoint to pullback when images exist

Equations