nLab
discrete mathematics

A good part of mathematics refers to continuous or even smooth spaces of various kinds. Discrete mathematics is about discrete structures: logic and combinatorics are typical fields in this domain. Much of algebra, set theory, type theory, category theory and higher category theory are discrete. Infinity category theory is discrete as well, thus including homotopy type theory and much of synthetic homotopy theory in discrete mathematics. Continuous structures in mathematics are typically structures with some notion of continuous topology, smoothness, or continuous cohesion or structures expressed in a geometric theory. In essence, discrete mathematics is about homotopy type theory, while continuous mathematics is about continuous homotopy type theory or real-cohesive homotopy type theory. There is a good deal of overlap between discrete mathematics and finite mathematics, and not every author distinguishes them. While modern number theory mixes ideas of discrete and continuous, in its original problematics most of the number theory may be considered discrete. However socially, and often in methods, modern number theory is for many closer to algebraic geometry and analysis than to combinatorics.

In nnlab many items are dedicated to the foundational issues. Set theory has many standard basic notions like set, proper class, empty set, singleton, subset, relation, reflexive relation, transitive relation, symmetric relation, function, partial function, injection, surjection, bijection, union, disjoint union, complement, intersection, symmetric difference, power set, pointed set along with more foundational items like axiom of choice, axiom of extensionality, axiom of foundation, axiom of infinity, Zorn's lemma, well-ordering theorem, decidable subset, material set theory, inhabited set, COSHEP, Markov's principle, Grothendieck universe, choice operator, pure set, hereditarily finite set). Logic also has some entries; among them are truth value or 0-poset, predicate, excluded middle, implication. We pay attention to the alternative approaches to logic and set theory, like the internal language of a topos; cf. Mitchell-Benabou language, Lawvere’s ETCS, Nelson’s internal set theory, etc. Concepts in type theory also has entries, such as type, term, dependent type, context, cut rule, beta-reduction, eta-conversion, empty type, unit type, product type, sum type, function type, dependent sum type, dependent product type, identity type, inductive type, coinductive type, higher inductive type, judgmental equality, propositional equality, type of types, Martin-Löf dependent type theory, FOLDS, Axiom K, univalence axiom, propositions are types?, homotopy type theory, etc, and its semantic interpretations in higher category theory: i.e. groupoid, n-groupoid, (-1)-groupoid, 0-groupoid, infinity-groupoid, object, morphism, n-morphism, composition, weak category, locally cartesian closed category, (n,1)-category, (infinity,1)-category, elementary topos (n,1)-topos, elementary (infinity,1)-topos, functor, limit, product, pullback, terminal object, equaliser, colimit, coproduct, coequalizer, pushout, initial object, (infinity,1)-limit, homotopy pullback, path space object, over category, under category, base change, dependent sum, dependent product, exponential object, monomorphism, epimorphism, essentially surjective morphism, full morphism, faithful morphism, truncated object, connected object, orthogonal factorization system, (n-connected, n-truncated) factorization system, subobject classifier, discrete object classifier, object classifier in an (infinity,1)-topos, internalization, internal logic, internal set theory, groupoid object in an (infinity,1)-category, etc…

Some other basic discrete structures which have their own entry in nnlab are preorder, order, partial order, total order, well-order, equivalence relation, quotient set, poset, proset, cyclic order, semilattice, lattice, distributive lattice, meet, join, supremum, infimum, suplattice, multiset, graph, quiver, tree, filter, span, multispan, natural number, sequence, …

Of course, a plain old category is a discrete structure per se.

Last revised on June 11, 2021 at 12:16:49. See the history of this page for a list of all contributions to it.