The real projective spaces in homotopy type theory

Authors

Ulrik Buchholtz, Egbert Rijke

Type: Preprint

Publication Date: 2017-06-01

Citations: 16

DOI: https://doi.org/10.1109/lics.2017.8005146

Ask PDF

Abstract

Homotopy type theory is a version of Martin-Löf type theory taking advantage of its homotopical models. In particular, we can use and construct objects of homotopy theory and reason about them using higher inductive types. In this article, we construct the real projective spaces, key players in homotopy theory, as certain higher inductive types in homotopy type theory. The classical definition of ℝP n , as the quotient space identifying antipodal points of the n-sphere, does not translate directly to homotopy type theory. Instead, we define ℝP n by induction on n simultaneously with its tautological bundle of 2-element sets. As the base case, we take ℝP -1 to be the empty type. In the inductive step, we take ℝP n+1 to be the mapping cone of the projection map of the tautological bundle of ℝP n , and we use its universal property and the univalence axiom to define the tautological bundle on ℝP n+1 . By showing that the total space of the tautological bundle of ℝP n is the n-sphere S n , we retrieve the classical description of ℝP n+1 as ℝP n with an (n + 1)-disk attached to it. The infinite dimensional real projective space ℝP ∞ , defined as the sequential colimit of ℝP n with the canonical inclusion maps, is equivalent to the Eilenberg-MacLane space K(ℤ/2ℤ, 1), which here arises as the subtype of the universe consisting of 2-element types. Indeed, the infinite dimensional projective space classifies the 0-sphere bundles, which one can think of as synthetic line bundles. These constructions in homotopy type theory further illustrate the utility of homotopy type theory, including the interplay of type theoretic and homotopy theoretic ideas.

Locations

arXiv (Cornell University)
View PDF

Ask a Question About This Paper

Summary

The real projective spaces in homotopy type theory

2017-01-01

Ulrik Buchholtz , Egbert Rijke

Homotopy type theory is a version of Martin-L\"of type theory taking advantage of its homotopical models. In particular, we can use and construct objects of homotopy theory and reason about … Homotopy type theory is a version of Martin-L\"of type theory taking advantage of its homotopical models. In particular, we can use and construct objects of homotopy theory and reason about them using higher inductive types. In this article, we construct the real projective spaces, key players in homotopy theory, as certain higher inductive types in homotopy type theory. The classical definition of RP(n), as the quotient space identifying antipodal points of the n-sphere, does not translate directly to homotopy type theory. Instead, we define RP(n) by induction on n simultaneously with its tautological bundle of 2-element sets. As the base case, we take RP(-1) to be the empty type. In the inductive step, we take RP(n+1) to be the mapping cone of the projection map of the tautological bundle of RP(n), and we use its universal property and the univalence axiom to define the tautological bundle on RP(n+1). By showing that the total space of the tautological bundle of RP(n) is the n-sphere, we retrieve the classical description of RP(n+1) as RP(n) with an (n+1)-cell attached to it. The infinite dimensional real projective space, defined as the sequential colimit of the RP(n) with the canonical inclusion maps, is equivalent to the Eilenberg-MacLane space K(Z/2Z,1), which here arises as the subtype of the universe consisting of 2-element types. Indeed, the infinite dimensional projective space classifies the 0-sphere bundles, which one can think of as synthetic line bundles. These constructions in homotopy type theory further illustrate the utility of homotopy type theory, including the interplay of type theoretic and homotopy theoretic ideas.

View PDF Chat

The real projective spaces in homotopy type theory

2017-06-20

Ulrik Buchholtz , Egbert Rijke

Homotopy type theory is a version of Martin-Lof type theory taking advantage of its homotopical models. In particular, we can use and construct objects of homotopy theory and reason about … Homotopy type theory is a version of Martin-Lof type theory taking advantage of its homotopical models. In particular, we can use and construct objects of homotopy theory and reason about them using higher inductive types. In this article, we construct the real projective spaces, key players in homotopy theory, as certain higher inductive types in homotopy type theory. The classical definition of RPn, as the quotient space identifying antipodal points of the n-sphere, does not translate directly to homotopy type theory. Instead, we define RPn by induction on n simultaneously with its tautological bundle of 2-element sets. As the base case, we take RP-1 to be the empty type. In the inductive step, we take RPn+1 to be the mapping cone of the projection map of the tautological bundle of RPn, and we use its universal property and the univalence axiom to define the tautological bundle on RPn+1.By showing that the total space of the tautological bundle of RPn is the n-sphere Sn, we retrieve the classical description of RPn+1 as RPn with an (n + 1)-disk attached to it. The infinite dimensional real projective space RP∞, defined as the sequential colimit of RPn with the canonical inclusion maps, is equivalent to the Eilenberg-MacLane space K(Z/2Z, 1), which here arises as the subtype of the universe consisting of 2-element types. Indeed, the infinite dimensional projective space classifies the 0-sphere bundles, which one can think of as synthetic line bundles.These constructions in homotopy type theory further illustrate the utility of homotopy type theory, including the interplay of type theoretic and homotopy theoretic ideas.

NOTE ON THE HOMOTOPY OF THE SPACE OF MAPS BETWEEN REAL PROJECTIVE SPACES

2012-01-01

Kohhei Yamaguchi

We study the homotopy types of the space consisting of all base-point preseving continuous maps from the m dimensional real projective space into the n dimensional real projective space. When … We study the homotopy types of the space consisting of all base-point preseving continuous maps from the m dimensional real projective space into the n dimensional real projective space. When 2 ≤ m < n, it has two path connected components and we investigate whether these two path-components have the same homotopy type or not.

Rational homotopy of spaces of maps into spheres and complex projective spaces

1985-01-01

Jesper M. Møller , Martin Raußen

We investigate the rational homotopy classification problem for the components of some function spaces with <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper S Superscript n"> <mml:semantics> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:msup> <mml:mi>S</mml:mi> <mml:mi>n</mml:mi> </mml:msup> … We investigate the rational homotopy classification problem for the components of some function spaces with <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper S Superscript n"> <mml:semantics> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:msup> <mml:mi>S</mml:mi> <mml:mi>n</mml:mi> </mml:msup> </mml:mrow> <mml:annotation encoding="application/x-tex">{S^n}</mml:annotation> </mml:semantics> </mml:math> </inline-formula> or <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="bold upper C upper P Superscript n"> <mml:semantics> <mml:mrow> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="bold">C</mml:mi> </mml:mrow> </mml:mrow> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:msup> <mml:mi>P</mml:mi> <mml:mi>n</mml:mi> </mml:msup> </mml:mrow> </mml:mrow> <mml:annotation encoding="application/x-tex">{\mathbf {C}}{P^n}</mml:annotation> </mml:semantics> </mml:math> </inline-formula> as target space.

View PDF Chat

A note on the concordance homotopy group of real projective space

1977-02-01

H. Schneider , Rebecca Wells

By means of the mapping torus construction the following theorem is proved Theorem. <italic>If</italic> <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="r identical-to 3 mod 4"> <mml:semantics> <mml:mrow> <mml:mi>r</mml:mi> <mml:mo>≡</mml:mo> <mml:mn>3</mml:mn> <mml:mo lspace="thickmathspace" … By means of the mapping torus construction the following theorem is proved Theorem. <italic>If</italic> <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="r identical-to 3 mod 4"> <mml:semantics> <mml:mrow> <mml:mi>r</mml:mi> <mml:mo>≡</mml:mo> <mml:mn>3</mml:mn> <mml:mo lspace="thickmathspace" rspace="thickmathspace">mod</mml:mo> <mml:mn>4</mml:mn> </mml:mrow> <mml:annotation encoding="application/x-tex">r \equiv 3 \bmod 4</mml:annotation> </mml:semantics> </mml:math> </inline-formula> <italic>and</italic> <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="r greater-than-or-slanted-equals 7"> <mml:semantics> <mml:mrow> <mml:mi>r</mml:mi> <mml:mo>⩾</mml:mo> <mml:mn>7</mml:mn> </mml:mrow> <mml:annotation encoding="application/x-tex">r \geqslant 7</mml:annotation> </mml:semantics> </mml:math> </inline-formula>, <italic>and</italic> <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="script upper P Subscript r"> <mml:semantics> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:msub> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi class="MJX-tex-caligraphic" mathvariant="script">P</mml:mi> </mml:mrow> <mml:mi>r</mml:mi> </mml:msub> </mml:mrow> <mml:annotation encoding="application/x-tex">{\mathcal {P}_r}</mml:annotation> </mml:semantics> </mml:math> </inline-formula> <italic>is a homotopy</italic> <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper P Subscript r"> <mml:semantics> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:msub> <mml:mi>P</mml:mi> <mml:mi>r</mml:mi> </mml:msub> </mml:mrow> <mml:annotation encoding="application/x-tex">{P_r}</mml:annotation> </mml:semantics> </mml:math> </inline-formula>, <italic>then there is an isomorphism</italic> <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="pi 0 upper D i f f Superscript plus Baseline colon script upper P Subscript r Baseline approximately-equals pi 0 upper D i f f Superscript plus Baseline colon upper P Subscript r Baseline"> <mml:semantics> <mml:mrow> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:msub> <mml:mi>π</mml:mi> <mml:mn>0</mml:mn> </mml:msub> </mml:mrow> <mml:mspace width="thickmathspace"/> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:msup> <mml:mi>Diff</mml:mi> <mml:mo>+</mml:mo> </mml:msup> </mml:mrow> <mml:mo>:</mml:mo> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:msub> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi class="MJX-tex-caligraphic" mathvariant="script">P</mml:mi> </mml:mrow> <mml:mi>r</mml:mi> </mml:msub> </mml:mrow> <mml:mo>≅</mml:mo> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:msub> <mml:mi>π</mml:mi> <mml:mn>0</mml:mn> </mml:msub> </mml:mrow> <mml:mspace width="thickmathspace"/> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:msup> <mml:mi>Diff</mml:mi> <mml:mo>+</mml:mo> </mml:msup> </mml:mrow> <mml:mo>:</mml:mo> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:msub> <mml:mi>P</mml:mi> <mml:mi>r</mml:mi> </mml:msub> </mml:mrow> </mml:mrow> <mml:annotation encoding="application/x-tex">{\pi _0}\;{\operatorname {Diff}^ + }:{\mathcal {P}_r} \cong {\pi _0}\;{\operatorname {Diff}^ + }:{P_r}</mml:annotation> </mml:semantics> </mml:math> </inline-formula>.

View PDF Chat

Bordism classes of vector bundles over real projective spaces

1993-01-01

Bruce F. Torrence

A basis is presented for the <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="bold upper R bold upper P Superscript n"> <mml:semantics> <mml:mrow> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="bold">R</mml:mi> </mml:mrow> </mml:mrow> <mml:mrow class="MJX-TeXAtom-ORD"> … A basis is presented for the <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="bold upper R bold upper P Superscript n"> <mml:semantics> <mml:mrow> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="bold">R</mml:mi> </mml:mrow> </mml:mrow> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:msup> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="bold">P</mml:mi> </mml:mrow> </mml:mrow> <mml:mi>n</mml:mi> </mml:msup> </mml:mrow> </mml:mrow> <mml:annotation encoding="application/x-tex">{\mathbf {R}}{{\mathbf {P}}^n}</mml:annotation> </mml:semantics> </mml:math> </inline-formula> classes in <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="German upper N Subscript n Baseline left-parenthesis upper B upper O right-parenthesis"> <mml:semantics> <mml:mrow> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:msub> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="fraktur">N</mml:mi> </mml:mrow> <mml:mi>n</mml:mi> </mml:msub> </mml:mrow> <mml:mo stretchy="false">(</mml:mo> <mml:mi>B</mml:mi> <mml:mi>O</mml:mi> <mml:mo stretchy="false">)</mml:mo> </mml:mrow> <mml:annotation encoding="application/x-tex">{\mathfrak {N}_n}(BO)</mml:annotation> </mml:semantics> </mml:math> </inline-formula>. This basis is used to prove that every smooth involution <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="left-parenthesis upper M comma upper T right-parenthesis"> <mml:semantics> <mml:mrow> <mml:mo stretchy="false">(</mml:mo> <mml:mi>M</mml:mi> <mml:mo>,</mml:mo> <mml:mi>T</mml:mi> <mml:mo stretchy="false">)</mml:mo> </mml:mrow> <mml:annotation encoding="application/x-tex">(M,T)</mml:annotation> </mml:semantics> </mml:math> </inline-formula> on a closed manifold bounds if its fixed point set is a disjoint union of odd-dimensional projective spaces of constant dimension.

View PDF Chat

Homotopy Types

2020-02-03

David Corfield

A further innovation is the introduction of an <italic>intensional</italic> type theory. Here one need not reduce equivalence to mere identity. <italic>How</italic> two entities are the same tells us more than … A further innovation is the introduction of an <italic>intensional</italic> type theory. Here one need not reduce equivalence to mere identity. <italic>How</italic> two entities are the same tells us more than <italic>whether</italic> they are the same. This is explained by the homotopical aspect of HoTT, where types are taken to resemble spaces of points, paths, paths between paths, and so on. This allows us to rethink Russell’s <italic>definite descriptions</italic>. Mathematicians use a ‘generalized the’ in situations where it appears that they might be talking about a multiplicity of instances, but there is essentially a unique instance. Taken together with the ‘univalence axiom’ there results a language in which anything that can be said of a type can be said of an equivalent type. This allows homotopy type theory to become the language of choice for a structuralist, avoiding the need for any kind of abstraction away from multiple instantiations.

A homotopy theory of pro-spaces

1975-01-01

Jerrold W. Grossman

The category of towers of spaces, <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="ellipsis right-arrow upper X Subscript s plus 1 Baseline right-arrow upper X Subscript s Baseline right-arrow ellipsis right-arrow upper X … The category of towers of spaces, <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="ellipsis right-arrow upper X Subscript s plus 1 Baseline right-arrow upper X Subscript s Baseline right-arrow ellipsis right-arrow upper X 0"> <mml:semantics> <mml:mrow> <mml:mo>…</mml:mo> <mml:mo stretchy="false">→</mml:mo> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:msub> <mml:mi>X</mml:mi> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi>s</mml:mi> <mml:mo>+</mml:mo> <mml:mn>1</mml:mn> </mml:mrow> </mml:msub> </mml:mrow> <mml:mo stretchy="false">→</mml:mo> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:msub> <mml:mi>X</mml:mi> <mml:mi>s</mml:mi> </mml:msub> </mml:mrow> <mml:mo stretchy="false">→</mml:mo> <mml:mo>…</mml:mo> <mml:mo stretchy="false">→</mml:mo> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:msub> <mml:mi>X</mml:mi> <mml:mn>0</mml:mn> </mml:msub> </mml:mrow> </mml:mrow> <mml:annotation encoding="application/x-tex">\ldots \to {X_{s + 1}} \to {X_s} \to \ldots \to {X_0}</mml:annotation> </mml:semantics> </mml:math> </inline-formula>, viewed as pro-spaces, appears to be useful in the study of the relation between homology and homotopy of nonsimply connected spaces. We show that this category admits the structure of a closed model category, in the sense of Quillen; notions of fibration, cofibration, and weak equivalence are defined and shown to satisfy fundamental properties that the corresponding notions satisfy in the category of spaces. This enables one to develop a “homotopy theory” for pro-spaces.

View PDF Chat

The level of real projective spaces

1989-12-01

Stephan Stolz

On spaces of maps between complex projective spaces

1984-01-01

Jesper M. Møller

When <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="1 less-than-or-slanted-equals m less-than-or-slanted-equals n"> <mml:semantics> <mml:mrow> <mml:mn>1</mml:mn> <mml:mo>⩽</mml:mo> <mml:mi>m</mml:mi> <mml:mo>⩽</mml:mo> <mml:mi>n</mml:mi> </mml:mrow> <mml:annotation encoding="application/x-tex">1 \leqslant m \leqslant n</mml:annotation> </mml:semantics> </mml:math> … When <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="1 less-than-or-slanted-equals m less-than-or-slanted-equals n"> <mml:semantics> <mml:mrow> <mml:mn>1</mml:mn> <mml:mo>⩽</mml:mo> <mml:mi>m</mml:mi> <mml:mo>⩽</mml:mo> <mml:mi>n</mml:mi> </mml:mrow> <mml:annotation encoding="application/x-tex">1 \leqslant m \leqslant n</mml:annotation> </mml:semantics> </mml:math> </inline-formula>, the space <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper M left-parenthesis upper P Superscript m Baseline comma upper P Superscript n Baseline right-parenthesis"> <mml:semantics> <mml:mrow> <mml:mi>M</mml:mi> <mml:mo stretchy="false">(</mml:mo> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:msup> <mml:mi>P</mml:mi> <mml:mi>m</mml:mi> </mml:msup> </mml:mrow> <mml:mo>,</mml:mo> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:msup> <mml:mi>P</mml:mi> <mml:mi>n</mml:mi> </mml:msup> </mml:mrow> <mml:mo stretchy="false">)</mml:mo> </mml:mrow> <mml:annotation encoding="application/x-tex">M({P^m},{P^n})</mml:annotation> </mml:semantics> </mml:math> </inline-formula> of maps of complex projective <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="m"> <mml:semantics> <mml:mi>m</mml:mi> <mml:annotation encoding="application/x-tex">m</mml:annotation> </mml:semantics> </mml:math> </inline-formula>-space <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper P Superscript m"> <mml:semantics> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:msup> <mml:mi>P</mml:mi> <mml:mi>m</mml:mi> </mml:msup> </mml:mrow> <mml:annotation encoding="application/x-tex">{P^m}</mml:annotation> </mml:semantics> </mml:math> </inline-formula> into complex projective <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="n"> <mml:semantics> <mml:mi>n</mml:mi> <mml:annotation encoding="application/x-tex">n</mml:annotation> </mml:semantics> </mml:math> </inline-formula>-space <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper P Superscript n"> <mml:semantics> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:msup> <mml:mi>P</mml:mi> <mml:mi>n</mml:mi> </mml:msup> </mml:mrow> <mml:annotation encoding="application/x-tex">{P^n}</mml:annotation> </mml:semantics> </mml:math> </inline-formula> has a countably infinite number of components enumerated by degrees of maps in <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper H squared left-parenthesis upper P Superscript m Baseline semicolon bold upper Z right-parenthesis"> <mml:semantics> <mml:mrow> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:msup> <mml:mi>H</mml:mi> <mml:mn>2</mml:mn> </mml:msup> </mml:mrow> <mml:mo stretchy="false">(</mml:mo> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:msup> <mml:mi>P</mml:mi> <mml:mi>m</mml:mi> </mml:msup> </mml:mrow> <mml:mo>;</mml:mo> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="bold">Z</mml:mi> </mml:mrow> </mml:mrow> <mml:mo stretchy="false">)</mml:mo> </mml:mrow> <mml:annotation encoding="application/x-tex">{H^2}({P^m};{\mathbf {Z}})</mml:annotation> </mml:semantics> </mml:math> </inline-formula>. By calculating their <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="left-parenthesis 2 n minus 2 m plus 1 right-parenthesis"> <mml:semantics> <mml:mrow> <mml:mo stretchy="false">(</mml:mo> <mml:mn>2</mml:mn> <mml:mi>n</mml:mi> <mml:mo>−</mml:mo> <mml:mn>2</mml:mn> <mml:mi>m</mml:mi> <mml:mo>+</mml:mo> <mml:mn>1</mml:mn> <mml:mo stretchy="false">)</mml:mo> </mml:mrow> <mml:annotation encoding="application/x-tex">(2n - 2m + 1)</mml:annotation> </mml:semantics> </mml:math> </inline-formula>-dimensional integral homology group we show that two components of <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper M left-parenthesis upper P Superscript m Baseline comma upper P Superscript n Baseline right-parenthesis"> <mml:semantics> <mml:mrow> <mml:mi>M</mml:mi> <mml:mo stretchy="false">(</mml:mo> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:msup> <mml:mi>P</mml:mi> <mml:mi>m</mml:mi> </mml:msup> </mml:mrow> <mml:mo>,</mml:mo> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:msup> <mml:mi>P</mml:mi> <mml:mi>n</mml:mi> </mml:msup> </mml:mrow> <mml:mo stretchy="false">)</mml:mo> </mml:mrow> <mml:annotation encoding="application/x-tex">M({P^m},{P^n})</mml:annotation> </mml:semantics> </mml:math> </inline-formula> are homotopy equivalent if and only if their associated degrees have the same absolute value.

View PDF Chat

The power of the tangent bundle of the real projective space, its complexification and extendibility

2005-06-13

Teiichi KOBAYASHI , Hironori Yamasaki , Toshio Yoshida

We establish the formulas on the power <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="tau Superscript k"> <mml:semantics> <mml:msup> <mml:mi>τ</mml:mi> <mml:mi>k</mml:mi> </mml:msup> <mml:annotation encoding="application/x-tex">\tau ^k</mml:annotation> </mml:semantics> </mml:math> </inline-formula> of the tangent bundle <inline-formula … We establish the formulas on the power <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="tau Superscript k"> <mml:semantics> <mml:msup> <mml:mi>τ</mml:mi> <mml:mi>k</mml:mi> </mml:msup> <mml:annotation encoding="application/x-tex">\tau ^k</mml:annotation> </mml:semantics> </mml:math> </inline-formula> of the tangent bundle <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="tau equals tau left-parenthesis upper R upper P Superscript n Baseline right-parenthesis"> <mml:semantics> <mml:mrow> <mml:mi>τ</mml:mi> <mml:mo>=</mml:mo> <mml:mi>τ</mml:mi> <mml:mo stretchy="false">(</mml:mo> <mml:mi>R</mml:mi> <mml:msup> <mml:mi>P</mml:mi> <mml:mi>n</mml:mi> </mml:msup> <mml:mo stretchy="false">)</mml:mo> </mml:mrow> <mml:annotation encoding="application/x-tex">\tau =\tau (RP^n)</mml:annotation> </mml:semantics> </mml:math> </inline-formula> of the real projective <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="n"> <mml:semantics> <mml:mi>n</mml:mi> <mml:annotation encoding="application/x-tex">n</mml:annotation> </mml:semantics> </mml:math> </inline-formula>-space <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper R upper P Superscript n"> <mml:semantics> <mml:mrow> <mml:mi>R</mml:mi> <mml:msup> <mml:mi>P</mml:mi> <mml:mi>n</mml:mi> </mml:msup> </mml:mrow> <mml:annotation encoding="application/x-tex">RP^n</mml:annotation> </mml:semantics> </mml:math> </inline-formula> and its complexification <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="c tau Superscript k"> <mml:semantics> <mml:mrow> <mml:mi>c</mml:mi> <mml:msup> <mml:mi>τ</mml:mi> <mml:mi>k</mml:mi> </mml:msup> </mml:mrow> <mml:annotation encoding="application/x-tex">c\tau ^k</mml:annotation> </mml:semantics> </mml:math> </inline-formula>, and apply the formulas to the problem of extendibility and stable extendiblity of <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="tau Superscript k"> <mml:semantics> <mml:msup> <mml:mi>τ</mml:mi> <mml:mi>k</mml:mi> </mml:msup> <mml:annotation encoding="application/x-tex">\tau ^k</mml:annotation> </mml:semantics> </mml:math> </inline-formula> and <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="c tau Superscript k"> <mml:semantics> <mml:mrow> <mml:mi>c</mml:mi> <mml:msup> <mml:mi>τ</mml:mi> <mml:mi>k</mml:mi> </mml:msup> </mml:mrow> <mml:annotation encoding="application/x-tex">c\tau ^k</mml:annotation> </mml:semantics> </mml:math> </inline-formula>.

π n (S n ) in Homotopy Type Theory

2013-01-01

Daniel R. Licata , Guillaume Brunerie

Higher Categories and Homotopical Algebra

2019-04-25

Denis-Charles Cisinski

This book provides an introduction to modern homotopy theory through the lens of higher categories after Joyal and Lurie, giving access to methods used at the forefront of research in … This book provides an introduction to modern homotopy theory through the lens of higher categories after Joyal and Lurie, giving access to methods used at the forefront of research in algebraic topology and algebraic geometry in the twenty-first century. The text starts from scratch - revisiting results from classical homotopy theory such as Serre's long exact sequence, Quillen's theorems A and B, Grothendieck's smooth/proper base change formulas, and the construction of the Kan–Quillen model structure on simplicial sets - and develops an alternative to a significant part of Lurie's definitive reference Higher Topos Theory, with new constructions and proofs, in particular, the Yoneda Lemma and Kan extensions. The strong emphasis on homotopical algebra provides clear insights into classical constructions such as calculus of fractions, homotopy limits and derived functors. For graduate students and researchers from neighbouring fields, this book is a user-friendly guide to advanced tools that the theory provides for application.

A projective homotopy theory for non-additive categories

1993-01-01

K. A. Hardie , J.J.C. Vermeulen

The homotopy of spaces of maps between real projective spaces

2006-10-01

Kohhei Yamaguchi

We study the homotopy groups of spaces of continuous maps between real projective spaces and we generalize the results given in [5], [8] and [12]. In particular, we determine the … We study the homotopy groups of spaces of continuous maps between real projective spaces and we generalize the results given in [5], [8] and [12]. In particular, we determine the rational homotopy types of these spaces and compute their fundamental groups explicitly.

View PDF Chat

The Hom-spaces between projective functors

2001-09-10

Erik Backelin

The category of projective functors on a block of the category <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="script upper O left-parenthesis German g right-parenthesis"> <mml:semantics> <mml:mrow> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi class="MJX-tex-caligraphic" mathvariant="script">O</mml:mi> </mml:mrow> … The category of projective functors on a block of the category <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="script upper O left-parenthesis German g right-parenthesis"> <mml:semantics> <mml:mrow> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi class="MJX-tex-caligraphic" mathvariant="script">O</mml:mi> </mml:mrow> <mml:mo stretchy="false">(</mml:mo> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="fraktur">g</mml:mi> </mml:mrow> <mml:mo stretchy="false">)</mml:mo> </mml:mrow> <mml:annotation encoding="application/x-tex">\mathcal O(\mathfrak g)</mml:annotation> </mml:semantics> </mml:math> </inline-formula> of Bernstein, Gelfand and Gelfand, over a complex semisimple Lie algebra <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="German g"> <mml:semantics> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="fraktur">g</mml:mi> </mml:mrow> <mml:annotation encoding="application/x-tex">\mathfrak g</mml:annotation> </mml:semantics> </mml:math> </inline-formula>, embeds to a corresponding block of the category <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="script upper O left-parenthesis German g times German g right-parenthesis"> <mml:semantics> <mml:mrow> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi class="MJX-tex-caligraphic" mathvariant="script">O</mml:mi> </mml:mrow> <mml:mo stretchy="false">(</mml:mo> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="fraktur">g</mml:mi> </mml:mrow> <mml:mo>×</mml:mo> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="fraktur">g</mml:mi> </mml:mrow> <mml:mo stretchy="false">)</mml:mo> </mml:mrow> <mml:annotation encoding="application/x-tex">\mathcal O(\mathfrak g \times \mathfrak g)</mml:annotation> </mml:semantics> </mml:math> </inline-formula>. In this paper we give a nice description of the object <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper V"> <mml:semantics> <mml:mi>V</mml:mi> <mml:annotation encoding="application/x-tex">V</mml:annotation> </mml:semantics> </mml:math> </inline-formula> in <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="script upper O left-parenthesis German g times German g right-parenthesis"> <mml:semantics> <mml:mrow> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi class="MJX-tex-caligraphic" mathvariant="script">O</mml:mi> </mml:mrow> <mml:mo stretchy="false">(</mml:mo> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="fraktur">g</mml:mi> </mml:mrow> <mml:mo>×</mml:mo> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="fraktur">g</mml:mi> </mml:mrow> <mml:mo stretchy="false">)</mml:mo> </mml:mrow> <mml:annotation encoding="application/x-tex">\mathcal O(\mathfrak g \times \mathfrak g)</mml:annotation> </mml:semantics> </mml:math> </inline-formula> corresponding to the identity functor; we show that <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper V"> <mml:semantics> <mml:mi>V</mml:mi> <mml:annotation encoding="application/x-tex">V</mml:annotation> </mml:semantics> </mml:math> </inline-formula> is isomorphic to the module of invariants, under the diagonal action of the center <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="script upper Z"> <mml:semantics> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi class="MJX-tex-caligraphic" mathvariant="script">Z</mml:mi> </mml:mrow> <mml:annotation encoding="application/x-tex">\mathcal Z</mml:annotation> </mml:semantics> </mml:math> </inline-formula> of the universal enveloping algebra of <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="German g"> <mml:semantics> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="fraktur">g</mml:mi> </mml:mrow> <mml:annotation encoding="application/x-tex">\mathfrak g</mml:annotation> </mml:semantics> </mml:math> </inline-formula>, in the so-called anti-dominant projective. As an application we use Soergel’s theory about modules over the coinvariant algebra <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper C"> <mml:semantics> <mml:mi>C</mml:mi> <mml:annotation encoding="application/x-tex">C</mml:annotation> </mml:semantics> </mml:math> </inline-formula>, of the Weyl group, to describe the space of homomorphisms of two projective functors <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper T"> <mml:semantics> <mml:mi>T</mml:mi> <mml:annotation encoding="application/x-tex">T</mml:annotation> </mml:semantics> </mml:math> </inline-formula> and <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper T prime"> <mml:semantics> <mml:msup> <mml:mi>T</mml:mi> <mml:mo>′</mml:mo> </mml:msup> <mml:annotation encoding="application/x-tex">T’</mml:annotation> </mml:semantics> </mml:math> </inline-formula>. We show that there exists a natural <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper C"> <mml:semantics> <mml:mi>C</mml:mi> <mml:annotation encoding="application/x-tex">C</mml:annotation> </mml:semantics> </mml:math> </inline-formula>-bimodule structure on <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper H o m Subscript StartSet upper F u n c t o r s EndSet Baseline left-parenthesis upper T comma upper T prime right-parenthesis"> <mml:semantics> <mml:mrow> <mml:msub> <mml:mi>Hom</mml:mi> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mo fence="false" stretchy="false">{</mml:mo> <mml:mi>Functors</mml:mi> <mml:mo fence="false" stretchy="false">}</mml:mo> </mml:mrow> </mml:msub> <mml:mo>⁡</mml:mo> <mml:mo stretchy="false">(</mml:mo> <mml:mi>T</mml:mi> <mml:mo>,</mml:mo> <mml:msup> <mml:mi>T</mml:mi> <mml:mo>′</mml:mo> </mml:msup> <mml:mo stretchy="false">)</mml:mo> </mml:mrow> <mml:annotation encoding="application/x-tex">\operatorname {Hom}_{\{\operatorname {Functors}\}}(T, T’)</mml:annotation> </mml:semantics> </mml:math> </inline-formula> such that this space becomes free as a left (and right) <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper C"> <mml:semantics> <mml:mi>C</mml:mi> <mml:annotation encoding="application/x-tex">C</mml:annotation> </mml:semantics> </mml:math> </inline-formula>-module and that evaluation induces a canonical isomorphism <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="k circled-times Subscript upper C Baseline upper H o m Subscript StartSet upper F u n c t o r s EndSet Baseline left-parenthesis upper T comma upper T Superscript prime Baseline right-parenthesis approximately-equals upper H o m Subscript script upper O left-parenthesis German g right-parenthesis Baseline left-parenthesis upper T left-parenthesis upper M Subscript e Baseline right-parenthesis comma upper T prime left-parenthesis upper M Subscript e Baseline right-parenthesis right-parenthesis"> <mml:semantics> <mml:mrow> <mml:mi>k</mml:mi> <mml:msub> <mml:mo>⊗</mml:mo> <mml:mi>C</mml:mi> </mml:msub> <mml:msub> <mml:mi>Hom</mml:mi> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mo fence="false" stretchy="false">{</mml:mo> <mml:mi>Functors</mml:mi> <mml:mo fence="false" stretchy="false">}</mml:mo> </mml:mrow> </mml:msub> <mml:mo>⁡</mml:mo> <mml:mo stretchy="false">(</mml:mo> <mml:mi>T</mml:mi> <mml:mo>,</mml:mo> <mml:msup> <mml:mi>T</mml:mi> <mml:mo>′</mml:mo> </mml:msup> <mml:mo stretchy="false">)</mml:mo> <mml:mo>≅</mml:mo> <mml:msub> <mml:mi>Hom</mml:mi> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi class="MJX-tex-caligraphic" mathvariant="script">O</mml:mi> </mml:mrow> <mml:mo stretchy="false">(</mml:mo> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="fraktur">g</mml:mi> </mml:mrow> <mml:mo stretchy="false">)</mml:mo> </mml:mrow> </mml:msub> <mml:mo>⁡</mml:mo> <mml:mo stretchy="false">(</mml:mo> <mml:mi>T</mml:mi> <mml:mo stretchy="false">(</mml:mo> <mml:msub> <mml:mi>M</mml:mi> <mml:mi>e</mml:mi> </mml:msub> <mml:mo stretchy="false">)</mml:mo> <mml:mo>,</mml:mo> <mml:msup> <mml:mi>T</mml:mi> <mml:mo>′</mml:mo> </mml:msup> <mml:mo stretchy="false">(</mml:mo> <mml:msub> <mml:mi>M</mml:mi> <mml:mi>e</mml:mi> </mml:msub> <mml:mo stretchy="false">)</mml:mo> <mml:mo stretchy="false">)</mml:mo> </mml:mrow> <mml:annotation encoding="application/x-tex">k \otimes _C \operatorname {Hom}_{\{\operatorname {Functors}\}} (T, T’) \cong \operatorname {Hom}_{\mathcal O(\mathfrak g)}(T(M_e), T’(M_e))</mml:annotation> </mml:semantics> </mml:math> </inline-formula>, where <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper M Subscript e"> <mml:semantics> <mml:msub> <mml:mi>M</mml:mi> <mml:mi>e</mml:mi> </mml:msub> <mml:annotation encoding="application/x-tex">M_e</mml:annotation> </mml:semantics> </mml:math> </inline-formula> denotes the dominant Verma module in the block and <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="k"> <mml:semantics> <mml:mi>k</mml:mi> <mml:annotation encoding="application/x-tex">k</mml:annotation> </mml:semantics> </mml:math> </inline-formula> is the complex numbers.

Shape Theory in Homotopy Theory and Algebraic Geometry

2018-06-15

Joseph Berner

This work defines the etale homotopy type in the context of non-archimedean geometry, in both Berkovich’s and Huber’s formalisms. To do this we take the shape of a site’s associated … This work defines the etale homotopy type in the context of non-archimedean geometry, in both Berkovich’s and Huber’s formalisms. To do this we take the shape of a site’s associated hypercomplete 1-topos. This naturally leads to discussing localizations of the category of pro-spaces. For a prime number p, we introduce a new localization intermediate between profinite spaces and {p}`-profinite spaces. This new category is well suited for comparison theorems when working over a discrete valuation ring of mixed characteristic. We prove a new comparison theorem on the level of topoi for the formalisms of Berkovich and Huber, and prove an analog of smooth-proper base change for nonarchimedean analytic spaces. This provides a necessary result for the non-archimedean analog of Friedlander’s homotopy fiber theorem, which we prove. For a variety over a non-archimedean field, we prove a comparison theorem between the classical etale homotopy type and our etale homotopy type of the variety’s analytification. Finally, we examine certain log formal schemes over the formal spectrum of a complete discrete valuation ring, and compare their Kummer etale homotopy type with the etale homotopy type of the associated non-archimedean analytic space.

Pro-objects in the homotopy category

1969-01-01

Michael Artin , Barry Mazur

The topology of spaces of maps between real projective spaces

2003-01-01

Kohhei Yamaguchi

View PDF Chat

Basic constructions in the 𝐾-theory of homotopy ring spaces

1994-01-01

R. Schwänzl , R. M. Vogt

Using the language of category theory and universal algebra we formalize the passage from the permutative category of finitely generated free <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper R"> <mml:semantics> <mml:mi>R</mml:mi> <mml:annotation … Using the language of category theory and universal algebra we formalize the passage from the permutative category of finitely generated free <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper R"> <mml:semantics> <mml:mi>R</mml:mi> <mml:annotation encoding="application/x-tex">R</mml:annotation> </mml:semantics> </mml:math> </inline-formula>-modules to the algebraic <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper K"> <mml:semantics> <mml:mi>K</mml:mi> <mml:annotation encoding="application/x-tex">K</mml:annotation> </mml:semantics> </mml:math> </inline-formula>-theory <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper K upper R"> <mml:semantics> <mml:mrow> <mml:mi>K</mml:mi> <mml:mi>R</mml:mi> </mml:mrow> <mml:annotation encoding="application/x-tex">KR</mml:annotation> </mml:semantics> </mml:math> </inline-formula> of <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper R"> <mml:semantics> <mml:mi>R</mml:mi> <mml:annotation encoding="application/x-tex">R</mml:annotation> </mml:semantics> </mml:math> </inline-formula> and thus make it applicable to homotopy ring spaces. As applications we construct a Waldhausen type of algebraic <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper K"> <mml:semantics> <mml:mi>K</mml:mi> <mml:annotation encoding="application/x-tex">K</mml:annotation> </mml:semantics> </mml:math> </inline-formula>-theory for arbitrary homotopy ring spaces, show its equivalence with constructions of May and Steiner, prove its Morita invariance and show that the algebraic <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper K"> <mml:semantics> <mml:mi>K</mml:mi> <mml:annotation encoding="application/x-tex">K</mml:annotation> </mml:semantics> </mml:math> </inline-formula>-theory <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper K upper X"> <mml:semantics> <mml:mrow> <mml:mi>K</mml:mi> <mml:mi>X</mml:mi> </mml:mrow> <mml:annotation encoding="application/x-tex">KX</mml:annotation> </mml:semantics> </mml:math> </inline-formula> of an <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper E Subscript normal infinity"> <mml:semantics> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:msub> <mml:mi>E</mml:mi> <mml:mi mathvariant="normal">∞</mml:mi> </mml:msub> </mml:mrow> <mml:annotation encoding="application/x-tex">{E_\infty }</mml:annotation> </mml:semantics> </mml:math> </inline-formula> ring <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper X"> <mml:semantics> <mml:mi>X</mml:mi> <mml:annotation encoding="application/x-tex">X</mml:annotation> </mml:semantics> </mml:math> </inline-formula> is itself an <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper E Subscript normal infinity"> <mml:semantics> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:msub> <mml:mi>E</mml:mi> <mml:mi mathvariant="normal">∞</mml:mi> </mml:msub> </mml:mrow> <mml:annotation encoding="application/x-tex">{E_\infty }</mml:annotation> </mml:semantics> </mml:math> </inline-formula> ring. Finally we investigate the monomial map <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper Q left-parenthesis upper B upper X Subscript plus Superscript asterisk Baseline right-parenthesis right-arrow upper K upper X"> <mml:semantics> <mml:mrow> <mml:mi>Q</mml:mi> <mml:mo stretchy="false">(</mml:mo> <mml:mi>B</mml:mi> <mml:msubsup> <mml:mi>X</mml:mi> <mml:mo>+</mml:mo> <mml:mo>∗</mml:mo> </mml:msubsup> <mml:mo stretchy="false">)</mml:mo> <mml:mo stretchy="false">→</mml:mo> <mml:mi>K</mml:mi> <mml:mi>X</mml:mi> </mml:mrow> <mml:annotation encoding="application/x-tex">Q(BX_ + ^\ast ) \to KX</mml:annotation> </mml:semantics> </mml:math> </inline-formula>.

View PDF Chat

Cellular Cohomology in Homotopy Type Theory

2018-01-01

Ulrik Buchholtz , Kuen-Bang Hou

We present a development of cellular cohomology in homotopy type theory. Cohomology associates to each space a sequence of abelian groups capturing part of its structure, and has the advantage … We present a development of cellular cohomology in homotopy type theory. Cohomology associates to each space a sequence of abelian groups capturing part of its structure, and has the advantage over homotopy groups in that these abelian groups of many common spaces are easier to compute. Cellular cohomology is a special kind of cohomology designed for cell complexes: these are built in stages by attaching spheres of progressively higher dimension, and cellular cohomology defines the groups out of the combinatorial description of how spheres are attached. Our main result is that for finite cell complexes, a wide class of cohomology theories (including the ones defined through Eilenberg-MacLane spaces) can be calculated via cellular cohomology. This result was formalized in the Agda proof assistant.

View PDF Chat

Higher Structures in Homotopy Type Theory

2019-01-01

Ulrik Buchholtz

View PDF Chat

Delooping cyclic groups with lens spaces in homotopy type theory

2024-06-21

Samuel Mimram , Émile Oleon

View PDF Chat

On symmetries of spheres in univalent foundations

2024-06-21

Pierre Cagne , Ulrik Buchholtz , Nicolai Kraus +1 more

View PDF Chat

Higher Groups in Homotopy Type Theory

2018-06-27

Ulrik Buchholtz , Floris van Doorn , Egbert Rijke

We present a development of the theory of higher groups, including infinity groups and connective spectra, in homotopy type theory. An infinity group is simply the loops in a pointed, … We present a development of the theory of higher groups, including infinity groups and connective spectra, in homotopy type theory. An infinity group is simply the loops in a pointed, connected type, where the group structure comes from the structure inherent in the identity types of Martin-Löf type theory. We investigate ordinary groups from this viewpoint, as well as higher dimensional groups and groups that can be delooped more than once. A major result is the stabilization theorem, which states that if an n-type can be delooped n + 2 times, then it is an infinite loop type. Most of the results have been formalized in the Lean proof assistant.

View PDF Chat

Path Spaces of Higher Inductive Types in Homotopy Type Theory

2019-06-01

Nicolai Kraus , Jakob von Raumer

The study of equality types is central to homotopy type theory. Characterizing these types is often tricky, and various strategies, such as the encode-decode method, have been developed. We prove … The study of equality types is central to homotopy type theory. Characterizing these types is often tricky, and various strategies, such as the encode-decode method, have been developed. We prove a theorem about equality types of coequalizers and pushouts, reminiscent of an induction principle and without any restrictions on the truncation levels. This result makes it possible to reason directly about certain equality types and to streamline existing proofs by eliminating the necessity of auxiliary constructions. To demonstrate this, we give a very short argument for the calculation of the fundamental group of the circle (Licata and Shulman [1]), and for the fact that pushouts preserve embeddings. Further, our development suggests a higher version of the Seifert-van Kampen theorem, and the set-truncation operator maps it to the standard Seifert-van Kampen theorem (due to Favonia and Shulman [2]). We provide a formalization of the main technical results in the proof assistant Lean.

View PDF Chat

Quotient Inductive-Inductive Types

2018-01-01

Thorsten Altenkirch , Paolo Capriotti , Gabe Dijkstra +2 more

View PDF Chat

Duality Notions in Real Projective Plane

2021-12-01

Roland Coghetto

Summary In this article, we check with the Mizar system [1], [2], the converse of Desargues’ theorem and the converse of Pappus’ theorem of the real projective plane. It is … Summary In this article, we check with the Mizar system [1], [2], the converse of Desargues’ theorem and the converse of Pappus’ theorem of the real projective plane. It is well known that in the projective plane, the notions of points and lines are dual [11], [9], [15], [8]. Some results (analytical, synthetic, combinatorial) of projective geometry are already present in some libraries Lean/Hott [5], Isabelle/Hol [3], Coq [13], [14], [4], Agda [6], . . . . Proofs of dual statements by proof assistants have already been proposed, using an axiomatic method (for example see in [13] - the section on duality: “[...] For every theorem we prove, we can easily derive its dual using our function swap [...] 2 ”). In our formalisation, we use an analytical rather than a synthetic approach using the definitions of Leończuk and Prażmowski of the projective plane [12]. Our motivation is to show that it is possible by developing dual definitions to find proofs of dual theorems in a few lines of code. In the first part, rather technical, we introduce definitions that allow us to construct the duality between the points of the real projective plane and the lines associated to this projective plane. In the second part, we give a natural definition of line concurrency and prove that this definition is dual to the definition of alignment. Finally, we apply these results to find, in a few lines, the dual properties and theorems of those defined in the article [12] (transitive, Vebleian, at_least_3rank, Fanoian, Desarguesian, 2-dimensional). We hope that this methodology will allow us to continued more quickly the proof started in [7] that the Beltrami-Klein plane is a model satisfying the axioms of the hyperbolic plane (in the sense of Tarski geometry [10]).

View PDF Chat

Constructing Higher Inductive Types as Groupoid Quotients

2021-04-22

Niccolò Veltri , Niels van der Weide

In this paper, we study finitary 1-truncated higher inductive types (HITs) in homotopy type theory. We start by showing that all these types can be constructed from the groupoid quotient. … In this paper, we study finitary 1-truncated higher inductive types (HITs) in homotopy type theory. We start by showing that all these types can be constructed from the groupoid quotient. We define an internal notion of signatures for HITs, and for each signature, we construct a bicategory of algebras in 1-types and in groupoids. We continue by proving initial algebra semantics for our signatures. After that, we show that the groupoid quotient induces a biadjunction between the bicategories of algebras in 1-types and in groupoids. Then we construct a biinitial object in the bicategory of algebras in groupoids, which gives the desired algebra. From all this, we conclude that all finitary 1-truncated HITs can be constructed from the groupoid quotient. We present several examples of HITs which are definable using our notion of signature. In particular, we show that each signature gives rise to a HIT corresponding to the freely generated algebraic structure over it. We also start the development of universal algebra in 1-types. We show that the bicategory of algebras has PIE limits, i.e. products, inserters and equifiers, and we prove a version of the first isomorphism theorem for 1-types. Finally, we give an alternative characterization of the foundamental groups of some HITs, exploiting our construction of HITs via the groupoid quotient. All the results are formalized over the UniMath library of univalent mathematics in Coq.

View PDF Chat

Cellular Cohomology in Homotopy Type Theory

2018-06-27

Ulrik Buchholtz , Kuen-Bang Hou Favonia

View PDF Chat

Higher Groups in Homotopy Type Theory

2018-02-12

Ulrik Buchholtz , Floris van Doorn , Egbert Rijke

We present a development of the theory of higher groups, including infinity groups and connective spectra, in homotopy type theory. An infinity group is simply the loops in a pointed, … We present a development of the theory of higher groups, including infinity groups and connective spectra, in homotopy type theory. An infinity group is simply the loops in a pointed, connected type, where the group structure comes from the structure inherent in the identity types of Martin-Lof type theory. We investigate ordinary groups from this viewpoint, as well as higher dimensional groups and groups that can be delooped more than once. A major result is the stabilization theorem, which states that if an $n$-type can be delooped $n+2$ times, then it is an infinite loop type. Most of the results have been formalized in the Lean proof assistant.

Constructing Higher Inductive Types as Groupoid Quotients

2020-05-26

Niels van der Weide

In this paper, we show that all finitary 1-truncated higher inductive types (HITs) can be constructed from the groupoid quotient. We start by defining internally a notion of signatures for … In this paper, we show that all finitary 1-truncated higher inductive types (HITs) can be constructed from the groupoid quotient. We start by defining internally a notion of signatures for HITs, and for each signature, we construct a bicategory of algebras in 1-types and in groupoids. We continue by proving initial algebra semantics for our signatures. After that, we show that the groupoid quotient induces a biadjunction between the bicategories of algebras in 1-types and in groupoids. We finish by constructing a biinitial object in the bicategory of algebras in groupoids. From all this, we conclude that all finitary 1-truncated HITs can be constructed from the groupoid quotient. All the results are formalized over the UniMath library of univalent mathematics in Coq.

View PDF Chat

From Reversible Programs to Univalent Universes and Back

2018-04-01

Jacques Carette , Chao-Hong Chen , Vikraman Choudhury +1 more

We establish a close connection between a reversible programming language based on type isomorphisms and a formally presented univalent universe. The correspondence relates combinators witnessing type isomorphisms in the programming … We establish a close connection between a reversible programming language based on type isomorphisms and a formally presented univalent universe. The correspondence relates combinators witnessing type isomorphisms in the programming language to paths in the univalent universe; and combinator optimizations in the programming language to 2-paths in the univalent universe. The result suggests a simple computational interpretation of paths and of univalence in terms of familiar programming constructs whenever the universe in question is computable.

View PDF Chat

Symmetries in reversible programming: from symmetric rig groupoids to reversible programming languages

2022-01-12

Vikraman Choudhury , Jacek Karwowski , Amr Sabry

The Pi family of reversible programming languages for boolean circuits is presented as a syntax of combinators witnessing type isomorphisms of algebraic data types. In this paper, we give a … The Pi family of reversible programming languages for boolean circuits is presented as a syntax of combinators witnessing type isomorphisms of algebraic data types. In this paper, we give a denotational semantics for this language, using weak groupoids à la Homotopy Type Theory, and show how to derive an equational theory for it, presented by 2-combinators witnessing equivalences of type isomorphisms. We establish a correspondence between the syntactic groupoid of the language and a formally presented univalent subuniverse of finite types. The correspondence relates 1-combinators to 1-paths, and 2-combinators to 2-paths in the universe, which is shown to be sound and complete for both levels, forming an equivalence of groupoids. We use this to establish a Curry-Howard-Lambek correspondence between Reversible Logic, Reversible Programming Languages, and Symmetric Rig Groupoids, by showing that the syntax of Pi is presented by the free symmetric rig groupoid, given by finite sets and bijections. Using the formalisation of our results, we perform normalisation-by-evaluation, verification and synthesis of reversible logic gates, motivated by examples from quantum computing. We also show how to reason about and transfer theorems between different representations of reversible circuits.

View PDF Chat

Constructing the propositional truncation using non-recursive HITs

2016-01-12

Floris van Doorn

In homotopy type theory, we construct the propositional truncation as a colimit, using only non-recursive higher inductive types (HITs). This is a first step towards reducing recursive HITs to non-recursive … In homotopy type theory, we construct the propositional truncation as a colimit, using only non-recursive higher inductive types (HITs). This is a first step towards reducing recursive HITs to non-recursive HITs. This construction gives a characterization of functions from the propositional truncation to an arbitrary type, extending the universal property of the propositional truncation. We have fully formalized all the results in a new proof assistant, Lean.

View PDF Chat

Brouwer's fixed-point theorem in real-cohesive homotopy type theory

2015-09-25

Michael Shulman

We combine Homotopy Type Theory with axiomatic cohesion, expressing the latter internally with a version of adjoint logic in which the discretization and codiscretization modalities are characterized using a judgmental … We combine Homotopy Type Theory with axiomatic cohesion, expressing the latter internally with a version of adjoint logic in which the discretization and codiscretization modalities are characterized using a judgmental formalism of crisp variables. This yields type theories that we call spatial and cohesive, in which the types can be viewed as having independent topological and homotopical structure. These type theories can then be used to study formally the process by which topology gives rise to homotopy theory (the fundamental $\infty$-groupoid or shape), disentangling the identifications of Homotopy Type Theory from the paths of topology. In a further refinement called real-cohesion, the shape is determined by continuous maps from the real numbers, as in classical algebraic topology. This enables us to reproduce formally some of the classical applications of homotopy theory to topology. As an example, we prove Brouwer's fixed-point theorem.

Constructions with Non-Recursive Higher Inductive Types

2016-07-05

Nicolai Kraus

Higher inductive types (HITs) in homotopy type theory are a powerful generalization of inductive types. Not only can they have ordinary constructors to define elements, but also higher constructors to … Higher inductive types (HITs) in homotopy type theory are a powerful generalization of inductive types. Not only can they have ordinary constructors to define elements, but also higher constructors to define equalities (paths). We say that a HIT H is non-recursive if its constructors do not quantify over elements or paths in H. The advantage of non-recursive HITs is that their elimination principles are easier to apply than those of general HITs.

View PDF Chat

The Simplicial Model of Univalent Foundations (after Voevodsky)

2012-11-12

Chris Kapulkin , Peter LeFanu Lumsdaine

We present Voevodsky's construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categorical models … We present Voevodsky's construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categorical models of dependent type theory, using universes to obtain coherence. We then construct a (weakly) universal Kan fibration, and use it to exhibit a model in simplicial sets. Lastly, we introduce the Univalence Axiom, in several equivalent formulations, and show that it holds in our model. As a corollary, we conclude that Martin-Lof type theory with one univalent universe (formulated in terms of contextual categories) is at least as consistent as ZFC with two inaccessible cardinals.

The join construction

2017-01-26

Egbert Rijke

In homotopy type theory we can define the join of maps as a binary operation on maps with a common co-domain. This operation is commutative, associative, and the unique map … In homotopy type theory we can define the join of maps as a binary operation on maps with a common co-domain. This operation is commutative, associative, and the unique map from the empty type into the common codomain is a neutral element. Moreover, we show that the idempotents of the join of maps are precisely the embeddings, and we prove the `join connectivity theorem', which states that the connectivity of the join of maps equals the join of the connectivities of the individual maps. We define the image of a map $f:A\to X$ in $U$ via the join construction, as the colimit of the finite join powers of $f$. The join powers therefore provide approximations of the image inclusion, and the join connectivity theorem implies that the approximating maps into the image increase in connectivity. A modified version of the join construction can be used to show that for any map $f:A\to X$ in which $X$ is only assumed to be locally small, the image is a small type. We use the modified join construction to give an alternative construction of set-quotients, the Rezk completion of a precategory, and we define the $n$-truncation for any $n:\mathbb{N}$. Thus we see that each of these are definable operations on a univalent universe for Martin-Lof type theory with a natural numbers object, that is moreover closed under homotopy coequalizers.

Algebraic topology

2001-12-03

Allen Hatcher

Homotopy theoretic models of identity types

2008-07-14

Steve Awodey , Michael A. Warren

This paper presents a novel connection between homotopical algebra and mathematical logic. It is shown that a form of intensional type theory is valid in any Quillen model category, generalizing … This paper presents a novel connection between homotopical algebra and mathematical logic. It is shown that a form of intensional type theory is valid in any Quillen model category, generalizing the Hofmann-Streicher groupoid model of Martin-Loef type theory.

View PDF Chat

Brouwer's fixed-point theorem in real-cohesive homotopy type theory

2015-01-01

Michael Shulman

We combine Homotopy Type Theory with axiomatic cohesion, expressing the latter internally with a version of "adjoint logic" in which the discretization and codiscretization modalities are characterized using a judgmental … We combine Homotopy Type Theory with axiomatic cohesion, expressing the latter internally with a version of "adjoint logic" in which the discretization and codiscretization modalities are characterized using a judgmental formalism of "crisp variables". This yields type theories that we call "spatial" and "cohesive", in which the types can be viewed as having independent topological and homotopical structure. These type theories can then be used to study formally the process by which topology gives rise to homotopy theory (the "fundamental $\infty$-groupoid" or "shape"), disentangling the "identifications" of Homotopy Type Theory from the "continuous paths" of topology. In a further refinement called "real-cohesion", the shape is determined by continuous maps from the real numbers, as in classical algebraic topology. This enables us to reproduce formally some of the classical applications of homotopy theory to topology. As an example, we prove Brouwer's fixed-point theorem.

View PDF Chat

Cubical Type Theory: a constructive interpretation of the univalence axiom

2015-05-18

Cyril Cohen , Thierry Coquand , Simon Huber +1 more

This paper presents a type theory in which it is possible to directly manipulate n-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in … This paper presents a type theory in which it is possible to directly manipulate n-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in a cubical set model. This enables new ways to reason about identity types, for instance, function extensionality is directly provable in the system. Further, Voevodsky's univalence axiom is provable in this system. We also explain an extension with some higher inductive types like the circle and propositional truncation. Finally we provide semantics for this cubical type theory in a constructive meta-theory.

View PDF Chat