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₁} [CategoryTheory.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.

Equations

• CategoryTheory.MonoOver X = CategoryTheory.FullSubcategory fun (f : CategoryTheory.Over X) => CategoryTheory.Mono f.hom

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

Equations

• CategoryTheory.instCategoryMonoOver X = CategoryTheory.FullSubcategory.category fun (f : CategoryTheory.Over X) => CategoryTheory.Mono f.hom

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

Construct a MonoOver X.

Equations

• CategoryTheory.MonoOver.mk' f = { obj := CategoryTheory.Over.mk f, property := hf }

@[simp]

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

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

The inclusion from monomorphisms over X to morphisms over X.

Equations

• CategoryTheory.MonoOver.forget X = CategoryTheory.fullSubcategoryInclusion fun (f : CategoryTheory.Over X) => CategoryTheory.Mono f.hom

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

Equations

• CategoryTheory.MonoOver.instCoeOut = { coe := fun (Y : CategoryTheory.MonoOver X) => Y.obj.left }

@[simp]

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

@[simp]

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

@[reducible, inline]

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

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

Equations

• f.arrow = ((CategoryTheory.MonoOver.forget X).obj f).hom

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.MonoOver.fullyFaithfulForget X = CategoryTheory.fullyFaithfulFullSubcategoryInclusion fun (f : CategoryTheory.Over X) => CategoryTheory.Mono f.hom

instance CategoryTheory.MonoOver.instFullOverForget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} : (CategoryTheory.MonoOver.forget X).Full

Equations

• ⋯ = ⋯

instance CategoryTheory.MonoOver.instFaithfulOverForget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} : (CategoryTheory.MonoOver.forget X).Faithful

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

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

@[reducible, inline]

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

Convenience constructor for a morphism in monomorphisms over X.

Equations

• CategoryTheory.MonoOver.homMk h w = CategoryTheory.Over.homMk h w

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

• CategoryTheory.MonoOver.isoMk h w = { hom := CategoryTheory.MonoOver.homMk h.hom w, inv := CategoryTheory.MonoOver.homMk h.inv ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

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

def CategoryTheory.MonoOver.mk'ArrowIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (f : CategoryTheory.MonoOver X) : CategoryTheory.MonoOver.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.

Equations

• f.mk'ArrowIso = CategoryTheory.MonoOver.isoMk (CategoryTheory.Iso.refl (CategoryTheory.MonoOver.mk' f.arrow).obj.left) ⋯

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

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.

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.MonoOver.liftIso h₁ h₂ i = CategoryTheory.Functor.fullyFaithfulCancelRight (CategoryTheory.MonoOver.forget X) (CategoryTheory.isoWhiskerLeft (CategoryTheory.MonoOver.forget Y) i)

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

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

MonoOver.lift preserves the identity functor.

Equations

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

@[simp]

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

@[simp]

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

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

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.

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

Equations

• CategoryTheory.MonoOver.pullback f = CategoryTheory.MonoOver.lift (CategoryTheory.Over.pullback f) ⋯

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

pullback commutes with composition (up to a natural isomorphism)

Equations

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

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

pullback preserves the identity (up to a natural isomorphism)

Equations

• CategoryTheory.MonoOver.pullbackId = CategoryTheory.MonoOver.liftIso ⋯ ⋯ CategoryTheory.Over.pullbackId ≪≫ CategoryTheory.MonoOver.liftId

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.MonoOver.map f = CategoryTheory.MonoOver.lift (CategoryTheory.Over.map f) ⋯

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

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

Equations

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

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

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

Equations

• CategoryTheory.MonoOver.mapId X = CategoryTheory.MonoOver.liftIso ⋯ ⋯ (CategoryTheory.Over.mapId X) ≪≫ CategoryTheory.MonoOver.liftId

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Isomorphic objects have equivalent MonoOver categories.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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.

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

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

Equations

• CategoryTheory.MonoOver.pullbackMapSelf f = (CategoryTheory.asIso (CategoryTheory.MonoOver.mapPullbackAdj f).unit).symm

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

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

Equations

• CategoryTheory.MonoOver.imageMonoOver f = CategoryTheory.MonoOver.mk' (CategoryTheory.Limits.image.ι f)

@[simp]

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

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

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.

@[simp]

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

@[simp]

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

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

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.

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

Equations

• ⋯ = ⋯

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

Equations

• CategoryTheory.MonoOver.reflective = CategoryTheory.Reflective.mk CategoryTheory.MonoOver.image CategoryTheory.MonoOver.imageForgetAdj

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

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

Equations

• CategoryTheory.MonoOver.forgetImage = CategoryTheory.asIso CategoryTheory.MonoOver.imageForgetAdj.counit

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

Equations

• CategoryTheory.MonoOver.exists f = (CategoryTheory.MonoOver.forget X).comp ((CategoryTheory.Over.map f).comp CategoryTheory.MonoOver.image)

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

Equations

• ⋯ = ⋯

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

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.

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

exists is adjoint to pullback when images exist

Equations

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