mathlib documentation

category_theory.subobject.mono_over

Monomorphisms over a fixed object #

As preparation for defining subobject X, we set up the theory for mono_over X := {f : over X // mono f.hom}.

Here mono_over 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 mono_over X.

We provide

Notes #

This development originally appeared in Bhavik Mehta's "Topos theory for Lean" repository, and was ported to mathlib by Scott Morrison.

def category_theory.mono_over {C : Type u₁} [category_theory.category 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
Instances for category_theory.mono_over

Construct a mono_over X.

Equations
@[simp]
@[reducible]

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

@[simp]
@[protected, instance]
@[protected, instance]

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

theorem category_theory.mono_over.w {C : Type u₁} [category_theory.category C] {X : C} {f g : category_theory.mono_over X} (k : f g) :
theorem category_theory.mono_over.w_assoc {C : Type u₁} [category_theory.category C] {X : C} {f g : category_theory.mono_over X} (k : f g) {X' : C . "obviously"} (f' : X X') :
k.left g.arrow f' = f.arrow f'
@[reducible]
def category_theory.mono_over.hom_mk {C : Type u₁} [category_theory.category C] {X : C} {f g : category_theory.mono_over X} (h : f.obj.left g.obj.left) (w : h g.arrow = f.arrow) :
f g

Convenience constructor for a morphism in monomorphisms over X.

def category_theory.mono_over.iso_mk {C : Type u₁} [category_theory.category C] {X : C} {f g : category_theory.mono_over X} (h : f.obj.left g.obj.left) (w : h.hom g.arrow = f.arrow) :
f g

Convenience constructor for an isomorphism in monomorphisms over X.

Equations
@[simp]

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

Equations

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

Equations

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

Equations

pullback preserves the identity (up to a natural isomorphism)

Equations

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

Equations
Instances for category_theory.mono_over.map

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

Equations

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

Equations

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.

Equations
Instances for category_theory.mono_over.exists