directed_system

A directed system is a functor from the category (directed poset) to another category. This is used for abelian groups and rings and fields because their maps are not bundled. See module.directed_system

module.directed_system

A directed system is a functor from the category (directed poset) to the category of R-modules.

module.direct_limit

The direct limit of a directed system is the modules glued together along the maps.

module.direct_limit.of

The canonical map from a component to the direct limit.

module.direct_limit.exists_of

Every element of the direct limit corresponds to some element in some component of the directed system.

module.direct_limit.lift

The universal property of the direct limit: maps from the components to another module that respect the directed system structure (i.e. make some diagram commute) give rise to a unique map out of the direct limit.

module.direct_limit.of.zero_exact

A component that corresponds to zero in the direct limit is already zero in some bigger module in the directed system.

add_comm_group.direct_limit

The direct limit of a directed system is the abelian groups glued together along the maps.

add_comm_group.direct_limit.of

The canonical map from a component to the direct limit.

add_comm_group.direct_limit.of.zero_exact

A component that corresponds to zero in the direct limit is already zero in some bigger module in the directed system.

add_comm_group.direct_limit.lift

The universal property of the direct limit: maps from the components to another abelian group that respect the directed system structure (i.e. make some diagram commute) give rise to a unique map out of the direct limit.

ring.direct_limit

The direct limit of a directed system is the rings glued together along the maps.

ring.direct_limit.of

The canonical map from a component to the direct limit.

ring.direct_limit.exists_of

Every element of the direct limit corresponds to some element in some component of the directed system.

ring.direct_limit.of.zero_exact

A component that corresponds to zero in the direct limit is already zero in some bigger module in the directed system.

ring.direct_limit.of_inj

If the maps in the directed system are injective, then the canonical maps from the components to the direct limits are injective.

ring.direct_limit.lift

The universal property of the direct limit: maps from the components to another ring that respect the directed system structure (i.e. make some diagram commute) give rise to a unique map out of the direct limit.