# Monomorphisms over a fixed object #

As preparation for defining Subobject X, we set up the theory for MonoOver X := { f : Over X // Mono f.hom}.

Here MonoOver 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 MonoOver X.

We provide

• def pullback [HasPullbacks C] (f : X ⟶ Y) : MonoOver Y ⥤ MonoOver X
• def map (f : X ⟶ Y) [Mono f] : MonoOver X ⥤ MonoOver Y
• def «exists» [HasImages C] (f : X ⟶ Y) : MonoOver X ⥤ MonoOver 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 CategoryTheory.MonoOver {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
instance CategoryTheory.instCategoryMonoOver {C : Type u₁} [] (X : C) :
Equations
@[simp]
theorem CategoryTheory.MonoOver.mk'_obj {C : Type u₁} [] {X : C} {A : C} (f : A X) [hf : ] :
def CategoryTheory.MonoOver.mk' {C : Type u₁} [] {X : C} {A : C} (f : A X) [hf : ] :

Construct a MonoOver X.

Equations
• = { obj := , property := hf }
Instances For
def CategoryTheory.MonoOver.forget {C : Type u₁} [] (X : C) :

The inclusion from monomorphisms over X to morphisms over X.

Equations
Instances For
instance CategoryTheory.MonoOver.instCoeOut {C : Type u₁} [] {X : C} :
Equations
• CategoryTheory.MonoOver.instCoeOut = { coe := fun (Y : ) => Y.obj.left }
@[simp]
theorem CategoryTheory.MonoOver.forget_obj_left {C : Type u₁} [] {X : C} {f : } :
(.obj f).left = f.obj.left
@[simp]
theorem CategoryTheory.MonoOver.mk'_coe' {C : Type u₁} [] {X : C} {A : C} (f : A X) :
.obj.left = A
@[reducible, inline]
abbrev CategoryTheory.MonoOver.arrow {C : Type u₁} [] {X : C} (f : ) :
f.obj.left X

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

Equations
• f.arrow = (.obj f).hom
Instances For
@[simp]
theorem CategoryTheory.MonoOver.mk'_arrow {C : Type u₁} [] {X : C} {A : C} (f : A X) :
.arrow = f
@[simp]
theorem CategoryTheory.MonoOver.forget_obj_hom {C : Type u₁} [] {X : C} {f : } :
(.obj f).hom = f.arrow
def CategoryTheory.MonoOver.fullyFaithfulForget {C : Type u₁} [] (X : C) :
.FullyFaithful

The forget functor MonoOver X ⥤ Over X is fully faithful.

Equations
Instances For
instance CategoryTheory.MonoOver.instFullOverForget {C : Type u₁} [] {X : C} :
.Full
Equations
• =
instance CategoryTheory.MonoOver.instFaithfulOverForget {C : Type u₁} [] {X : C} :
.Faithful
Equations
• =
instance CategoryTheory.MonoOver.mono {C : Type u₁} [] {X : C} (f : ) :
Equations
• =
instance CategoryTheory.MonoOver.isThin {C : Type u₁} [] {X : C} :

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

Equations
• =
theorem CategoryTheory.MonoOver.w_assoc {C : Type u₁} [] {X : C} {f : } {g : } (k : f g) {Z : C} (h : X Z) :
theorem CategoryTheory.MonoOver.w {C : Type u₁} [] {X : C} {f : } {g : } (k : f g) :
CategoryTheory.CategoryStruct.comp k.left g.arrow = f.arrow
@[reducible, inline]
abbrev CategoryTheory.MonoOver.homMk {C : Type u₁} [] {X : C} {f : } {g : } (h : f.obj.left g.obj.left) (w : autoParam ( = f.arrow) _auto✝) :
f g

Convenience constructor for a morphism in monomorphisms over X.

Equations
Instances For
@[simp]
theorem CategoryTheory.MonoOver.isoMk_hom {C : Type u₁} [] {X : C} {f : } {g : } (h : f.obj.left g.obj.left) (w : autoParam (CategoryTheory.CategoryStruct.comp h.hom g.arrow = f.arrow) _auto✝) :
.hom =
@[simp]
theorem CategoryTheory.MonoOver.isoMk_inv {C : Type u₁} [] {X : C} {f : } {g : } (h : f.obj.left g.obj.left) (w : autoParam (CategoryTheory.CategoryStruct.comp h.hom g.arrow = f.arrow) _auto✝) :
.inv =
def CategoryTheory.MonoOver.isoMk {C : Type u₁} [] {X : C} {f : } {g : } (h : f.obj.left g.obj.left) (w : autoParam (CategoryTheory.CategoryStruct.comp h.hom g.arrow = f.arrow) _auto✝) :
f g

Convenience constructor for an isomorphism in monomorphisms over X.

Equations
• = { hom := , inv := , hom_inv_id := , inv_hom_id := }
Instances For
def CategoryTheory.MonoOver.mk'ArrowIso {C : Type u₁} [] {X : C} (f : ) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.MonoOver.lift_obj_obj {C : Type u₁} [] {X : C} {D : Type u₂} [] {Y : D} (F : ) (h : ∀ (f : ), CategoryTheory.Mono (F.obj (.obj f)).hom) (f : ) :
(.obj f).obj = F.obj (.obj f)
@[simp]
theorem CategoryTheory.MonoOver.lift_map {C : Type u₁} [] {X : C} {D : Type u₂} [] {Y : D} (F : ) (h : ∀ (f : ), CategoryTheory.Mono (F.obj (.obj f)).hom) :
∀ {X_1 Y_1 : } (k : X_1 Y_1), .map k = (.comp F).map k
def CategoryTheory.MonoOver.lift {C : Type u₁} [] {X : C} {D : Type u₂} [] {Y : D} (F : ) (h : ∀ (f : ), CategoryTheory.Mono (F.obj (.obj f)).hom) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.MonoOver.liftIso {C : Type u₁} [] {X : C} {D : Type u₂} [] {Y : D} {F₁ : } {F₂ : } (h₁ : ∀ (f : ), CategoryTheory.Mono (F₁.obj (.obj f)).hom) (h₂ : ∀ (f : ), CategoryTheory.Mono (F₂.obj (.obj f)).hom) (i : F₁ F₂) :

Isomorphic functors Over Y ⥤ Over X lift to isomorphic functors MonoOver Y ⥤ MonoOver X.

Equations
Instances For
def CategoryTheory.MonoOver.liftComp {C : Type u₁} [] {D : Type u₂} [] {X : C} {Z : C} {Y : D} (F : ) (G : ) (h₁ : ∀ (f : ), CategoryTheory.Mono (F.obj (.obj f)).hom) (h₂ : ∀ (f : ), CategoryTheory.Mono (G.obj (.obj f)).hom) :
().comp () CategoryTheory.MonoOver.lift (F.comp G)

MonoOver.lift commutes with composition of functors.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.MonoOver.liftId {C : Type u₁} [] {X : C} :

MonoOver.lift preserves the identity functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.MonoOver.lift_comm {C : Type u₁} [] {X : C} {Y : C} (F : ) (h : ∀ (f : ), CategoryTheory.Mono (F.obj (.obj f)).hom) :
.comp = .comp F
@[simp]
theorem CategoryTheory.MonoOver.lift_obj_arrow {C : Type u₁} [] {X : C} {D : Type u₂} [] {Y : D} (F : ) (h : ∀ (f : ), CategoryTheory.Mono (F.obj (.obj f)).hom) (f : ) :
(.obj f).arrow = (F.obj (.obj f)).hom
def CategoryTheory.MonoOver.slice {C : Type u₁} [] {A : C} {f : } (h₁ : ∀ (g : ), CategoryTheory.Mono (f.iteratedSliceEquiv.functor.obj (.obj g)).hom) (h₂ : ∀ (g : CategoryTheory.MonoOver f.left), CategoryTheory.Mono (f.iteratedSliceEquiv.inverse.obj (().obj g)).hom) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.MonoOver.pullback {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

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

Equations
Instances For
def CategoryTheory.MonoOver.pullbackComp {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) :

pullback commutes with composition (up to a natural isomorphism)

Equations
• One or more equations did not get rendered due to their size.
Instances For

pullback preserves the identity (up to a natural isomorphism)

Equations
Instances For
@[simp]
theorem CategoryTheory.MonoOver.pullback_obj_left {C : Type u₁} [] {X : C} {Y : C} (f : X Y) (g : ) :
(.obj g).obj.left = CategoryTheory.Limits.pullback g.arrow f
@[simp]
theorem CategoryTheory.MonoOver.pullback_obj_arrow {C : Type u₁} [] {X : C} {Y : C} (f : X Y) (g : ) :
(.obj g).arrow = CategoryTheory.Limits.pullback.snd
def CategoryTheory.MonoOver.map {C : Type u₁} [] {X : C} {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
def CategoryTheory.MonoOver.mapComp {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For

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

Equations
• = ≪≫ CategoryTheory.MonoOver.liftId
Instances For
@[simp]
theorem CategoryTheory.MonoOver.map_obj_left {C : Type u₁} [] {X : C} {Y : C} (f : X Y) (g : ) :
(.obj g).obj.left = g.obj.left
@[simp]
theorem CategoryTheory.MonoOver.map_obj_arrow {C : Type u₁} [] {X : C} {Y : C} (f : X Y) (g : ) :
(.obj g).arrow =
instance CategoryTheory.MonoOver.full_map {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
.Full
Equations
• =
instance CategoryTheory.MonoOver.faithful_map {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
.Faithful
Equations
• =
@[simp]
theorem CategoryTheory.MonoOver.mapIso_counitIso {C : Type u₁} [] {A : C} {B : C} (e : A B) :
.counitIso = (CategoryTheory.MonoOver.mapComp e.inv e.hom).symm ≪≫
@[simp]
theorem CategoryTheory.MonoOver.mapIso_unitIso {C : Type u₁} [] {A : C} {B : C} (e : A B) :
.unitIso = ((CategoryTheory.MonoOver.mapComp e.hom e.inv).symm ≪≫ ).symm
@[simp]
theorem CategoryTheory.MonoOver.mapIso_functor {C : Type u₁} [] {A : C} {B : C} (e : A B) :
.functor =
@[simp]
theorem CategoryTheory.MonoOver.mapIso_inverse {C : Type u₁} [] {A : C} {B : C} (e : A B) :
.inverse =
def CategoryTheory.MonoOver.mapIso {C : Type u₁} [] {A : C} {B : C} (e : A B) :

Isomorphic objects have equivalent MonoOver categories.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.MonoOver.congr_counitIso {C : Type u₁} [] (X : C) {D : Type u₂} [] (e : C D) :
.counitIso = CategoryTheory.NatIso.ofComponents (fun (Y : CategoryTheory.MonoOver (e.functor.obj X)) => CategoryTheory.MonoOver.isoMk (e.counitIso.app Y.obj.left) )
@[simp]
theorem CategoryTheory.MonoOver.congr_unitIso {C : Type u₁} [] (X : C) {D : Type u₂} [] (e : C D) :
.unitIso = CategoryTheory.NatIso.ofComponents (fun (Y : ) => CategoryTheory.MonoOver.isoMk (e.unitIso.app Y.obj.left) )
@[simp]
theorem CategoryTheory.MonoOver.congr_functor {C : Type u₁} [] (X : C) {D : Type u₂} [] (e : C D) :
@[simp]
theorem CategoryTheory.MonoOver.congr_inverse {C : Type u₁} [] (X : C) {D : Type u₂} [] (e : C D) :
.inverse = (CategoryTheory.MonoOver.lift (CategoryTheory.Over.post e.inverse) ).comp (CategoryTheory.MonoOver.mapIso (e.unitIso.symm.app X)).functor
def CategoryTheory.MonoOver.congr {C : Type u₁} [] (X : C) {D : Type u₂} [] (e : C D) :
CategoryTheory.MonoOver (e.functor.obj X)

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.MonoOver.mapPullbackAdj {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.MonoOver.pullbackMapSelf {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

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

Equations
Instances For
def CategoryTheory.MonoOver.imageMonoOver {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.MonoOver.imageMonoOver_arrow {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
@[simp]
theorem CategoryTheory.MonoOver.image_map {C : Type u₁} [] {X : C} {f : } {g : } (k : f g) :
CategoryTheory.MonoOver.image.map k = .preimage (CategoryTheory.Over.homMk (CategoryTheory.Limits.image.lift ()) )
@[simp]
theorem CategoryTheory.MonoOver.image_obj {C : Type u₁} [] {X : C} (f : ) :
CategoryTheory.MonoOver.image.obj f =
def CategoryTheory.MonoOver.image {C : Type u₁} [] {X : C} :

Taking the image of a morphism gives a functor Over X ⥤ MonoOver X.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.MonoOver.imageForgetAdj {C : Type u₁} [] {X : C} :
CategoryTheory.MonoOver.image

MonoOver.image : Over X ⥤ MonoOver X is left adjoint to MonoOver.forget : MonoOver X ⥤ Over X

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.MonoOver.instIsRightAdjointOverForget {C : Type u₁} [] {X : C} :
.IsRightAdjoint
Equations
• =
instance CategoryTheory.MonoOver.reflective {C : Type u₁} [] {X : C} :
Equations
def CategoryTheory.MonoOver.forgetImage {C : Type u₁} [] {X : C} :
.comp CategoryTheory.MonoOver.image

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

Equations
Instances For
def CategoryTheory.MonoOver.exists {C : Type u₁} [] {X : C} {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 MonoOver.map f.

Equations
• = .comp (.comp CategoryTheory.MonoOver.image)
Instances For
instance CategoryTheory.MonoOver.faithful_exists {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
.Faithful
Equations
• =
def CategoryTheory.MonoOver.existsIsoMap {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.MonoOver.existsPullbackAdj {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

exists is adjoint to pullback when images exist

Equations
• One or more equations did not get rendered due to their size.
Instances For