Decide on a research project #12

New issue

Closed

opened 2024-04-22 04:35:00 +00:00 by michael · 3 comments

michael commented

2024-04-22 04:35:00 +00:00

Owner

Possible ideas from meeting on 2024-04-18 with Favonia:

Check in with Axel to see if any of the ideas from last year are still being worked on / need help
~~Port POPL paper to Ocaml~~
~~Component libraries of the proof assistants (will be much harder, need to figure out what is involved)~~

Possible ideas from meeting on 2024-04-18 with Favonia: - [x] Check in with Axel to see if any of the ideas from last year are still being worked on / need help - [x] ~~Port [POPL paper][1] to Ocaml~~ - [x] ~~Component libraries of the proof assistants (will be much harder, need to figure out what is involved)~~ [1]: https://favonia.org/files/logarithm.pdf

michael added this to the (deleted) project 2024-04-22 04:35:00 +00:00

michael added a new dependency 2024-04-22 04:35:54 +00:00

#11 Thesis Project

michael referenced this issue

2024-04-22 04:36:13 +00:00

Thesis Project #11

michael modified the project from (deleted) to research

2024-04-25 13:44:42 +00:00

michael commented

2024-05-16 14:04:49 +00:00

Author

Owner

As discussed in 2024-05-09 meeting with Favonia, will reconsider focus towards just formalizing some math theorems.

michael commented

2024-05-17 06:05:36 +00:00

Author

Owner

Notes from this morning's meeting with Axel

Cellular homology
- Doing homology rather than cohomology
Loïc Pujet collaborator
CW complexes
- doing it differently than paper https://arxiv.org/pdf/1802.02191
- prove that their theory is functorial by comparing it to another cohomology theory
current work is proving functoriality directly
- map between 2 cw complexes -> cellular approximation
- constructed homology functor
Eilenberg-steenrod axioms
- characterizing cohomology theory
- dualizing homology
- Hurewicz theorem
  - issue is they have everything in the library
Mayor Vietoris sequence (long exact sequence of cohomology groups
Evan cavallo
- formlaized cohomology theory, being a functor that satisfies the eilenberg steenrod axioms
- proved if u have cohomology, then u can construct mayor vietoris sequence
- IDEA corresponding theory for homology rather than cohomology
  - construct mayer vietoris sequence
- https://ecavallo.net/works/thesis15.pdf
  - uses some outdated ways of writing proofs in hott
  - look primarily at the statements
homology axioms
- https://arxiv.org/pdf/1706.01540
  - definition 1 1 is some of the eilenberg steenrod axioms
  - some times people functorality assumptions as an axiom
- https://en.wikipedia.org/wiki/Eilenberg%E2%80%93Steenrod_axioms
- https://ncatlab.org/nlab/show/ordinary+homology
IDEA formalize spectral sequences (Floris van Doorn's PHD thesis)
- https://florisvandoorn.com/talks/Bonn2018spectralsequences.pdf
- formalized previously, but not in cubical
- https://florisvandoorn.com/papers/dissertation.pdf
- spectral sequences for homology (instead of cohomology)
nice direction is just computing homology groups of specific spaces
- compute cohomology groups, running proof by computation, see if you can actually normalize certain proof termss
- https://aljungstrom.github.io/publication/CSL22
- https://arxiv.org/abs/1606.05916
advice
- learn by formalizing more homotopy theoretical mathematics
- hatcher

Notes from this morning's meeting with Axel - Cellular homology - Doing homology rather than cohomology - Loïc Pujet collaborator - CW complexes - doing it differently than paper https://arxiv.org/pdf/1802.02191 - prove that their theory is functorial by comparing it to another cohomology theory - current work is proving functoriality directly - map between 2 cw complexes -> cellular approximation - constructed homology functor - Eilenberg-steenrod axioms - characterizing cohomology theory - dualizing homology - Hurewicz theorem - issue is they have everything in the library - Mayor Vietoris sequence (long exact sequence of cohomology groups - Evan cavallo - formlaized cohomology theory, being a functor that satisfies the eilenberg steenrod axioms - proved if u have cohomology, then u can construct mayor vietoris sequence - IDEA corresponding theory for homology rather than cohomology - construct mayer vietoris sequence - https://ecavallo.net/works/thesis15.pdf - uses some outdated ways of writing proofs in hott - look primarily at the statements - homology axioms - https://arxiv.org/pdf/1706.01540 - definition 1 1 is some of the eilenberg steenrod axioms - some times people functorality assumptions as an axiom - https://en.wikipedia.org/wiki/Eilenberg%E2%80%93Steenrod_axioms - https://ncatlab.org/nlab/show/ordinary+homology - IDEA formalize spectral sequences (Floris van Doorn's PHD thesis) - https://florisvandoorn.com/talks/Bonn2018spectralsequences.pdf - formalized previously, but not in cubical - https://florisvandoorn.com/papers/dissertation.pdf - spectral sequences for homology (instead of cohomology) - nice direction is just computing homology groups of specific spaces - compute cohomology groups, running proof by computation, see if you can actually normalize certain proof termss - https://aljungstrom.github.io/publication/CSL22 - https://arxiv.org/abs/1606.05916 - advice - learn by formalizing more homotopy theoretical mathematics - hatcher

michael commented

2024-05-23 15:19:29 +00:00

Author

Owner

Decided on: formalize spectral sequences (Floris van Doorn's PHD thesis)

https://florisvandoorn.com/talks/Bonn2018spectralsequences.pdf
formalized previously, but not in cubical
https://florisvandoorn.com/papers/dissertation.pdf

Decided on: formalize spectral sequences (Floris van Doorn's PHD thesis) - https://florisvandoorn.com/talks/Bonn2018spectralsequences.pdf - formalized previously, but not in cubical - https://florisvandoorn.com/papers/dissertation.pdf

michael closed this issue

2024-05-23 15:19:29 +00:00