From 8dbf76724a7fe1f1e25b8f463e31b635ed79a5b5 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Thu, 23 Nov 2017 20:59:38 +0100 Subject: [PATCH] Appendix: CMRA morphisms are homomorphisms --- CHANGELOG.md | 2 +- docs/algebra.tex | 10 ++++++---- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index a3305d69..de7d68ab 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,7 +8,7 @@ Coq development, but not every API-breaking change is listed. Changes marked Changes in and extensions of the theory: * [#] Add new modality: ■ ("plainly"). -* [#] Camera morphisms have to be homomorphisms, not just monotone functions. +* Camera morphisms have to be homomorphisms, not just monotone functions. * Add a proof that f has a fixed point if f^k is contractive. * Constructions for least and greatest fixed points over monotone predicates (defined in the logic of Iris using impredicative quantification). diff --git a/docs/algebra.tex b/docs/algebra.tex index 972778a8..9cfed25e 100644 --- a/docs/algebra.tex +++ b/docs/algebra.tex @@ -213,14 +213,16 @@ Note that for RAs, this and the RA-based definition of a frame-preserving update Note that every RA is a discrete CMRA, by picking the discrete COFE for the equivalence relation. Furthermore, discrete CMRAs can be turned into RAs by ignoring their COFE structure, as well as the step-index of $\mval$. -\begin{defn} - A function $f : \monoid_1 \to \monoid_2$ between two CMRAs is \emph{monotone} (written $f : \monoid_1 \monra \monoid_2$) if it satisfies the following conditions: +\begin{defn}[CMRA homomorphism] + A function $f : \monoid_1 \to \monoid_2$ between two CMRAs is \emph{a CMRA homomorphism} if it satisfies the following conditions: \begin{enumerate}[itemsep=0pt] \item $f$ is non-expansive + \item $f$ commutes with composition:\\ + $\All \melt_1 \in \monoid_1, \melt_2 \in \monoid_1. f(\melt_1) \mtimes f(\melt_2) = f(\melt_1 \mtimes \melt_2)$ + \item $f$ commutes with the core:\\ + $\All \melt \in \monoid_1. \mcore{f(\melt)} = f(\mcore{\melt})$ \item $f$ preserves validity: \\ $\All n, \melt \in \monoid_1. \melt \in \mval_n \Ra f(\melt) \in \mval_n$ - \item $f$ preserves CMRA inclusion:\\ - $\All \melt \in \monoid_1, \meltB \in \monoid_1. \melt \mincl \meltB \Ra f(\melt) \mincl f(\meltB)$ \end{enumerate} \end{defn} -- GitLab