Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] Real Projective space (and other projective spaces too)
@ 2018-08-18 14:30 Ali Caglayan
  2018-08-18 14:33 ` [HoTT] " Ali Caglayan
  2018-08-18 14:45 ` [HoTT] " Dan Christensen
  0 siblings, 2 replies; 6+ messages in thread
From: Ali Caglayan @ 2018-08-18 14:30 UTC (permalink / raw)
  To: Homotopy Type Theory


[-- Attachment #1.1: Type: text/plain, Size: 1921 bytes --]

There are a family of fibrations called "generalised hopf fibrations". 

For the real hopf fibrations we have:
S⁰→Sⁿ→ℝℙⁿ
For the complex (usual) hopf fibrations we have:
S¹→S²ⁿ⁺¹→ℂℙⁿ
For the quarternionic hopf fibrations we have:
S³→S⁴ⁿ⁺³→ℍℙⁿ
And finally (only when n <= 2) we have the octionic hopf fibrations:
S⁷→S⁸ⁿ⁺⁷→𝕆ℙⁿ

This screams to me an alternative definition for ℝℙⁿ (and maybe ℂℙⁿ,...)

Inductive RP (n:ℕ) :=
  | map : Sⁿ -> RP n
  | glue : (x y:S⁰) -> map(in x) = map(in y)

Where in : S⁰→Sⁿ is the obvious inclusion map.

Now showing that this is equivalent to the usual definition would 
essentially require a construction of the fibrations they were defined 
from. This fibration is not so easy however, as we cannot 'cheat' and use 
the H-space fibration.

Now the main advantage I see with this definition is that it allows the 
complex, quarterionic etc. projective spaces to be constructed similarly. I 
don't think anybody has constructed quarternionic projective space although 
it should definitely be doable. the main questions arise when octionic 
projective space is considered as in classical AT it degernates pretty 
quickly. (Does this still happen in HoTT, if yes, how so?).

Finally a disclaimer, I thought about these whilst traveling and haven't 
had the time to really put some meat on them. Though hopefully it might 
strike a chord with anyone who has considered a similar thing.

I would love to hear your thoughts and feelings about such things.

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.2: Type: text/html, Size: 5051 bytes --]

^ permalink raw reply	[flat|nested] 6+ messages in thread

end of thread, other threads:[~2018-08-19  6:36 UTC | newest]

Thread overview: 6+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2018-08-18 14:30 [HoTT] Real Projective space (and other projective spaces too) Ali Caglayan
2018-08-18 14:33 ` [HoTT] " Ali Caglayan
2018-08-18 14:45 ` [HoTT] " Dan Christensen
2018-08-18 16:17   ` Guillaume Brunerie
2018-08-18 19:35     ` Dan Christensen
2018-08-19  6:36       ` Guillaume Brunerie

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).