```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.

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

```* [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 Caglayan
2018-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.

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

```* 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 Christensen
2018-08-18 16:17   ` Guillaume Brunerie
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.

```* Re: [HoTT] Real Projective space (and other projective spaces too)
2018-08-18 14:45 ` [HoTT] " Dan Christensen
@ 2018-08-18 16:17   ` Guillaume Brunerie
2018-08-18 19:35     ` Dan Christensen
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
> 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.

[-- Attachment #2: Type: text/html, Size: 3052 bytes --]

```* Re: [HoTT] Real Projective space (and other projective spaces too)
2018-08-18 16:17   ` Guillaume Brunerie
@ 2018-08-18 19:35     ` Dan Christensen
2018-08-19  6:36       ` Guillaume Brunerie
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
>  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.

```* Re: [HoTT] Real Projective space (and other projective spaces too)
2018-08-18 19:35     ` Dan Christensen
@ 2018-08-19  6:36       ` Guillaume Brunerie
0 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
> >  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
> 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.

[-- Attachment #2: Type: text/html, Size: 4184 bytes --]

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

```This is a public inbox, see mirroring instructions