Free pro-p groups on a type

The free pro-p group on X is defined directly as the maximal pro-p quotient of the free profinite group on X. A map from X to a pro-p profinite group in the same universe extends uniquely to a continuous homomorphism. Extensionality for homomorphisms out of the free pro-p group only requires a Hausdorff group target, which may live in any universe.

The canonical comparison with the free pro-C group for the class of finite p-groups is used to derive the universal property and functoriality, and to see that the generators generate the free pro-p group topologically. The file also records that a surjection of generating types induces a surjection of free pro-p groups, and that a topologically finitely generated pro-p group is a continuous image of the free pro-p group on any finite type with at least topologicalGeneratorRankNat elements.

Main definitions

• TauCeti.freeProP: the free pro-p group on a type.
• TauCeti.freeProP.of: its canonical generators.
• TauCeti.freeProPGen: the generators of freeProP p (Fin n) indexed by ℕ, with value 1 out of range.
• TauCeti.freeProP.fromFreeGroup: the canonical homomorphism from the discrete free group.
• TauCeti.freeProP.lift: extension from the generators.
• TauCeti.freeProP.map: functoriality in the generating type.
• TauCeti.freeProP.congr: the topological isomorphism induced by a bijection of generating types.
• TauCeti.freeProP.finSuccRetract: the retraction of the free pro-p group on Fin (n + 1) onto the free pro-p group on Fin n killing the first generator, a left inverse of freeProP.map Fin.succ.
• TauCeti.freeProC.equivFreeProP: comparison with the finite-p specialization of freeProC.

Main results

• TauCeti.isProP_freeProP: a free pro-p group is pro-p.
• TauCeti.freeProP.topologicalClosure_closure_range_of_eq_top: the generators generate the free pro-p group topologically.
• TauCeti.isTopologicallyFinitelyGenerated_freeProP: for finite X, the free pro-p group on X is topologically finitely generated.
• TauCeti.freeProP.hom_ext: homomorphisms agreeing on the generators are equal.
• TauCeti.freeProP.existsUnique_lift: the universal property.
• TauCeti.freeProP.lift_surjective: a topologically generating map lifts to a surjection.
• TauCeti.freeProP.map_surjective: a surjection of generating types induces a surjection.
• TauCeti.freeProP.existsUnique_continuousMulEquiv: the free pro-p group is unique up to a unique topological isomorphism matching the generators.
• TauCeti.IsProP.exists_surjective_freeProP: a topologically finitely generated pro-p group is a continuous image of the free pro-p group on any finite type with at least topologicalGeneratorRankNat elements.
• TauCeti.freeProC.equivFreeProP_of: the comparison preserves the generators.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Chapter 3.

@[reducible, inline]

noncomputable abbrev TauCeti.freeProP (p : ℕ) (X : Type u) : Type u

The free pro-p group on X, obtained directly as the maximal pro-p quotient of the free profinite group on X.

Equations

• TauCeti.freeProP p X = TauCeti.maximalProPQuotient p ↑(TauCeti.freeProfiniteGroup X).toProfinite.toTop

theorem TauCeti.isProP_freeProP (p : ℕ) (X : Type u) : IsProP p (freeProP p X)

A free pro-p group is pro-p.

noncomputable def TauCeti.freeProP.fromFreeProfiniteGroup (p : ℕ) (X : Type u) : ↑(freeProfiniteGroup X).toProfinite.toTop →ₜ* freeProP p X

The canonical continuous quotient map from the free profinite group to the free pro-p group.

Equations

• TauCeti.freeProP.fromFreeProfiniteGroup x✝¹ x✝ = { toMonoidHom := TauCeti.maximalProPQuotient.mk x✝¹ ↑(TauCeti.freeProfiniteGroup x✝).toProfinite.toTop, continuous_toFun := ⋯ }

@[simp]

theorem TauCeti.freeProP.fromFreeProfiniteGroup_apply (p : ℕ) (X : Type u) (x : ↑(freeProfiniteGroup X).toProfinite.toTop) : (fromFreeProfiniteGroup p X) x = (maximalProPQuotient.mk p ↑(freeProfiniteGroup X).toProfinite.toTop) x

Evaluation of the canonical quotient map agrees with the underlying quotient homomorphism.

noncomputable def TauCeti.freeProP.of {p : ℕ} {X : Type u} (x : X) : freeProP p X

The canonical map from the generating type into the free pro-p group.

Equations

• TauCeti.freeProP.of x = (TauCeti.freeProP.fromFreeProfiniteGroup p X) (TauCeti.freeProfiniteGroup.of x)

@[simp]

theorem TauCeti.freeProP.fromFreeProfiniteGroup_of {p : ℕ} {X : Type u} (x : X) : (fromFreeProfiniteGroup p X) (freeProfiniteGroup.of x) = of x

The canonical quotient map sends a free profinite generator to the corresponding free pro-p generator.

theorem TauCeti.freeProP.fromFreeProfiniteGroup_surjective {p : ℕ} {X : Type u} : Function.Surjective ⇑(fromFreeProfiniteGroup p X)

The canonical map from the free profinite group to the free pro-p group is surjective.

noncomputable def TauCeti.freeProP.fromFreeGroup (p : ℕ) (X : Type u) : FreeGroup X →* freeProP p X

The canonical homomorphism from the discrete free group on X to the free pro-p group on X: the unit of the profinite completion followed by the maximal pro-p quotient map.

Equations

• TauCeti.freeProP.fromFreeGroup p X = (TauCeti.freeProP.fromFreeProfiniteGroup p X).comp (TauCeti.freeProfiniteGroup.fromFreeGroup X)

@[simp]

theorem TauCeti.freeProP.fromFreeGroup_of {p : ℕ} {X : Type u} (x : X) : (fromFreeGroup p X) (FreeGroup.of x) = of x

fromFreeGroup carries the free-group generator at x to the generator of x.

Comparison with free pro-C groups

noncomputable def TauCeti.freeProC.equivFreeProP (p : ℕ) (X : Type u) : freeProC (finiteGroupClassP p) X ≃ₜ* freeProP p X

For the class of finite p-groups, the free pro-C group is canonically isomorphic to the free pro-p group.

Equations

• TauCeti.freeProC.equivFreeProP p X = TauCeti.proCCompletion.equivMaximalProPQuotient p ↑(TauCeti.freeProfiniteGroup X).toProfinite.toTop

@[simp]

theorem TauCeti.freeProC.equivFreeProP_fromFreeProfiniteGroup (p : ℕ) (X : Type u) (x : ↑(freeProfiniteGroup X).toProfinite.toTop) : (equivFreeProP p X) ↑x = (freeProP.fromFreeProfiniteGroup p X) x

The comparison with the free pro-p group commutes with the canonical quotient maps.

@[simp]

theorem TauCeti.freeProC.equivFreeProP_of {X : Type u} (p : ℕ) (x : X) : (equivFreeProP p X) (of x) = freeProP.of x

The comparison with the free pro-p group preserves each canonical generator.

@[simp]

theorem TauCeti.freeProC.equivFreeProP_symm_of {X : Type u} (p : ℕ) (x : X) : (equivFreeProP p X).symm (freeProP.of x) = of x

The inverse comparison with the free pro-p group preserves each canonical generator.

@[simp]

theorem TauCeti.freeProC.equivFreeProP_symm_fromFreeProfiniteGroup (p : ℕ) (X : Type u) (x : ↑(freeProfiniteGroup X).toProfinite.toTop) : (equivFreeProP p X).symm ↑x = ↑x

The inverse comparison commutes with the canonical quotient maps.

theorem TauCeti.freeProP.topologicalClosure_closure_range_of_eq_top (p : ℕ) (X : Type u) : (Subgroup.closure (Set.range of)).topologicalClosure = ⊤

The canonical generators of a free pro-p group generate it topologically.

theorem TauCeti.isTopologicallyFinitelyGenerated_freeProP (p : ℕ) (X : Type u) [Finite X] : IsTopologicallyFinitelyGenerated (freeProP p X)

The free pro-p group on a finite type is topologically finitely generated.

theorem TauCeti.freeProP.hom_ext {p : ℕ} {X : Type u} {Q : Type v} [Group Q] [TopologicalSpace Q] [T2Space Q] {f g : freeProP p X →ₜ* Q} (h : ∀ (x : X), f (of x) = g (of x)) : f = g

Two continuous homomorphisms out of a free pro-p group that agree on the generators are equal.

theorem TauCeti.freeProP.hom_ext_iff {p : ℕ} {X : Type u} {Q : Type v} [Group Q] [TopologicalSpace Q] [T2Space Q] {f g : freeProP p X →ₜ* Q} : f = g ↔ ∀ (x : X), f (of x) = g (of x)

theorem ContinuousMonoidHom.comp_eq_of_forall_inv_mul_apply_mem_ker {p : ℕ} {X : Type u} {Q : Type v} [Group Q] [TopologicalSpace Q] [T2Space Q] (χ : TauCeti.freeProP p X →ₜ* Q) (φ : TauCeti.freeProP p X →ₜ* TauCeti.freeProP p X) (hφ : ∀ (j : X), (TauCeti.freeProP.of j)⁻¹ * φ (TauCeti.freeProP.of j) ∈ χ.ker) : χ.comp φ = χ

A continuous homomorphism is unchanged by an endomorphism moving each generator inside its kernel.

noncomputable def TauCeti.freeProP.lift {p : ℕ} {X P : Type u} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) (f : X → P) : freeProP p X →ₜ* P

The continuous homomorphism from a free pro-p group extending a map on its generators.

Equations

• TauCeti.freeProP.lift hP f = (TauCeti.freeProC.lift ⋯ f).comp ↑(TauCeti.freeProC.equivFreeProP p X).symm

@[simp]

theorem TauCeti.freeProP.lift_comp_fromFreeProfiniteGroup {p : ℕ} {X P : Type u} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) (f : X → P) : (lift hP f).comp (fromFreeProfiniteGroup p X) = freeProfiniteGroup.lift f

The free pro-p lift recovers the free profinite lift along the quotient map.

@[simp]

theorem TauCeti.freeProP.lift_fromFreeProfiniteGroup {p : ℕ} {X P : Type u} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) (f : X → P) (x : ↑(freeProfiniteGroup X).toProfinite.toTop) : (lift hP f) ↑x = (freeProfiniteGroup.lift f) x

The free pro-p lift evaluates on the image of the free profinite group as the free profinite lift.

@[simp]

theorem TauCeti.freeProP.lift_of {p : ℕ} {X P : Type u} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) (f : X → P) (x : X) : (lift hP f) (of x) = f x

The lift of f agrees with f on every canonical generator.

theorem TauCeti.freeProP.lift_unique {p : ℕ} {X P : Type u} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) (f : X → P) (g : freeProP p X →ₜ* P) (hg : ∀ (x : X), g (of x) = f x) : g = lift hP f

A continuous homomorphism restricting to f on the generators is the canonical lift of f.

theorem TauCeti.freeProP.existsUnique_lift {p : ℕ} {X P : Type u} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) (f : X → P) : ∃! g : freeProP p X →ₜ* P, ∀ (x : X), g (of x) = f x

The universal property of the free pro-p group. Every map from X to a profinite pro-p group extends uniquely to a continuous homomorphism from freeProP p X.

@[simp]

theorem TauCeti.freeProP.comp_lift {p : ℕ} {X P : Type u} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q] [CompactSpace Q] [TotallyDisconnectedSpace Q] (hP : IsProP p P) (hQ : IsProP p Q) (g : P →ₜ* Q) (f : X → P) : g.comp (lift hP f) = lift hQ (⇑g ∘ f)

The free pro-p lift is natural in its target.

theorem TauCeti.freeProP.lift_surjective {p : ℕ} {X P : Type u} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) {f : X → P} (hf : Dense ↑(Subgroup.closure (Set.range f))) : Function.Surjective ⇑(lift hP f)

A map whose range generates the target topologically lifts to a surjection.

@[simp]

theorem TauCeti.freeProC.freeProP_lift_comp_equivFreeProP {p : ℕ} {X P : Type u} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) (f : X → P) : (freeProP.lift hP f).comp ↑(equivFreeProP p X) = lift ⋯ f

Lifting from either construction of a free pro-p group gives the same homomorphism.

noncomputable def TauCeti.freeProP.map {p : ℕ} {X Y : Type u} (f : X → Y) : freeProP p X →ₜ* freeProP p Y

The continuous homomorphism of free pro-p groups induced by a map of generating types.

Equations

• TauCeti.freeProP.map f = (↑(TauCeti.freeProC.equivFreeProP p Y)).comp ((TauCeti.freeProC.map f).comp ↑(TauCeti.freeProC.equivFreeProP p X).symm)

@[simp]

theorem TauCeti.freeProP.map_of {p : ℕ} {X Y : Type u} (f : X → Y) (x : X) : (map f) (of x) = of (f x)

map f carries the generator at x to the generator at f x.

@[simp]

theorem TauCeti.freeProP.lift_comp_map {p : ℕ} {X Y P : Type u} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) (f : Y → P) (g : X → Y) : (lift hP f).comp (map g) = lift hP (f ∘ g)

The free pro-p lift is natural in the generating type.

@[simp]

theorem TauCeti.freeProP.map_id {p : ℕ} {X : Type u} : map id = ContinuousMonoidHom.id (freeProP p X)

Mapping the generating type by the identity induces the identity homomorphism.

@[simp]

theorem TauCeti.freeProP.map_comp {p : ℕ} {X Y Z : Type u} (f : X → Y) (g : Y → Z) : map (g ∘ f) = (map g).comp (map f)

The maps induced by maps of generating types compose functorially.

@[simp]

theorem TauCeti.freeProP.map_comp_fromFreeProfiniteGroup {p : ℕ} {X Y : Type u} (f : X → Y) : (map f).comp (fromFreeProfiniteGroup p X) = (fromFreeProfiniteGroup p Y).comp (freeProfiniteGroup.map f)

The map induced on free pro-p groups commutes with the canonical maps from the free profinite groups.

@[simp]

theorem TauCeti.freeProP.map_fromFreeProfiniteGroup {p : ℕ} {X Y : Type u} (f : X → Y) (x : ↑(freeProfiniteGroup X).toProfinite.toTop) : (map f) ↑x = (fromFreeProfiniteGroup p Y) ((freeProfiniteGroup.map f) x)

The map induced on free pro-p groups evaluates compatibly with the map induced on free profinite groups.

theorem TauCeti.freeProP.map_surjective {p : ℕ} {X Y : Type u} {f : X → Y} (hf : Function.Surjective f) : Function.Surjective ⇑(map f)

A surjection of generating types induces a surjection of free pro-p groups.

noncomputable def TauCeti.freeProP.congr {p : ℕ} {X Y : Type u} (σ : X ≃ Y) : freeProP p X ≃ₜ* freeProP p Y

The isomorphism of free pro-p groups induced by a bijection of the generating types. It sends the generator at x to the generator at σ x; its inverse is induced by σ⁻¹.

Equations

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

theorem TauCeti.freeProP.coe_congr {p : ℕ} {X Y : Type u} (σ : X ≃ Y) : ⇑(congr σ) = ⇑(map ⇑σ)

The isomorphism induced by a bijection of generating types is the induced homomorphism TauCeti.freeProP.map.

@[simp]

theorem TauCeti.freeProP.congr_symm {p : ℕ} {X Y : Type u} (σ : X ≃ Y) : (congr σ).symm = congr σ.symm

The inverse of the isomorphism induced by a bijection is induced by the inverse bijection.

@[simp]

theorem TauCeti.freeProP.congr_refl {p : ℕ} {X : Type u} : congr (Equiv.refl X) = ContinuousMulEquiv.refl (freeProP p X)

The isomorphism induced by the identity bijection is the identity.

@[simp]

theorem TauCeti.freeProP.congr_trans {p : ℕ} {X Y Z : Type u} (σ : X ≃ Y) (τ : Y ≃ Z) : congr (σ.trans τ) = (congr σ).trans (congr τ)

The isomorphisms induced by bijections of generating types compose functorially.

@[simp]

theorem TauCeti.freeProP.congr_of {p : ℕ} {X Y : Type u} (σ : X ≃ Y) (x : X) : (congr σ) (of x) = of (σ x)

The isomorphism induced by a bijection of generating types sends the generator at x to the generator at σ x.

@[simp]

theorem TauCeti.freeProC.equivFreeProP_comp_map {X Y : Type u} (p : ℕ) (f : X → Y) : (↑(equivFreeProP p Y)).comp (map f) = (freeProP.map f).comp ↑(equivFreeProP p X)

The comparison between the two free pro-p constructions is natural in the generators.

@[simp]

theorem TauCeti.freeProC.equivFreeProP_map {X Y : Type u} (p : ℕ) (f : X → Y) (x : freeProC (finiteGroupClassP p) X) : (equivFreeProP p Y) ((map f) x) = (freeProP.map f) ((equivFreeProP p X) x)

The comparison between the two free pro-p constructions evaluates naturally on maps of generators.

theorem TauCeti.freeProP.existsUnique_continuousMulEquiv {p : ℕ} {X G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (ι : X → G) (h : ∀ (P : Type u) [inst : Group P] [inst_1 : TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P], IsProP p P → ∀ (f : X → P), ∃! φ : G →ₜ* P, ∀ (x : X), φ (ι x) = f x) : ∃! e : freeProP p X ≃ₜ* G, ∀ (x : X), e (of x) = ι x

The free pro-p group is unique up to a unique isomorphism. A pro-p group G with a map ι : X → G through which every map from X to a pro-p profinite group factors uniquely is topologically isomorphic to freeProP p X by a unique isomorphism matching the two families of generators.

Topologically finitely generated pro-p groups as images of free pro-p groups

theorem TauCeti.IsProP.exists_surjective_freeProP {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (h : IsTopologicallyFinitelyGenerated G) (X : Type u) [Finite X] (hX : topologicalGeneratorRankNat G h ≤ Nat.card X) : ∃ (φ : freeProP p X →ₜ* G), Function.Surjective ⇑φ

A topologically finitely generated pro-p group is a continuous image of the free pro-p group on any finite type with at least topologicalGeneratorRankNat G elements.

The generators of a free pro-p group on Fin n, indexed by ℕ

noncomputable def TauCeti.freeProPGen (p n i : ℕ) : freeProP p (Fin n)

The generators of the free pro-p group on Fin n, indexed by ℕ, with value 1 out of range. A word in the generators written on such a tuple, such as a relator of a presentation on Fin n, carries no index-bound side conditions.

Equations

• TauCeti.freeProPGen p n i = if h : i < n then TauCeti.freeProP.of ⟨i, h⟩ else 1

@[simp]

theorem TauCeti.freeProPGen_of_lt (p : ℕ) {n i : ℕ} (h : i < n) : freeProPGen p n i = freeProP.of ⟨i, h⟩

In range, freeProPGen p n i is the i-th free generator.

@[simp]

theorem TauCeti.freeProPGen_eq_one_of_le (p : ℕ) {n i : ℕ} (h : n ≤ i) : freeProPGen p n i = 1

Out of range, freeProPGen p n i is 1.

theorem TauCeti.freeProPGen_val (p : ℕ) {n : ℕ} (i : Fin n) : freeProPGen p n ↑i = freeProP.of i

On the values of Fin n, freeProPGen p n is the canonical generator.

theorem TauCeti.finite_range_freeProPGen (p n : ℕ) : (Set.range (freeProPGen p n)).Finite

The ℕ-indexed generators take finitely many values: the canonical generators and 1.

theorem TauCeti.topologicalClosure_closure_eq_top_of_range_freeProPGen_subset (p : ℕ) {n : ℕ} {s : Set (freeProP p (Fin n))} (hs : Set.range (freeProPGen p n) ⊆ s) : (Subgroup.closure s).topologicalClosure = ⊤

A set containing every ℕ-indexed generator generates the free pro-p group topologically.

theorem TauCeti.topologicalClosure_closure_insert_insert_image_freeProPGen_eq_top (p : ℕ) {n : ℕ} (j k : ℕ) : (Subgroup.closure (insert (freeProPGen p n j) (insert (freeProPGen p n k) (freeProPGen p n '' {i : ℕ | i ≠ j ∧ i ≠ k})))).topologicalClosure = ⊤

Two marked generators x_j, x_k together with the remaining generators x_i, i ≠ j, k, generate the free pro-p group topologically.

theorem TauCeti.map_freeProPGen (p : ℕ) {n : ℕ} {K : Type u_1} {F : Type u_2} [Group K] [FunLike F (freeProP p (Fin n)) K] [MonoidHomClass F (freeProP p (Fin n)) K] (φ : F) (i : ℕ) : φ (freeProPGen p n i) = if h : i < n then φ (freeProP.of ⟨i, h⟩) else 1

The value of a homomorphism on the ℕ-indexed generators.

theorem TauCeti.freeProP.lift_freeProPGen (p : ℕ) {n : ℕ} {P : Type} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) (g : Fin n → P) (i : ℕ) : (lift hP g) (freeProPGen p n i) = if h : i < n then g ⟨i, h⟩ else 1

The value of the universal map on the ℕ-indexed generators: the prescribed value in range, 1 out of range.

The first generator of a free pro-p group on Fin (n + 1) and the others

noncomputable def TauCeti.freeProP.finSuccRetract {p n : ℕ} : freeProP p (Fin (n + 1)) →ₜ* freeProP p (Fin n)

The retraction onto the last n generators. The continuous homomorphism from the free pro-p group on Fin (n + 1) to the free pro-p group on Fin n killing the first generator and sending the generator at j.succ to the generator at j. It is a left inverse of freeProP.map Fin.succ (TauCeti.freeProP.finSuccRetract_map_succ).

Equations

• TauCeti.freeProP.finSuccRetract = TauCeti.freeProP.lift ⋯ (Fin.cons 1 TauCeti.freeProP.of)

@[simp]

theorem TauCeti.freeProP.finSuccRetract_of_zero {p n : ℕ} : finSuccRetract (of 0) = 1

The retraction onto the last n generators kills the first generator.

@[simp]

theorem TauCeti.freeProP.finSuccRetract_of_succ {p n : ℕ} (j : Fin n) : finSuccRetract (of j.succ) = of j

The retraction onto the last n generators sends the generator at j.succ to the generator at j.

theorem TauCeti.freeProP.finSuccRetract_comp_map_succ {p n : ℕ} : finSuccRetract.comp (map Fin.succ) = ContinuousMonoidHom.id (freeProP p (Fin n))

The retraction onto the last n generators is a left inverse of freeProP.map Fin.succ.

@[simp]

theorem TauCeti.freeProP.finSuccRetract_map_succ {p n : ℕ} (y : freeProP p (Fin n)) : finSuccRetract ((map Fin.succ) y) = y

The retraction onto the last n generators is a left inverse of freeProP.map Fin.succ.

@[simp]

theorem TauCeti.freeProP.map_succ_freeProPGen {p n : ℕ} (i : ℕ) : (map Fin.succ) (freeProPGen p n i) = freeProPGen p (n + 1) (i + 1)

The map induced by Fin.succ shifts the ℕ-indexed generators by one.

theorem TauCeti.freeProP.map_succ_finSuccRetract_of_mem_topologicalClosure_closure {p n : ℕ} {y : freeProP p (Fin (n + 1))} (hy : y ∈ (Subgroup.closure (Set.range fun (j : Fin n) => of j.succ)).topologicalClosure) : (map Fin.succ) (finSuccRetract y) = y

An element of the closed subgroup generated by the last n generators x_{j+1} is recovered from its retraction onto them: map Fin.succ ∘ finSuccRetract is the identity on each x_{j+1}, hence on the closed subgroup they generate.