Struct DblModelMorphism

pub struct DblModelMorphism<'a, Map, Dom, Cod>(pub &'a Map, pub &'a Dom, pub &'a Cod);

A functor between models of a double theory defined by a mapping.

This struct borrows its data to perform validation. The domain and codomain are assumed to be valid models of double theories. If that is in question, the models should be validated before validating this object.

Tuple Fields

0: &'a Map

1: &'a Dom

2: &'a Cod

Implementations

impl<'a, DomId, CodId, Cat> DblModelMorphism<'a, DiscreteDblModelMapping<DomId, CodId>, DiscreteDblModel<DomId, Cat>, DiscreteDblModel<CodId, Cat>>

where DomId: Eq + Clone + Hash, CodId: Eq + Clone + Hash, Cat: FgCategory, Cat::Ob: Hash, Cat::Mor: Hash,

pub fn iter_invalid( &self, ) -> impl Iterator<Item = InvalidDblModelMorphism<DomId, DomId>> + 'a + use<'a, DomId, CodId, Cat>

Iterates over failures of the mapping to be a model morphism.

pub fn is_injective_objects(&self) -> bool

Is the model morphism injective on objects?

pub fn is_free_simple_faithful(&self) -> bool

Is the model morphism faithful?

This check is a nontrivial computation since we cannot enumerate all of the morphisms of the domain category. We simplify the problem by only allowing free models. Furthermore, we restrict the mapping to send generating morphisms in the domain to simple paths in the codomain. If any of these assumptions are violated, the function will panic.

pub fn is_free_simple_monic(&self) -> bool

Is the model morphism a monomorphism?

A monomorphism in Cat is an injective on objects and faithful functor. Thus, we check injectivity on objects and faithfulness. Note that the latter check is subject to the same limitations as is_free_simple_faithful.