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.

def 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.instCategoryMonoOver {C : Type u₁} [Category.{v₁, u₁} C] (X : C) : Category.{v₁, max u₁ v₁} (MonoOver X)

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

def 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

@[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

@[simp]

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.instFullOverForget {C : Type u₁} [Category.{v₁, u₁} C] {X : C} : (forget X).Full

instance CategoryTheory.MonoOver.instFaithfulOverForget {C : Type u₁} [Category.{v₁, u₁} C] {X : C} : (forget X).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,s 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.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.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 cat_disch) : 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.mk'ArrowIso {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.mk'ArrowIso_inv_left {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (f : MonoOver X) : f.mk'ArrowIso.inv.left = CategoryStruct.id f.obj.left

@[simp]

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

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

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.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_map {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} (k : X✝ ⟶ Y✝) : (lift F h).map k = ((forget Y).comp F).map k

@[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) (f : MonoOver Y) : ((lift F h).obj f).obj = F.obj ((forget Y).obj f)

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.

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_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_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

@[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_functor {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} (e : A ≅ B) : (mapIso e).functor = map e.hom

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_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) ⋯

@[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) ⋯) ⋯

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