Alphabeta MathDimension Constructible Images and Dimensions of Fibres
About this page
Pipeline-generated
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.
✓ 2 results · all verified · 0 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 2 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.
1 · Prerequisites
- Affine Algebraic Sets and Coordinate Rings
- Algebraic Extensions, Extension Degree, and Finite Fields
- Associated Primes and Primary Decomposition
- Binary Operations, Monoids, Groups and Subgroups
- Categories, Functors and Natural Transformations
- Chain Conditions, Semisimple Modules and the Wedderburn–Artin Theorem
- Classical Affine Varieties: Coordinate Rings, Morphisms, and Rational Maps
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Determinants of Matrices over a Commutative Ring
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Eigenvalues, Eigenvectors and the Characteristic Polynomial
- Finite Counting, Factorials and Binomial Coefficients
- Finite Fields and Cyclotomic Extensions
- Foundations of the Real Numbers for Analysis
- Free Modules, Exact Sequences, Projective and Injective Modules
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Group Homomorphisms and the Isomorphism Theorems
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Integral Extensions and Going Up
- Krull Dimension and Height Theorems
- Limits and Colimits
- Linear Independence, Bases and Dimension
- Localisation of Modules and Support
- Modules, Submodules, Quotient Modules and the Isomorphism Theorems
- Morphisms Local Rings and Rational Maps of Affine Varieties
- Noether Normalisation and Nullstellensatz
- Noetherian Rings and Hilbert Basis
- Normal Subgroups and Quotient Groups
- Order, Zorn's Lemma, and the Axiom of Choice
- Ordinals, Cardinals, and Transfinite Recursion
- Polynomial Rings, the Division Algorithm and Roots
- Presheaves Sheaves Stalks and Sheafification
- Prime Spectra and Radicals
- Products Segre and Veronese Embeddings and Grassmannians
- Projective Algebraic Sets Projective Morphisms and Cones
- Rees Modules Artin Rees and Hilbert Samuel Theory
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Roots, Rational Powers, and Classical Inequalities
- Sheaf Operations Exactness Ringed Spaces and Module Pullback
- Simple Field Extensions and the Construction of the Complex Numbers
- Splitting Fields
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- Tensor Products of Modules
- The Determinant of a Linear Operator, Cofactors and Cramer's Rule
- The Field of Fractions and Localisation
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Vector Spaces, Linear Subspaces, Span and Direct Sums
- Zariski Topology on Prime Spectra
2 · Logical flowchart
3 · Items
Definition
Chain dimension and the empty-space convention
Lemma
Dimension of a finite closed union
Lemma
Dimension can be computed on an open cover
Lemma
Classical varieties have finite irreducible decompositions
Definition
Global and local dimension of classical varieties
Theorem
Affine geometric dimension equals ring dimension
Lemma
Function fields and dominant pullbacks on general varieties
Theorem
Dimension equals transcendence degree
Lemma
Nonempty opens preserve irreducible dimension
Corollary
Affine and projective n-space have dimension n
Corollary
Dimension is birationally invariant
Theorem
Dimensions add under products
Definition
Codimension of an irreducible closed subvariety
Theorem
A nontrivial principal section has pure codimension one
Lemma
r equations lower dimension by at most r
Lemma
Closed-point local dimension equals ambient irreducible dimension
Lemma
A point is locally cut out by dim X functions
Lemma
Zero-dimensional varieties are finite sets
Corollary
Maximal chains in an irreducible variety
Definition
Locally closed and constructible subsets
Lemma
Constructible subsets form a Boolean algebra
Lemma
Dense constructible subsets contain an open
Lemma
A dominant affine map factors finitely over relative affine space after shrinking the base
Lemma
Dominant affine images contain a principal open
Theorem
Chevalley: images of constructible sets are constructible
Corollary
A dominant image contains a dense open
Definition
Reduced closed-point fibres and their dimension
Theorem
Every fibre component has the expected lower bound
Theorem
Fibres have pure expected dimension over a dense open
Corollary
Image dimension and the generic fibre formula
Definition
Quasi-finite classical morphisms
Theorem
Equal dimension is equivalent to generic quasi-finiteness
Lemma
Affine intersection bound via the diagonal
Lemma
A nonempty projective cone raises dimension by one
Lemma
Nontrivial projective hypersurface sections
Corollary
Several homogeneous equations in projective space
Theorem
Projective intersection dimension and nonemptiness
Lemma
Dimension is detected by avoiding linear subspaces
Lemma
Projective space over a classical base and homogeneous closed loci
Theorem
Projection from projective space over a variety is closed
Definition
Projective classical morphisms
Theorem
Projective fibre dimension is upper semicontinuous
Corollary
Closed families with irreducible equal-dimensional fibres
Definition
Module-finite affine maps for the quasi-finite comparison
Corollary
Module-finite affine maps have finite fibres
Remark
Hypotheses and conventions in dimension theory
Sources
- Milne §3l Definition 3.39 and §2m Definition 2.48
- Milne §2m 2.49 p.54: maximum over irreducible components
- Milne §3l chain interpretation; §5j p.115
- Milne §5j p.115
- Milne §5j p.115 and §3c Note 3.13 p.63; local-dimension convention prescribed by AV-5 design
- Milne Definition 3.39 and chain/prime dictionary §3l
- Milne §§5j–k pp.115–116
- Milne §5j, p.115
- Arapura §4.1, p.30
- Arapura Example 4.1.1
- Milne §5l, Proposition 5.39, p.117
- Milne Proposition 5.35, §5j
- Milne §3l and §5j
- Milne Theorem 3.42, p.76
- Arapura Theorem 4.1.6, p.31; restricted to irreducible X
- Milne Corollary 3.45
- Milne §3l, chain-height interpretation
- Milne Proposition 3.47 specialized to a point
- Arapura §4.1 opening, p.30
- Milne §5j finite components and §9b fibres
- Milne Corollaries 3.43–3.44, pp.76–77
- Milne §9a p.200
- Milne §9a p.200, paragraph preceding Proposition 9.6
- Milne Proposition 9.6
- Vakil Theorem 12.4.1 proof, pp.354–356 (July 27 2024)
- Milne Theorem 9.1, p.198
- Vakil Theorem 12.4.1 proof, pp.354–356
- Milne Theorem 9.7
- Milne Theorem 9.1 and Proposition 9.6
- Arapura §4.2, pp.31–32
- Milne §9b, pp.201–204
- Arapura Theorem 4.2.1, p.31
- Milne Theorem 9.9(b), lower-bound proof, p.203
- Vakil Theorem 12.4.1 and Corollary 12.4.2, pp.354–356
- Milne §9b opening and Theorem 9.9
- Milne §8c Quasi-finite maps, p.185
- Arapura Corollary 4.2.2, p.31
- Arapura Lemma 4.1.3 and Corollary 4.2.2
- Milne Proposition 5.36
- Milne §6p proof of Theorem 6.43 and Corollary 6.47
- Milne Theorem 6.43, printed p.156
- Milne Corollary 6.44, p.156
- Milne Corollary 6.47
- Milne Proposition 6.48 and Lemma 6.49
- Milne §6q Lemma 6.51(a,b), p.158
- Milne Theorem 7.22, pp.164–165
- Vakil Class 38 §3, proof of Theorem 3.1
- Vakil Class 38 Exercise 3.B and its preceding proof, pp.4–5
- Milne Proposition 9.11
- Milne §8c Definition 8.17, affine case, p.181
- Milne Proposition 8.28 and Lemma 8.29, p.185
- Milne §§5j, 9b; qualifications explained in the local theorems
- Arapura Chapter 4, §§4.1–4.2