About this video

• Video Title: Infinity Categories Explained for Undergrads | Emily Riehl
• Channel: Curt Jaimungal
• Speakers: Curt Jaimungal, Emily Riehl
• Duration: 02:43:41

Overview

This video features mathematician Emily Riehl explaining the concept of infinity categories, a complex topic even for experts, to an undergraduate audience. She proposes that advancements in foundational mathematics, specifically homotopy type theory, could make infinity categories as accessible as abstract algebra. The discussion covers the core principles of category theory, the Curry-Howard correspondence, propositions as types, identity types, univalence, and the structure of infinity groupoids, highlighting how a more sophisticated foundation like homotopy type theory can simplify understanding and teaching advanced mathematical concepts, and even facilitate computer formalization of proofs.

Key takeaways

• The Dream of Accessible Infinity Categories: The central thesis is that by adopting homotopy type theory as a foundational system for mathematics, infinity categories could become a standard topic in undergraduate education, similar to abstract algebra.
• Category Theory as a Unifying Language: Category theory provides an abstract framework to identify common structures across different areas of mathematics, allowing for unified proofs and a more profound understanding of mathematical concepts.
• Homotopy Type Theory as a Modern Foundation: Homotopy type theory offers a richer foundation than traditional set theory, integrating concepts of "higher structure" and "sameness up to homotopy" directly into its framework. This is seen as key to making infinity category theory more accessible.
• Infinity Categories vs. One-Dimensional Categories: Infinity categories, unlike traditional one-dimensional categories, incorporate higher-dimensional morphisms (like homotopies) and relax strict equality to notions of equivalence. This richer structure is essential for capturing complex mathematical phenomena.
• The Role of Computer Formalization: The use of computer proof assistants and formal systems like simplicial type theory, built upon homotopy type theory, is crucial for rigorously defining and verifying proofs in infinity category theory, making it more reliable and potentially easier to teach.

Here's a summary of the points made in the video between 03:54 and 10:17:

• Category Theory as a Tool for Simplification: The speaker begins by illustrating how abstract concepts, like those introduced by Galois in group theory, can initially be difficult to grasp but become more accessible through abstraction and generalization. This sets the stage for category theory's role in simplifying complex mathematics.
• Unified Proofs: Category theory allows mathematicians to find common underlying structures in seemingly disparate mathematical results from different fields (like set theory, linear algebra, and abstract algebra). This enables a single, unified proof that applies across these areas.
• Examples of Unified Proofs:
  • Set Theory: The inverse image function preserves unions and intersections, while the direct image function preserves only unions.
  • Linear Algebra: The tensor product distributes over direct sums of vector spaces (e.g., U ⊗ (V ⊕ W) ≅ (U ⊗ V) ⊕ (U ⊗ W)).
  • Abstract Algebra: The free group on the disjoint union of two sets is isomorphic to the free product of their respective free groups.
• The Yoneda Lemma: The proof for the vector space example hinges on the Yoneda lemma, which relates isomorphisms between objects to bijections between Hom-sets (sets of arrows). It states that two objects are isomorphic if and only if their Hom-sets into any other object X are naturally isomorphic.
• Proof Structure: The proof of the vector space identity involves demonstrating a natural bijection between linear maps from U ⊗ (V ⊕ W) to an arbitrary vector space X, and linear maps from (U ⊗ V) ⊕ (U ⊗ W) to X. This is achieved through a series of steps involving "currying" and the properties of direct sums.
• Defining a Category: A category consists of objects and arrows (morphisms) between them, with a specified identity arrow for each object and a composition rule for composable arrows, subject to associativity and unitality axioms.
• Isomorphism in Categories: Two objects in a category are isomorphic if there exist arrows in both directions such that their compositions yield the identity arrows.
• The Goal: The objective is to use the Yoneda lemma and categorical language to prove general theorems, such as "left adjoint functors preserve colimits," which encompasses the specific examples discussed.

Here's a summary of the points discussed in the video from 10:17 to 15:37, covering "Key Concepts of Category Theory" and touching upon the "Curry-Howard Correspondence" in its broader sense:

• Category Definition: A category consists of objects and arrows (also called morphisms). Each arrow has a source and target object. Every object has an identity arrow, and for any composable pair of arrows, there's a defined composite arrow. These compositions and identities must satisfy associativity and unitality axioms.
• Isomorphism: Two objects in a category are considered isomorphic if there are arrows in both directions between them, such that the composition of these arrows in each direction results in the respective identity arrows.
• Nature of "Equality" in Categories: The speaker clarifies that in a standard (one-dimensional) category, arrows between the same two objects are either identical or distinct. There's no intermediate level of relationship beyond equality or inequality. This contrasts with higher-dimensional categories where such concepts can be relaxed.
• Yoneda Lemma's Role: The Yoneda lemma is presented as a powerful tool that allows us to understand isomorphisms between objects by examining the sets of arrows from those objects to all other objects in the category. Specifically, objects A and B are isomorphic if and only if their Hom-sets (Hom(A, X) and Hom(B, X)) are naturally isomorphic for all objects X.
• Naturality: While not formally defined, "naturality" in this context implies that transformations between Hom-sets are not arbitrary but arise from a consistent, structural relationship that respects the category's composition.
• Proof Strategy using Yoneda Lemma: To prove that two vector spaces (or objects in a category) are isomorphic, it suffices to show that the set of linear maps (arrows) from each space into an arbitrary space X are naturally isomorphic.
• Coproducts: The definition of a coproduct (like the direct sum of vector spaces) is introduced. It involves a new object and two maps into it from the original objects. The defining property is a universal one: any other pair of maps into an object X from the original objects uniquely factors through the coproduct. This means maps out of the coproduct can be understood by decomposing them into maps from the original objects.
• Adjunctions: The concept of an adjunction between two categories is explained through a pair of functors (or functions in this context) F: C → D and U: D → C. An adjunction exists if there's a natural bijection between Hom-sets of the form Hom_D(F(C), D) and Hom_C(C, U(D)) for all objects C in C and D in D. F is the left adjoint, and U is the right adjoint.
• Currying/Uncurrying Analogy: The relationship in vector spaces between mapping out of a tensor product and mapping into a space of linear maps is an example of an adjunction, analogous to currying and uncurrying operations in computer science.
• Curry-Howard Correspondence (Implicit): The idea that types can encode propositions and terms can encode proofs is introduced in the context of understanding how homotopy type theory works. This correspondence is highlighted as a way to unify "construction and logic" or "construction and proof." The example of proving a logical tautology (A ∧ (A → B)) → B using type theory rules demonstrates this.

Here are the key points from the video between 15:37 and 24:38, focusing on "Understanding Left Adjoint Functors":

• Category Theory's Essence: Category theory's purpose is to abstract and generalize common patterns found across different mathematical disciplines, enabling unified proofs and a higher-level understanding.
• Category as a Structure: A category is defined by a collection of objects and arrows (morphisms). Arrows have a source and target, an identity arrow exists for each object, and composable arrows have a defined composite that is associative and unital.
• Isomorphism: Objects are isomorphic if there are arrows in both directions between them, whose compositions are the respective identities.
• The Yoneda Lemma: This lemma is crucial for proving isomorphisms by relating them to natural bijections between Hom-sets (sets of arrows). It states that objects A and B are isomorphic if and only if Hom(A, X) and Hom(B, X) are naturally isomorphic for all objects X.
• Coproducts: A coproduct of two objects A and B is an object C with maps from A to C and B to C, such that any other pair of maps from A to X and B to X factors uniquely through C. This universal property allows maps out of the coproduct to be decomposed into maps from the original objects.
• Adjunctions: An adjunction between categories C and D, defined by functors F: C → D and U: D → C, exists if there's a natural bijection between Hom_D(F(C), D) and Hom_C(C, U(D)) for all objects C in C and D in D. F is the left adjoint, and U is the right adjoint.
• Example of Adjunction: The tensor product (e.g., U ⊗ V) and the space of linear maps (Hom(U, W)) in linear algebra form an adjoint pair. This is demonstrated by the correspondence between linear maps from U ⊗ V to W and linear maps from V to Hom(U, W). This operation is also referred to as "currying."
• Theorem: Left Adjoints Preserve Coproducts: The core theorem discussed is that left adjoint functors preserve coproducts. This means if F is a left adjoint and A and B have a coproduct in their category, then F(A) and F(B) will have a coproduct that is isomorphic to F applied to the coproduct of A and B.
• Proof Outline: The proof involves using the Yoneda lemma to establish an isomorphism between F(coproduct(A, B)) and coproduct(F(A), F(B)) by showing a natural equivalence between their Hom-sets. This is achieved by composing operations related to the adjunction and the coproduct's universal property.
• Generalization: This theorem holds broadly across categories, specializing to specific cases like vector spaces, sets (disjoint union and free products), and other mathematical structures.

Here is a comprehensive list of the main points from the video with their corresponding time codes:

• 00:00:00 - 00:14:56 (Introduction and Motivation)

  • 00:00:00: The speaker's "dream" is that advanced topics like infinity category theory could be taught to undergraduates, similar to abstract algebra.
  • 00:01:55: Introduction to the concept of infinity categories.
  • 00:03:54: Category theory as a tool to unify proofs across different mathematical fields (set theory, linear algebra, group theory) by identifying common underlying structures.
  • 00:10:17: Explanation of the core components of a category: objects, arrows (morphisms), identity arrows, composition, and the axioms of associativity and unitality.
  • 00:12:01: The concept of isomorphism in categories: two objects are isomorphic if there are inverse arrows between them whose compositions are identities.
  • 00:15:37: The Yoneda lemma is introduced as a key insight: objects are isomorphic if and only if their Hom-sets into any other object X are naturally isomorphic.
  • 00:24:38: The "Innate Lemma" (likely a misstatement or informal reference to the Yoneda lemma's principle) is used to show isomorphisms by comparing Hom-sets.
  • 00:38:29: The proof of an isomorphism between vector spaces U ⊗ (V ⊕ W) and (U ⊗ V) ⊕ (U ⊗ W) is detailed, involving steps like currying and the universal property of direct sums, all connected via the Yoneda lemma.
  • 00:41:50: Abstraction and generalization are key to making complicated mathematics understandable and teachable.
  • 00:44:04: A "crash course" in category theory begins, defining categories, isomorphisms, and the role of Hom-sets.
  • 00:56:27: Discussion of fundamental infinity groupoids.
  • 01:03:34: Answering "What are Infinity Categories?"
  • 01:09:12: The "case for" infinity categories is presented.
  • 01:18:12: Transition to Homotopy Type Theory.
  • 01:22:49: A crash course in Homotopy Type Theory begins.

• 01:30:56 - 02:08:36 (Homotopy Type Theory and Foundations)

  • 01:30:56: Type constructors (like product types, function types) are explained with formation, introduction, and elimination rules.
  • 01:34:19: The Curry-Howard correspondence is presented: types correspond to propositions, and terms correspond to proofs. This unifies construction and logic.
  • 01:42:50: Dependent types are introduced, where types can depend on terms of other types (e.g., R^n depending on n).
  • 01:49:01: Identity types are explained: the type representing the equality between two terms X and Y of the same type A. Proofs in this type are called "paths." Path induction is a key principle.
  • 01:54:03: The structure of infinity groupoids is related to iterated identity types in homotopy type theory. A type can be seen as an infinity groupoid where terms are objects, and paths (terms of identity types) are morphisms.
  • 01:59:33: Hierarchies of types (propositions, sets, 1-types, etc.) are introduced based on the structure of their identity types.
  • 02:06:19: The univalence axiom is discussed: the idea that identity between types (paths in the universe of types) corresponds to equivalence between types. This axiom is central to homotopy type theory.
  • 02:08:36: Transition back to Infinity Category Theory, framed within Homotopy Type Theory.

• 02:10:04 - 02:40:02 (Infinity Category Theory in Homotopy Type Theory)

  • 02:10:04: An introduction to simplicial type theory, a formal system extending homotopy type theory to handle simplicial shapes (like simplices and their sub-shapes).
  • 02:14:56: A type is defined as a "pre-infinity category" if every composable pair of arrows has a unique composite, which in homotopy type theory means the type of composites is contractible.
  • 02:24:32: Isomorphisms in infinity categories are defined using left and right inverses, and the "identity is equivalent to equivalence" principle connects paths (from identity types) to isomorphisms.
  • 02:31:48: The theorem that left adjoint functors preserve coproducts is re-proven in the context of infinity categories within homotopy type theory, highlighting that naturality is "for free" in this framework.
  • 02:40:02: Conclusion: The benefits of using homotopy type theory as a foundation for infinity category theory, including simplification, intuitiveness, and the potential for computer formalization, are reiterated. The challenges and ongoing work in formalizing these concepts are also mentioned.