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 Kim Morrison.

@[reducible, inline]

abbrev CategoryTheory.Over.isMono {C : Type u₁} [Category.{v₁, u₁} C] (X : C) : ObjectProperty (Over X)

The object property in Over X of the structure morphism being a monomorphism.

@[reducible, inline]

abbrev CategoryTheory.MonoOver {C : Type u₁} [Category.{v₁, u₁} C] (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.

instance CategoryTheory.MonoOver.mono_obj_hom {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : MonoOver X) : Mono S.obj.hom

def CategoryTheory.MonoOver.mk {C : Type u₁} [Category.{v₁, u₁} C] {X A : C} (f : A ⟶ X) [hf : Mono f] : MonoOver X

Construct a MonoOver X.

@[simp]

theorem CategoryTheory.MonoOver.mk_obj {C : Type u₁} [Category.{v₁, u₁} C] {X A : C} (f : A ⟶ X) [hf : Mono f] : (mk f).obj = Over.mk f

@[deprecated CategoryTheory.MonoOver.mk (since := "2025-12-18")]

def CategoryTheory.MonoOver.mk' {C : Type u₁} [Category.{v₁, u₁} C] {X A : C} (f : A ⟶ X) [hf : Mono f] : MonoOver X

Alias of CategoryTheory.MonoOver.mk.

---

Construct a MonoOver X.

@[reducible, inline]

abbrev CategoryTheory.MonoOver.forget {C : Type u₁} [Category.{v₁, u₁} C] (X : C) : Functor (MonoOver X) (Over X)

The inclusion from monomorphisms over X to morphisms over X.

instance CategoryTheory.MonoOver.instCoeOut {C : Type u₁} [Category.{v₁, u₁} C] {X : C} : CoeOut (MonoOver X) C

@[simp]

theorem CategoryTheory.MonoOver.forget_obj_left {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {f : MonoOver X} : ((forget X).obj f).left = f.obj.left

@[simp]

theorem CategoryTheory.MonoOver.mk_coe {C : Type u₁} [Category.{v₁, u₁} C] {X A : C} (f : A ⟶ X) [Mono f] : (mk f).obj.left = A

@[deprecated CategoryTheory.MonoOver.mk_coe (since := "2025-12-18")]

theorem CategoryTheory.MonoOver.mk'_coe' {C : Type u₁} [Category.{v₁, u₁} C] {X A : C} (f : A ⟶ X) [Mono f] : (mk f).obj.left = A

Alias of CategoryTheory.MonoOver.mk_coe.

@[reducible, inline]

abbrev CategoryTheory.MonoOver.arrow {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (f : MonoOver X) : f.obj.left ⟶ X

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

@[simp]

theorem CategoryTheory.MonoOver.mk_arrow {C : Type u₁} [Category.{v₁, u₁} C] {X A : C} (f : A ⟶ X) [Mono f] : (mk f).arrow = f

@[deprecated CategoryTheory.MonoOver.mk_arrow (since := "2025-12-18")]

theorem CategoryTheory.MonoOver.mk'_arrow {C : Type u₁} [Category.{v₁, u₁} C] {X A : C} (f : A ⟶ X) [Mono f] : (mk f).arrow = f

Alias of CategoryTheory.MonoOver.mk_arrow.

theorem CategoryTheory.MonoOver.forget_obj_hom {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {f : MonoOver X} : ((forget X).obj f).hom = f.arrow

def CategoryTheory.MonoOver.fullyFaithfulForget {C : Type u₁} [Category.{v₁, u₁} C] (X : C) : (forget X).FullyFaithful

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

instance CategoryTheory.MonoOver.mono {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (f : MonoOver X) : Mono f.arrow

instance CategoryTheory.MonoOver.instMonoHomDiscretePUnitObjOverForget {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {f : MonoOver X} : Mono ((forget X).obj f).hom

instance CategoryTheory.MonoOver.isThin {C : Type u₁} [Category.{v₁, u₁} C] {X : C} : Quiver.IsThin (MonoOver X)

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

theorem CategoryTheory.MonoOver.w {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {f g : MonoOver X} (k : f ⟶ g) : CategoryStruct.comp k.hom.left g.arrow = f.arrow

theorem CategoryTheory.MonoOver.w_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {f g : MonoOver X} (k : f ⟶ g) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp k.hom.left (CategoryStruct.comp g.arrow h) = CategoryStruct.comp f.arrow h

@[reducible, inline]

abbrev CategoryTheory.MonoOver.homMk {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {f g : MonoOver X} (h : f.obj.left ⟶ g.obj.left) (w : CategoryStruct.comp h g.arrow = f.arrow := by aesop_cat) : f ⟶ g

Convenience constructor for a morphism in monomorphisms over X.

def CategoryTheory.MonoOver.isoMk {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {f g : MonoOver X} (h : f.obj.left ≅ g.obj.left) (w : CategoryStruct.comp h.hom g.arrow = f.arrow := by cat_disch) : f ≅ g

Convenience constructor for an isomorphism in monomorphisms over X.

@[simp]

theorem CategoryTheory.MonoOver.isoMk_inv {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {f g : MonoOver X} (h : f.obj.left ≅ g.obj.left) (w : CategoryStruct.comp h.hom g.arrow = f.arrow := by cat_disch) : (isoMk h w).inv = homMk h.inv ⋯

@[simp]

theorem CategoryTheory.MonoOver.isoMk_hom {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {f g : MonoOver X} (h : f.obj.left ≅ g.obj.left) (w : CategoryStruct.comp h.hom g.arrow = f.arrow := by cat_disch) : (isoMk h w).hom = homMk h.hom w

def CategoryTheory.MonoOver.mkArrowIso {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (f : MonoOver X) : mk f.arrow ≅ f

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

@[simp]

theorem CategoryTheory.MonoOver.mkArrowIso_inv_hom_left {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (f : MonoOver X) : f.mkArrowIso.inv.hom.left = CategoryStruct.id f.obj.left

@[simp]

theorem CategoryTheory.MonoOver.mkArrowIso_hom_hom_left {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (f : MonoOver X) : f.mkArrowIso.hom.hom.left = CategoryStruct.id f.obj.left

@[deprecated CategoryTheory.MonoOver.mkArrowIso (since := "2025-12-18")]

def CategoryTheory.MonoOver.mk'ArrowIso {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (f : MonoOver X) : mk f.arrow ≅ f

Alias of CategoryTheory.MonoOver.mkArrowIso.

---

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

instance CategoryTheory.MonoOver.instIsIsoLeftDiscretePUnitHomFullSubcategoryOverIsMono {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {A B : MonoOver X} (f : A ⟶ B) [IsIso f] : IsIso f.hom.left

theorem CategoryTheory.MonoOver.isIso_iff_isIso_hom_left {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {A B : MonoOver X} (f : A ⟶ B) : IsIso f ↔ IsIso f.hom.left

@[deprecated CategoryTheory.MonoOver.isIso_iff_isIso_hom_left (since := "2025-12-18")]

theorem CategoryTheory.MonoOver.isIso_iff_isIso_left {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {A B : MonoOver X} (f : A ⟶ B) : IsIso f ↔ IsIso f.hom.left

Alias of CategoryTheory.MonoOver.isIso_iff_isIso_hom_left.

def CategoryTheory.MonoOver.lift {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {D : Type u₂} [Category.{v₂, u₂} D] {Y : D} (F : Functor (Over Y) (Over X)) (h : ∀ (f : MonoOver Y), Mono (F.obj ((forget Y).obj f)).hom) : Functor (MonoOver Y) (MonoOver X)

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

@[simp]

theorem CategoryTheory.MonoOver.lift_obj_obj {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {D : Type u₂} [Category.{v₂, u₂} D] {Y : D} (F : Functor (Over Y) (Over X)) (h : ∀ (f : MonoOver Y), Mono (F.obj ((forget Y).obj f)).hom) (X✝ : MonoOver Y) : ((lift F h).obj X✝).obj = F.obj X✝.obj

@[simp]

theorem CategoryTheory.MonoOver.lift_map_hom {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {D : Type u₂} [Category.{v₂, u₂} D] {Y : D} (F : Functor (Over Y) (Over X)) (h : ∀ (f : MonoOver Y), Mono (F.obj ((forget Y).obj f)).hom) {X✝ Y✝ : MonoOver Y} (f : X✝ ⟶ Y✝) : ((lift F h).map f).hom = F.map f.hom

def CategoryTheory.MonoOver.liftIso {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {D : Type u₂} [Category.{v₂, u₂} D] {Y : D} {F₁ F₂ : Functor (Over Y) (Over X)} (h₁ : ∀ (f : MonoOver Y), Mono (F₁.obj ((forget Y).obj f)).hom) (h₂ : ∀ (f : MonoOver Y), Mono (F₂.obj ((forget Y).obj f)).hom) (i : F₁ ≅ F₂) : lift F₁ h₁ ≅ lift F₂ h₂

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

def CategoryTheory.MonoOver.liftComp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X Z : C} {Y : D} (F : Functor (Over X) (Over Y)) (G : Functor (Over Y) (Over Z)) (h₁ : ∀ (f : MonoOver X), Mono (F.obj ((forget X).obj f)).hom) (h₂ : ∀ (f : MonoOver Y), Mono (G.obj ((forget Y).obj f)).hom) : (lift F h₁).comp (lift G h₂) ≅ lift (F.comp G) ⋯

MonoOver.lift commutes with composition of functors.

def CategoryTheory.MonoOver.liftId {C : Type u₁} [Category.{v₁, u₁} C] {X : C} : lift (Functor.id (Over X)) ⋯ ≅ Functor.id (MonoOver X)

MonoOver.lift preserves the identity functor.

@[simp]

theorem CategoryTheory.MonoOver.lift_comm {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (F : Functor (Over Y) (Over X)) (h : ∀ (f : MonoOver Y), Mono (F.obj ((forget Y).obj f)).hom) : (lift F h).comp (forget X) = (forget Y).comp F

@[simp]

theorem CategoryTheory.MonoOver.lift_obj_arrow {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {D : Type u₂} [Category.{v₂, u₂} D] {Y : D} (F : Functor (Over Y) (Over X)) (h : ∀ (f : MonoOver Y), Mono (F.obj ((forget Y).obj f)).hom) (f : MonoOver Y) : ((lift F h).obj f).arrow = (F.obj ((forget Y).obj f)).hom

def CategoryTheory.MonoOver.slice {C : Type u₁} [Category.{v₁, u₁} C] {A : C} {f : Over A} (h₁ : ∀ (g : MonoOver f), Mono (f.iteratedSliceEquiv.functor.obj ((forget f).obj g)).hom) (h₂ : ∀ (g : MonoOver f.left), Mono (f.iteratedSliceEquiv.inverse.obj ((forget f.left).obj g)).hom) : MonoOver f ≌ MonoOver f.left

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

instance CategoryTheory.MonoOver.instIsClosedUnderLimitsOfShapeOverIsMono {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₃} [Category.{v₃, u₃} J] (X : C) : (Over.isMono X).IsClosedUnderLimitsOfShape J

instance CategoryTheory.MonoOver.hasLimit {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₃} [Category.{v₃, u₃} J] (X : C) (F : Functor J (MonoOver X)) [Limits.HasLimit (F.comp (Over.isMono X).ι)] : Limits.HasLimit F

instance CategoryTheory.MonoOver.hasLimitsOfShape {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₃} [Category.{v₃, u₃} J] (X : C) [Limits.HasLimitsOfShape J (Over X)] : Limits.HasLimitsOfShape J (MonoOver X)

instance CategoryTheory.MonoOver.hasFiniteLimits {C : Type u₁} [Category.{v₁, u₁} C] (X : C) [Limits.HasFiniteLimits (Over X)] : Limits.HasFiniteLimits (MonoOver X)

instance CategoryTheory.MonoOver.hasLimitsOfSize {C : Type u₁} [Category.{v₁, u₁} C] (X : C) [Limits.HasLimitsOfSize.{w, w', v₁, max u₁ v₁} (Over X)] : Limits.HasLimitsOfSize.{w, w', v₁, max u₁ v₁} (MonoOver X)

def CategoryTheory.MonoOver.strongEpiMonoFactorisationSigmaDesc {C : Type u₁} [Category.{v₁, u₁} C] {Y : C} [Limits.HasCoproducts C] [Limits.HasStrongEpiMonoFactorisations C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J (MonoOver Y)) : Limits.StrongEpiMonoFactorisation (Limits.Sigma.desc fun (i : J) => (F.obj i).arrow)

A helper function, providing the strong epi-mono factorization used construct to colimits.

def CategoryTheory.MonoOver.coconeOfHasStrongEpiMonoFactorisation {C : Type u₁} [Category.{v₁, u₁} C] {Y : C} [Limits.HasCoproducts C] [Limits.HasStrongEpiMonoFactorisations C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J (MonoOver Y)) : Limits.Cocone F

If a category C has strong epi-mono factorization, for any Y : C and functor F : J ⥤ MonoOver Y, there is a cocone under F.

theorem CategoryTheory.MonoOver.commSqOfHasStrongEpiMonoFactorisation {C : Type u₁} [Category.{v₁, u₁} C] {Y : C} [Limits.HasCoproducts C] [Limits.HasStrongEpiMonoFactorisations C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J (MonoOver Y)) (c : Limits.Cocone F) : CommSq (Limits.Sigma.desc fun (i : J) => (c.ι.app i).hom.left) (strongEpiMonoFactorisationSigmaDesc F).e c.pt.arrow (strongEpiMonoFactorisationSigmaDesc F).m

def CategoryTheory.MonoOver.liftStructOfHasStrongEpiMonoFactorisation {C : Type u₁} [Category.{v₁, u₁} C] {Y : C} [Limits.HasCoproducts C] [Limits.HasStrongEpiMonoFactorisations C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J (MonoOver Y)) (c : Limits.Cocone F) : ⋯.LiftStruct

A helper function, providing the lift structure used to construct colimits.

def CategoryTheory.MonoOver.isColimitCoconeOfHasStrongEpiMonoFactorisation {C : Type u₁} [Category.{v₁, u₁} C] {Y : C} [Limits.HasCoproducts C] [Limits.HasStrongEpiMonoFactorisations C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J (MonoOver Y)) : Limits.IsColimit (coconeOfHasStrongEpiMonoFactorisation F)

The cocone coconeOfHasStrongEpiMonoFactorisation F is a colimit

instance CategoryTheory.MonoOver.hasColimitsOfSize_of_hasStrongEpiMonoFactorisations {C : Type u₁} [Category.{v₁, u₁} C] {Y : C} [Limits.HasCoproducts C] [Limits.HasStrongEpiMonoFactorisations C] : Limits.HasColimitsOfSize.{w, w', v₁, max u₁ v₁} (MonoOver Y)

def CategoryTheory.MonoOver.pullback {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Limits.HasPullbacks C] (f : X ⟶ Y) : Functor (MonoOver Y) (MonoOver X)

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

def CategoryTheory.MonoOver.pullbackComp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} [Limits.HasPullbacks C] (f : X ⟶ Y) (g : Y ⟶ Z) : pullback (CategoryStruct.comp f g) ≅ (pullback g).comp (pullback f)

pullback commutes with composition (up to a natural isomorphism)

def CategoryTheory.MonoOver.pullbackId {C : Type u₁} [Category.{v₁, u₁} C] {X : C} [Limits.HasPullbacks C] : pullback (CategoryStruct.id X) ≅ Functor.id (MonoOver X)

pullback preserves the identity (up to a natural isomorphism)

@[simp]

theorem CategoryTheory.MonoOver.pullback_obj_left {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Limits.HasPullbacks C] (f : X ⟶ Y) (g : MonoOver Y) : ((pullback f).obj g).obj.left = Limits.pullback g.arrow f

@[simp]

theorem CategoryTheory.MonoOver.pullback_obj_arrow {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Limits.HasPullbacks C] (f : X ⟶ Y) (g : MonoOver Y) : ((pullback f).obj g).arrow = Limits.pullback.snd ((forget Y).obj g).hom f

def CategoryTheory.MonoOver.pullbackObjIsoOfIsPullback {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasPullbacks C] {X Y : C} (f : Y ⟶ X) (S : MonoOver X) (T : MonoOver Y) (f' : T.obj.left ⟶ S.obj.left) (h : IsPullback f' T.arrow S.arrow f) : (pullback f).obj S ≅ T

Given two monomorphisms S and T over X and Y and two morphisms f and f' between them forming the following pullback square:

(T : C) -f'-> (S : C)
   |             |
T.arrow       S.arrow
   |             |
   v             v
   Y -----f----> X

we get an isomorphism between T and the pullback of S along f through the pullback functor.

def CategoryTheory.MonoOver.map {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [Mono f] : Functor (MonoOver X) (MonoOver Y)

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

def CategoryTheory.MonoOver.mapComp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [Mono f] [Mono g] : map (CategoryStruct.comp f g) ≅ (map f).comp (map g)

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

def CategoryTheory.MonoOver.mapId {C : Type u₁} [Category.{v₁, u₁} C] (X : C) : map (CategoryStruct.id X) ≅ Functor.id (MonoOver X)

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

@[simp]

theorem CategoryTheory.MonoOver.map_obj_left {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [Mono f] (g : MonoOver X) : ((map f).obj g).obj.left = g.obj.left

@[simp]

theorem CategoryTheory.MonoOver.map_obj_arrow {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [Mono f] (g : MonoOver X) : ((map f).obj g).arrow = CategoryStruct.comp g.arrow f

instance CategoryTheory.MonoOver.full_map {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [Mono f] : (map f).Full

instance CategoryTheory.MonoOver.faithful_map {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [Mono f] : (map f).Faithful

def CategoryTheory.MonoOver.mapIso {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} (e : A ≅ B) : MonoOver A ≌ MonoOver B

Isomorphic objects have equivalent MonoOver categories.

@[simp]

theorem CategoryTheory.MonoOver.mapIso_inverse {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} (e : A ≅ B) : (mapIso e).inverse = map e.inv

@[simp]

theorem CategoryTheory.MonoOver.mapIso_unitIso {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} (e : A ≅ B) : (mapIso e).unitIso = ((mapComp e.hom e.inv).symm ≪≫ eqToIso ⋯ ≪≫ mapId A).symm

@[simp]

theorem CategoryTheory.MonoOver.mapIso_functor {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} (e : A ≅ B) : (mapIso e).functor = map e.hom

@[simp]

theorem CategoryTheory.MonoOver.mapIso_counitIso {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} (e : A ≅ B) : (mapIso e).counitIso = (mapComp e.inv e.hom).symm ≪≫ eqToIso ⋯ ≪≫ mapId B

def CategoryTheory.MonoOver.congr {C : Type u₁} [Category.{v₁, u₁} C] (X : C) {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : MonoOver X ≌ 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.

@[simp]

theorem CategoryTheory.MonoOver.congr_unitIso {C : Type u₁} [Category.{v₁, u₁} C] (X : C) {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : (congr X e).unitIso = NatIso.ofComponents (fun (Y : MonoOver X) => isoMk (e.unitIso.app Y.obj.left) ⋯) ⋯

@[simp]

theorem CategoryTheory.MonoOver.congr_inverse {C : Type u₁} [Category.{v₁, u₁} C] (X : C) {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : (congr X e).inverse = (lift (Over.post e.inverse) ⋯).comp (mapIso (e.unitIso.symm.app X)).functor

@[simp]

theorem CategoryTheory.MonoOver.congr_counitIso {C : Type u₁} [Category.{v₁, u₁} C] (X : C) {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : (congr X e).counitIso = NatIso.ofComponents (fun (Y : MonoOver (e.functor.obj X)) => isoMk (e.counitIso.app Y.obj.left) ⋯) ⋯

@[simp]

theorem CategoryTheory.MonoOver.congr_functor {C : Type u₁} [Category.{v₁, u₁} C] (X : C) {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : (congr X e).functor = lift (Over.post e.functor) ⋯

def CategoryTheory.MonoOver.mapPullbackAdj {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Limits.HasPullbacks C] (f : X ⟶ Y) [Mono f] : map f ⊣ pullback f

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

def CategoryTheory.MonoOver.pullbackMapSelf {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Limits.HasPullbacks C] (f : X ⟶ Y) [Mono f] : (map f).comp (pullback f) ≅ Functor.id (MonoOver X)

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

def CategoryTheory.MonoOver.imageMonoOver {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [Limits.HasImage f] : MonoOver Y

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

@[simp]

theorem CategoryTheory.MonoOver.imageMonoOver_arrow {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [Limits.HasImage f] : (imageMonoOver f).arrow = Limits.image.ι f

def CategoryTheory.MonoOver.image {C : Type u₁} [Category.{v₁, u₁} C] {X : C} [Limits.HasImages C] : Functor (Over X) (MonoOver X)

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

@[simp]

theorem CategoryTheory.MonoOver.image_obj {C : Type u₁} [Category.{v₁, u₁} C] {X : C} [Limits.HasImages C] (f : Over X) : image.obj f = imageMonoOver f.hom

@[simp]

theorem CategoryTheory.MonoOver.image_map {C : Type u₁} [Category.{v₁, u₁} C] {X : C} [Limits.HasImages C] {f g : Over X} (k : f ⟶ g) : image.map k = (forget X).preimage (Over.homMk (Limits.image.lift { I := Limits.image g.hom, m := Limits.image.ι g.hom, m_mono := ⋯, e := CategoryStruct.comp k.left (Limits.factorThruImage g.hom), fac := ⋯ }) ⋯)

def CategoryTheory.MonoOver.imageForgetAdj {C : Type u₁} [Category.{v₁, u₁} C] {X : C} [Limits.HasImages C] : image ⊣ forget X

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

instance CategoryTheory.MonoOver.instIsRightAdjointOverForget {C : Type u₁} [Category.{v₁, u₁} C] {X : C} [Limits.HasImages C] : (forget X).IsRightAdjoint

instance CategoryTheory.MonoOver.reflective {C : Type u₁} [Category.{v₁, u₁} C] {X : C} [Limits.HasImages C] : Reflective (forget X)

def CategoryTheory.MonoOver.forgetImage {C : Type u₁} [Category.{v₁, u₁} C] {X : C} [Limits.HasImages C] : (forget X).comp image ≅ Functor.id (MonoOver X)

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

def CategoryTheory.MonoOver.exists {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Limits.HasImages C] (f : X ⟶ Y) : Functor (MonoOver X) (MonoOver 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.

instance CategoryTheory.MonoOver.faithful_exists {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Limits.HasImages C] (f : X ⟶ Y) : («exists» f).Faithful

def CategoryTheory.MonoOver.existsIsoMap {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Limits.HasImages C] (f : X ⟶ Y) [Mono f] : «exists» f ≅ map f

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

def CategoryTheory.MonoOver.existsPullbackAdj {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} [Limits.HasImages C] (f : X ⟶ Y) [Limits.HasPullbacks C] : «exists» f ⊣ pullback f

exists is adjoint to pullback when images exist