nLab n-monomorphism

Contents

Context

$(\infty,1)$-Category theory

(∞,1)-category theory

Background

Basic concepts

Universal constructions

Local presentation

Theorems

Extra stuff, structure, properties

Models

Contents

Definition

For $n \in \mathbb{N}$ a morphism $f \colon X \to Y$ in an (infinity,1)-category is an $n$-monomorphism equivalently if

In homotopy type theory

In homotopy type theory, a function $f \colon X \to Y$ is an $n$-monomorphism if its $n$-image factorization is via an equivalence in homotopy type theory.

More explicitly, given a natural number $n:\mathbb{N}$ and types $A$ and $B$, a function $f:A \to B$ is a $n$-monomorphism if for all terms $b:B$ the fiber of $f$ over $b$ has an homotopy level of $n$.

$isMonic(n, f) \coloneqq \prod_{b:B} hasHLevel(n, fiber(f, b))$

A equivalence is a $0$-monomorphism. $1$-monomorphisms are typically just called monomorphisms or embeddings.

The type of all $n$-monomorphisms with domain $A$ and codomain $B$ is defined as

$Monos(n, A, B): \sum_{f:A \to B} isMonic(n, f)$

Dual concept

The dual concept is that of n-epimorphism.

Examples

• $0$-monomorphism are precisely the equivalences.

• Every morphism is an $\infty$-monomorphism.

• 1-monomorphisms are often just called monomorphisms in an (∞,1)-category. The 1-monomorphisms into a fixed object are called the subobjects of that object.

• A 1-monomorphism between 0-truncated objects is precisely an ordinary monomorphism in the underlying 1-topos.

Last revised on June 17, 2022 at 17:56:42. See the history of this page for a list of all contributions to it.