Как определить взаимно однозначное отношение в сплаве

У меня есть три подписи из сплава, как показано ниже:

sig A{}
sig B{}
sig C{}

Как я могу определить биективное отношение (или изоморфизм) между C и A + B.


person qartal    schedule 08.12.2014    source источник
comment
Биекции бывают как взаимно однозначные, так и на / инъективные и сюръективные. Я не знаком со сплавом, чтобы помочь вам в дальнейшем, но я подумал, что хочу убедиться, что определение биекции было ясным. Более того, поскольку я не уверен, что вы использовали эти термины как синонимы, изоморфизм - это не просто биективное отображение. Это должно быть биективное линейное отображение (оно должно сохранять сложение и скалярное умножение векторного пространства).   -  person Zéychin    schedule 08.12.2014


Ответы (1)


Отношение взаимно однозначности должно быть инъективным и сюръективным. поэтому ответ будет следующим:

sig A {}
sig B{}
sig C{r : one A+B}

fact { 
    all c1,c2: C | c1.r=c2.r implies c1=c2   // r is injective
    all ab: A+B | some c:C | c.r=ab   // r in surjective
} 

Наверное, есть более короткий способ написать это. Другие люди могут комментировать.

Спасибо

person qartal    schedule 08.12.2014
comment
[code] fact r_bijective {r in C one- ›one (A + B)} [/ code] должно быть достаточно. - person user1513683; 10.12.2014