Basepoint change for fundamental-group subgroups

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.

Mathlib already supplies the fundamental-group isomorphism FundamentalGroup.fundamentalGroupMulEquivOfPath; the declarations here are only the subgroup and normalizer-quotient bookkeeping needed by the universal-covers roadmap.

Main declarations

• TauCeti.FundamentalGroup.basepointChangeSubgroup: transport a subgroup of π₁(X, x₀) along a path γ : Path x₀ x₁.
• Domain-specific membership, inclusion, monotonicity, and normality lemmas for basepointChangeSubgroup.
• TauCeti.FundamentalGroup.basepointChangeNormalizerQuotientEquiv: the corresponding isomorphism N(H) / H ≃* N(γ₊H) / γ₊H.
• TauCeti.FundamentalGroup.mem_basepointChangeSubgroup and the representative [simp] lemmas for membership and quotient calculations under these domain-specific names.

References

This supplies a small prerequisite for TauCetiRoadmap/UniversalCovers/README.md, Stage 2, items 7 and 8: the pointed cover attached to H ≤ π₁(X, x₀), conjugacy under basepoint change, and the normalizer quotient N(H) / H appearing as the deck group of that cover.

noncomputable def TauCeti.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

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

theorem TauCeti.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, (FundamentalGroup.fundamentalGroupMulEquivOfPath γ) h = g

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

@[simp]

theorem TauCeti.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 ↔ (FundamentalGroup.fundamentalGroupMulEquivOfPath γ).symm g ∈ H

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

theorem TauCeti.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 (↑(FundamentalGroup.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 TauCeti.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 (↑(FundamentalGroup.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.FundamentalGroup.basepointChangeNormalizerQuotientEquiv {X : Type u_1} [TopologicalSpace X] {x₀ x₁ : X} (γ : Path x₀ x₁) (H : Subgroup (FundamentalGroup X x₀)) : Subgroup.normalizerQuotient H ≃* Subgroup.normalizerQuotient (basepointChangeSubgroup γ H)

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.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 ⋯) ((Subgroup.normalizerEquivMap H (FundamentalGroup.fundamentalGroupMulEquivOfPath γ)) g))

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

@[simp]

theorem TauCeti.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 = ↑((Subgroup.normalizerEquivMap H (FundamentalGroup.fundamentalGroupMulEquivOfPath γ)).symm ((MulEquiv.subgroupCongr ⋯).symm g))

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

theorem TauCeti.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) ((Subgroup.normalizerQuotientMk H) g) = (Subgroup.normalizerQuotientMk (basepointChangeSubgroup γ H)) ((MulEquiv.subgroupCongr ⋯) ⟨(FundamentalGroup.fundamentalGroupMulEquivOfPath γ) ↑g, ⋯⟩)

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