Page 91 - Textos de Matemática Vol. 41

12.2. Composition of entourages 77 general. However, as we shall see below, restricted to relations given by open
sublocales, it is indeed associative and provides a nice calculus.
12.2.1. Theorem. Applied to relations given by open sublocales the composite above is given by
o(E)◦o(F)=o{a⊕b|a⊕c⊆E,c⊕b⊆F for some c̸=0}. (12.12.1)
Proof. The categorical composite of jE : o(E) → L⊕L with jF : o(F) → L⊕L istheimagem:M′ →L⊕Loftheuniquemapφ:M→L⊕Lsuch that p1φ = p1jFφ1 and p2φ = p2jEφ2, where (M,φ1,φ2) is the pullback of (p1jE,p2jF):
L ⊕ L p2 ``B hhQQQ
B QQm
B QQQQQ
BB QQQ ′
// L FF

p1
B φ2 // M o(E)
φ
B B
OOOO p2 jE Be
BM
nnnnnnnnno(F) p2jF vvnnnnnn p1jF
//
φ1

p1jE L
L
We need to show that the sublocale m : M′ → L ⊕ L is precisely
jo(E◦F) :o(E◦F)→L⊕L where E ◦ F denotes the saturated
{a⊕b|a⊕c⊆E,c⊕b⊆F forsomec̸=0}.
We shall use the fact from 6.2 that any open sublocale jE : o(E) → L ⊕ L is identified with the nucleus jEjE∗ (G) = E → G, which is also given by the localic map (G → E → G) :↓E → L⊕L. So it suffices to check that mm∗(G) = (E ◦ F ) → G for every G ∈ L ⊕ L. In order to do that we need to construct φ : M → L ⊕ L. We do that in two steps:
(1) The pullback of (p′1, p′2) = (p1jE , p2jF ) is the locale
M =↓IE,G ={G∈L⊕L⊕L|G⊆IE,F},