Alexandrov Monotone Continuity

Abstract

Maps between upper Alexandrov spaces are continuous exactly when they are monotone.

Theorem 1.1 (Continuity between upper Alexandrov spaces is monotonicity).

$$\begin{array}{c}\forall relationX:X\to X\to \mathrm{Prop},relationY:Y\to Y\to \mathrm{Prop},map:X\to Y,\\ [\mathrm{Refl}\left(relationX\right)][\mathrm{IsTrans}\left(X,relationX\right)][\mathrm{Refl}\left(relationY\right)][\mathrm{IsTrans}\left(Y,relationY\right)]\Rightarrow \\ (\mathrm{Continuous}\left(\mathrm{upperSetTopology}\left(relationX\right),\mathrm{upperSetTopology}\left(relationY\right),map\right)⟺\mathrm{RelationMonotone}\left(relationX,relationY,map\right)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DependencyTopology/AlexandrovMonotoneContinuity.continuous_upperSetTopology_iff_monotone (✓ std3). ∎

Source. Repository-derived.

Commentary.

Fix reflexive and transitive relations on the source and target and give each carrier its upper-set Alexandrov topology.

Continuity pulls the principal upset of a mapped source point back to an open source set. Upward closure of that preimage forces the map to preserve the relation.

Conversely, a relation-preserving map sends every source relation step to a target relation step, so preimages of target upper sets are upper and therefore open.

Theorem 1.2 (A monotone dependency map is continuous).

$$\begin{gathered} \forall edgeX:X\to X\to \mathrm{Prop},edgeY:Y\to Y\to \mathrm{Prop},map:X\to Y, \\ \mathrm{RelationMonotone}\left(\mathrm{Reachable}\left(edgeX\right),\mathrm{Reachable}\left(edgeY\right),map\right)\Rightarrow \\ \mathrm{Continuous}\left(\mathrm{dependencyTopology}\left(edgeX\right),\mathrm{dependencyTopology}\left(edgeY\right),map\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DependencyTopology/AlexandrovMonotoneContinuity.monotone_continuous_dependencyTopology (✓ std3). ∎

Source. Repository-derived.

Commentary.

RelationMonotone here means that the map preserves reflexive-transitive dependency reachability from the source graph to the target graph.

Applying the upper-Alexandrov equivalence to those two reachability relations yields continuity between the corresponding dependency topologies.

References

• Truth anchor: D5/S3/ConceptDynamics/DependencyTopology/AlexandrovMonotoneContinuity.continuous_upperSetTopology_iff_monotone
• Truth anchor: D5/S3/ConceptDynamics/DependencyTopology/AlexandrovMonotoneContinuity.monotone_continuous_dependencyTopology
• Dependency: D5/S3/ConceptDynamics/DependencyTopology/AlexandrovDependencyTopology