#!/usr/bin/env catnip
# Recollement de sections sur un espace fini
#
# Un préfaisceau associe à chaque ouvert U un ensemble de sections — ici les
# applications de U vers les entiers — et à chaque inclusion V ⊆ U une
# restriction. Ce préfaisceau est un faisceau quand toute famille de sections
# locales qui coïncident sur les intersections provient d'une unique section
# globale. Pour un recouvrement (U_i), la condition de descente s'écrit :
#
# s_i | (U_i ∩ U_j) = s_j | (U_i ∩ U_j) pour toute paire i, j
#
# Elle est vérifiée avant toute construction. Un recouvrement incompatible
# n'échoue donc pas en produisant une section arbitraire, mais en nommant le
# point et les deux valeurs qui se contredisent.
#
# Source:
# Mac Lane et Moerdijk (1992), "Sheaves in Geometry and Logic: A First
# Introduction to Topos Theory", Springer, chapitre II.
# Une section porte ses valeurs point par point. Son domaine effectif est
# l'ensemble des clés.
struct Section {
points: dict[str, int];
domain(self): set[str] => { set(*self.points.keys()) }
}
# Une paire d'indices du recouvrement, soit une arête du nerf de Čech.
#
# Le broadcast traite une struct comme une feuille, là où un tuple serait
# traversé élément par élément. Porter les paires dans une struct permet donc
# d'appliquer la loi de restriction à toute la famille d'un seul geste, sans
# imposer d'ordre entre les arêtes.
struct Pair { i: int; j: int; }
struct Conflict {
point: str; left: int; right: int;
display(self): str => { f"{self.point} vaut {self.left} d'un côté, {self.right} de l'autre" }
}
# Tous les désaccords relevés sur une intersection. Un recouvrement satisfait
# la descente quand chaque intersection en est dépourvue.
struct Overlap {
left: int; right: int; shared: set[str]; conflicts: list[Conflict];
ok(self): bool => { len(self.conflicts) == 0 }
}
# Restriction d'une section à un sous-ouvert. La section d'origine n'est pas
# mutée : le résultat est une nouvelle section.
#
# Les points sont parcourus dans l'ordre pour que l'affichage d'une section ne
# dépende pas de l'ordre d'itération du set qui la porte.
restrict = (section: Section, region: set[str]): Section => {
kept = dict()
for point in sorted(region) {
if point in section.points {
kept[point] = section.points[point]
}
}
Section(kept)
}
# Toutes les arêtes du nerf, y compris celles d'intersection vide : une
# intersection vide impose une contrainte vide, jamais un conflit.
index_pairs = (size: int): list[Pair] => {
pairs = list()
for i in range(size) {
for j in range(i + 1, size) {
pairs = pairs + list(Pair(i, j))
}
}
pairs
}
# Compare deux sections sur leur intersection et retient chaque désaccord.
#
# La closure capture le recouvrement et la famille, de sorte que la fonction
# rendue ne dépende plus que de l'arête. C'est cette fonction que le broadcast
# applique.
overlap_checker = (regions: list[set[str]], sections: list[Section]) => {
(pair: Pair): Overlap => {
shared = regions[pair.i].intersection(regions[pair.j])
left = restrict(sections[pair.i], shared)
right = restrict(sections[pair.j], shared)
conflicts = list()
for point in sorted(shared) {
if left.points[point] != right.points[point] {
found = Conflict(point, left.points[point], right.points[point])
conflicts = conflicts + list(found)
}
}
Overlap(pair.i, pair.j, shared, conflicts)
}
}
# Vérifie toute la famille. Les domaines sont contrôlés d'abord : une section
# qui ne couvre pas l'ouvert annoncé ne définit pas d'élément de F(U_i), et
# comparer ses restrictions n'aurait pas de sens.
descent = (regions: list[set[str]], sections: list[Section]): list[Overlap] => {
if len(regions) != len(sections) {
raise ValueError("un recouvrement et sa famille de sections doivent avoir la même taille")
}
for i in range(len(regions)) {
if sections[i].domain() != regions[i] {
raise ValueError(f"la section s{i} n'est pas définie exactement sur U{i}")
}
}
index_pairs(len(regions)).[overlap_checker(regions, sections)]
}
# Construit la section globale, ou refuse en localisant le premier désaccord.
glue = (regions: list[set[str]], sections: list[Section]): Section => {
overlaps = descent(regions, sections)
for overlap in overlaps {
if not overlap.ok() {
raise ValueError(
f"descente rejetée sur U{overlap.left} ∩ U{overlap.right} : {overlap.conflicts[0].display()}"
)
}
}
glued = dict()
for i in range(len(regions)) {
for point in sorted(regions[i]) {
glued[point] = sections[i].points[point]
}
}
Section(glued)
}
# L'unicité se contrôle par le bas : la section globale doit redonner chaque
# section locale par restriction.
is_gluing_of = (whole: Section, regions: list[set[str]], sections: list[Section]): bool => {
agreements = list()
for i in range(len(regions)) {
agreements = agreements + list(restrict(whole, regions[i]) == sections[i])
}
all(agreements)
}
# Les points sur lesquels au moins une paire d'ouverts se contredit.
conflict_points = (overlaps: list[Overlap]): set[str] => {
flagged = set()
for overlap in overlaps {
for conflict in overlap.conflicts {
flagged = flagged.union(set(conflict.point))
}
}
flagged
}
# Une ligne par ouvert, une colonne par point du site, une case vide là où
# l'ouvert ne contient pas le point.
#
# La condition de descente se lit alors par colonne : un point est recollable
# quand tous les ouverts qui le contiennent lui donnent la même valeur, et une
# colonne portant deux valeurs distinctes est exactement un échec de descente.
# Le recollement est la lecture de chaque colonne constante.
print_table = (regions: list[set[str]], sections: list[Section], site: list[str], flagged: set[str]) => {
header = " "
for point in site {
header = header + f"{point:>6}"
}
print(header.rstrip())
for i in range(len(regions)) {
row = f" U{i} "
for point in site {
if point in sections[i].points {
row = row + f"{sections[i].points[point]:>6}"
} else {
row = row + " "
}
}
print(row.rstrip())
}
if len(flagged) > 0 {
marks = " "
for point in site {
if point in flagged {
marks = marks + f"{'↑':>6}"
} else {
marks = marks + " "
}
}
print(marks.rstrip())
}
}
# ⇒ Le site fini
#
# A ---- B ---- C U0 = {A, B}
# | U1 = {B, C}
# D U2 = {B, D}
#
# Les trois ouverts se rencontrent en B, qui porte donc toute la contrainte.
U0 = set("A", "B")
U1 = set("B", "C")
U2 = set("B", "D")
regions = list(U0, U1, U2)
covered = set()
for region in regions {
covered = covered.union(region)
}
site = sorted(covered)
print("⇒ Site fini")
print(" points :", site)
print(" U0 =", sorted(U0))
print(" U1 =", sorted(U1))
print(" U2 =", sorted(U2))
print(" arêtes du nerf :", len(index_pairs(len(regions))))
print()
# ⇒ Famille compatible
compatible = list(
Section(dict(A=12, B=18)),
Section(dict(B=18, C=25)),
Section(dict(B=18, D=31)),
)
print("⇒ Famille compatible")
compatible_overlaps = descent(regions, compatible)
print_table(regions, compatible, site, conflict_points(compatible_overlaps))
print()
for overlap in compatible_overlaps {
print(f" U{overlap.left} ∩ U{overlap.right} = {sorted(overlap.shared)} : {overlap.ok()}")
}
whole = glue(regions, compatible)
print(" section globale :", whole.points)
print(" redonne chaque section locale :", is_gluing_of(whole, regions, compatible))
print()
if whole.domain() != covered {
raise RuntimeError("la section globale ne couvre pas l'union du recouvrement")
}
if not is_gluing_of(whole, regions, compatible) {
raise RuntimeError("la section globale ne se restreint pas à la famille locale")
}
# ⇒ Famille incompatible
#
# U1 affirme maintenant B = 99 là où U0 et U2 affirment B = 18. Deux arêtes
# sur trois deviennent contradictoires, et le recollement est refusé avant
# d'avoir écrit le moindre point.
incompatible = list(
Section(dict(A=12, B=18)),
Section(dict(B=99, C=25)),
Section(dict(B=18, D=31)),
)
print("⇒ Famille incompatible")
overlaps = descent(regions, incompatible)
print_table(regions, incompatible, site, conflict_points(overlaps))
print()
for overlap in overlaps {
print(f" U{overlap.left} ∩ U{overlap.right} = {sorted(overlap.shared)} : {overlap.ok()}")
}
if all(overlaps.[(overlap: Overlap): bool => { overlap.ok() }]) {
raise RuntimeError("la descente aurait dû rejeter cette famille")
}
try {
impossible = glue(regions, incompatible)
raise RuntimeError(f"section globale inattendue : {impossible.points}")
} except {
error: ValueError => { print(" recollement impossible —", error) }
}