From 42e38556eeeae273d4ab2d180fbfd3257aa9772d Mon Sep 17 00:00:00 2001 From: Ruizsolveall Date: Fri, 17 Jul 2026 10:07:00 +0100 Subject: [PATCH 1/8] =?UTF-8?q?feat(Topology/Covering):=20fundamental=20gr?= =?UTF-8?q?oup=20of=20the=20circle=20is=20=E2=84=A4?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../Covering/FundamentalGroupCircle.lean | 101 ++++++++++++++++++ 1 file changed, 101 insertions(+) create mode 100644 Mathlib/Topology/Covering/FundamentalGroupCircle.lean diff --git a/Mathlib/Topology/Covering/FundamentalGroupCircle.lean b/Mathlib/Topology/Covering/FundamentalGroupCircle.lean new file mode 100644 index 00000000000000..1e6d6f248c6957 --- /dev/null +++ b/Mathlib/Topology/Covering/FundamentalGroupCircle.lean @@ -0,0 +1,101 @@ +/- +Copyright (c) 2025 Ruize Chen. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Ruize Chen +-/ +module + +public import Mathlib.Topology.Covering.AddCircle +public import Mathlib.Topology.Homotopy.Lifting +public import Mathlib.Topology.Instances.ZMultiples +public import Mathlib.Analysis.Convex.Contractible +public import Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected +public import Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup + +/-! +# The fundamental group of the circle +-/ + +public section + +open unitInterval + +theorem IsCoveringMap.coe_monodromy_mk {E X : Type*} [TopologicalSpace E] [TopologicalSpace X] + {p : E → X} (cov : IsCoveringMap p) {x y : X} (γ : Path x y) (e : p ⁻¹' {x}) : + (cov.monodromy (.mk γ) e : E) = + cov.liftPath γ.toContinuousMap e (γ.source.trans e.2.symm) 1 := + rfl + +namespace AddCircle + +/-- The loop in `AddCircle 1` that winds `n` times, defined as `t ↦ n • t`. -/ +def zsmulLoop (n : ℤ) : Path (0 : AddCircle (1 : ℝ)) 0 where + toFun t := n • t + source' := by simp + target' := by simp [coe_period] + continuous_toFun := (continuous_zsmul n).comp + (continuous_quotient_mk'.comp continuous_subtype_val) + +lemma liftPath_zsmulLoop (n : ℤ) (t : I) : + (isCoveringMap_coe 1).liftPath (zsmulLoop n).toContinuousMap 0 (by simp) t = (n : ℝ) * t := by + have h : (⟨fun t : I ↦ (n : ℝ) * t, by fun_prop⟩ : C(I, ℝ)) = + (isCoveringMap_coe 1).liftPath (zsmulLoop n).toContinuousMap 0 (by simp) := by + rw [IsCoveringMap.eq_liftPath_iff'] + refine ⟨funext fun t ↦ ?_, by simp⟩ + simp only [Function.comp_apply, ContinuousMap.coe_mk, zsmulLoop, ← zsmul_eq_mul, coe_zsmul] + exact (DFunLike.congr_fun h t).symm + +lemma monodromy_zsmulLoop (n : ℤ) : + (((isCoveringMap_coe (1 : ℝ)).monodromy (.mk (zsmulLoop n)) ⟨0, by simp⟩ : _) : ℝ) = n := by + simp [IsCoveringMap.coe_monodromy_mk, liftPath_zsmulLoop] + +/-- The isomorphism between the subgroup of integer multiples of `1 : ℝ` and `ℤ`, +sending `m • (1 : ℝ)` to `m`. -/ +noncomputable def zmultiplesOneEquivInt : AddSubgroup.zmultiples (1 : ℝ) ≃+ ℤ := + (AddEquiv.addSubgroupCongr (AddSubgroup.range_zmultiplesHom (1 : ℝ)).symm).trans + (AddMonoidHom.ofInjective (f := zmultiplesHom ℝ (1 : ℝ)) + (smul_left_injective ℤ one_ne_zero)).symm + +@[simp] +lemma coe_zmultiplesOneEquivInt_symm (m : ℤ) : + ((zmultiplesOneEquivInt.symm m : AddSubgroup.zmultiples (1 : ℝ)) : ℝ) = m := by + simp only [zmultiplesOneEquivInt, AddEquiv.symm_trans_apply, AddEquiv.symm_symm, + AddEquiv.addSubgroupCongr_symm_apply] + exact (AddMonoidHom.ofInjective_apply _).trans (by simp) + +lemma zmultiplesOneEquivInt_apply_intCast (m : ℤ) + (h : (m : ℝ) ∈ AddSubgroup.zmultiples (1 : ℝ)) : + zmultiplesOneEquivInt ⟨(m : ℝ), h⟩ = m := + zmultiplesOneEquivInt.apply_eq_iff_eq_symm_apply.mpr <| + Subtype.ext (coe_zmultiplesOneEquivInt_symm m).symm + +/-- **The fundamental group of the circle is `ℤ`**: the isomorphism sends the class of the loop +winding `n` times around the circle to `n` -/ +noncomputable def windingNumberIso : + FundamentalGroup (AddCircle (1 : ℝ)) 0 ≃* Multiplicative ℤ := + ((isAddQuotientCoveringMap_coe (1 : ℝ)).fundamentalGroupEquiv (x := 0) ⟨0, by simp⟩).trans <| + MulOpposite.opMulEquiv.symm.trans zmultiplesOneEquivInt.toMultiplicative + +theorem windingNumberIso_zsmulLoop (n : ℤ) : + windingNumberIso (FundamentalGroup.fromPath (.mk (zsmulLoop n))) = + Multiplicative.ofAdd n := by + have h : (isAddQuotientCoveringMap_coe (1 : ℝ)).fundamentalGroupEquiv (x := 0) ⟨0, by simp⟩ + (FundamentalGroup.fromPath (.mk (zsmulLoop n))) = + MulOpposite.op (Multiplicative.ofAdd + (⟨(n : ℝ), ⟨n, by simp⟩⟩ : AddSubgroup.zmultiples (1 : ℝ))) := + (IsAddQuotientCoveringMap.fundamentalGroupToMulOpposite_apply_eq_Iff + (isAddQuotientCoveringMap_coe (1 : ℝ))).mpr <| by + simp [monodromy_zsmulLoop, AddSubgroup.vadd_def, vadd_eq_add] + simp only [windingNumberIso, MulEquiv.trans_apply, h, MulOpposite.coe_symm_opMulEquiv, + MulOpposite.unop_op] + exact congrArg Multiplicative.ofAdd (zmultiplesOneEquivInt_apply_intCast n ⟨n, by simp⟩) + +/-- The winding number of a loop in the circle, defined as its image under `windingNumberIso`. -/ +noncomputable def windingNumber (γ : FundamentalGroup (AddCircle (1 : ℝ)) 0) : ℤ := + Multiplicative.toAdd (windingNumberIso γ) + +lemma windingNumber_zsmulLoop (n : ℤ) : + windingNumber (FundamentalGroup.fromPath (.mk (zsmulLoop n))) = n := + congrArg Multiplicative.toAdd (windingNumberIso_zsmulLoop n) + +end AddCircle From ed2aa20d5388eabc43b16c604b13d991fd1b191a Mon Sep 17 00:00:00 2001 From: Ruizsolveall Date: Fri, 17 Jul 2026 12:05:54 +0100 Subject: [PATCH 2/8] run mk_all --- Mathlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib.lean b/Mathlib.lean index c1d24ccd4a4ae3..25dc66bccf4de6 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -7900,6 +7900,7 @@ public import Mathlib.Topology.Convenient.Localization public import Mathlib.Topology.Convenient.OpenClosed public import Mathlib.Topology.Covering.AddCircle public import Mathlib.Topology.Covering.Basic +public import Mathlib.Topology.Covering.FundamentalGroupCircle public import Mathlib.Topology.Covering.Quotient public import Mathlib.Topology.Defs.Basic public import Mathlib.Topology.Defs.Filter From 4a1f4b8bf1a32dd2734cd68d01db22f2af31bc62 Mon Sep 17 00:00:00 2001 From: Ruizsolveall Date: Thu, 3 Sep 2026 17:30:36 +0100 Subject: [PATCH 3/8] chore: replace deprecated Equiv.apply_eq_iff_eq_symm_apply --- Mathlib/Topology/Covering/FundamentalGroupCircle.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/Covering/FundamentalGroupCircle.lean b/Mathlib/Topology/Covering/FundamentalGroupCircle.lean index 1e6d6f248c6957..894e1686b167e7 100644 --- a/Mathlib/Topology/Covering/FundamentalGroupCircle.lean +++ b/Mathlib/Topology/Covering/FundamentalGroupCircle.lean @@ -66,7 +66,7 @@ lemma coe_zmultiplesOneEquivInt_symm (m : ℤ) : lemma zmultiplesOneEquivInt_apply_intCast (m : ℤ) (h : (m : ℝ) ∈ AddSubgroup.zmultiples (1 : ℝ)) : zmultiplesOneEquivInt ⟨(m : ℝ), h⟩ = m := - zmultiplesOneEquivInt.apply_eq_iff_eq_symm_apply.mpr <| + zmultiplesOneEquivInt.eq_symm_apply.mp <| Subtype.ext (coe_zmultiplesOneEquivInt_symm m).symm /-- **The fundamental group of the circle is `ℤ`**: the isomorphism sends the class of the loop From 4dd080371d37db69fc3a122688d20b8033daac97 Mon Sep 17 00:00:00 2001 From: Ruizsolveall Date: Mon, 7 Sep 2026 13:59:31 +0100 Subject: [PATCH 4/8] feat: zmultiplesEquivInt and basepoint independence of fundamentalGroupEquiv MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- .../Group/Subgroup/ZPowers/Lemmas.lean | 27 ++++++++++ Mathlib/Topology/Homotopy/Lifting.lean | 54 +++++++++++++++++++ 2 files changed, 81 insertions(+) diff --git a/Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean b/Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean index 9086a7f8d6c3c1..b380a299b9e313 100644 --- a/Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean +++ b/Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean @@ -44,12 +44,39 @@ theorem finsetSup_zpowers (s : Finset G) : s.sup zpowers = closure s := by end Subgroup +theorem zmultiplesHom_injective [IsAddTorsionFree A] {a : A} (ha : a ≠ 0) : + Function.Injective (zmultiplesHom A a) := + (injective_iff_map_eq_zero _).2 fun _ hn ↦ (IsAddTorsionFree.zsmul_eq_zero_iff_left ha).1 hn + namespace AddSubgroup @[simp] theorem range_zmultiplesHom (a : A) : (zmultiplesHom A a).range = zmultiples a := rfl +section IsAddTorsionFree + +variable [IsAddTorsionFree A] {a : A} + +/-- The subgroup generated by a non-torsion element `a` is isomorphic to `ℤ`, sending `n • a` +to `n`. -/ +noncomputable def zmultiplesEquivInt (ha : a ≠ 0) : zmultiples a ≃+ ℤ := + ((AddMonoidHom.ofInjective (zmultiplesHom_injective ha)).trans + (AddEquiv.addSubgroupCongr (range_zmultiplesHom a))).symm + +@[simp] +theorem coe_zmultiplesEquivInt_symm_apply (ha : a ≠ 0) (n : ℤ) : + ((zmultiplesEquivInt ha).symm n : A) = n • a := by + simp only [zmultiplesEquivInt, AddEquiv.symm_symm, AddEquiv.trans_apply, + AddEquiv.addSubgroupCongr_apply, AddMonoidHom.ofInjective_apply, zmultiplesHom_apply] + +@[simp] +theorem zmultiplesEquivInt_apply_zsmul (ha : a ≠ 0) (n : ℤ) : + zmultiplesEquivInt ha ⟨n • a, zsmul_mem_zmultiples a n⟩ = n := + (zmultiplesEquivInt ha).eq_symm_apply.mp (Subtype.ext (by simp)) + +end IsAddTorsionFree + section Ring variable {R : Type*} [Ring R] (r : R) (k : ℤ) diff --git a/Mathlib/Topology/Homotopy/Lifting.lean b/Mathlib/Topology/Homotopy/Lifting.lean index f5a47dfa109fb3..35d859308d6ac2 100644 --- a/Mathlib/Topology/Homotopy/Lifting.lean +++ b/Mathlib/Topology/Homotopy/Lifting.lean @@ -392,6 +392,10 @@ def monodromy {x y : X} (γ : Path.Homotopic.Quotient x y) : congr($(cov.liftPath_lifts ..) 1).trans γ.target⟩) fun _ _ h ↦ Subtype.ext (cov.liftPath_apply_one_eq_of_homotopicRel h ..) +theorem coe_monodromy_mk {x y : X} (γ : Path x y) (e : p ⁻¹' {x}) : + (cov.monodromy (.mk γ) e : E) = cov.liftPath γ e (γ.source.trans e.2.symm) 1 := + rfl + /-- Lift a homotopy class of paths to a covering space. -/ def liftPathQuotient {x y : X} (γ : Path.Homotopic.Quotient x y) (e : p ⁻¹' {x}) : Path.Homotopic.Quotient e.1 (cov.monodromy γ e) := @@ -652,6 +656,25 @@ theorem unop_fundamentalGroupToMulOpposite_smul : (hp.fundamentalGroupToMulOpposite e γ).unop • e.1 = hp.isCoveringMap.monodromy γ e := by simp [fundamentalGroupToMulOpposite, fiberEquivGroup_smul_self] +variable {e} in +/-- Moving the basepoint `e` in the fiber by `g` conjugates `fundamentalGroupToMulOpposite` +by `g`. -/ +theorem fundamentalGroupToMulOpposite_toPermFiber : + hp.fundamentalGroupToMulOpposite (hp.toPermFiber x g e) γ = + MulOpposite.op (g * (hp.fundamentalGroupToMulOpposite e γ).unop * g⁻¹) := by + rw [fundamentalGroupToMulOpposite_apply_eq_Iff, hp.monodromy_toPermFiber] + simp only [MulOpposite.unop_op, toPermFiber_apply_apply_coe, + ← hp.unop_fundamentalGroupToMulOpposite_smul, mul_smul, inv_smul_smul] + +/-- If `G` is commutative, `fundamentalGroupToMulOpposite` does not depend on the choice of the +basepoint `e` in the fiber. -/ +theorem fundamentalGroupToMulOpposite_eq [IsMulCommutative G] (e' : p ⁻¹' {x}) : + hp.fundamentalGroupToMulOpposite e = hp.fundamentalGroupToMulOpposite e' := by + obtain ⟨g, rfl⟩ := hp.exists_toPermFiber_eq e e' + ext γ + rw [fundamentalGroupToMulOpposite_toPermFiber, mul_comm' g, mul_inv_cancel_right, + MulOpposite.op_unop] + variable {e} in theorem fundamentalGroupToMulOpposite_eq_one_iff : hp.fundamentalGroupToMulOpposite e γ = 1 ↔ hp.isCoveringMap.monodromy γ e = e where @@ -693,6 +716,12 @@ def fundamentalGroupEquiv [SimplyConnectedSpace E] : ⟨hp.fundamentalGroupToMulOpposite_injective e, hp.fundamentalGroupToMulOpposite_surjective e⟩ +/-- If `G` is commutative, `fundamentalGroupEquiv` does not depend on the choice of the +basepoint `e` in the fiber. -/ +theorem fundamentalGroupEquiv_eq [SimplyConnectedSpace E] [IsMulCommutative G] (e' : p ⁻¹' {x}) : + hp.fundamentalGroupEquiv e = hp.fundamentalGroupEquiv e' := + MulEquiv.ext fun γ ↦ congr($(hp.fundamentalGroupToMulOpposite_eq e e') γ) + end IsQuotientCoveringMap namespace IsAddQuotientCoveringMap @@ -750,6 +779,23 @@ theorem unop_fundamentalGroupToMulOpposite_smul : (hp.fundamentalGroupToMulOpposite e γ).unop • e.1 = hp.isCoveringMap.monodromy γ e := hp.toMultiplicative.unop_fundamentalGroupToMulOpposite_smul +variable {e} in +/-- Moving the basepoint `e` in the fiber by `g` conjugates `fundamentalGroupToMulOpposite` +by `g`. -/ +theorem fundamentalGroupToMulOpposite_toPermFiber : + hp.fundamentalGroupToMulOpposite (hp.toMultiplicative.toPermFiber x g e) γ = + MulOpposite.op (Multiplicative.ofAdd g * (hp.fundamentalGroupToMulOpposite e γ).unop * + (Multiplicative.ofAdd g)⁻¹) := + hp.toMultiplicative.fundamentalGroupToMulOpposite_toPermFiber + +/-- If `G` is commutative, `fundamentalGroupToMulOpposite` does not depend on the choice of the +basepoint `e` in the fiber. -/ +theorem fundamentalGroupToMulOpposite_eq [IsAddCommutative G] (e' : p ⁻¹' {x}) : + hp.fundamentalGroupToMulOpposite e = hp.fundamentalGroupToMulOpposite e' := + haveI : IsMulCommutative (Multiplicative G) := + ⟨⟨fun a b ↦ add_comm' (Multiplicative.toAdd a) (Multiplicative.toAdd b)⟩⟩ + hp.toMultiplicative.fundamentalGroupToMulOpposite_eq e e' + variable {e} in theorem fundamentalGroupToMulOpposite_eq_one_iff : hp.fundamentalGroupToMulOpposite e γ = 1 ↔ hp.isCoveringMap.monodromy γ e = e := @@ -773,4 +819,12 @@ def fundamentalGroupEquiv [SimplyConnectedSpace E] : FundamentalGroup X x ≃* (Multiplicative G)ᵐᵒᵖ := hp.toMultiplicative.fundamentalGroupEquiv e +/-- If `G` is commutative, `fundamentalGroupEquiv` does not depend on the choice of the +basepoint `e` in the fiber. -/ +theorem fundamentalGroupEquiv_eq [SimplyConnectedSpace E] [IsAddCommutative G] (e' : p ⁻¹' {x}) : + hp.fundamentalGroupEquiv e = hp.fundamentalGroupEquiv e' := + haveI : IsMulCommutative (Multiplicative G) := + ⟨⟨fun a b ↦ add_comm' (Multiplicative.toAdd a) (Multiplicative.toAdd b)⟩⟩ + hp.toMultiplicative.fundamentalGroupEquiv_eq e e' + end IsAddQuotientCoveringMap From 7faa4df5c1b5f8f6c0ded74c405ca24c0f033320 Mon Sep 17 00:00:00 2001 From: Ruizsolveall Date: Mon, 7 Sep 2026 13:59:31 +0100 Subject: [PATCH 5/8] refactor: generalize to AddCircle p at an arbitrary basepoint MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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`. --- .../Covering/FundamentalGroupCircle.lean | 131 ++++++++---------- 1 file changed, 60 insertions(+), 71 deletions(-) diff --git a/Mathlib/Topology/Covering/FundamentalGroupCircle.lean b/Mathlib/Topology/Covering/FundamentalGroupCircle.lean index 894e1686b167e7..9835364ac73bad 100644 --- a/Mathlib/Topology/Covering/FundamentalGroupCircle.lean +++ b/Mathlib/Topology/Covering/FundamentalGroupCircle.lean @@ -14,88 +14,77 @@ public import Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup /-! # The fundamental group of the circle + +For `0 < p`, the fundamental group of `AddCircle p` at any basepoint is isomorphic to `ℤ` +(`AddCircle.windingNumberIso`). The winding number of a loop is `(f 1 - f 0) / p` for any +continuous lift `f : I → ℝ` of the loop (`AddCircle.windingNumber_eq_div`); in particular the +loop `t ↦ n • (t * p) + x` has winding number `n` (`AddCircle.windingNumber_zsmulLoop`). -/ public section open unitInterval -theorem IsCoveringMap.coe_monodromy_mk {E X : Type*} [TopologicalSpace E] [TopologicalSpace X] - {p : E → X} (cov : IsCoveringMap p) {x y : X} (γ : Path x y) (e : p ⁻¹' {x}) : - (cov.monodromy (.mk γ) e : E) = - cov.liftPath γ.toContinuousMap e (γ.source.trans e.2.symm) 1 := - rfl - namespace AddCircle -/-- The loop in `AddCircle 1` that winds `n` times, defined as `t ↦ n • t`. -/ -def zsmulLoop (n : ℤ) : Path (0 : AddCircle (1 : ℝ)) 0 where - toFun t := n • t +variable (p : ℝ) + +/-- The loop in `AddCircle p` based at `x` that winds `n` times, defined as +`t ↦ n • (t * p) + x`. -/ +def zsmulLoop (x : ℝ) (n : ℤ) : Path (x : AddCircle p) x where + toFun t := ((n • ((t : ℝ) * p) + x : ℝ) : AddCircle p) source' := by simp target' := by simp [coe_period] - continuous_toFun := (continuous_zsmul n).comp - (continuous_quotient_mk'.comp continuous_subtype_val) - -lemma liftPath_zsmulLoop (n : ℤ) (t : I) : - (isCoveringMap_coe 1).liftPath (zsmulLoop n).toContinuousMap 0 (by simp) t = (n : ℝ) * t := by - have h : (⟨fun t : I ↦ (n : ℝ) * t, by fun_prop⟩ : C(I, ℝ)) = - (isCoveringMap_coe 1).liftPath (zsmulLoop n).toContinuousMap 0 (by simp) := by - rw [IsCoveringMap.eq_liftPath_iff'] - refine ⟨funext fun t ↦ ?_, by simp⟩ - simp only [Function.comp_apply, ContinuousMap.coe_mk, zsmulLoop, ← zsmul_eq_mul, coe_zsmul] - exact (DFunLike.congr_fun h t).symm - -lemma monodromy_zsmulLoop (n : ℤ) : - (((isCoveringMap_coe (1 : ℝ)).monodromy (.mk (zsmulLoop n)) ⟨0, by simp⟩ : _) : ℝ) = n := by - simp [IsCoveringMap.coe_monodromy_mk, liftPath_zsmulLoop] - -/-- The isomorphism between the subgroup of integer multiples of `1 : ℝ` and `ℤ`, -sending `m • (1 : ℝ)` to `m`. -/ -noncomputable def zmultiplesOneEquivInt : AddSubgroup.zmultiples (1 : ℝ) ≃+ ℤ := - (AddEquiv.addSubgroupCongr (AddSubgroup.range_zmultiplesHom (1 : ℝ)).symm).trans - (AddMonoidHom.ofInjective (f := zmultiplesHom ℝ (1 : ℝ)) - (smul_left_injective ℤ one_ne_zero)).symm - -@[simp] -lemma coe_zmultiplesOneEquivInt_symm (m : ℤ) : - ((zmultiplesOneEquivInt.symm m : AddSubgroup.zmultiples (1 : ℝ)) : ℝ) = m := by - simp only [zmultiplesOneEquivInt, AddEquiv.symm_trans_apply, AddEquiv.symm_symm, - AddEquiv.addSubgroupCongr_symm_apply] - exact (AddMonoidHom.ofInjective_apply _).trans (by simp) - -lemma zmultiplesOneEquivInt_apply_intCast (m : ℤ) - (h : (m : ℝ) ∈ AddSubgroup.zmultiples (1 : ℝ)) : - zmultiplesOneEquivInt ⟨(m : ℝ), h⟩ = m := - zmultiplesOneEquivInt.eq_symm_apply.mp <| - Subtype.ext (coe_zmultiplesOneEquivInt_symm m).symm - -/-- **The fundamental group of the circle is `ℤ`**: the isomorphism sends the class of the loop -winding `n` times around the circle to `n` -/ -noncomputable def windingNumberIso : - FundamentalGroup (AddCircle (1 : ℝ)) 0 ≃* Multiplicative ℤ := - ((isAddQuotientCoveringMap_coe (1 : ℝ)).fundamentalGroupEquiv (x := 0) ⟨0, by simp⟩).trans <| - MulOpposite.opMulEquiv.symm.trans zmultiplesOneEquivInt.toMultiplicative - -theorem windingNumberIso_zsmulLoop (n : ℤ) : - windingNumberIso (FundamentalGroup.fromPath (.mk (zsmulLoop n))) = - Multiplicative.ofAdd n := by - have h : (isAddQuotientCoveringMap_coe (1 : ℝ)).fundamentalGroupEquiv (x := 0) ⟨0, by simp⟩ - (FundamentalGroup.fromPath (.mk (zsmulLoop n))) = + continuous_toFun := by fun_prop + +variable {p} [hp : Fact (0 < p)] + +/-- **The fundamental group of the circle is `ℤ`**: the isomorphism sends the class of a loop to +its winding number (`windingNumber_eq_div`). It does not depend on the choice of a lift of the +basepoint (`IsAddQuotientCoveringMap.fundamentalGroupEquiv_eq`). -/ +noncomputable def windingNumberIso (x : AddCircle p) : + FundamentalGroup (AddCircle p) x ≃* Multiplicative ℤ := + ((isAddQuotientCoveringMap_coe p).fundamentalGroupEquiv (x := x) + ⟨(equivIco p 0 x : ℝ), coe_equivIco⟩).trans <| + MulOpposite.opMulEquiv.symm.trans (AddSubgroup.zmultiplesEquivInt hp.out.ne').toMultiplicative + +/-- The winding number of a loop in `AddCircle p`, defined as its image under `windingNumberIso`. -/ +noncomputable def windingNumber {x : AddCircle p} (γ : FundamentalGroup (AddCircle p) x) : ℤ := + Multiplicative.toAdd (windingNumberIso x γ) + +/-- The winding number of a loop in `AddCircle p` is `(f 1 - f 0) / p`, for any continuous lift +`f` of the loop to `ℝ`. -/ +theorem windingNumber_eq_div {x : AddCircle p} (γ : Path x x) (f : C(I, ℝ)) + (hf : ∀ t, (f t : AddCircle p) = γ t) : + (windingNumber (FundamentalGroup.fromPath (.mk γ)) : ℝ) = (f 1 - f 0) / p := by + have h0 : ((f 0 : ℝ) : AddCircle p) = x := (hf 0).trans γ.source + obtain ⟨n, hn⟩ : ∃ n : ℤ, n • p = f 1 - f 0 := + AddSubgroup.mem_zmultiples_iff.mp <| QuotientAddGroup.eq_iff_sub_mem.mp <| + (hf 1).trans <| γ.target.trans h0.symm + have hlift : (isCoveringMap_coe p).liftPath γ (f 0) (γ.source.trans h0.symm) = f := + (((isCoveringMap_coe p).eq_liftPath_iff' _).mpr ⟨funext hf, rfl⟩).symm + have hmono : ((isCoveringMap_coe p).monodromy (.mk γ) ⟨f 0, h0⟩ : ℝ) = f 1 := by + rw [IsCoveringMap.coe_monodromy_mk, hlift] + have h : (isAddQuotientCoveringMap_coe p).fundamentalGroupEquiv (x := x) ⟨f 0, h0⟩ + (FundamentalGroup.fromPath (.mk γ)) = MulOpposite.op (Multiplicative.ofAdd - (⟨(n : ℝ), ⟨n, by simp⟩⟩ : AddSubgroup.zmultiples (1 : ℝ))) := + (⟨n • p, AddSubgroup.zsmul_mem_zmultiples p n⟩ : AddSubgroup.zmultiples p)) := (IsAddQuotientCoveringMap.fundamentalGroupToMulOpposite_apply_eq_Iff - (isAddQuotientCoveringMap_coe (1 : ℝ))).mpr <| by - simp [monodromy_zsmulLoop, AddSubgroup.vadd_def, vadd_eq_add] - simp only [windingNumberIso, MulEquiv.trans_apply, h, MulOpposite.coe_symm_opMulEquiv, - MulOpposite.unop_op] - exact congrArg Multiplicative.ofAdd (zmultiplesOneEquivInt_apply_intCast n ⟨n, by simp⟩) - -/-- The winding number of a loop in the circle, defined as its image under `windingNumberIso`. -/ -noncomputable def windingNumber (γ : FundamentalGroup (AddCircle (1 : ℝ)) 0) : ℤ := - Multiplicative.toAdd (windingNumberIso γ) - -lemma windingNumber_zsmulLoop (n : ℤ) : - windingNumber (FundamentalGroup.fromPath (.mk (zsmulLoop n))) = n := - congrArg Multiplicative.toAdd (windingNumberIso_zsmulLoop n) + (isAddQuotientCoveringMap_coe p)).mpr <| by + simp [hmono, AddSubgroup.vadd_def, vadd_eq_add, hn] + have hw : windingNumber (FundamentalGroup.fromPath (.mk γ)) = n := by + simp only [windingNumber, windingNumberIso] + rw [(isAddQuotientCoveringMap_coe p).fundamentalGroupEquiv_eq _ ⟨f 0, h0⟩] + simp only [MulEquiv.trans_apply, h, MulOpposite.coe_symm_opMulEquiv, MulOpposite.unop_op] + exact AddSubgroup.zmultiplesEquivInt_apply_zsmul hp.out.ne' n + rw [hw, eq_div_iff hp.out.ne', ← zsmul_eq_mul, hn] + +/-- The loop `t ↦ n • (t * p) + x` has winding number `n`. -/ +theorem windingNumber_zsmulLoop (x : ℝ) (n : ℤ) : + windingNumber (FundamentalGroup.fromPath (.mk (zsmulLoop p x n))) = n := by + refine Int.cast_injective (α := ℝ) ?_ + rw [windingNumber_eq_div (zsmulLoop p x n) ⟨fun t ↦ n • ((t : ℝ) * p) + x, by fun_prop⟩ + fun _ ↦ rfl] + simp [hp.out.ne'] end AddCircle From 0af7ea56c4c8b126f06b6ee85bf37b2e80225584 Mon Sep 17 00:00:00 2001 From: Ruizsolveall Date: Mon, 7 Sep 2026 14:20:37 +0100 Subject: [PATCH 6/8] refactor: transport IsMulCommutative across type tags; move zmultiplesHom_injective MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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`. --- .../Group/Subgroup/ZPowers/Lemmas.lean | 8 ++--- Mathlib/Algebra/Group/TypeTags/Basic.lean | 6 ++++ Mathlib/Data/Int/Cast/Lemmas.lean | 5 +++ .../Covering/FundamentalGroupCircle.lean | 32 ++++++++++--------- Mathlib/Topology/Homotopy/Lifting.lean | 4 --- 5 files changed, 30 insertions(+), 25 deletions(-) diff --git a/Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean b/Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean index b380a299b9e313..813967eb8f71ed 100644 --- a/Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean +++ b/Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean @@ -44,10 +44,6 @@ theorem finsetSup_zpowers (s : Finset G) : s.sup zpowers = closure s := by end Subgroup -theorem zmultiplesHom_injective [IsAddTorsionFree A] {a : A} (ha : a ≠ 0) : - Function.Injective (zmultiplesHom A a) := - (injective_iff_map_eq_zero _).2 fun _ hn ↦ (IsAddTorsionFree.zsmul_eq_zero_iff_left ha).1 hn - namespace AddSubgroup @[simp] @@ -58,8 +54,8 @@ section IsAddTorsionFree variable [IsAddTorsionFree A] {a : A} -/-- The subgroup generated by a non-torsion element `a` is isomorphic to `ℤ`, sending `n • a` -to `n`. -/ +/-- The subgroup generated by a nonzero element `a` of a torsion-free additive group is isomorphic +to `ℤ`, sending `n • a` to `n`. -/ noncomputable def zmultiplesEquivInt (ha : a ≠ 0) : zmultiples a ≃+ ℤ := ((AddMonoidHom.ofInjective (zmultiplesHom_injective ha)).trans (AddEquiv.addSubgroupCongr (range_zmultiplesHom a))).symm diff --git a/Mathlib/Algebra/Group/TypeTags/Basic.lean b/Mathlib/Algebra/Group/TypeTags/Basic.lean index bc013a65d865c4..60010624de18f8 100644 --- a/Mathlib/Algebra/Group/TypeTags/Basic.lean +++ b/Mathlib/Algebra/Group/TypeTags/Basic.lean @@ -483,6 +483,12 @@ instance [Monoid α] [IsMulTorsionFree α] : IsAddTorsionFree (Additive α) wher instance [AddMonoid α] [IsAddTorsionFree α] : IsMulTorsionFree (Multiplicative α) where pow_left_injective _ := nsmul_right_injective (M := α) +instance [Mul α] [IsMulCommutative α] : IsAddCommutative (Additive α) where + is_comm := ⟨fun a b ↦ congrArg Additive.ofMul (mul_comm' a.toMul b.toMul)⟩ + +instance [Add α] [IsAddCommutative α] : IsMulCommutative (Multiplicative α) where + is_comm := ⟨fun a b ↦ congrArg Multiplicative.ofAdd (add_comm' a.toAdd b.toAdd)⟩ + /-- If `α` has some multiplicative structure and coerces to a function, then `Additive α` should also coerce to the same function. diff --git a/Mathlib/Data/Int/Cast/Lemmas.lean b/Mathlib/Data/Int/Cast/Lemmas.lean index e76e5b8ad63947..9b1d7b3e0dbe61 100644 --- a/Mathlib/Data/Int/Cast/Lemmas.lean +++ b/Mathlib/Data/Int/Cast/Lemmas.lean @@ -287,6 +287,11 @@ def zpowersHom : α ≃ (Multiplicative ℤ →* α) := @[simp] lemma zmultiplesHom_symm_apply (f : ℤ →+ β) : (zmultiplesHom β).symm f = f 1 := rfl +variable {β} in +lemma zmultiplesHom_injective [IsAddTorsionFree β] {x : β} (hx : x ≠ 0) : + Function.Injective (zmultiplesHom β x) := + (injective_iff_map_eq_zero _).2 fun _ hn ↦ (IsAddTorsionFree.zsmul_eq_zero_iff_left hx).1 hn + @[simp] lemma zpowersHom_apply (x : α) (n : Multiplicative ℤ) : zpowersHom α x n = x ^ n.toAdd := rfl diff --git a/Mathlib/Topology/Covering/FundamentalGroupCircle.lean b/Mathlib/Topology/Covering/FundamentalGroupCircle.lean index 9835364ac73bad..f81c8876d0a0b1 100644 --- a/Mathlib/Topology/Covering/FundamentalGroupCircle.lean +++ b/Mathlib/Topology/Covering/FundamentalGroupCircle.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2025 Ruize Chen. All rights reserved. +Copyright (c) 2026 Ruize Chen. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Ruize Chen -/ @@ -9,19 +9,18 @@ public import Mathlib.Topology.Covering.AddCircle public import Mathlib.Topology.Homotopy.Lifting public import Mathlib.Topology.Instances.ZMultiples public import Mathlib.Analysis.Convex.Contractible -public import Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected -public import Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup /-! # The fundamental group of the circle For `0 < p`, the fundamental group of `AddCircle p` at any basepoint is isomorphic to `ℤ` -(`AddCircle.windingNumberIso`). The winding number of a loop is `(f 1 - f 0) / p` for any -continuous lift `f : I → ℝ` of the loop (`AddCircle.windingNumber_eq_div`); in particular the -loop `t ↦ n • (t * p) + x` has winding number `n` (`AddCircle.windingNumber_zsmulLoop`). +(`AddCircle.windingNumberIso`). The winding number `AddCircle.windingNumber` of a loop is +`(f 1 - f 0) / p` for any continuous lift `f : I → ℝ` of the loop +(`AddCircle.windingNumber_eq_div`); in particular the loop `t ↦ n • (t * p) + x` has winding +number `n` (`AddCircle.windingNumber_zsmulLoop`). -/ -public section +@[expose] public section open unitInterval @@ -37,6 +36,11 @@ def zsmulLoop (x : ℝ) (n : ℤ) : Path (x : AddCircle p) x where target' := by simp [coe_period] continuous_toFun := by fun_prop +@[simp] +theorem zsmulLoop_apply (x : ℝ) (n : ℤ) (t : I) : + zsmulLoop p x n t = ((n • ((t : ℝ) * p) + x : ℝ) : AddCircle p) := + rfl + variable {p} [hp : Fact (0 < p)] /-- **The fundamental group of the circle is `ℤ`**: the isomorphism sends the class of a loop to @@ -50,7 +54,7 @@ noncomputable def windingNumberIso (x : AddCircle p) : /-- The winding number of a loop in `AddCircle p`, defined as its image under `windingNumberIso`. -/ noncomputable def windingNumber {x : AddCircle p} (γ : FundamentalGroup (AddCircle p) x) : ℤ := - Multiplicative.toAdd (windingNumberIso x γ) + (windingNumberIso x γ).toAdd /-- The winding number of a loop in `AddCircle p` is `(f 1 - f 0) / p`, for any continuous lift `f` of the loop to `ℝ`. -/ @@ -73,18 +77,16 @@ theorem windingNumber_eq_div {x : AddCircle p} (γ : Path x x) (f : C(I, ℝ)) (isAddQuotientCoveringMap_coe p)).mpr <| by simp [hmono, AddSubgroup.vadd_def, vadd_eq_add, hn] have hw : windingNumber (FundamentalGroup.fromPath (.mk γ)) = n := by - simp only [windingNumber, windingNumberIso] - rw [(isAddQuotientCoveringMap_coe p).fundamentalGroupEquiv_eq _ ⟨f 0, h0⟩] - simp only [MulEquiv.trans_apply, h, MulOpposite.coe_symm_opMulEquiv, MulOpposite.unop_op] + simp only [windingNumber, windingNumberIso, + (isAddQuotientCoveringMap_coe p).fundamentalGroupEquiv_eq _ ⟨f 0, h0⟩, + MulEquiv.trans_apply, h, MulOpposite.coe_symm_opMulEquiv, MulOpposite.unop_op] exact AddSubgroup.zmultiplesEquivInt_apply_zsmul hp.out.ne' n rw [hw, eq_div_iff hp.out.ne', ← zsmul_eq_mul, hn] /-- The loop `t ↦ n • (t * p) + x` has winding number `n`. -/ theorem windingNumber_zsmulLoop (x : ℝ) (n : ℤ) : windingNumber (FundamentalGroup.fromPath (.mk (zsmulLoop p x n))) = n := by - refine Int.cast_injective (α := ℝ) ?_ - rw [windingNumber_eq_div (zsmulLoop p x n) ⟨fun t ↦ n • ((t : ℝ) * p) + x, by fun_prop⟩ - fun _ ↦ rfl] - simp [hp.out.ne'] + simpa [hp.out.ne'] using windingNumber_eq_div (zsmulLoop p x n) + ⟨fun t ↦ n • ((t : ℝ) * p) + x, by fun_prop⟩ fun _ ↦ rfl end AddCircle diff --git a/Mathlib/Topology/Homotopy/Lifting.lean b/Mathlib/Topology/Homotopy/Lifting.lean index 35d859308d6ac2..f9bfc13205e004 100644 --- a/Mathlib/Topology/Homotopy/Lifting.lean +++ b/Mathlib/Topology/Homotopy/Lifting.lean @@ -792,8 +792,6 @@ theorem fundamentalGroupToMulOpposite_toPermFiber : basepoint `e` in the fiber. -/ theorem fundamentalGroupToMulOpposite_eq [IsAddCommutative G] (e' : p ⁻¹' {x}) : hp.fundamentalGroupToMulOpposite e = hp.fundamentalGroupToMulOpposite e' := - haveI : IsMulCommutative (Multiplicative G) := - ⟨⟨fun a b ↦ add_comm' (Multiplicative.toAdd a) (Multiplicative.toAdd b)⟩⟩ hp.toMultiplicative.fundamentalGroupToMulOpposite_eq e e' variable {e} in @@ -823,8 +821,6 @@ def fundamentalGroupEquiv [SimplyConnectedSpace E] : basepoint `e` in the fiber. -/ theorem fundamentalGroupEquiv_eq [SimplyConnectedSpace E] [IsAddCommutative G] (e' : p ⁻¹' {x}) : hp.fundamentalGroupEquiv e = hp.fundamentalGroupEquiv e' := - haveI : IsMulCommutative (Multiplicative G) := - ⟨⟨fun a b ↦ add_comm' (Multiplicative.toAdd a) (Multiplicative.toAdd b)⟩⟩ hp.toMultiplicative.fundamentalGroupEquiv_eq e e' end IsAddQuotientCoveringMap From 9e2c3eea65f0d37bd28f740a77a9750fa67b73fa Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Mon, 21 Sep 2026 01:41:17 +0800 Subject: [PATCH 7/8] extract lemmas and golf --- .../Covering/FundamentalGroupCircle.lean | 40 +++++++------------ Mathlib/Topology/Homotopy/Lifting.lean | 19 +++++++++ 2 files changed, 33 insertions(+), 26 deletions(-) diff --git a/Mathlib/Topology/Covering/FundamentalGroupCircle.lean b/Mathlib/Topology/Covering/FundamentalGroupCircle.lean index f81c8876d0a0b1..bef4ed2cbdecaa 100644 --- a/Mathlib/Topology/Covering/FundamentalGroupCircle.lean +++ b/Mathlib/Topology/Covering/FundamentalGroupCircle.lean @@ -31,14 +31,14 @@ variable (p : ℝ) /-- The loop in `AddCircle p` based at `x` that winds `n` times, defined as `t ↦ n • (t * p) + x`. -/ def zsmulLoop (x : ℝ) (n : ℤ) : Path (x : AddCircle p) x where - toFun t := ((n • ((t : ℝ) * p) + x : ℝ) : AddCircle p) + toFun t := n • (t * p : ℝ) + x source' := by simp target' := by simp [coe_period] continuous_toFun := by fun_prop @[simp] theorem zsmulLoop_apply (x : ℝ) (n : ℤ) (t : I) : - zsmulLoop p x n t = ((n • ((t : ℝ) * p) + x : ℝ) : AddCircle p) := + zsmulLoop p x n t = n • (t * p : ℝ) + x := rfl variable {p} [hp : Fact (0 < p)] @@ -58,35 +58,23 @@ noncomputable def windingNumber {x : AddCircle p} (γ : FundamentalGroup (AddCir /-- The winding number of a loop in `AddCircle p` is `(f 1 - f 0) / p`, for any continuous lift `f` of the loop to `ℝ`. -/ -theorem windingNumber_eq_div {x : AddCircle p} (γ : Path x x) (f : C(I, ℝ)) - (hf : ∀ t, (f t : AddCircle p) = γ t) : - (windingNumber (FundamentalGroup.fromPath (.mk γ)) : ℝ) = (f 1 - f 0) / p := by - have h0 : ((f 0 : ℝ) : AddCircle p) = x := (hf 0).trans γ.source +theorem windingNumber_eq_div {x : AddCircle p} (γ : Path x x) (f : C(I, ℝ)) (hf : (↑) ∘ f = γ) : + (windingNumber (.mk γ) : ℝ) = (f 1 - f 0) / p := by + have h0 : (f 0 : AddCircle p) = x := congr($hf 0).trans γ.source obtain ⟨n, hn⟩ : ∃ n : ℤ, n • p = f 1 - f 0 := AddSubgroup.mem_zmultiples_iff.mp <| QuotientAddGroup.eq_iff_sub_mem.mp <| - (hf 1).trans <| γ.target.trans h0.symm - have hlift : (isCoveringMap_coe p).liftPath γ (f 0) (γ.source.trans h0.symm) = f := - (((isCoveringMap_coe p).eq_liftPath_iff' _).mpr ⟨funext hf, rfl⟩).symm - have hmono : ((isCoveringMap_coe p).monodromy (.mk γ) ⟨f 0, h0⟩ : ℝ) = f 1 := by - rw [IsCoveringMap.coe_monodromy_mk, hlift] - have h : (isAddQuotientCoveringMap_coe p).fundamentalGroupEquiv (x := x) ⟨f 0, h0⟩ - (FundamentalGroup.fromPath (.mk γ)) = - MulOpposite.op (Multiplicative.ofAdd - (⟨n • p, AddSubgroup.zsmul_mem_zmultiples p n⟩ : AddSubgroup.zmultiples p)) := - (IsAddQuotientCoveringMap.fundamentalGroupToMulOpposite_apply_eq_Iff - (isAddQuotientCoveringMap_coe p)).mpr <| by - simp [hmono, AddSubgroup.vadd_def, vadd_eq_add, hn] - have hw : windingNumber (FundamentalGroup.fromPath (.mk γ)) = n := by - simp only [windingNumber, windingNumberIso, - (isAddQuotientCoveringMap_coe p).fundamentalGroupEquiv_eq _ ⟨f 0, h0⟩, - MulEquiv.trans_apply, h, MulOpposite.coe_symm_opMulEquiv, MulOpposite.unop_op] - exact AddSubgroup.zmultiplesEquivInt_apply_zsmul hp.out.ne' n - rw [hw, eq_div_iff hp.out.ne', ← zsmul_eq_mul, hn] + congr($hf 1).trans <| γ.target.trans h0.symm + have h : (isAddQuotientCoveringMap_coe p).fundamentalGroupEquiv (x := x) ⟨f 0, h0⟩ (.mk γ) = + .op (.ofAdd ⟨n • p, n, rfl⟩) := + (isAddQuotientCoveringMap_coe p).fundamentalGroupToMulOpposite_apply_mk_eq hf rfl (by simp [hn]) + simp [windingNumber, windingNumberIso, AddSubgroup.zmultiplesEquivInt_apply_zsmul hp.out.ne' n, + (isAddQuotientCoveringMap_coe p).fundamentalGroupEquiv_eq _ ⟨f 0, h0⟩, h, + eq_div_iff hp.out.ne', ← zsmul_eq_mul, ← hn] /-- The loop `t ↦ n • (t * p) + x` has winding number `n`. -/ theorem windingNumber_zsmulLoop (x : ℝ) (n : ℤ) : - windingNumber (FundamentalGroup.fromPath (.mk (zsmulLoop p x n))) = n := by + windingNumber (x := x) (.mk (zsmulLoop p x n)) = n := by simpa [hp.out.ne'] using windingNumber_eq_div (zsmulLoop p x n) - ⟨fun t ↦ n • ((t : ℝ) * p) + x, by fun_prop⟩ fun _ ↦ rfl + ⟨fun t ↦ n • (t * p) + x, by fun_prop⟩ rfl end AddCircle diff --git a/Mathlib/Topology/Homotopy/Lifting.lean b/Mathlib/Topology/Homotopy/Lifting.lean index f9bfc13205e004..8d960cda587d3a 100644 --- a/Mathlib/Topology/Homotopy/Lifting.lean +++ b/Mathlib/Topology/Homotopy/Lifting.lean @@ -396,6 +396,11 @@ theorem coe_monodromy_mk {x y : X} (γ : Path x y) (e : p ⁻¹' {x}) : (cov.monodromy (.mk γ) e : E) = cov.liftPath γ e (γ.source.trans e.2.symm) 1 := rfl +lemma monodromy_eq_apply_one {x y : X} {γ : Path x y} {e : p ⁻¹' {x}} {Γ : C(I, E)} + (hpΓ : p ∘ Γ = γ) (Γ_0 : Γ 0 = e) : cov.monodromy (.mk γ) e = Γ 1 := by + rw [show Γ = cov.liftPath γ e (γ.source.trans e.2.symm) from (eq_liftPath_iff' ..).mpr ⟨hpΓ, Γ_0⟩, + coe_monodromy_mk] + /-- Lift a homotopy class of paths to a covering space. -/ def liftPathQuotient {x y : X} (γ : Path.Homotopic.Quotient x y) (e : p ⁻¹' {x}) : Path.Homotopic.Quotient e.1 (cov.monodromy γ e) := @@ -651,6 +656,13 @@ theorem fundamentalGroupToMulOpposite_apply_eq_Iff {g : Gᵐᵒᵖ} : have := hp.isCancelSMul.right_cancel' aesop +variable {e} in +theorem fundamentalGroupToMulOpposite_apply_mk_eq {γ : Path x x} {g : G} {Γ : C(I, E)} + (hpΓ : p ∘ Γ = γ) (Γ_0 : Γ 0 = e) (Γ_1 : Γ 1 = g • e) : + hp.fundamentalGroupToMulOpposite e (.mk γ) = .op g := + hp.fundamentalGroupToMulOpposite_apply_eq_Iff.mpr <| by + simp [hp.isCoveringMap.monodromy_eq_apply_one hpΓ Γ_0, Γ_1] + variable {e} in theorem unop_fundamentalGroupToMulOpposite_smul : (hp.fundamentalGroupToMulOpposite e γ).unop • e.1 = hp.isCoveringMap.monodromy γ e := by @@ -774,6 +786,13 @@ theorem fundamentalGroupToMulOpposite_apply_eq_Iff {g : (Multiplicative G)ᵐᵒ hp.fundamentalGroupToMulOpposite e γ = g ↔ g.unop • e.1 = hp.isCoveringMap.monodromy γ e := hp.toMultiplicative.fundamentalGroupToMulOpposite_apply_eq_Iff +variable {e} in +theorem fundamentalGroupToMulOpposite_apply_mk_eq {γ : Path x x} {g : Multiplicative G} {Γ : C(I, E)} + (hpΓ : p ∘ Γ = γ) (Γ_0 : Γ 0 = e) (Γ_1 : Γ 1 = g • e) : + hp.fundamentalGroupToMulOpposite e (.mk γ) = .op g := + hp.fundamentalGroupToMulOpposite_apply_eq_Iff.mpr <| by + rw [hp.isCoveringMap.monodromy_eq_apply_one hpΓ Γ_0, Γ_1]; rfl + variable {e} in theorem unop_fundamentalGroupToMulOpposite_smul : (hp.fundamentalGroupToMulOpposite e γ).unop • e.1 = hp.isCoveringMap.monodromy γ e := From 14d04a8003625e01a57abd6697aaaca067820fab Mon Sep 17 00:00:00 2001 From: Ruizsolveall Date: Mon, 21 Sep 2026 11:31:07 +0100 Subject: [PATCH 8/8] style: wrap long line --- Mathlib/Topology/Homotopy/Lifting.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Topology/Homotopy/Lifting.lean b/Mathlib/Topology/Homotopy/Lifting.lean index 8d960cda587d3a..67d1e6c41dead7 100644 --- a/Mathlib/Topology/Homotopy/Lifting.lean +++ b/Mathlib/Topology/Homotopy/Lifting.lean @@ -787,8 +787,8 @@ theorem fundamentalGroupToMulOpposite_apply_eq_Iff {g : (Multiplicative G)ᵐᵒ hp.toMultiplicative.fundamentalGroupToMulOpposite_apply_eq_Iff variable {e} in -theorem fundamentalGroupToMulOpposite_apply_mk_eq {γ : Path x x} {g : Multiplicative G} {Γ : C(I, E)} - (hpΓ : p ∘ Γ = γ) (Γ_0 : Γ 0 = e) (Γ_1 : Γ 1 = g • e) : +theorem fundamentalGroupToMulOpposite_apply_mk_eq {γ : Path x x} {g : Multiplicative G} + {Γ : C(I, E)} (hpΓ : p ∘ Γ = γ) (Γ_0 : Γ 0 = e) (Γ_1 : Γ 1 = g • e) : hp.fundamentalGroupToMulOpposite e (.mk γ) = .op g := hp.fundamentalGroupToMulOpposite_apply_eq_Iff.mpr <| by rw [hp.isCoveringMap.monodromy_eq_apply_one hpΓ Γ_0, Γ_1]; rfl