Module Tensor.Morphism

type 'a obj := 'a t
include module type of Morphism
type 'a obj := 'a t
type ('a, 'b) t

The type of morphisms from a tensor indexed by 'a to a tensor indexed by 'b.

val underlying : ('a, 'b) t -> 'a m -> 'b m

Get the map on positions underlying the shape morphism.

val domain : ('a, 'b) t -> 'a obj

domain m is the domain of the morphism m, ie a tensor indexed by 'a.

val range : ('a, 'b) t -> 'b obj

range m is the range of the morphism m, ie a tensor indexed by 'b.

val identity : 'a obj -> ('a, 'a) t

identity s is the identity morphism at the shape s.

val compose : ('a, 'b) t -> ('b, 'c) t -> ('a, 'c) t

compose is sequential morphism composition.

val tensor : ('a, 'b) t -> ('c, 'd) t -> ('a * 'c, 'b * 'd) t

tensor m1 m2 is the parallel composition of m1 and m2

val pullback_at_path : (pos, pos) t -> 'a Path.t -> 'a obj -> ('a, 'a) t k

pullback_at_path m p s extends m to s by constructing a morphism equal to m at p and acting as the identity on s elsewhere.

raises Dimensions_mismatch

if range m is different from proj s p.

val pullback_pointwise : (pos, pos) t -> 'a obj -> ('a, 'a) t k

pullback_pointwise m s extends m to s by applying it pointwise to every position in

raises Dimensions_mismatch

if any rank one sub-tensor of s is different from range m.

val sub : ofs:pos m -> pos obj -> pos obj -> (pos, pos) t k

sub ofs dom range constructs a morphism corresponding to the inclusion of dom, a rank-one tensor of dimension say m, into range, a rank-one tensor of dimension say n, such that the underlying positions of dom are mapped starting at index ofs in range.

Concretely, sub ofs dom range constructs a morphism mapping positions n in dom to positions n + ofs in range.

raises Dimensions_mismatch

if ofs <= 0 || dim dom <= 0 || ofs + dim dom > dim range.