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 Xdef map (f : X ⟶ Y) [Mono f] : MonoOver X ⥤ MonoOver Ydef «exists» [HasImages C] (f : X ⟶ Y) : MonoOver X ⥤ MonoOver Yand 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₁}
[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.
Instances For
instance
CategoryTheory.instCategoryMonoOver
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(X : C)
:
@[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]
:
def
CategoryTheory.MonoOver.mk'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{A : C}
(f : A ⟶ X)
[hf : CategoryTheory.Mono f]
:
Construct a MonoOver X.
Instances For
The inclusion from monomorphisms over X to morphisms over X.
Instances For
instance
CategoryTheory.MonoOver.instCoeOutMonoOver
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
:
@[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
@[inline, reducible]
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.
Instances For
@[simp]
theorem
CategoryTheory.MonoOver.mk'_arrow
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{A : C}
(f : A ⟶ X)
[CategoryTheory.Mono 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 = CategoryTheory.MonoOver.arrow f
instance
CategoryTheory.MonoOver.mono
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
(f : CategoryTheory.MonoOver X)
:
instance
CategoryTheory.MonoOver.isThin
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
:
The category of monomorphisms over X is a thin category, which makes defining its skeleton easy.
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)
:
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)
:
@[inline, reducible]
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 (CategoryTheory.MonoOver.arrow g) = CategoryTheory.MonoOver.arrow f)
_auto✝)
:
f ⟶ g
Convenience constructor for a morphism in monomorphisms over X.
Instances For
@[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 (CategoryTheory.MonoOver.arrow g) = CategoryTheory.MonoOver.arrow f)
_auto✝)
:
(CategoryTheory.MonoOver.isoMk h).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 (CategoryTheory.MonoOver.arrow g) = CategoryTheory.MonoOver.arrow f)
_auto✝)
:
(CategoryTheory.MonoOver.isoMk h).hom = CategoryTheory.MonoOver.homMk h.hom
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 (CategoryTheory.MonoOver.arrow g) = CategoryTheory.MonoOver.arrow f)
_auto✝)
:
f ≅ g
Convenience constructor for an isomorphism in monomorphisms over X.
Instances For
def
CategoryTheory.MonoOver.mk'ArrowIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
(f : CategoryTheory.MonoOver X)
:
If f : MonoOver X, then mk' f.arrow is of course just f, but not definitionally, so we
package it as an isomorphism.
Instances For
@[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 Y : CategoryTheory.MonoOver Y} (k : X ⟶ Y),
(CategoryTheory.MonoOver.lift F h).map k = (CategoryTheory.MonoOver.forget X).preimage
((CategoryTheory.Functor.comp (CategoryTheory.MonoOver.forget Y) F).map k)
@[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)
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)
:
Lift a functor between over categories to a functor between MonoOver categories,
given suitable evidence that morphisms are taken to monomorphisms.
Instances For
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₂)
:
Isomorphic functors Over Y ⥤ Over X lift to isomorphic functors MonoOver Y ⥤ MonoOver X.
Instances For
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.Functor.comp (CategoryTheory.MonoOver.lift F h₁) (CategoryTheory.MonoOver.lift G h₂) ≅ CategoryTheory.MonoOver.lift (CategoryTheory.Functor.comp F G) fun f =>
h₂ { obj := F.obj ((CategoryTheory.MonoOver.forget X).obj f), property := h₁ f }
MonoOver.lift commutes with composition of functors.
Instances For
def
CategoryTheory.MonoOver.liftId
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
:
CategoryTheory.MonoOver.lift (CategoryTheory.Functor.id (CategoryTheory.Over X))
(_ : ∀ (f : CategoryTheory.MonoOver X), CategoryTheory.Mono f.obj.hom) ≅ CategoryTheory.Functor.id (CategoryTheory.MonoOver X)
MonoOver.lift preserves the identity functor.
Instances For
@[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)
:
@[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.arrow ((CategoryTheory.MonoOver.lift F h).obj f) = (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
((CategoryTheory.Over.iteratedSliceEquiv f).functor.obj ((CategoryTheory.MonoOver.forget f).obj g)).hom)
(h₂ : ∀ (g : CategoryTheory.MonoOver f.left),
CategoryTheory.Mono
((CategoryTheory.Over.iteratedSliceEquiv f).inverse.obj ((CategoryTheory.MonoOver.forget f.left).obj g)).hom)
:
Monomorphisms over an object f : Over A in an over category
are equivalent to monomorphisms over the source of f.
Instances For
def
CategoryTheory.MonoOver.pullback
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks 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.
Instances For
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)
:
pullback commutes with composition (up to a natural isomorphism)
Instances For
def
CategoryTheory.MonoOver.pullbackId
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
[CategoryTheory.Limits.HasPullbacks C]
:
pullback preserves the identity (up to a natural isomorphism)
Instances For
@[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 (CategoryTheory.MonoOver.arrow g) 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.arrow ((CategoryTheory.MonoOver.pullback f).obj g) = CategoryTheory.Limits.pullback.snd
def
CategoryTheory.MonoOver.map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
We can map monomorphisms over X to monomorphisms over Y
by post-composition with a monomorphism f : X ⟶ Y.
Instances For
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]
:
MonoOver.map commutes with composition (up to a natural isomorphism).
Instances For
MonoOver.map preserves the identity (up to a natural isomorphism).
Instances For
@[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)
:
instance
CategoryTheory.MonoOver.fullMap
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
instance
CategoryTheory.MonoOver.faithful_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
@[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_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.map (CategoryTheory.CategoryStruct.comp e.hom e.inv) = CategoryTheory.MonoOver.map (CategoryTheory.CategoryStruct.id A)) ≪≫ CategoryTheory.MonoOver.mapId).symm
@[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.map (CategoryTheory.CategoryStruct.comp e.inv e.hom) = CategoryTheory.MonoOver.map (CategoryTheory.CategoryStruct.id B)) ≪≫ CategoryTheory.MonoOver.mapId
@[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.mapIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A : C}
{B : C}
(e : A ≅ B)
:
Isomorphic objects have equivalent MonoOver categories.
Instances For
@[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.Functor.comp
(CategoryTheory.MonoOver.lift (CategoryTheory.Over.post e.inverse)
(_ :
∀ (f : CategoryTheory.MonoOver (e.functor.obj X)),
CategoryTheory.Mono
((CategoryTheory.Over.post e.inverse).obj ((CategoryTheory.MonoOver.forget (e.functor.obj X)).obj f)).hom))
(CategoryTheory.MonoOver.mapIso (e.unitIso.symm.app X)).functor
@[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)
(_ :
∀ (f : CategoryTheory.MonoOver X),
CategoryTheory.Mono ((CategoryTheory.Over.post e.functor).obj ((CategoryTheory.MonoOver.forget X).obj f)).hom)
@[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.isoMk (e.unitIso.app Y.obj.left)
@[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.isoMk (e.counitIso.app Y.obj.left)
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.
Instances For
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]
:
map f is left adjoint to pullback f when f is a monomorphism
Instances For
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]
:
MonoOver.map f followed by MonoOver.pullback f is the identity.
Instances For
def
CategoryTheory.MonoOver.imageMonoOver
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
:
The MonoOver Y for the image inclusion for a morphism f : X ⟶ Y.
Instances For
@[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]
:
@[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
@[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)))))
def
CategoryTheory.MonoOver.image
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
[CategoryTheory.Limits.HasImages C]
:
Taking the image of a morphism gives a functor Over X ⥤ MonoOver X.
Instances For
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
Instances For
instance
CategoryTheory.MonoOver.reflective
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
[CategoryTheory.Limits.HasImages C]
:
def
CategoryTheory.MonoOver.forgetImage
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
[CategoryTheory.Limits.HasImages C]
:
CategoryTheory.Functor.comp (CategoryTheory.MonoOver.forget X) 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.
Instances For
def
CategoryTheory.MonoOver.exists
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasImages 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.
Instances For
instance
CategoryTheory.MonoOver.faithful_exists
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasImages C]
(f : X ⟶ Y)
:
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]
:
When f : X ⟶ Y is a monomorphism, exists f agrees with map f.
Instances For
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]
:
exists is adjoint to pullback when images exist