Define LES #25

New issue

Open

opened 2024-10-10 06:17:19 +00:00 by michael · 3 comments

michael commented

2024-10-10 06:17:19 +00:00

Owner

Step 1 (#40): Define the fiber sequence of f
Step 2: Show that this sequence is equivalent to a sequence involving iterated loop spaces
Step 3: Fix negation signs in the exact sequence
Step 4: Index the sequence over \mathbb{N} \times \mathsf{fin}_3
Step 5: 0-truncate the sequence to obtain the sequence in 4.1.1

- [ ] Step 1 (#40): Define the fiber sequence of $f$ - [ ] Step 2: Show that this sequence is equivalent to a sequence involving iterated loop spaces - [ ] Step 3: Fix negation signs in the exact sequence - [ ] Step 4: Index the sequence over $\mathbb{N} \times \mathsf{fin}_3$ - [ ] Step 5: 0-truncate the sequence to obtain the sequence in 4.1.1

michael added this to the research project 2024-10-10 06:28:22 +00:00

michael commented

2024-10-10 06:32:12 +00:00

Author

Owner

Currently trying to define \mathsf{h1}_n : \Omega^n(X) \rightarrow \Omega^n(Y)

Currently trying to define $\mathsf{h1}_n : \Omega^n(X) \rightarrow \Omega^n(Y)$

michael referenced this issue from a commit

2024-10-10 09:41:55 +00:00

LES definition similar to the one used by Floris, closes #25

michael closed this issue

2024-10-10 09:41:55 +00:00

michael commented

2024-10-10 09:42:27 +00:00

Author

Owner

Still many warnings left tho

warning: -W[no]UnsupportedIndexedMatch
This clause uses pattern-matching features that are not yet
supported by Cubical Agda, the function to which it belongs will
not compute when applied to transports.
Reason: It relies on injectivity of the data constructor suc, which
        is not yet supported
when checking the definition of LES-edge

also need to figure out why expressions like (Ω^ n) (F , x , f-eq) .snd don't simplify

Still many warnings left tho ``` warning: -W[no]UnsupportedIndexedMatch This clause uses pattern-matching features that are not yet supported by Cubical Agda, the function to which it belongs will not compute when applied to transports. Reason: It relies on injectivity of the data constructor suc, which is not yet supported when checking the definition of LES-edge ``` also need to figure out why expressions like `(Ω^ n) (F , x , f-eq) .snd` don't simplify

michael commented

2024-10-15 05:04:31 +00:00

Author

Owner

This makes me wonder if my current definition of LES is the best possible one. This might change later on...

michael reopened this issue

2024-10-16 06:36:28 +00:00

michael referenced this issue

2024-10-16 06:41:47 +00:00

Formalize section 4.1, proving π₃(S²) ≃ ℤ #35