*[HoTT] Real Projective space (and other projective spaces too)@ 2018-08-18 14:30 Ali Caglayan2018-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

*[HoTT] Re: Real Projective space (and other projective spaces too)2018-08-18 14:30 [HoTT] Real Projective space (and other projective spaces too) Ali Caglayan@ 2018-08-18 14:33 ` Ali Caglayan2018-08-18 14:45 ` [HoTT] " Dan Christensen 1 sibling, 0 replies; 6+ messages in thread From: Ali Caglayan @ 2018-08-18 14:33 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 437 bytes --] The octionic one doesn't actually work for the projective plane now that I think about it as there is no fibration S^7 -> S^23 -> OP^2 -- 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: 632 bytes --] ^ permalink raw reply [flat|nested] 6+ messages in thread

*Re: [HoTT] Real Projective space (and other projective spaces too)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 ` Dan Christensen2018-08-18 16:17 ` Guillaume Brunerie 1 sibling, 1 reply; 6+ messages in thread From: Dan Christensen @ 2018-08-18 14:45 UTC (permalink / raw) To: Homotopy Type Theory On Aug 18, 2018, Ali Caglayan <alizter@gmail.com> wrote: > 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. That HIT would be S^n with four edges attached: two edges connecting the north pole to the south pole, and a self-loop at each pole. So homotopically it would be S^n wedged with a wedge of four circles. To get the right space with the right bundle over it, see: The real projective spaces in homotopy type theory Ulrik Buchholtz, Egbert Rijke https://arxiv.org/abs/1704.05770 Dan -- 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. ^ permalink raw reply [flat|nested] 6+ messages in thread

*Re: [HoTT] Real Projective space (and other projective spaces too)2018-08-18 14:45 ` [HoTT] " Dan Christensen@ 2018-08-18 16:17 ` Guillaume Brunerie2018-08-18 19:35 ` Dan Christensen 0 siblings, 1 reply; 6+ messages in thread From: Guillaume Brunerie @ 2018-08-18 16:17 UTC (permalink / raw) To: alizter;+Cc:Homotopy Type Theory [-- Attachment #1: Type: text/plain, Size: 1890 bytes --] As Dan said, this is not a correct definition of RP^n. More specifically, the issue is that you identified the points "map south" and "map north" in two different ways: "glue south north" and "inv (glue north south)". You could try to add another constructor glue² : (x y : S^n) -> glue x y = inv (glue y x) but of course you're now again identifying them in two different ways, so you've just shifted the problem one dimension up. Den lör 18 aug. 2018 16:46Dan Christensen <jdc@uwo.ca> skrev: > On Aug 18, 2018, Ali Caglayan <alizter@gmail.com> wrote: > > > 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. > > That HIT would be S^n with four edges attached: two edges connecting > the north pole to the south pole, and a self-loop at each pole. So > homotopically it would be S^n wedged with a wedge of four circles. > > To get the right space with the right bundle over it, see: > > The real projective spaces in homotopy type theory > Ulrik Buchholtz, Egbert Rijke > https://arxiv.org/abs/1704.05770 > > Dan > > -- > 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. > -- 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 #2: Type: text/html, Size: 3052 bytes --] ^ permalink raw reply [flat|nested] 6+ messages in thread

*Re: [HoTT] Real Projective space (and other projective spaces too)2018-08-18 16:17 ` Guillaume Brunerie@ 2018-08-18 19:35 ` Dan Christensen2018-08-19 6:36 ` Guillaume Brunerie 0 siblings, 1 reply; 6+ messages in thread From: Dan Christensen @ 2018-08-18 19:35 UTC (permalink / raw) To: Homotopy Type Theory The extra identifications are one of the problems, but a more fundamental problem is that while the north pole has been identified with the south pole, no other pairs of antipodal points have been identified. Dan On Aug 18, 2018, Guillaume Brunerie <guillaume.brunerie@gmail.com> wrote: > As Dan said, this is not a correct definition of RP^n. > > More specifically, the issue is that you identified the points "map south" and "map north" in two different ways: "glue south north" and > "inv (glue north south)". > You could try to add another constructor > glue² : (x y : S^n) -> glue x y = inv (glue y x) > but of course you're now again identifying them in two different ways, so you've just shifted the problem one dimension up. > > Den lör 18 aug. 2018 16:46Dan Christensen <jdc@uwo.ca> skrev: > > On Aug 18, 2018, Ali Caglayan <alizter@gmail.com> wrote: > > > 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. > > That HIT would be S^n with four edges attached: two edges connecting > the north pole to the south pole, and a self-loop at each pole. So > homotopically it would be S^n wedged with a wedge of four circles. > > To get the right space with the right bundle over it, see: > > The real projective spaces in homotopy type theory > Ulrik Buchholtz, Egbert Rijke > https://arxiv.org/abs/1704.05770 > > Dan > > -- > 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. -- 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. ^ permalink raw reply [flat|nested] 6+ messages in thread

*2018-08-18 19:35 ` Dan ChristensenRe: [HoTT] Real Projective space (and other projective spaces too)@ 2018-08-19 6:36 ` Guillaume Brunerie0 siblings, 0 replies; 6+ messages in thread From: Guillaume Brunerie @ 2018-08-19 6:36 UTC (permalink / raw) To: Dan Christensen;+Cc:Homotopy Type Theory [-- Attachment #1: Type: text/plain, Size: 2754 bytes --] Ah, indeed, I misread the proposed definition. Den lör 18 aug. 2018 21:35Dan Christensen <jdc@uwo.ca> skrev: > The extra identifications are one of the problems, but a more > fundamental problem is that while the north pole has been identified > with the south pole, no other pairs of antipodal points have been > identified. > > Dan > > On Aug 18, 2018, Guillaume Brunerie <guillaume.brunerie@gmail.com> wrote: > > > As Dan said, this is not a correct definition of RP^n. > > > > More specifically, the issue is that you identified the points "map > south" and "map north" in two different ways: "glue south north" and > > "inv (glue north south)". > > You could try to add another constructor > > glue² : (x y : S^n) -> glue x y = inv (glue y x) > > but of course you're now again identifying them in two different ways, > so you've just shifted the problem one dimension up. > > > > Den lör 18 aug. 2018 16:46Dan Christensen <jdc@uwo.ca> skrev: > > > > On Aug 18, 2018, Ali Caglayan <alizter@gmail.com> wrote: > > > > > 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. > > > > That HIT would be S^n with four edges attached: two edges connecting > > the north pole to the south pole, and a self-loop at each pole. So > > homotopically it would be S^n wedged with a wedge of four circles. > > > > To get the right space with the right bundle over it, see: > > > > The real projective spaces in homotopy type theory > > Ulrik Buchholtz, Egbert Rijke > > https://arxiv.org/abs/1704.05770 > > > > Dan > > > > -- > > 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. > > -- > 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. > -- 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 #2: Type: text/html, Size: 4184 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).