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.
Equations
- CategoryTheory.MonoOver X = CategoryTheory.FullSubcategory fun (f : CategoryTheory.Over X) => CategoryTheory.Mono f.hom
Instances For
instance
CategoryTheory.instCategoryMonoOver
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(X : C)
:
Equations
@[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.
Equations
- CategoryTheory.MonoOver.mk' f = { obj := CategoryTheory.Over.mk f, property := hf }
Instances For
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
Instances For
instance
CategoryTheory.MonoOver.instCoeOutMonoOver
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
:
Equations
- CategoryTheory.MonoOver.instCoeOutMonoOver = { 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
@[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.
Equations
- CategoryTheory.MonoOver.arrow f = ((CategoryTheory.MonoOver.forget X).obj f).hom
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.instFullMonoOverInstCategoryMonoOverOverInstCategoryOverForget
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
:
Equations
- CategoryTheory.MonoOver.instFullMonoOverInstCategoryMonoOverOverInstCategoryOverForget = CategoryTheory.FullSubcategory.full fun (f : CategoryTheory.Over X) => CategoryTheory.Mono f.hom
instance
CategoryTheory.MonoOver.instFaithfulMonoOverInstCategoryMonoOverOverInstCategoryOverForget
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.MonoOver.mono
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
(f : CategoryTheory.MonoOver X)
:
Equations
- ⋯ = ⋯
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.
Equations
- ⋯ = ⋯
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.
Equations
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 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 (CategoryTheory.MonoOver.arrow g) = CategoryTheory.MonoOver.arrow f)
_auto✝)
:
(CategoryTheory.MonoOver.isoMk h w).hom = CategoryTheory.MonoOver.homMk h.hom 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 (CategoryTheory.MonoOver.arrow g) = CategoryTheory.MonoOver.arrow f)
_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 := ⋯ }
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.
Equations
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_1 Y_1 : CategoryTheory.MonoOver Y} (k : X_1 ⟶ Y_1),
(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.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
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)
:
MonoOver.lift commutes with composition of functors.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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₁}
[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.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
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)
Equations
- One or more equations did not get rendered due to their size.
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)
Equations
- CategoryTheory.MonoOver.pullbackId = CategoryTheory.MonoOver.liftIso ⋯ ⋯ CategoryTheory.Over.pullbackId ≪≫ CategoryTheory.MonoOver.liftId
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.
Equations
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).
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.mapId X = CategoryTheory.MonoOver.liftIso ⋯ ⋯ (CategoryTheory.Over.mapId X) ≪≫ CategoryTheory.MonoOver.liftId
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]
:
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.MonoOver.faithful_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
Equations
- ⋯ = ⋯
@[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.mapId A).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.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.mapIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{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_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) ⋯)
(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) ⋯
@[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_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.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.
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
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
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.
Equations
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.
Equations
- One or more equations did not get rendered due to their size.
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
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.MonoOver.instIsRightAdjointOverInstCategoryOverMonoOverInstCategoryMonoOverForget
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
[CategoryTheory.Limits.HasImages C]
:
Equations
- CategoryTheory.MonoOver.instIsRightAdjointOverInstCategoryOverMonoOverInstCategoryMonoOverForget = { left := CategoryTheory.MonoOver.image, adj := CategoryTheory.MonoOver.imageForgetAdj }
instance
CategoryTheory.MonoOver.reflective
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
[CategoryTheory.Limits.HasImages C]
:
Equations
- CategoryTheory.MonoOver.reflective = CategoryTheory.Reflective.mk
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.
Equations
- CategoryTheory.MonoOver.forgetImage = CategoryTheory.asIso CategoryTheory.MonoOver.imageForgetAdj.counit
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 MonoOver.map f.
Equations
- CategoryTheory.MonoOver.exists f = CategoryTheory.Functor.comp (CategoryTheory.MonoOver.forget X) (CategoryTheory.Functor.comp (CategoryTheory.Over.map f) CategoryTheory.MonoOver.image)
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)
:
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]
:
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₁}
[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
Equations
- One or more equations did not get rendered due to their size.