catlog/dbl/discrete/
model_morphism.rs

1//! Morphisms between models of a discrete double theory.
2
3use std::collections::{HashMap, HashSet};
4use std::hash::Hash;
5use std::rc::Rc;
6
7use derivative::Derivative;
8use nonempty::NonEmpty;
9
10use crate::dbl::{model::*, model_morphism::*};
11use crate::one::graph_algorithms::{bounded_simple_paths, simple_paths, spec_order};
12use crate::one::*;
13use crate::validate::{self, Validate};
14use crate::zero::{Column, HashColumn, Mapping, MutMapping};
15
16/** A mapping between models of a discrete double theory.
17
18Because a discrete double theory has only trivial operations, the naturality
19axioms for a model morphism are also trivial.
20 */
21#[derive(Clone, Debug, Derivative)]
22#[derivative(Default(bound = ""))]
23#[derivative(PartialEq(bound = "DomId: Eq + Hash, CodId: PartialEq"))]
24pub struct DiscreteDblModelMapping<DomId, CodId>(pub DiscreteDblModelMappingData<DomId, CodId>);
25
26type DiscreteDblModelMappingData<DomId, CodId> =
27    FpFunctorData<HashColumn<DomId, CodId>, HashColumn<DomId, Path<CodId, CodId>>>;
28
29impl<DomId, CodId> DiscreteDblModelMapping<DomId, CodId>
30where
31    DomId: Clone + Eq + Hash,
32    CodId: Clone + Eq + Hash,
33{
34    /// Constructs a model mapping from a pair of hash maps.
35    pub fn new(ob_map: HashMap<DomId, CodId>, mor_map: HashMap<DomId, Path<CodId, CodId>>) -> Self {
36        Self(FpFunctorData::new(HashColumn::new(ob_map), HashColumn::new(mor_map)))
37    }
38
39    /// Assigns an object generator, returning the previous assignment.
40    pub fn assign_ob(&mut self, x: DomId, y: CodId) -> Option<CodId> {
41        self.0.ob_generator_map.set(x, y)
42    }
43
44    /// Assigns a morphism generator, returning the previous assignment.
45    pub fn assign_mor(&mut self, e: DomId, n: Path<CodId, CodId>) -> Option<Path<CodId, CodId>> {
46        self.0.mor_generator_map.set(e, n)
47    }
48
49    /// Unassigns an object generator, returning the previous assignment.
50    pub fn unassign_ob(&mut self, x: &DomId) -> Option<CodId> {
51        self.0.ob_generator_map.unset(x)
52    }
53
54    /// Unassigns a morphism generator, returning the previous assignment.
55    pub fn unassign_mor(&mut self, e: &DomId) -> Option<Path<CodId, CodId>> {
56        self.0.mor_generator_map.unset(e)
57    }
58
59    /// Interprets the data as a functor into the given model.
60    pub fn functor_into<'a, Cat: FgCategory>(
61        &'a self,
62        cod: &'a DiscreteDblModel<CodId, Cat>,
63    ) -> FpFunctor<'a, DiscreteDblModelMappingData<DomId, CodId>, FpCategory<CodId, CodId>> {
64        self.0.functor_into(&cod.category)
65    }
66
67    /** Basic objects and morphisms in the image of the model morphism.
68
69    Note this method does not compute the set-theoretic image of the model
70    morphism, as the image of a functor need not even form a category
71    ([Math.SE](https://math.stackexchange.com/a/4399114)), nor does it compute
72    submodel spanned by the image, generalizing the subcategory spanned by the
73    image of a functor. Instead, this method constructs a "syntactical image"
74    comprising all *basic* objects and morphisms appearing in the image of the
75    model morphism, possibly inside composites.
76     */
77    pub fn syntactic_image<Cat: FgCategory>(
78        &self,
79        cod: &DiscreteDblModel<CodId, Cat>,
80    ) -> DiscreteDblModel<CodId, Cat>
81    where
82        Cat::Ob: Hash,
83        Cat::Mor: Hash,
84    {
85        // TODO: For non-free models, we should filter the equations to those
86        // involving only generators that appear in the image.
87        assert!(cod.is_free(), "Codomain model should be free");
88
89        let mut im = DiscreteDblModel::new(cod.theory_rc());
90        for x in self.0.ob_generator_map.values() {
91            im.add_ob(x.clone(), cod.ob_type(x));
92        }
93        for path in self.0.mor_generator_map.values() {
94            for e in path.iter() {
95                let (x, y) = (cod.mor_generator_dom(e), cod.mor_generator_cod(e));
96                if !im.has_ob(&x) {
97                    im.add_ob(x.clone(), cod.ob_type(&x));
98                }
99                if !im.has_ob(&y) {
100                    im.add_ob(y.clone(), cod.ob_type(&y));
101                }
102                im.add_mor(e.clone(), x, y, cod.mor_generator_type(e));
103            }
104        }
105        im
106    }
107
108    /// Finder of morphisms between two models of a discrete double theory.
109    pub fn morphisms<'a, Cat: FgCategory>(
110        dom: &'a DiscreteDblModel<DomId, Cat>,
111        cod: &'a DiscreteDblModel<CodId, Cat>,
112    ) -> DiscreteDblModelMorphismFinder<'a, DomId, CodId, Cat>
113    where
114        Cat::Ob: Hash,
115        Cat::Mor: Hash,
116    {
117        DiscreteDblModelMorphismFinder::new(dom, cod)
118    }
119}
120
121/** A functor between models of a double theory.
122
123This struct borrows its data to perform validation. The domain and codomain are
124assumed to be valid models of double theories. If that is in question, the
125models should be validated *before* validating this object.
126 */
127pub struct DblModelMorphism<'a, Map, Dom, Cod>(pub &'a Map, pub &'a Dom, pub &'a Cod);
128
129/// A morphism between models of a discrete double theory.
130pub type DiscreteDblModelMorphism<'a, DomId, CodId, Cat> = DblModelMorphism<
131    'a,
132    DiscreteDblModelMapping<DomId, CodId>,
133    DiscreteDblModel<DomId, Cat>,
134    DiscreteDblModel<CodId, Cat>,
135>;
136
137impl<'a, DomId, CodId, Cat> DiscreteDblModelMorphism<'a, DomId, CodId, Cat>
138where
139    DomId: Eq + Clone + Hash,
140    CodId: Eq + Clone + Hash,
141    Cat: FgCategory,
142    Cat::Ob: Hash,
143    Cat::Mor: Hash,
144{
145    /// Iterates over failures of the mapping to be a model morphism.
146    pub fn iter_invalid(
147        &self,
148    ) -> impl Iterator<Item = InvalidDblModelMorphism<DomId, DomId>> + 'a + use<'a, DomId, CodId, Cat>
149    {
150        let DblModelMorphism(DiscreteDblModelMapping(mapping), dom, cod) = *self;
151        let category_errors: Vec<_> = mapping
152            .functor_into(&cod.category)
153            .iter_invalid_on(&dom.category)
154            .map(|err| match err {
155                InvalidFpFunctor::ObGen(x) => InvalidDblModelMorphism::Ob(x),
156                InvalidFpFunctor::MorGen(m) => InvalidDblModelMorphism::Mor(m),
157                InvalidFpFunctor::Dom(m) => InvalidDblModelMorphism::Dom(m),
158                InvalidFpFunctor::Cod(m) => InvalidDblModelMorphism::Cod(m),
159                InvalidFpFunctor::Eq(id) => InvalidDblModelMorphism::Eq(id),
160            })
161            .collect();
162        let ob_type_errors = dom.ob_generators().filter_map(|x| {
163            if let Some(y) = mapping.ob_generator_map.get(&x)
164                && cod.has_ob(y)
165                && dom.ob_type(&x) != cod.ob_type(y)
166            {
167                Some(InvalidDblModelMorphism::ObType(x))
168            } else {
169                None
170            }
171        });
172        let th_cat = cod.theory().category();
173        let mor_type_errors = dom.mor_generators().filter_map(|f| {
174            if let Some(g) = mapping.mor_generator_map.get(&f)
175                && cod.has_mor(g)
176                && !th_cat.morphisms_are_equal(dom.mor_generator_type(&f), cod.mor_type(g))
177            {
178                Some(InvalidDblModelMorphism::MorType(f))
179            } else {
180                None
181            }
182        });
183        category_errors.into_iter().chain(ob_type_errors).chain(mor_type_errors)
184    }
185
186    /// Are morphism generators sent to simple composites of morphisms in the
187    /// codomain?
188    fn is_simple(&self) -> bool {
189        let DblModelMorphism(DiscreteDblModelMapping(mapping), dom, _) = *self;
190        dom.mor_generators()
191            .all(|e| mapping.apply_edge(e).map(|p| p.is_simple()).unwrap_or(true))
192    }
193
194    /// Is the model morphism injective on objects?
195    pub fn is_injective_objects(&self) -> bool {
196        let DblModelMorphism(DiscreteDblModelMapping(mapping), dom, _) = *self;
197        let mut seen_obs: HashSet<_> = HashSet::new();
198        for x in dom.ob_generators() {
199            if let Some(f_x) = mapping.apply_vertex(x) {
200                if seen_obs.contains(&f_x) {
201                    return false; // not monic
202                } else {
203                    seen_obs.insert(f_x);
204                }
205            }
206        }
207        true
208    }
209
210    /** Is the model morphism faithful?
211
212    This check is a nontrivial computation since we cannot enumerate all of the
213    morphisms of the domain category. We simplify the problem by only allowing
214    free models. Furthermore, we restrict the mapping to send generating
215    morphisms in the domain to simple paths in the codomain. If any of these
216    assumptions are violated, the function will panic.
217     */
218    pub fn is_free_simple_faithful(&self) -> bool {
219        let DblModelMorphism(DiscreteDblModelMapping(mapping), dom, cod) = *self;
220
221        assert!(dom.is_free(), "Domain model should be free");
222        assert!(cod.is_free(), "Codomain model should be free");
223        assert!(self.is_simple(), "Morphism assignments should be simple");
224
225        let functor = mapping.functor_into(&cod.category);
226        for x in dom.ob_generators() {
227            for y in dom.ob_generators() {
228                let mut seen: HashSet<_> = HashSet::new();
229                for path in simple_paths(dom.generating_graph(), &x, &y) {
230                    if let Some(f_path) = functor.apply_mor(path) {
231                        if seen.contains(&f_path) {
232                            return false; // not faithful
233                        } else {
234                            seen.insert(f_path);
235                        }
236                    }
237                }
238            }
239        }
240        true
241    }
242
243    /** Is the model morphism a monomorphism?
244
245    A monomorphism in Cat is an injective on objects and faithful functor. Thus,
246    we check injectivity on objects and faithfulness. Note that the latter check
247    is subject to the same limitations as
248    [`is_free_simple_faithful`](DblModelMorphism::is_free_simple_faithful).
249     */
250    pub fn is_free_simple_monic(&self) -> bool {
251        self.is_injective_objects() && self.is_free_simple_faithful()
252    }
253}
254
255impl<DomId, CodId, Cat> Validate for DiscreteDblModelMorphism<'_, DomId, CodId, Cat>
256where
257    DomId: Eq + Clone + Hash,
258    CodId: Eq + Clone + Hash,
259    Cat: FgCategory,
260    Cat::Ob: Hash,
261    Cat::Mor: Hash,
262{
263    type ValidationError = InvalidDblModelMorphism<DomId, DomId>;
264
265    fn validate(&self) -> Result<(), NonEmpty<Self::ValidationError>> {
266        validate::wrap_errors(self.iter_invalid())
267    }
268}
269
270/** Finds morphisms between two models of a discrete double theory.
271
272Morphisms are found using backtracking search. In general, there can be
273infinitely many morphisms between two models, so not all of them can be
274reported. The search is restricted to morphisms that send each basic morphism in
275the domain to a [simple path](crate::one::graph_algorithms::simple_paths) of
276basic morphisms in the codomain.
277*/
278pub struct DiscreteDblModelMorphismFinder<'a, DomId, CodId, Cat: FgCategory> {
279    dom: &'a DiscreteDblModel<DomId, Cat>,
280    cod: &'a DiscreteDblModel<CodId, Cat>,
281    map: DiscreteDblModelMapping<DomId, CodId>,
282    results: Vec<DiscreteDblModelMapping<DomId, CodId>>,
283    var_order: Vec<GraphElem<DomId, DomId>>,
284    max_path_len: Option<usize>,
285    injective_ob: bool,
286    faithful: bool,
287    ob_init: HashColumn<DomId, CodId>,
288    mor_init: HashColumn<DomId, Path<CodId, CodId>>,
289    ob_inv: HashColumn<CodId, DomId>,
290}
291
292impl<'a, DomId, CodId, Cat> DiscreteDblModelMorphismFinder<'a, DomId, CodId, Cat>
293where
294    DomId: Clone + Eq + Hash,
295    CodId: Clone + Eq + Hash,
296    Cat: FgCategory,
297    Cat::Ob: Hash,
298    Cat::Mor: Hash,
299{
300    fn new(dom: &'a DiscreteDblModel<DomId, Cat>, cod: &'a DiscreteDblModel<CodId, Cat>) -> Self {
301        assert!(
302            Rc::ptr_eq(&dom.theory_rc(), &cod.theory_rc()),
303            "Domain and codomain model should have the same theory"
304        );
305        assert!(dom.is_free(), "Domain model should be free");
306
307        // Order the variables of the CSP, which are the elements of the domain
308        // graph. Prefer vertices with high degree since they are more
309        // constrained. This is a version of the well known "most constrained
310        // variable" heuristic in CSP.
311        let dom_graph = dom.generating_graph();
312        let mut vertices: Vec<_> = dom_graph.vertices().collect();
313        vertices.sort_by_key(|v| std::cmp::Reverse(dom_graph.degree(v)));
314        let var_order = spec_order(dom_graph, vertices.into_iter());
315
316        Self {
317            dom,
318            cod,
319            map: Default::default(),
320            results: Default::default(),
321            var_order,
322            max_path_len: None,
323            injective_ob: false,
324            faithful: false,
325            ob_init: Default::default(),
326            mor_init: Default::default(),
327            ob_inv: Default::default(),
328        }
329    }
330
331    /// Restrict the maximum length of the image of a generator.
332    pub fn max_path_len(&mut self, n: usize) -> &mut Self {
333        self.max_path_len = Some(n);
334        self
335    }
336
337    /// Restrict the search to monomorphisms between models.
338    pub fn monic(&mut self) -> &mut Self {
339        self.injective_ob = true;
340        self.faithful = true;
341        self
342    }
343
344    /// Restrict the search to model morphisms that are injective on objects.
345    pub fn injective_ob(&mut self) -> &mut Self {
346        self.injective_ob = true;
347        self
348    }
349
350    /** Restrict the search to model morphisms that are faithful.
351
352    A faithful morphism is an injective map on morphisms when restricted to any
353    domain/codomain pair of objects in the domain.
354
355    In future work, this will be efficiently checked for early search tree
356    pruning; however, this is currently enforced by filtering with
357    [is_free_simple_faithful](DiscreteDblModelMorphism::is_free_simple_faithful).
358     */
359    pub fn faithful(&mut self) -> &mut Self {
360        self.faithful = true;
361        self
362    }
363
364    /// Require morphisms to send object `ob` in domain to `val` in codomain.
365    pub fn initialize_ob(&mut self, ob: DomId, val: CodId) -> &mut Self {
366        self.ob_init.set(ob, val);
367        self
368    }
369
370    /// Require morphisms to send morphism `m` in domain to `val` in codomain.
371    pub fn initialize_mor(&mut self, m: DomId, val: Path<CodId, CodId>) -> &mut Self {
372        self.mor_init.set(m, val);
373        self
374    }
375
376    /// Finds all morphisms.
377    pub fn find_all(&mut self) -> Vec<DiscreteDblModelMapping<DomId, CodId>> {
378        self.search(0);
379        std::mem::take(&mut self.results)
380    }
381
382    fn search(&mut self, depth: usize) {
383        if depth >= self.var_order.len() {
384            if !self.faithful
385                || DblModelMorphism(&self.map, self.dom, self.cod).is_free_simple_faithful()
386            {
387                self.results.push(self.map.clone());
388            }
389            return;
390        }
391        let var = &self.var_order[depth];
392        match var.clone() {
393            GraphElem::Vertex(x) => {
394                if let Some(y) = self.ob_init.apply_to_ref(&x) {
395                    let can_assign = self.assign_ob(x.clone(), y.clone());
396                    if can_assign {
397                        self.search(depth + 1);
398                        self.unassign_ob(x, y)
399                    }
400                } else {
401                    for y in self.cod.ob_generators_with_type(&self.dom.ob_type(&x)) {
402                        let can_assign = self.assign_ob(x.clone(), y.clone());
403                        if can_assign {
404                            self.search(depth + 1);
405                            self.unassign_ob(x.clone(), y)
406                        }
407                    }
408                }
409            }
410            GraphElem::Edge(m) => {
411                if let Some(path) = self.mor_init.apply_to_ref(&m) {
412                    self.map.assign_mor(m, path);
413                    self.search(depth + 1);
414                } else {
415                    let functor = self.map.0.functor_into(&self.cod.category);
416                    let mor_type = self.dom.mor_generator_type(&m);
417                    let w = functor
418                        .apply_ob(self.dom.mor_generator_dom(&m))
419                        .expect("Domain should already be assigned");
420                    let z = functor
421                        .apply_ob(self.dom.mor_generator_cod(&m))
422                        .expect("Codomain should already be assigned");
423
424                    let cod_graph = self.cod.generating_graph();
425                    let th_cat = self.cod.theory().category();
426                    for path in bounded_simple_paths(cod_graph, &w, &z, self.max_path_len) {
427                        if th_cat.morphisms_are_equal(self.cod.mor_type(&path), mor_type.clone())
428                            && !(self.faithful && path.is_empty())
429                        {
430                            self.map.assign_mor(m.clone(), path);
431                            self.search(depth + 1);
432                        }
433                    }
434                }
435            }
436        }
437    }
438
439    /// Attempt an object assignment, returning true iff successful.
440    fn assign_ob(&mut self, x: DomId, y: CodId) -> bool {
441        if self.injective_ob {
442            if let Some(y_inv) = self.ob_inv.get(&y) {
443                if *y_inv != x {
444                    return false;
445                }
446            }
447        }
448        self.map.assign_ob(x.clone(), y.clone());
449        self.ob_inv.set(y, x);
450        true
451    }
452
453    /// Undo an object assignment.
454    fn unassign_ob(&mut self, _: DomId, y: CodId) {
455        self.ob_inv.unset(&y);
456    }
457}
458
459#[cfg(test)]
460mod tests {
461    use ustr::ustr;
462
463    use super::*;
464    use crate::dbl::model::UstrDiscreteDblModel;
465    use crate::one::Path;
466    use crate::stdlib::*;
467    use crate::validate::Validate;
468
469    #[test]
470    fn find_positive_loops() {
471        let th = Rc::new(th_signed_category());
472        let positive_loop = positive_loop(th.clone());
473        let pos = positive_loop.mor_generators().next().unwrap().into();
474
475        let maps = DiscreteDblModelMapping::morphisms(&positive_loop, &positive_loop).find_all();
476        assert_eq!(maps.len(), 2);
477        let mors: Vec<_> = maps
478            .into_iter()
479            .map(|map| map.functor_into(&positive_loop).mor_map().apply_to_ref(&pos))
480            .collect();
481        assert!(mors.iter().any(|mor| matches!(mor, Some(Path::Id(_)))));
482        assert!(mors.iter().any(|mor| matches!(mor, Some(Path::Seq(_)))));
483
484        let maps = DiscreteDblModelMapping::morphisms(&positive_loop, &positive_loop)
485            .monic()
486            .find_all();
487        assert_eq!(maps.len(), 1);
488        assert!(matches!(
489            maps[0].functor_into(&positive_loop).apply_mor(pos),
490            Some(Path::Seq(_))
491        ));
492    }
493
494    /// The [simple path](crate::one::graph_algorithms::simple_paths) should
495    /// give identical results to hom search from a walking morphism (assuming
496    /// all the object/morphism types are the same).
497    #[test]
498    fn find_simple_paths() {
499        let th = Rc::new(th_signed_category());
500
501        let mut walking = UstrDiscreteDblModel::new(th.clone());
502        let (a, b) = (ustr("A"), ustr("B"));
503        walking.add_ob(a, ustr("Object"));
504        walking.add_ob(b, ustr("Object"));
505        walking.add_mor(ustr("f"), a, b, Path::Id(ustr("Object")));
506
507        //     y         Graph with lots of cyclic paths.
508        //   ↗  ↘
509        // ↻x ⇆ z
510        let mut model = UstrDiscreteDblModel::new(th);
511        let (x, y, z) = (ustr("X"), ustr("Y"), ustr("Z"));
512        model.add_ob(x, ustr("Object"));
513        model.add_ob(y, ustr("Object"));
514        model.add_ob(z, ustr("Object"));
515        model.add_mor(ustr("xy"), x, y, Path::Id(ustr("Object")));
516        model.add_mor(ustr("yz"), y, z, Path::Id(ustr("Object")));
517        model.add_mor(ustr("zx"), z, x, Path::Id(ustr("Object")));
518        model.add_mor(ustr("xz"), x, z, Path::Id(ustr("Object")));
519        model.add_mor(ustr("xx"), x, x, Path::Id(ustr("Object")));
520
521        for i in model.ob_generators() {
522            for j in model.ob_generators() {
523                let maps: HashSet<_> = DiscreteDblModelMapping::morphisms(&walking, &model)
524                    .initialize_ob(ustr("A"), i)
525                    .initialize_ob(ustr("B"), j)
526                    .find_all()
527                    .into_iter()
528                    .map(|map| map.functor_into(&model).apply_mor_generator(ustr("f")).unwrap())
529                    .collect();
530                let spaths: HashSet<_> = simple_paths(model.generating_graph(), &i, &j).collect();
531                assert_eq!(maps, spaths);
532            }
533        }
534    }
535
536    #[test]
537    fn find_negative_loops() {
538        let th = Rc::new(th_signed_category());
539        let negative_loop = negative_loop(th.clone());
540        let base_pt = negative_loop.ob_generators().next().unwrap();
541
542        let negative_feedback = negative_feedback(th);
543        let maps = DiscreteDblModelMapping::morphisms(&negative_loop, &negative_feedback)
544            .max_path_len(2)
545            .find_all();
546        assert_eq!(maps.len(), 2);
547        let obs: Vec<_> = maps
548            .iter()
549            .map(|map| map.functor_into(&negative_feedback).apply_ob(base_pt))
550            .collect();
551        assert!(obs.contains(&Some(ustr("x"))));
552        assert!(obs.contains(&Some(ustr("y"))));
553
554        let im = maps[0].syntactic_image(&negative_feedback);
555        assert!(im.validate().is_ok());
556        assert!(im.has_mor(&Path::single(ustr("positive"))));
557        assert!(im.has_mor(&Path::single(ustr("negative"))));
558
559        let maps = DiscreteDblModelMapping::morphisms(&negative_loop, &negative_feedback)
560            .max_path_len(1)
561            .find_all();
562        assert!(maps.is_empty());
563    }
564
565    #[test]
566    fn validate_model_morphism() {
567        let theory = Rc::new(th_signed_category());
568        let negloop = negative_loop(theory.clone());
569        let posfeed = positive_feedback(theory.clone());
570
571        let f = DiscreteDblModelMapping::new(
572            [(ustr("x"), ustr("x"))].into(),
573            [(ustr(""), Path::Id(ustr("negative")))].into(),
574        );
575        let dmm = DblModelMorphism(&f, &negloop, &negloop);
576        assert!(dmm.validate().is_err());
577
578        // A bad map from h to itself that is wrong for the ob (it is in the map
579        // but sent to something that doesn't exist) and for the hom generator
580        // (not in the map)
581        let f = DiscreteDblModelMapping::new(
582            [(ustr("x"), ustr("y"))].into(),
583            [(ustr("y"), Path::Id(ustr("y")))].into(),
584        );
585        let dmm = DblModelMorphism(&f, &negloop, &negloop);
586        let errs: Vec<_> = dmm.validate().unwrap_err().into();
587        assert!(
588            errs == vec![
589                InvalidDblModelMorphism::Ob(ustr("x")),
590                InvalidDblModelMorphism::Mor(ustr("loop")),
591            ]
592        );
593
594        // A bad map that doesn't preserve dom
595        let f = DiscreteDblModelMapping::new(
596            [(ustr("x"), ustr("x"))].into(),
597            [(ustr("loop"), Path::single(ustr("positive1")))].into(),
598        );
599        let dmm = DblModelMorphism(&f, &negloop, &posfeed);
600        let errs: Vec<_> = dmm.validate().unwrap_err().into();
601        assert!(
602            errs == vec![
603                InvalidDblModelMorphism::Cod(ustr("loop")),
604                InvalidDblModelMorphism::MorType(ustr("loop")),
605            ]
606        );
607
608        // A bad map that doesn't preserve codom
609        let f = DiscreteDblModelMapping::new(
610            [(ustr("x"), ustr("x"))].into(),
611            [(ustr("loop"), Path::single(ustr("positive2")))].into(),
612        );
613        let dmm = DblModelMorphism(&f, &negloop, &posfeed);
614        let errs: Vec<_> = dmm.validate().unwrap_err().into();
615        assert!(
616            errs == vec![
617                InvalidDblModelMorphism::Dom(ustr("loop")),
618                InvalidDblModelMorphism::MorType(ustr("loop")),
619            ]
620        );
621    }
622
623    #[test]
624    fn validate_is_free_simple_monic() {
625        let theory = Rc::new(th_signed_category());
626        let negloop = positive_loop(theory.clone());
627
628        // Identity map
629        let f = DiscreteDblModelMapping::new(
630            [(ustr("x"), ustr("x"))].into(),
631            [(ustr("loop"), Path::single(ustr("loop")))].into(),
632        );
633        let dmm = DblModelMorphism(&f, &negloop, &negloop);
634        assert!(dmm.validate().is_ok());
635        assert!(dmm.is_free_simple_monic());
636
637        // Send generator to identity
638        let f = DiscreteDblModelMapping::new(
639            [(ustr("x"), ustr("x"))].into(),
640            [(ustr("loop"), Path::Id(ustr("x")))].into(),
641        );
642        let dmm = DblModelMorphism(&f, &negloop, &negloop);
643        assert!(dmm.validate().is_ok());
644        assert!(!dmm.is_free_simple_monic());
645    }
646
647    #[test]
648    fn monic_constraint() {
649        // The number of endomonomorphisms of a set |N| is N!.
650        let theory = Rc::new(th_signed_category());
651        let mut model = UstrDiscreteDblModel::new(theory.clone());
652        let (q, x, y, z) = (ustr("Q"), ustr("X"), ustr("Y"), ustr("Z"));
653        let ob = ustr("Object");
654        model.add_ob(q, ob);
655        model.add_ob(x, ob);
656        model.add_ob(y, ob);
657        model.add_ob(z, ob);
658        assert_eq!(
659            DiscreteDblModelMapping::morphisms(&model, &model)
660                .monic()
661                .find_all()
662                .into_iter()
663                .len(),
664            4 * 3 * 2
665        );
666
667        // Hom from noncommuting triangle into a pair of triangles, only one one
668        // of which commutes. There is only one morphism that is faithful.
669        let (f, g, h, i, j) = (ustr("f"), ustr("g"), ustr("h"), ustr("i"), ustr("j"));
670        let mut freetri = UstrDiscreteDblModel::new(theory.clone());
671        freetri.add_ob(x, ob);
672        freetri.add_ob(y, ob);
673        freetri.add_ob(z, ob);
674        freetri.add_mor(f, x, y, Path::Id(ob));
675        freetri.add_mor(g, y, z, Path::Id(ob));
676        freetri.add_mor(h, x, z, Path::Id(ob));
677
678        let mut quad = UstrDiscreteDblModel::new(theory);
679        quad.add_ob(q, ob);
680        quad.add_ob(x, ob);
681        quad.add_ob(y, ob);
682        quad.add_ob(z, ob);
683        quad.add_mor(f, x, y, Path::Id(ob));
684        quad.add_mor(g, y, z, Path::Id(ob));
685        quad.add_mor(i, y, q, Path::Id(ob));
686        quad.add_mor(j, x, q, Path::Id(ob));
687
688        assert_eq!(
689            DiscreteDblModelMapping::morphisms(&freetri, &quad)
690                .faithful()
691                .find_all()
692                .into_iter()
693                .len(),
694            1
695        );
696    }
697}
catlog/dbl/discrete/model_morphism.rs

catlog/dbl/discrete/
model_morphism.rs
