[Merged by Bors] - feat(Topology/Covering): fundamental group of the circle is ℤ by Ruizsolveall · Pull Request #41856 · leanprover-community/mathlib4

Ruizsolveall · 2026-07-17T10:48:16Z

This is the promised follow-up to #40947 (see Zulip); most of the file is the computation that the loop t ↦ n • t is sent to n : ℤ.

I used Claude to navigate the quotient covering map API and for an initial frame of the proofs, which I then reworked; I understand and can vouch for all of it.

github-actions · 2026-07-17T10:48:26Z

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

github-actions · 2026-07-17T10:49:48Z

PR summary ed5019cef3

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Topology.Covering.FundamentalGroupCircle` (new file)	1839

Declarations diff (regex)

+ coe_monodromy_mk
+ coe_zmultiplesEquivInt_symm_apply
+ instance [Add α] [IsAddCommutative α] : IsMulCommutative (Multiplicative α)
+ instance [Mul α] [IsMulCommutative α] : IsAddCommutative (Additive α)
+ monodromy_eq_apply_one
+ windingNumber
+ windingNumberIso
+ windingNumber_eq_div
+ windingNumber_zsmulLoop
+ zmultiplesEquivInt
+ zmultiplesEquivInt_apply_zsmul
+ zmultiplesHom_injective
+ zsmulLoop
+ zsmulLoop_apply
++ fundamentalGroupEquiv_eq
++ fundamentalGroupToMulOpposite_apply_mk_eq
++ fundamentalGroupToMulOpposite_eq
++ fundamentalGroupToMulOpposite_toPermFiber

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit ed5019c).

+27 new declarations
−0 removed declarations

+AddCircle.windingNumber
+AddCircle.windingNumber.congr_simp
+AddCircle.windingNumberIso
+AddCircle.windingNumber_eq_div
+AddCircle.windingNumber_zsmulLoop
+AddCircle.zsmulLoop
+AddCircle.zsmulLoop_apply
+AddEquiv.addSubgroupCongr.congr_simp
+AddMonoidHom.ofInjective.congr_simp
+AddSubgroup.coe_zmultiplesEquivInt_symm_apply
+AddSubgroup.zmultiplesEquivInt
+AddSubgroup.zmultiplesEquivInt.congr_simp
+AddSubgroup.zmultiplesEquivInt_apply_zsmul
+IsAddQuotientCoveringMap.fundamentalGroupEquiv.congr_simp
+IsAddQuotientCoveringMap.fundamentalGroupEquiv_eq
+IsAddQuotientCoveringMap.fundamentalGroupToMulOpposite_apply_mk_eq
+IsAddQuotientCoveringMap.fundamentalGroupToMulOpposite_eq
+IsAddQuotientCoveringMap.fundamentalGroupToMulOpposite_toPermFiber
+IsCoveringMap.coe_monodromy_mk
+IsCoveringMap.monodromy_eq_apply_one
+IsQuotientCoveringMap.fundamentalGroupEquiv_eq
+IsQuotientCoveringMap.fundamentalGroupToMulOpposite_apply_mk_eq
+IsQuotientCoveringMap.fundamentalGroupToMulOpposite_eq
+IsQuotientCoveringMap.fundamentalGroupToMulOpposite_toPermFiber
+instIsAddCommutativeAdditiveOfIsMulCommutative
+instIsMulCommutativeMultiplicativeOfIsAddCommutative
+zmultiplesHom_injective

No changes to strong technical debt.

Increase in weak tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (weak)
exposed public sections	5067	1

Current commit ed5019cef3
Reference commit bd6c1abe5f

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

mathlib-merge-conflicts · 2026-08-28T23:21:58Z

This pull request has conflicts, please merge master and resolve them.

…upEquiv Add `AddSubgroup.zmultiplesEquivInt`, the isomorphism `zmultiples a ≃+ ℤ` for a non-torsion element `a`, together with `zmultiplesHom_injective`. In `Lifting.lean`, record `IsCoveringMap.coe_monodromy_mk` next to the definition of `monodromy`, and show that `IsQuotientCoveringMap.fundamentalGroupToMulOpposite` is conjugated by `g` when the basepoint is moved by `g`; in particular it (and `fundamentalGroupEquiv`) does not depend on the basepoint when the group is commutative.

The loop `zsmulLoop p x n` is `t ↦ n • (t * p) + x`, `windingNumberIso` is defined at any basepoint of `AddCircle p`, and the winding number of a loop is computed directly from any continuous lift as `(f 1 - f 0) / p`.

…sHom_injective Add the instances `IsAddCommutative (Additive α)` and `IsMulCommutative (Multiplicative α)` so the additive basepoint-independence lemmas in `Lifting.lean` need no ad hoc instance. Move `zmultiplesHom_injective` next to `zmultiplesHom`.

alreadydone · 2026-09-20T17:45:23Z

Thank you! This is almost ready except for some golfs I just suggested at Ruizsolveall#1.

Ruizsolveall · 2026-09-21T10:37:24Z

Merged your golfs, thanks a lot! Also wrapped one long line in the additive version.

alreadydone · 2026-09-23T06:41:25Z

Thank you!
maintainer merge

github-actions · 2026-09-23T06:41:53Z

🚀 Pull request has been placed on the maintainer queue by alreadydone.

ocfnash · 2026-09-29T13:58:06Z

Thanks!

bors merge

This is the promised follow-up to #40947 (see [Zulip](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/How.20to.20wisely.20state.20Homotopy.20lifting.20lemma)); most of the file is the computation that the loop `t ↦ n • t` is sent to `n : ℤ`. Co-authored-by: Ruizsolveall <ruizizchen@gmail.com> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

mathlib-bors · 2026-09-29T14:58:32Z

Build failed (retrying...):

ci (staging) / Post-CI job

This is the promised follow-up to #40947 (see [Zulip](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/How.20to.20wisely.20state.20Homotopy.20lifting.20lemma)); most of the file is the computation that the loop `t ↦ n • t` is sent to `n : ℤ`. Co-authored-by: Ruizsolveall <ruizizchen@gmail.com> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

mathlib-bors · 2026-09-29T16:43:40Z

Pull request successfully merged into master.

Build succeeded:

…over-community#41856) This is the promised follow-up to leanprover-community#40947 (see [Zulip](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/How.20to.20wisely.20state.20Homotopy.20lifting.20lemma)); most of the file is the computation that the loop `t ↦ n • t` is sent to `n : ℤ`. Co-authored-by: Ruizsolveall <ruizizchen@gmail.com> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

feat(Topology/Covering): fundamental group of the circle is ℤ

42e3855

github-actions Bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Jul 17, 2026

github-actions Bot added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Jul 17, 2026

run mk_all

ed2aa20

grunweg added the LLM-generated PRs with substantial input from LLMs - review accordingly label Jul 31, 2026

mathlib-triage Bot assigned ADedecker Aug 21, 2026

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 28, 2026

Ruizsolveall added 2 commits September 3, 2026 16:57

Merge branch 'master' into feat/circle-pi1

2a47eac

chore: replace deprecated Equiv.apply_eq_iff_eq_symm_apply

4a1f4b8

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 3, 2026

alreadydone reviewed Sep 6, 2026

View reviewed changes

Ruizsolveall added 3 commits September 7, 2026 13:59

refactor: generalize to AddCircle p at an arbitrary basepoint

7faa4df

The loop `zsmulLoop p x n` is `t ↦ n • (t * p) + x`, `windingNumberIso` is defined at any basepoint of `AddCircle p`, and the winding number of a loop is computed directly from any continuous lift as `(f 1 - f 0) / p`.

mathlib-triage Bot unassigned ADedecker Sep 14, 2026

extract lemmas and golf

9e2c3ee

style: wrap long line

14d04a8

mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Sep 23, 2026

Merge branch 'master' into feat/circle-pi1

ed5019c

mathlib-bors Bot added the ready-to-merge This PR has been sent to bors. label Sep 29, 2026

mathlib-triage Bot removed the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Sep 29, 2026

mathlib-bors Bot added the bors-staging This PR is currently being built by bors on the staging branch. label Sep 29, 2026

mathlib-bors Bot removed the bors-staging This PR is currently being built by bors on the staging branch. label Sep 29, 2026

mathlib-bors Bot added the bors-staging This PR is currently being built by bors on the staging branch. label Sep 29, 2026

mathlib-bors Bot changed the title ~~feat(Topology/Covering): fundamental group of the circle is ℤ~~ [Merged by Bors] - feat(Topology/Covering): fundamental group of the circle is ℤ Sep 29, 2026

mathlib-bors Bot closed this Sep 29, 2026

Conversation

Ruizsolveall commented Jul 17, 2026

Uh oh!

github-actions Bot commented Jul 17, 2026

Welcome new contributor!

Uh oh!

github-actions Bot commented Jul 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary ed5019cef3

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

mathlib-merge-conflicts Bot commented Aug 28, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

alreadydone commented Sep 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Ruizsolveall commented Sep 21, 2026

Uh oh!

alreadydone commented Sep 23, 2026

Uh oh!

github-actions Bot commented Sep 23, 2026

Uh oh!

ocfnash commented Sep 29, 2026

Uh oh!

mathlib-bors Bot commented Sep 29, 2026

Uh oh!

mathlib-bors Bot commented Sep 29, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

github-actions Bot commented Jul 17, 2026 •

edited

Loading

alreadydone commented Sep 20, 2026 •

edited

Loading