Basepoint change for fundamental groups

The pointed classification of connected covers records a subgroup of the fundamental group at a chosen basepoint. Changing the basepoint along a path transports that subgroup by the standard path-conjugation isomorphism of fundamental groups. This file packages that transport and the induced transport of the normalizer quotient N(H) / H used for deck groups of covers attached to subgroups. It also descends basepoint change to conjugacy classes, where the result is independent of the chosen path.

It also records the element-level behaviour of the transport: path-quotient formulas and its compatibility with concatenation of paths.

Mathlib already supplies the fundamental-group isomorphism FundamentalGroup.fundamentalGroupMulEquivOfPath; the declarations here are the computation rules, subgroup, and normalizer-quotient bookkeeping built on it.

Main declarations

• FundamentalGroup.basepointChangeSubgroup: transport a subgroup of π₁(X, x₀) along a path γ : Path x₀ x₁.
• Domain-specific membership, inclusion, monotonicity, and normality lemmas for basepointChangeSubgroup.
• FundamentalGroup.basepointChangeNormalizerQuotientEquiv: the corresponding isomorphism N(H) / H ≃* N(γ₊H) / γ₊H.
• FundamentalGroup.fundamentalGroupMulEquivOfPath_apply and FundamentalGroup.fundamentalGroupMulEquivOfPath_symm_apply: basepoint change as conjugation by the path in the path quotient.
• FundamentalGroup.fundamentalGroupMulEquivOfPath_trans: basepoint change along a concatenated path is the composite of the basepoint changes.
• FundamentalGroup.fundamentalGroupMulEquivOfPath_eq_conj: basepoint change along a loop is conjugation by its class.
• FundamentalGroup.conjClassesEquivOfPath: the induced equivalence of conjugacy classes.
• FundamentalGroup.conjClassesEquivOfPath_eq: this equivalence is independent of the path.
• FundamentalGroup.conjClassesEquivOfPathConnected_trans: canonical conjugacy-class transport in a path-connected space is natural under further path transport.
• FundamentalGroup.mem_basepointChangeSubgroup and the representative [simp] lemmas for membership and quotient calculations under these domain-specific names.

@[simp]

theorem FundamentalGroup.fundamentalGroupMulEquivOfPath_symm_apply {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (γ : Path x₀ x₁) (g : FundamentalGroup X x₁) : (fundamentalGroupMulEquivOfPath γ).symm g = (Path.Homotopic.Quotient.mk γ).trans (Path.Homotopic.Quotient.trans g (Path.Homotopic.Quotient.mk γ).symm)

The inverse basepoint-change equivalence is represented by conjugation with the reverse path. This path-quotient formula is the interface for computations with the equivalence.

theorem FundamentalGroup.fundamentalGroupMulEquivOfPath_eq_conj {X : Type u_1} [TopologicalSpace X] {x : X} (γ : Path x x) : fundamentalGroupMulEquivOfPath γ = MulAut.conj (fromPath (Path.Homotopic.Quotient.mk γ))

Basepoint change along a loop is an inner automorphism. For a loop γ at x, changing basepoint along γ is conjugation by the class of γ in π₁(X, x). In particular it is invisible to any homomorphism from π₁(X, x) to a commutative group.

@[simp]

theorem FundamentalGroup.fundamentalGroupMulEquivOfPath_apply {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (γ : Path x₀ x₁) (g : FundamentalGroup X x₀) : (fundamentalGroupMulEquivOfPath γ) g = (Path.Homotopic.Quotient.mk γ).symm.trans (Path.Homotopic.Quotient.trans g (Path.Homotopic.Quotient.mk γ))

Basepoint change along γ is represented by conjugation with γ in the path quotient: a loop g at x₀ goes to the class of γ⁻¹ ⬝ g ⬝ γ. This is the forward counterpart of FundamentalGroup.fundamentalGroupMulEquivOfPath_symm_apply.

@[simp]

theorem FundamentalGroup.fundamentalGroupMulEquivOfPath_trans {X : Type u_1} [TopologicalSpace X] {x₀ x₁ x₂ : X} (γ : Path x₀ x₁) (δ : Path x₁ x₂) : fundamentalGroupMulEquivOfPath (γ.trans δ) = (fundamentalGroupMulEquivOfPath γ).trans (fundamentalGroupMulEquivOfPath δ)

Basepoint change along a concatenated path is basepoint change along each piece in turn.

@[simp]

theorem FundamentalGroup.fundamentalGroupMulEquivOfPath_symm {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (γ : Path x₀ x₁) : fundamentalGroupMulEquivOfPath γ.symm = (fundamentalGroupMulEquivOfPath γ).symm

Reversing a basepoint-change path gives the inverse equivalence of fundamental groups.

@[simp]

theorem FundamentalGroup.fundamentalGroupMulEquivOfPath_refl {X : Type u_1} [TopologicalSpace X] (x : X) : fundamentalGroupMulEquivOfPath (Path.refl x) = MulEquiv.refl (FundamentalGroup X x)

Basepoint change along the constant path is the identity equivalence.

noncomputable def FundamentalGroup.conjClassesEquivOfPath {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (γ : Path x₀ x₁) : ConjClasses (FundamentalGroup X x₀) ≃ ConjClasses (FundamentalGroup X x₁)

Changing basepoint along a path induces an equivalence between conjugacy classes in the two fundamental groups.

Equations

• FundamentalGroup.conjClassesEquivOfPath γ = (FundamentalGroup.fundamentalGroupMulEquivOfPath γ).conjClassesEquiv

@[simp]

theorem FundamentalGroup.conjClassesEquivOfPath_mk {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (γ : Path x₀ x₁) (g : FundamentalGroup X x₀) : (conjClassesEquivOfPath γ) (ConjClasses.mk g) = ConjClasses.mk ((fundamentalGroupMulEquivOfPath γ) g)

On a representative, transport of conjugacy classes is induced by the usual basepoint-change equivalence of fundamental groups.

@[simp]

theorem FundamentalGroup.conjClassesEquivOfPath_trans {X : Type u_1} [TopologicalSpace X] {x₀ x₁ x₂ : X} (γ : Path x₀ x₁) (δ : Path x₁ x₂) : conjClassesEquivOfPath (γ.trans δ) = (conjClassesEquivOfPath γ).trans (conjClassesEquivOfPath δ)

Transport of conjugacy classes along a concatenated path is transport along each piece in turn.

@[simp]

theorem FundamentalGroup.conjClassesEquivOfPath_symm {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (γ : Path x₀ x₁) : conjClassesEquivOfPath γ.symm = (conjClassesEquivOfPath γ).symm

Reversing a path gives the inverse equivalence on conjugacy classes.

@[simp]

theorem FundamentalGroup.conjClassesEquivOfPath_symm_mk {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (γ : Path x₀ x₁) (g : FundamentalGroup X x₁) : (conjClassesEquivOfPath γ).symm (ConjClasses.mk g) = ConjClasses.mk ((fundamentalGroupMulEquivOfPath γ).symm g)

Inverse transport of a conjugacy-class representative is induced by inverse basepoint change on the representative.

@[simp]

theorem FundamentalGroup.conjClassesEquivOfPath_refl {X : Type u_1} [TopologicalSpace X] (x : X) : conjClassesEquivOfPath (Path.refl x) = Equiv.refl (ConjClasses (FundamentalGroup X x))

Transport along the constant path is the identity on conjugacy classes.

theorem FundamentalGroup.conjClassesEquivOfPath_eq {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (γ δ : Path x₀ x₁) : conjClassesEquivOfPath γ = conjClassesEquivOfPath δ

Conjugacy-class basepoint change is independent of the path. Two paths with the same endpoints can change individual fundamental-group elements by an inner automorphism, but induce the same equivalence on conjugacy classes.

noncomputable def FundamentalGroup.conjClassesEquivOfPathConnected {X : Type u_1} [TopologicalSpace X] [PathConnectedSpace X] (x₀ x₁ : X) : ConjClasses (FundamentalGroup X x₀) ≃ ConjClasses (FundamentalGroup X x₁)

In a path-connected space, conjugacy classes of fundamental groups at two points are canonically equivalent: the result does not depend on the path chosen by the instance.

Equations

• FundamentalGroup.conjClassesEquivOfPathConnected x₀ x₁ = (FundamentalGroup.fundamentalGroupMulEquivOfPathConnected x₀ x₁).conjClassesEquiv

@[simp]

theorem FundamentalGroup.conjClassesEquivOfPathConnected_mk {X : Type u_1} [TopologicalSpace X] [PathConnectedSpace X] (x₀ x₁ : X) (g : FundamentalGroup X x₀) : (conjClassesEquivOfPathConnected x₀ x₁) (ConjClasses.mk g) = ConjClasses.mk ((fundamentalGroupMulEquivOfPathConnected x₀ x₁) g)

Canonical transport sends the conjugacy class of a representative to the class of its image under Mathlib's canonical basepoint-change equivalence.

theorem FundamentalGroup.conjClassesEquivOfPathConnected_eq {X : Type u_1} [TopologicalSpace X] [PathConnectedSpace X] {x₀ x₁ : X} (γ : Path x₀ x₁) : conjClassesEquivOfPathConnected x₀ x₁ = conjClassesEquivOfPath γ

The canonical equivalence of conjugacy classes in a path-connected space agrees with transport along any specified path.

@[simp]

theorem FundamentalGroup.conjClassesEquivOfPathConnected_self {X : Type u_1} [TopologicalSpace X] [PathConnectedSpace X] (x : X) : conjClassesEquivOfPathConnected x x = Equiv.refl (ConjClasses (FundamentalGroup X x))

Canonical conjugacy-class transport from a point to itself is the identity.

@[simp]

theorem FundamentalGroup.conjClassesEquivOfPathConnected_symm {X : Type u_1} [TopologicalSpace X] [PathConnectedSpace X] (x₀ x₁ : X) : (conjClassesEquivOfPathConnected x₀ x₁).symm = conjClassesEquivOfPathConnected x₁ x₀

Reversing the endpoints of canonical conjugacy-class transport gives its inverse.

@[simp]

theorem FundamentalGroup.conjClassesEquivOfPathConnected_trans {X : Type u_1} [TopologicalSpace X] [PathConnectedSpace X] (b : X) {x₀ x₁ : X} (γ : Path x₀ x₁) : (conjClassesEquivOfPathConnected b x₀).trans (conjClassesEquivOfPath γ) = conjClassesEquivOfPathConnected b x₁

Canonical conjugacy-class transport in a path-connected space is compatible with subsequent transport along a specified path.

@[simp]

theorem FundamentalGroup.conjClassesEquivOfPath_conjClassesEquivOfPathConnected {X : Type u_1} [TopologicalSpace X] [PathConnectedSpace X] (b : X) {x₀ x₁ : X} (γ : Path x₀ x₁) (C : ConjClasses (FundamentalGroup X b)) : (conjClassesEquivOfPath γ) ((conjClassesEquivOfPathConnected b x₀) C) = (conjClassesEquivOfPathConnected b x₁) C

Applying path transport after canonical transport is canonical transport to the new basepoint.

@[simp]

theorem FundamentalGroup.conjClassesEquivOfPathConnected_trans_conjClassesEquivOfPathConnected {X : Type u_1} [TopologicalSpace X] [PathConnectedSpace X] (b x₀ x₁ : X) (C : ConjClasses (FundamentalGroup X b)) : (conjClassesEquivOfPathConnected x₀ x₁) ((conjClassesEquivOfPathConnected b x₀) C) = (conjClassesEquivOfPathConnected b x₁) C

Applying canonical transport twice is canonical transport directly to the final basepoint.

noncomputable def FundamentalGroup.basepointChangeSubgroup {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (γ : Path x₀ x₁) (H : Subgroup (FundamentalGroup X x₀)) : Subgroup (FundamentalGroup X x₁)

The subgroup of π₁(X, x₁) obtained from H ≤ π₁(X, x₀) by changing basepoint along a path γ : Path x₀ x₁. This is the subgroup-level form of conjugating loops by γ.

Equations

• FundamentalGroup.basepointChangeSubgroup γ H = Subgroup.map (↑(FundamentalGroup.fundamentalGroupMulEquivOfPath γ)) H

theorem FundamentalGroup.mem_basepointChangeSubgroup {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (γ : Path x₀ x₁) (H : Subgroup (FundamentalGroup X x₀)) (g : FundamentalGroup X x₁) : g ∈ basepointChangeSubgroup γ H ↔ ∃ h ∈ H, (fundamentalGroupMulEquivOfPath γ) h = g

Membership in the subgroup transported along a basepoint-change path.

@[simp]

theorem FundamentalGroup.mem_basepointChangeSubgroup_iff {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (γ : Path x₀ x₁) (H : Subgroup (FundamentalGroup X x₀)) (g : FundamentalGroup X x₁) : g ∈ basepointChangeSubgroup γ H ↔ (fundamentalGroupMulEquivOfPath γ).symm g ∈ H

Membership in a transported subgroup, expressed by applying the inverse basepoint-change isomorphism.

theorem FundamentalGroup.le_basepointChangeSubgroup_iff {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (γ : Path x₀ x₁) (K : Subgroup (FundamentalGroup X x₁)) (H : Subgroup (FundamentalGroup X x₀)) : K ≤ basepointChangeSubgroup γ H ↔ Subgroup.map (↑(fundamentalGroupMulEquivOfPath γ).symm) K ≤ H

A subgroup of the target fundamental group is contained in the transported subgroup iff its inverse basepoint-change image is contained in the original subgroup.

theorem FundamentalGroup.basepointChangeSubgroup_le_iff {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (γ : Path x₀ x₁) (H : Subgroup (FundamentalGroup X x₀)) (K : Subgroup (FundamentalGroup X x₁)) : basepointChangeSubgroup γ H ≤ K ↔ H ≤ Subgroup.comap (↑(fundamentalGroupMulEquivOfPath γ)) K

The transported subgroup is contained in a target subgroup iff the original subgroup is contained in the target subgroup's inverse image under basepoint change.

theorem FundamentalGroup.basepointChangeSubgroup_mono {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (γ : Path x₀ x₁) {H K : Subgroup (FundamentalGroup X x₀)} (h : H ≤ K) : basepointChangeSubgroup γ H ≤ basepointChangeSubgroup γ K

Basepoint-change transport is monotone on subgroups.

theorem FundamentalGroup.basepointChangeSubgroup_normal_iff {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (γ : Path x₀ x₁) (H : Subgroup (FundamentalGroup X x₀)) : (basepointChangeSubgroup γ H).Normal ↔ H.Normal

Normality is invariant under basepoint-change transport.

theorem FundamentalGroup.basepointChangeSubgroup.normal {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (γ : Path x₀ x₁) {H : Subgroup (FundamentalGroup X x₀)} (hH : H.Normal) : (basepointChangeSubgroup γ H).Normal

A normal subgroup remains normal after basepoint-change transport.

noncomputable def FundamentalGroup.basepointChangeNormalizerQuotientEquiv {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (γ : Path x₀ x₁) (H : Subgroup (FundamentalGroup X x₀)) : H.normalizerQuotient ≃* (basepointChangeSubgroup γ H).normalizerQuotient

The normalizer quotient N(H) / H transported along a basepoint-change path.

Equations

• FundamentalGroup.basepointChangeNormalizerQuotientEquiv γ H = (H.normalizerQuotientEquivMap (FundamentalGroup.fundamentalGroupMulEquivOfPath γ)).trans (Subgroup.normalizerQuotientCongr ⋯)

@[simp]

theorem FundamentalGroup.basepointChangeNormalizerQuotientEquiv_mk {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (γ : Path x₀ x₁) (H : Subgroup (FundamentalGroup X x₀)) (g : ↥(Subgroup.normalizer ↑H)) : (basepointChangeNormalizerQuotientEquiv γ H) ↑g = ↑((MulEquiv.subgroupCongr ⋯) ((H.normalizerEquivMap (fundamentalGroupMulEquivOfPath γ)) g))

On normalizer representatives, basepoint-change transport is induced by the path-conjugation isomorphism of fundamental groups.

@[simp]

theorem FundamentalGroup.basepointChangeNormalizerQuotientEquiv_symm_mk {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (γ : Path x₀ x₁) (H : Subgroup (FundamentalGroup X x₀)) (g : ↥(Subgroup.normalizer ↑(basepointChangeSubgroup γ H))) : (basepointChangeNormalizerQuotientEquiv γ H).symm ↑g = ↑((H.normalizerEquivMap (fundamentalGroupMulEquivOfPath γ)).symm ((MulEquiv.subgroupCongr ⋯).symm g))

The inverse basepoint-change transport sends a target representative to the inverse path-conjugation representative.

theorem FundamentalGroup.basepointChangeNormalizerQuotientEquiv_mk_coe {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (γ : Path x₀ x₁) (H : Subgroup (FundamentalGroup X x₀)) (g : ↥(Subgroup.normalizer ↑H)) : (basepointChangeNormalizerQuotientEquiv γ H) (H.normalizerQuotientMk g) = (basepointChangeSubgroup γ H).normalizerQuotientMk ((MulEquiv.subgroupCongr ⋯) ⟨(fundamentalGroupMulEquivOfPath γ) ↑g, ⋯⟩)

On representatives, basepoint-change transport applies the path-conjugation isomorphism of fundamental groups.