Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passverified 2026-08-04 (gpt-5.6-sol-codex-subscription)
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 cylinder and the Mobius band as quotients of the square by (0,y)∼(1,y) and by (0,y)∼(1,1−y), both by a closed quotient map

Example

Let S:=[0,1]×[0,1] be the unit square, which carries one topology by claim 1 of Products commute with subspaces; for infinite nonempty families, the closure identity ∏Ai‾=∏Ai‾ uses the Axiom of Choice (For n≥1 the product topology on n copies of the usual topology of R is the metric topology of d∞ on Rn, and hence also of d1 and d2, so Rn as a product and Rn as a metric space are one space, 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, Intervals of R: the nine order-convex forms, nondegeneracy, and length). Define two relations on S, in each case leaving every point not on the two vertical edges alone:

cylinder:(0,y)∼c(1,y);Mobius band:(0,y)∼m(1,1−y)(y∈[0,1]).

Precisely, ∼c has as classes the pairs {(0,y),(1,y)} and the singletons {(s,t)} with 0<s<1; ∼m has as classes the pairs {(0,y),(1,1−y)} and the same singletons. Write Mc:=S/ ⁣∼c (the cylinder) and Mm:=S/ ⁣∼m (the Mobius band), each with the quotient topology (The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection) and canonical projection Pc, Pm. Then:

  1. Both projections are closed quotient maps: the saturation of a closed subset of S is closed, so Pc and Pm carry closed sets to closed sets (A continuous open surjection, a continuous closed surjection, and a continuous surjection admitting a continuous section are all quotient maps).
  2. The cylinder is (R/Z)×[0,1]. With T=R/Z and its open quotient map q (R/Z: the quotient map is open, and the quotient is homeomorphic to [0,1] with its endpoints identified), the map Q1:=q×id[0,1] is an open quotient map R×[0,1]→T×[0,1] and induces a homeomorphism Mc≅T×[0,1] (Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological).

Nothing here claims that the cylinder and the Mobius band are different spaces. Distinguishing them needs an invariant, and the standard ones are not available at this point in the reading order (What the theory of these constructions still owes at this point in the reading order: preservation of quotient maps under products, separation beyond Hausdorff, and the invariants that tell the glued spaces apart). Both are recorded as constructions, and only the cylinder is identified with a space built earlier.

Facts & Assumptions

Given: The square S=[0,1]×[0,1]; the relations ∼c and ∼m with their quotients and projections; the edges E0:={0}×[0,1] and E1:={1}×[0,1]; T=R/Z with projection q; the maps Q1:=q×id:R×[0,1]→T×[0,1] and F1:R×[0,1]→Mc, F1(x,y):=Pc(x−⌊x⌋, y).

[A1]

For a quotient Z/ ⁣∼ with projection Π: Π is a surjection, W is open exactly when Π−1[W] is open, W is closed exactly when Π−1[W] is closed, and Π−1[Π[A]] is the saturation of A (The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection, The adjunction space Y∪fX glued along a continuous map, and, for a nonempty space, the cone and the suspension as quotients of X×[0,1]).

[A2]

q is a surjective open quotient map with q(x)=q(x′) exactly when x−x′∈Z; for every real x there is exactly one integer ⌊x⌋ with ⌊x⌋≤x<⌊x⌋+1, and ⌊x+m⌋=⌊x⌋+m for integers m (R/Z: the quotient map is open, and the quotient is homeomorphic to [0,1] with its endpoints identified, Integer part: for every real x there is exactly one integer m with m≤x<m+1, The integers as equivalence classes of pairs of naturals).

[L1]

A continuous closed surjection and a continuous open surjection are quotient maps (A continuous open surjection, a continuous closed surjection, and a continuous surjection admitting a continuous section are all quotient maps, clauses 1 and 2); for a quotient map s and a continuous f constant on its fibres there is exactly one continuous fˉ with fˉ∘s=f (For a quotient map q:X→Y, a map out of Y is continuous iff its composite with q is; a continuous map on X constant on the fibres of q factors uniquely through q; and a composite of quotient maps is a quotient map, claim 2).

[L5]

The pasting technique of The square with opposite edges identified is homeomorphic to the product (R/Z)×(R/Z): a map defined on R by taking a fractional part and then applying a quotient projection that identifies the two endpoints of [0,1] is continuous, because on [m−1,m+1] it agrees with a map glued from two continuous pieces over the finite closed cover {[m−1,m], [m,m+1]}, and the open intervals (m−1,m+1), m∈Z, cover R.

Verification

technique · direct
1.1

E0 and E1 are closed in S: each is the trace on S of a closed subset of R2, namely {0}×R and {1}×R, whose complements are open by [L2] and [L4].

L2L4
1.2

The maps τc(0,y):=(1,y) and τm(0,y):=(1,1−y) are homeomorphisms E0→E1, being y↦y and y↦1−y read through the homeomorphisms y↦(0,y) and y↦(1,y) of [0,1] onto E0 and E1, and both are continuous with continuous inverses by [L2], [L3] and [L4].

L2L3L4
1.3

For C⊆S the saturation of C under ∼c is C∪τc[C∩E0]∪τc−1[C∩E1], since the only non-singleton classes are the pairs {(0,y),(1,y)}; the same formula with τm gives the saturation under ∼m.

givenA1
1.4

Q1 is continuous, surjective and open: continuity and surjectivity are [L2] and [A2] coordinatewise, and Q1[U×V]=q[U]×V for U open in R and V open in [0,1], which is open by [A2] and [L2]; images of unions are unions of images. By [L1] it is an open quotient map.

A2L1L2
1.5

Q1(x,y)=Q1(x′,y′) exactly when x−x′∈Z and y=y′, by [A2]; so the restriction E:=Q1↾S has exactly the classes of ∼c as its fibres, and E is continuous by [L3] and surjective, since x−⌊x⌋∈[0,1) by [A2].

A2L3
1.6

F1 is constant on the fibres of Q1, since x−⌊x⌋ depends only on the class of x modulo Z by [A2], and it is continuous by [L5] applied in the first variable, the second variable being untouched, together with [L2] and [L3].

A2L2L3L5
2.1

If C is closed in S then C∩E0 is closed in E0 and hence in S by step 1.1 and [L4], so τc[C∩E0] is closed in E1 by step 1.2 and hence in S; likewise for τc−1[C∩E1]. So by step 1.3 the saturation of C is a union of three closed sets, hence closed, and Pc[C] is closed by [A1]. The same argument with τm gives the statement for Pm.

step 1.1step 1.2step 1.3A1L4
2.2

By step 1.5 and [L1] applied to the quotient map Pc and the continuous E, there is exactly one continuous Eˉ:Mc→T×[0,1] with Eˉ∘Pc=E; by step 1.6 and [L1] applied to the quotient map Q1 of step 1.4 and the continuous F1, there is exactly one continuous Fˉ:T×[0,1]→Mc with Fˉ∘Q1=F1.

step 1.4step 1.5step 1.6A1L1
3.1

Fˉ∘Eˉ=id and Eˉ∘Fˉ=id: for (s,t)∈S one has Fˉ(Eˉ(Pc(s,t)))=F1(s,t)=Pc(s−⌊s⌋, t), which is Pc(s,t) because ⌊s⌋=0 for s∈[0,1) and (0,t)∼c(1,t) for s=1; and for (x,y)∈R×[0,1] one has Eˉ(Fˉ(Q1(x,y)))=E(x−⌊x⌋, y)=Q1(x,y) by [A2]. Both Pc and Q1 are surjective.

step 1.4step 1.5step 2.2A1A2
4.1

Claim 1 is step 2.1, and claim 2 follows from steps 2.2 and 3.1, the maps Eˉ and Fˉ being mutually inverse and continuous, hence homeomorphisms.

step 2.1step 2.2step 3.1∎

Remarks

  • The two constructions differ in one sign and in nothing else. They use the same square, the same two edges and the same kind of relation; the Mobius band glues the left edge to the right edge after reversing it. Claim 1 is proved for both. Claim 2 is not: it identifies the cylinder with (R/Z)×[0,1], and no analogous description of the Mobius band is attempted here. Separating the two spaces would need an invariant, and none is claimed here.

  • Why closedness rather than openness. Neither projection is open. Take U:={ (s,t)∈S:s<1/2 }, which is open in S; its saturation is U∪({1}×[0,1]), and that is not open in S, because every neighbourhood in S of the point (1,1/2) contains points (s,1/2) with 1/2<s<1, which lie in neither piece. So Pc[U] is not open, and the same computation applies to Pm; this is the failure recorded in FALSE: every quotient map is an open map. Closedness holds instead because the two edges are closed and the gluing map between them is a homeomorphism, which is what step 2.1 uses.

  • The cylinder is a product and the Mobius band is not built as one. Claim 2 writes Mc as T×[0,1]; no analogous description is attempted for Mm, and none is available at this point in the reading order.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

81 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