Hopfovo vlaknenje v homotopski teoriji tipovSlapar, Jaka (Avtor) Swan, Andrew Wakelin (Mentor) homotopska teorija tipovHopfovo vlaknenjevišji induktivni tipiunivalenčni aksiomhomotopske grupesfereV delu obravnavamo Hopfovo vlaknenje v homotopski teoriji tipov. Predstavimo sintetično interpretacijo tipov kot prostorov in identifikacij kot poti ter razvijemo pojme transporta, homotopije, ekvivalence, povezanosti in homotopskih grup. Z višjimi induktivnimi tipi definiramo krog, suspenzije, sfere, potiske in spoje. S pomočjo $H$-strukture kroga in univalenčnega aksioma konstruiramo družino tipov nad sfero $\mathbb{S}^2$, katere izbrano vlakno je $\mathbb{S}^1$. Z lemo o sploščevanju pokažemo, da je njegov totalni prostor ekvivalenten sferi $\mathbb{S}^3$, in tako dobimo Hopfovo vlaknenje $$\mathbb{S}^1 \longrightarrow \mathbb{S}^3 \longrightarrow \mathbb{S}^2.$$ Izračunamo fundamentalno grupo kroga in pokažemo, da velja $\pi_1(\mathbb{S}^1)\simeq\mathbb{Z}$, njegove višje homotopske grupe pa so trivialne. Z uporabo dolgega eksaktnega zaporedja Hopfovega vlaknenja nato izpeljemo $$\pi_2(\mathbb{S}^2)\simeq\mathbb Z$$ ter $\pi_n(\mathbb{S}^2)\simeq\pi_n(\mathbb{S}^3)$ za vsak $n\geq 3$.20262026-09-19 08:15:27Delo diplomskega seminarja/zaključno seminarsko delo/naloga188192UDK: 515.1:510.6VisID: 164613COBISS_ID: 291892739sl