## 3 Mathematical Framework for Consistency
### Mathematical Representation of a Structural Model
#### 3.0.1 Port
Examples of direct belonging morphisms in the diagram for a model can be found in Figure 8; the plain black arrows are the direct belongings. Paths in the model formed by the composition of one or more direct belonging morphisms are the belonging morphisms; they correspond to the relations between a model element and its ancestors. The other significant kind of morphism is reference morphisms. The reference morphisms show the relation between a port and a connection that the port participates in. **Definition 14**. : _Reference morphism Let \(M\) be a model, let \(P,C\in Ob(M)\) such that \(P\) is a port and \(C\) a connection, and let \(f:A\longrightarrow B\) a morphism in \(M\)._  
_We call \(f\) a reference morphism if and only if \(f\) maps \(p\in P\) to \(P\in Ob(C)\)._  
Examples of reference morphisms can be found in Figure 8; they are the dotted arrows from P1 and P2 to C. The reference morphisms represent the encapsulation of the ports in the connections, as they are elements of the connection. We call injections a certain kind of functors between models. These functors represent the fact that a model is part of another model. **Definition 15**. : _Injection Let \(A\), \(B\) be two S2 ML models, and let \(F:A\longrightarrow B\) be a functor. We call \(F\) an injection if and only if \(F\) is injective on objects and faithful, and \(F\) lets an object's and morphism's properties remain unchanged, i.e., ports, blocks, and connections are, respectively, mapped to ports, blocks, and connections, and reference and belonging morphisms are, respectively, mapped to reference and belonging morphisms._  
Figure 8: Diagram of the system model from Figure 6.  
A graphical illustration of injection between two models can be found in Figure 9. Injections are functors that associate each object and morphism of its source with a unique object or morphism of the target. The existence of an injection between two models means that the structure of the first model is a part of the structure of the second one. Interesting properties of the objects can also be defined, which we use in the demonstrations of theorems. The order of an object is the number of depth levels in the system breakdown separating this object from the root object of the model. We also call the order of the model the number of depth levels of system breakdown of the model. Order of a model object, order of a model Let \(M\) be a model, and let \(X\in Ob(M)\). We call the order of \(X\) its distance to the root object, i.e., the number of direct belonging morphisms that have to be composed to obtain a morphism, \(f:X\longrightarrow R\). We call the order of \(M\) the upper bound of the orders of its objects. The root of the model is an object of order zero, and objects with a direct belonging towards the root are of the first order. As an example, in Figure 8, the object of order zero is the block System, objects of the first order are the blocks A and B and the connection C, and objects of the second order are the ports P1 and P2. The model itself is of the second order since the ports have the maximal order. We also define elementary blocks, which are blocks that do not contain other blocks. They are useful in inductive proofs, as they are the smaller blocks in the models, in the sense that they may be contained in other blocks that are subsequently \"bigger\" than them. Elementary block We call an elementary block any block that contains no other block. The S2 ML models with the injections are a category that we call \(S2 ML+Cat\). \(S2 ML+Cat\) is the frame within which we will study the characteristics of the models. \(S2 ML+Cat\) We define \(S2 ML+Cat\) as being the category composed of:  
\(Ob(S2 ML+Cat)\), the set of all S2 ML models. We call them the objects of \(S2 ML+Cat\);  
For each \(X,Y\in Ob(S2 ML+Cat)\), \(Hom(X,Y)\) is the set of the injections from \(X\) to \(Y\). S2 ML+Cat is a category. Proof. :  
* Identity: Let \(X\in S2 ML+Cat\). Figure 6.0 An injection between two models. The morphisms of S2 ML+Cat are the injections between S2 ML models.