Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)verified 2026-07-29 (claude-fable-5)
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The diagonal ΔX⊆X×X, the diagonal map δX, and the pairing ⟨f,g⟩ of two maps

Definition

Let (X,T) and (Y,TY) be topological spaces (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison). Throughout, X×Y is the binary product ∏i<2Xi with X0=X and X1=Y (The product set ∏i∈IXi of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space), carrying the product topology; a point of it is a function z on the von Neumann natural 2={0,1}, written (z0,z1), and π0,π1 are the two projections.

The basis used throughout. For the index set 2 the product basis and the box basis coincide, since a box ∏i<2Ui has all but finitely many factors unrestricted for the trivial reason that it has only two (The product set ∏i∈IXi of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space). So

{ U×V:U∈T, V∈TY }

is a basis for the product topology on X×Y, and every statement below that tests a basic open set tests a box of two open sets.

The diagonal. The diagonal of X is

ΔX  :=  { z∈X×X:z0=z1 }  =  { (x,x):x∈X },

the second description being the first read through the definition of a point of the product as a function on 2. It is a subset of X×X and is given the subspace topology (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace) whenever it is regarded as a space.

The diagonal map. The diagonal map of X is

δX:X→X×X,δX(x):=(x,x),

that is, the function sending x to the constant function 2→X with value x. Its two components are π0∘δX=idX and π1∘δX=idX, and by claim 2 of A map into a product is continuous iff each of its components is; the projections are continuous and open; and each projection is surjective when every factor is nonempty, which for an infinite index set uses the Axiom of Choice it is the unique function X→X×X with those two components. The same claim makes it continuous (Continuity of a map of topological spaces at a point and globally), the identity being continuous. Its image is ΔX, and it is injective, since δX(x)=δX(x′) forces x=x′ by reading the coordinate at 0. Whether δX is an embedding onto ΔX (Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological) is not asserted here; it is the content of the next item.

The pairing of two maps. For functions f:Z→X and g:Z→Y on a common domain, the pairing is

⟨f,g⟩:Z→X×Y,⟨f,g⟩(z):=(f(z),g(z)).

By claim 2 of A map into a product is continuous iff each of its components is; the projections are continuous and open; and each projection is surjective when every factor is nonempty, which for an infinite index set uses the Axiom of Choice it is the unique function Z→X×Y with π0∘⟨f,g⟩=f and π1∘⟨f,g⟩=g; no hypothesis on f and g is needed for the pairing to be defined, and continuity of the pairing is exactly continuity of both components, which is again that claim. In this notation

δX=⟨idX,idX⟩,

so the diagonal map is a special case of the pairing and needs no separate treatment.

The preimage identity that every later proof uses. For f,g:Z→Y,

⟨f,g⟩−1[ΔY]  =  { z∈Z:f(z)=g(z) },

directly from the definitions above: ⟨f,g⟩(z)∈ΔY says that the function (f(z),g(z)) on 2 takes the same value at 0 and at 1.

Remarks

Depends on

Used by

Dependency tree · two levels

18 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources