Seminar: Proof Lab: Simplicial Topology; WS 2021/22

News

The templates for reports/handouts are online (see below); of course, you can also produce the report/handout by other means.
According to current plans (30.09.2021): This course will be taught on campus in person. On request, I could turn this into a hybrid format (with live streaming). Please note that there will be no recordings of the lectures. The lectures are a precious opportunity for live interaction and I want to keep the atmosphere as casual and unintimidating as possible. Please let me know (by email) in case there is a need for the hybrid option!
The schedule is now available.
The organisational meeting for this seminar will be on Monday, July 12, at 12:15 in zoom; access data is provided on the GRIPS course page.
Alternatively, you can register for this seminar by sending an email to clara.loeh@mathematik.uni-r.de .

Seminar: Proof Lab: Simplicial Topology

Many topological objects admit simple combinatorial descriptions through so-called simplicial complexes (a higher-dimensional version of graphs). This simplifies the computation of invariants from algebraic topology. Conversely, many situations arising in real-world applications can be modelled by simplicial complexes.

In this seminar, we will study combinatorial aspects of algebraic topology and their applications. Moreover, for additional excitement, we will implement fragments of the theory in a proof assistant. Proof assistants are not only used within mathematics, but also in industrial settings to verify properties of complex systems.

Details: seminar schedule.

Time/Location

Wednesday, 8:30--10:00, M 104
(if in-person teaching is the preferred option; otherwise, this seminar will be taught online)

Material

Overview of all talks (and some organisatorial hints).
Lecture notes (for talk 1 and 2): pdf
Talk 1: skeleton for the Lean exercises: maps_exercise.lean
Talk 1: maps.lean (we did not cover all of this in the talk; the rest will be discussed in Talk 2)
Talk 2: skeleton for the Lean exercises: induction_exercise.lean
Talk 1: induction.lean
Talk 1: commutator.lean

LaTeX template for handouts: .tex, .pdf
(The template is in German, but that hopefully won't cause any problems).
LaTeX template for reports: .tex, .pdf
(The template is in German, but that hopefully won't cause any problems).
Hints on writing mathematical texts (in German)
More such hints
Small print on slide talks

Prerequisites

Analysis I/II, Linear Algebra I/II; basic group theory as taught in (Linear) Algebra; no previous knowledge in Algebraic Topology is necessary, but the seminar fits well with the Algebraic Topology I course in WS 21/22. No prior programming experience is necessary.
This seminar is suitable for Bachelor/Master students and Lehramtsstudenten with an interest in topology and combinatorics, and could be the starting point for a project under my supervision (e.g., bachelor/master thesis, Zulassungsarbeit).

Formalities/Credits

See the commented list of courses.

Last Change: October 27, 2021.