Peripheral actions on free pro-p groups

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremThe peripheral product identity#

For every unit u ∈ ℤ_pˣ, the basis x = basis e of a free pro-p group admits conjugators c on the basis, with c 0 = 1 in positive rank, and d on the cusp such that (∏_i (c i)⁻¹ * x i ^ u * c i) * (d⁻¹ * cusp x ^ u * d) = 1, the product taken in order and ^ u the p-adic power.

TauCeti.Peripheral.exists_defect_eq_one.{u_1} {p r : ℕ} [Fact (Nat.Prime p)] {F : Type u_1}
  [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F]
  [TotallyDisconnectedSpace F] (hF : TauCeti.IsProP p F) (e : F ≃ₜ* TauCeti.freeProP p (Fin r))
  (u : ℤ_[p]ˣ) :
  ∃ c d,
    (∀ (h0 : 0 < r), c ⟨0, h0⟩ = 1) ∧
      TauCeti.Peripheral.defect hF (TauCeti.Peripheral.basis e) (↑u) c d = 1
Lean

Formalized in Tau Ceti as TauCeti.Peripheral.exists_defect_eq_one.

Sources
LeanTauCeti.Peripheral.exists_defect_eq_one
Uses 2 · Used by 1
Proof usesThe compactness step · Solutions at every level
Used byThe peripheral-power theorem

TheoremSolutions at every level#

For a unit u, every peripheral level of the basis x = basis e of a free pro-p group contains a pair of conjugators whose conjugator at the first basis element is trivial when the rank is positive.

TauCeti.Peripheral.exists_mem_level.{u_1} {p r : ℕ} [Fact (Nat.Prime p)] {F : Type u_1} [Group F]
  [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F]
  (hF : TauCeti.IsProP p F) (e : F ≃ₜ* TauCeti.freeProP p (Fin r)) (u : ℤ_[p]ˣ) (n : ℕ) :
  ∃ c d,
    (∀ (h0 : 0 < r), c ⟨0, h0⟩ = 1) ∧
      (c, d) ∈ TauCeti.Peripheral.level hF (TauCeti.Peripheral.basis e) (↑u) n
Lean

Formalized in Tau Ceti as TauCeti.Peripheral.exists_mem_level.

Sources
LeanTauCeti.Peripheral.exists_mem_level
Uses 2 · Used by 1
Statement usesTauCeti.Peripheral.level
Proof usesTauCeti.Peripheral.exists_mem_level_succ
Used byThe peripheral product identity

TheoremThe compactness step#

If every peripheral level of a family x in a pro-p group contains a pair of conjugators whose conjugator at the first basis element is trivial when the rank is positive, then some such pair has trivial defect. The exponent u need not be a unit.

TauCeti.Peripheral.exists_defect_eq_one_of_forall_exists_mem_level.{u_1} {p r : ℕ}
  [Fact (Nat.Prime p)] {F : Type u_1} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
  [CompactSpace F] [TotallyDisconnectedSpace F] (hF : TauCeti.IsProP p F) (x : Fin r → F)
  (u : ℤ_[p])
  (h :
    ∀ (n : ℕ),
      ∃ c d, (∀ (h0 : 0 < r), c ⟨0, h0⟩ = 1) ∧ (c, d) ∈ TauCeti.Peripheral.level hF x u n) :
  ∃ c d, (∀ (h0 : 0 < r), c ⟨0, h0⟩ = 1) ∧ TauCeti.Peripheral.defect hF x u c d = 1
Lean

Formalized in Tau Ceti as TauCeti.Peripheral.exists_defect_eq_one_of_forall_exists_mem_level.

Sources
LeanTauCeti.Peripheral.exists_defect_eq_one_of_forall_exists_mem_level
Uses 2 · Used by 1
Statement usesTauCeti.Peripheral.level
Proof usesTauCeti.Peripheral.forall_mem_level_iff
Used byThe peripheral product identity

TheoremTauCeti.Peripheral.not_exists_peripheral_identity_two#

At exponent 2, no normalized peripheral product in a rank-two free pro-2 group is trivial even modulo the second closed lower-central-series term.

TauCeti.Peripheral.not_exists_peripheral_identity_two.{u_1} {F : Type u_1} [Group F]
  [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F]
  (hF : TauCeti.IsProP 2 F) (e : F ≃ₜ* TauCeti.freeProP 2 (Fin 2)) :
  ¬∃ c d,
      hF.padicPow (TauCeti.Peripheral.basis e 0) 2 *
            (c⁻¹ * hF.padicPow (TauCeti.Peripheral.basis e 1) 2 * c) *
          (d⁻¹ * hF.padicPow (TauCeti.Peripheral.cusp (TauCeti.Peripheral.basis e)) 2 * d) ∈
        TauCeti.closedLowerCentralSeries F 2
Lean

Formalized in Tau Ceti as TauCeti.Peripheral.not_exists_peripheral_identity_two.

Sources
LeanTauCeti.Peripheral.not_exists_peripheral_identity_two
Uses 1
Proof usesTauCeti.Peripheral.level

TheoremThe peripheral-power theorem#

For every unit u ∈ ℤ_pˣ there are a continuous automorphism φ of F, conjugators c on the basis x = basis e, with c 0 = 1 in positive rank, and a conjugator d on the cusp, such that φ (x i) = (c i)⁻¹ * x i ^ u * c i for every i and φ (cusp x) = d⁻¹ * cusp x ^ u * d, where ^ u is the p-adic power.

TauCeti.Peripheral.exists_peripheralAut.{u_1} {p r : ℕ} [Fact (Nat.Prime p)] {F : Type u_1}
  [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F]
  [TotallyDisconnectedSpace F] (hF : TauCeti.IsProP p F) (e : F ≃ₜ* TauCeti.freeProP p (Fin r))
  (u : ℤ_[p]ˣ) :
  ∃ φ c d,
    (∀ (h0 : 0 < r), c ⟨0, h0⟩ = 1) ∧
      (∀ (i : Fin r),
          φ (TauCeti.Peripheral.basis e i) =
            (c i)⁻¹ * hF.padicPow (TauCeti.Peripheral.basis e i) ↑u * c i) ∧
        φ (TauCeti.Peripheral.cusp (TauCeti.Peripheral.basis e)) =
          d⁻¹ * hF.padicPow (TauCeti.Peripheral.cusp (TauCeti.Peripheral.basis e)) ↑u * d
Lean

Formalized in Tau Ceti as TauCeti.Peripheral.exists_peripheralAut.

Sources
LeanTauCeti.Peripheral.exists_peripheralAut
Uses 2 · Used by 2
Proof usesBurnside's basis theorem, cardinal form · The peripheral product identity
Used byThe peripheral-power theorem for the conjugates of the cusp · The section of the exponent over the principal units

TheoremThe peripheral conjugators are not all equal#

For a free pro-p group of rank at least two and u ∈ ℤ_p other than 0 and 1, if an endomorphism φ satisfies φ (x i) = (c i)⁻¹ * x i ^ u * c i for every basis element and φ z = d⁻¹ * z ^ u * d on the cusp, then some c i differs from d.

TauCeti.Peripheral.exists_ne_of_apply_eq_conj.{u_1, u_2} {p : ℕ} [Fact (Nat.Prime p)] {F : Type u_1}
  [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F]
  [TotallyDisconnectedSpace F] {M : Type u_2} [FunLike M F F] [MonoidHomClass M F F] {n : ℕ}
  (hF : TauCeti.IsProP p F) (e : F ≃ₜ* TauCeti.freeProP p (Fin (n + 2))) {u : ℤ_[p]} (hu₀ : u ≠ 0)
  (hu₁ : u ≠ 1) (φ : M) {c : Fin (n + 2) → F} {d : F}
  (hc :
    ∀ (i : Fin (n + 2)),
      φ (TauCeti.Peripheral.basis e i) =
        (c i)⁻¹ * hF.padicPow (TauCeti.Peripheral.basis e i) u * c i)
  (hd :
    φ (TauCeti.Peripheral.cusp (TauCeti.Peripheral.basis e)) =
      d⁻¹ * hF.padicPow (TauCeti.Peripheral.cusp (TauCeti.Peripheral.basis e)) u * d) :
  ∃ i, c i ≠ d
Lean

Formalized in Tau Ceti as TauCeti.Peripheral.exists_ne_of_apply_eq_conj.

Sources
LeanTauCeti.Peripheral.exists_ne_of_apply_eq_conj

TheoremThe permutation and the exponent are determined in rank at least two#

For the basis of a free pro-p group of rank r ≥ 2, an automorphism peripheral for (σ, u) and for (σ', u') has σ = σ' and u = u'.

TauCeti.Peripheral.IsPeripheralPermAut.unique.{u_1} {p r : ℕ} [Fact (Nat.Prime p)] {F : Type u_1}
  [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F]
  [TotallyDisconnectedSpace F] {hF : TauCeti.IsProP p F} {e : F ≃ₜ* TauCeti.freeProP p (Fin r)}
  (hr : 2 ≤ r) {σ σ' : Equiv.Perm (Fin (r + 1))} {u u' : ℤ_[p]ˣ} {φ : TauCeti.ContinuousAut F}
  (h : TauCeti.Peripheral.IsPeripheralPermAut hF (TauCeti.Peripheral.basis e) σ u φ)
  (h' : TauCeti.Peripheral.IsPeripheralPermAut hF (TauCeti.Peripheral.basis e) σ' u' φ) :
  σ = σ' ∧ u = u'
Lean

Formalized in Tau Ceti as TauCeti.Peripheral.IsPeripheralPermAut.unique.

Sources
LeanTauCeti.Peripheral.IsPeripheralPermAut.unique
Used by 1
Used byThe permutation and the exponent of a permutation-peripheral automorphism

DefinitionThe permutation and the exponent of a permutation-peripheral automorphism#

The permutation and the exponent of a permutation-peripheral automorphism, for the basis of a free pro-p group of rank at least two, as a homomorphism.

TauCeti.Peripheral.permData.{u_1} {p r : ℕ} [Fact (Nat.Prime p)] {F : Type u_1} [Group F]
  [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F]
  (hF : TauCeti.IsProP p F) (e : F ≃ₜ* TauCeti.freeProP p (Fin r)) (hr : 2 ≤ r) :
  ↥(TauCeti.Peripheral.peripheralPermAut hF (TauCeti.Peripheral.basis e)) →*
    Equiv.Perm (Fin (r + 1)) × ℤ_[p]ˣ
Lean

Formalized in Tau Ceti as TauCeti.Peripheral.permData.

Sources
LeanTauCeti.Peripheral.permData
Uses 1
Proof usesThe permutation and the exponent are determined in rank at least two

TheoremThe data are not determined in rank one#

In rank one the peripheral tuple is (x, x⁻¹), and an automorphism with x ↦ x ^ u is peripheral both for the trivial permutation with exponent u and for the transposition with exponent -u.

TauCeti.Peripheral.exists_isPeripheralPermAut_swap_rank_one.{u_1} {p : ℕ} [Fact (Nat.Prime p)]
  {F : Type u_1} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F]
  [TotallyDisconnectedSpace F] (hF : TauCeti.IsProP p F) (e : F ≃ₜ* TauCeti.freeProP p (Fin 1))
  (u : ℤ_[p]ˣ) :
  ∃ φ,
    TauCeti.Peripheral.IsPeripheralPermAut hF (TauCeti.Peripheral.basis e) 1 u φ ∧
      TauCeti.Peripheral.IsPeripheralPermAut hF (TauCeti.Peripheral.basis e) (Equiv.swap 0 1) (-u) φ
Lean

Formalized in Tau Ceti as TauCeti.Peripheral.exists_isPeripheralPermAut_swap_rank_one.

Sources
LeanTauCeti.Peripheral.exists_isPeripheralPermAut_swap_rank_one
Uses 1
Proof usesBurnside's basis theorem, cardinal form

TheoremThe section of the exponent over the principal units#

Let F be a marked free pro-p group of positive rank, and let k ≥ 1, with k ≥ 2 when p = 2. Then the exponent character of the peripheral automorphism group has a continuous homomorphic section over the principal units U^(k) = 1 + p ^ k ℤ_p: a continuous homomorphism s : U^(k) →ₜ* peripheralAut hF (basis e) with exponent (s v) = v for every v.

TauCeti.Peripheral.exists_section_principalUnits.{u_1} {p r : ℕ} [Fact (Nat.Prime p)] {F : Type u_1}
  [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F]
  [TotallyDisconnectedSpace F] (hF : TauCeti.IsProP p F) (e : F ≃ₜ* TauCeti.freeProP p (Fin r))
  (hr : 0 < r) {k : ℕ} (hk : 0 < k) (hk₂ : p = 2 → 2 ≤ k) :
  ∃ s, ∀ (v : ↥(TauCeti.unitsPrincipal p k)), (TauCeti.Peripheral.exponent hF e hr) (s v) = ↑v
Lean

Formalized in Tau Ceti as TauCeti.Peripheral.exists_section_principalUnits.

Sources
LeanTauCeti.Peripheral.exists_section_principalUnits
Uses 10
Statement usesTauCeti.Peripheral.exponent · TauCeti.Peripheral.peripheralAut
Proof usesThe ℓ-adic comparison · The exponent character is continuous · The peripheral automorphisms form a closed subgroup · The peripheral-power theorem · The principal units are a copy of ℤ_p · The product decomposition of the profinite integers · The profinite power · TauCeti.ContinuousAut.compactSpace

TheoremThe peripheral automorphisms form a closed subgroup#

The peripheral automorphisms form a closed subgroup of ContinuousAut F for the congruence topology, when F is topologically finitely generated.

TauCeti.Peripheral.isClosed_peripheralAut.{u_1} {p r : ℕ} [Fact (Nat.Prime p)] {F : Type u_1}
  [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F]
  [TotallyDisconnectedSpace F] (hF : TauCeti.IsProP p F) (x : Fin r → F)
  (hfg : TauCeti.IsTopologicallyFinitelyGenerated F) :
  IsClosed ↑(TauCeti.Peripheral.peripheralAut hF x)
Lean

Formalized in Tau Ceti as TauCeti.Peripheral.isClosed_peripheralAut.

Sources
LeanTauCeti.Peripheral.isClosed_peripheralAut
Uses 1 · Used by 1
Statement usesTauCeti.Peripheral.peripheralAut
Used byThe section of the exponent over the principal units

TheoremThe exponent character is continuous#

Its graph is closed, being the peripheral graph of the basis, and its target ℤ_[p]ˣ is compact.

TauCeti.Peripheral.continuous_exponent.{u_1} {p r : ℕ} [Fact (Nat.Prime p)] {F : Type u_1} [Group F]
  [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F]
  (hF : TauCeti.IsProP p F) (e : F ≃ₜ* TauCeti.freeProP p (Fin r)) (hr : 0 < r) :
  Continuous ⇑(TauCeti.Peripheral.exponent hF e hr)
Lean

Formalized in Tau Ceti as TauCeti.Peripheral.continuous_exponent.

Sources
LeanTauCeti.Peripheral.continuous_exponent
Uses 2 · Used by 1
Statement usesTauCeti.Peripheral.exponent · TauCeti.Peripheral.peripheralAut
Used byThe section of the exponent over the principal units

DefinitionTauCeti.Peripheral.peripheralAut#

The continuous automorphisms peripheral for x with some common unit exponent.

TauCeti.Peripheral.peripheralAut.{u_1} {p r : ℕ} [Fact (Nat.Prime p)] {F : Type u_1} [Group F]
  [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F]
  (hF : TauCeti.IsProP p F) (x : Fin r → F) : Subgroup (TauCeti.ContinuousAut F)
Lean

Formalized in Tau Ceti as TauCeti.Peripheral.peripheralAut.

Sources
LeanTauCeti.Peripheral.peripheralAut
Used by 5
Used byTauCeti.Peripheral.exponent · TauCeti.Peripheral.peripheralAut_eq_top_rank_one · The exponent character is continuous · The peripheral automorphisms form a closed subgroup · The section of the exponent over the principal units

DefinitionTauCeti.Peripheral.exponent#

The unique common unit exponent of a peripheral automorphism of a marked free pro-p group of positive rank.

TauCeti.Peripheral.exponent.{u_1} {p r : ℕ} [Fact (Nat.Prime p)] {F : Type u_1} [Group F]
  [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F]
  (hF : TauCeti.IsProP p F) (e : F ≃ₜ* TauCeti.freeProP p (Fin r)) (hr : 0 < r) :
  ↥(TauCeti.Peripheral.peripheralAut hF (TauCeti.Peripheral.basis e)) →* ℤ_[p]ˣ
Lean

Formalized in Tau Ceti as TauCeti.Peripheral.exponent.

Sources
LeanTauCeti.Peripheral.exponent
Uses 1 · Used by 2
Statement usesTauCeti.Peripheral.peripheralAut
Used byThe exponent character is continuous · The section of the exponent over the principal units

TheoremTauCeti.Peripheral.peripheralAut_eq_top_rank_one#

In rank one the peripheral automorphism group is the whole group of continuous automorphisms.

TauCeti.Peripheral.peripheralAut_eq_top_rank_one.{u_1} {p : ℕ} {F : Type u_1} [Group F]
  [TopologicalSpace F] [Fact (Nat.Prime p)] [IsTopologicalGroup F] [CompactSpace F]
  [TotallyDisconnectedSpace F] (hF : TauCeti.IsProP p F) (e : F ≃ₜ* TauCeti.freeProP p (Fin 1)) :
  TauCeti.Peripheral.peripheralAut hF (TauCeti.Peripheral.basis e) = ⊤
Lean

Formalized in Tau Ceti as TauCeti.Peripheral.peripheralAut_eq_top_rank_one.

Sources
LeanTauCeti.Peripheral.peripheralAut_eq_top_rank_one
Uses 2
Statement usesTauCeti.Peripheral.peripheralAut
Proof usesTauCeti.profiniteFrattini

DefinitionTauCeti.Peripheral.level#

The n-th peripheral level is the set of conjugators whose defect lies in the n-th term of the closed lower central series.

TauCeti.Peripheral.level.{u_1} {p r : ℕ} [Fact (Nat.Prime p)] {F : Type u_1} [Group F]
  [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F]
  (hF : TauCeti.IsProP p F) (x : Fin r → F) (u : ℤ_[p]) (n : ℕ) : Set ((Fin r → F) × F)
Lean

Formalized in Tau Ceti as TauCeti.Peripheral.level.

Sources
LeanTauCeti.Peripheral.level
Used by 5
Used bySolutions at every level · TauCeti.Peripheral.exists_mem_level_succ · TauCeti.Peripheral.forall_mem_level_iff · TauCeti.Peripheral.not_exists_peripheral_identity_two · The compactness step

TheoremTauCeti.Peripheral.exists_mem_level_succ#

A pair of conjugators whose defect lies in γ_n, for positive n, can be corrected so that its defect lies in γ_{n+1}. The corrections lie in γ_{n-1}, and the correction at the first basis element is trivial. The unit hypothesis on u is used to rescale the required graded correction.

TauCeti.Peripheral.exists_mem_level_succ.{u_1} {p r : ℕ} [Fact (Nat.Prime p)] {F : Type u_1}
  [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F]
  [TotallyDisconnectedSpace F] (hF : TauCeti.IsProP p F) (e : F ≃ₜ* TauCeti.freeProP p (Fin r))
  (u : ℤ_[p]ˣ) (n : ℕ) (hn : 1 ≤ n) (c : Fin r → F) (d : F)
  (h : (c, d) ∈ TauCeti.Peripheral.level hF (TauCeti.Peripheral.basis e) (↑u) n) :
  ∃ c' d',
    (∀ (i : Fin r), c' i ∈ TauCeti.closedLowerCentralSeries F (n - 1)) ∧
      d' ∈ TauCeti.closedLowerCentralSeries F (n - 1) ∧
        (∀ (h0 : 0 < r), c' ⟨0, h0⟩ = 1) ∧
          (fun i => c i * c' i, d * d') ∈
            TauCeti.Peripheral.level hF (TauCeti.Peripheral.basis e) (↑u) (n + 1)
Lean

Formalized in Tau Ceti as TauCeti.Peripheral.exists_mem_level_succ.

Sources
LeanTauCeti.Peripheral.exists_mem_level_succ
Uses 1 · Used by 1
Statement usesTauCeti.Peripheral.level
Used bySolutions at every level

TheoremTauCeti.Peripheral.forall_mem_level_iff#

A pair of conjugators lies in every peripheral level exactly when its defect is trivial: in a pro-p group the terms of the closed lower central series have trivial intersection.

TauCeti.Peripheral.forall_mem_level_iff.{u_1} {p r : ℕ} [Fact (Nat.Prime p)] {F : Type u_1}
  [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F]
  [TotallyDisconnectedSpace F] (hF : TauCeti.IsProP p F) (x : Fin r → F) (u : ℤ_[p])
  (cd : (Fin r → F) × F) :
  (∀ (n : ℕ), cd ∈ TauCeti.Peripheral.level hF x u n) ↔
    TauCeti.Peripheral.defect hF x u cd.1 cd.2 = 1
Lean

Formalized in Tau Ceti as TauCeti.Peripheral.forall_mem_level_iff.

Sources
LeanTauCeti.Peripheral.forall_mem_level_iff
Uses 1 · Used by 1
Statement usesTauCeti.Peripheral.level
Used byThe compactness step

DefinitionThe principal units are a copy of ℤ_p#

For f ≥ 1, with f ≥ 2 when p = 2, and a unit w of exact level f, the p-adic power map l ↦ w ^ l is a topological group isomorphism from the additive group of ℤ_[p] onto U^(f) = 1 + p ^ f ℤ_p. It is onto because w topologically generates U^(f), and injective because w has infinite order.

TauCeti.principalUnitsEquiv {p : ℕ} [Fact (Nat.Prime p)] {f : ℕ} (hf : 0 < f) (hf₂ : p = 2 → 2 ≤ f)
  {w : ℤ_[p]ˣ} (hw : w ∈ TauCeti.unitsPrincipal p f) (hw' : w ∉ TauCeti.unitsPrincipal p (f + 1)) :
  Multiplicative ℤ_[p] ≃ₜ* ↥(TauCeti.unitsPrincipal p f)
Lean

Formalized in Tau Ceti as TauCeti.principalUnitsEquiv.

Sources
LeanTauCeti.principalUnitsEquiv
Used by 1
Used byThe section of the exponent over the principal units

TheoremThe peripheral-power theorem for the conjugates of the cusp#

For every unit u ∈ ℤ_pˣ there are a continuous automorphism φ of F, conjugators c on the basis x = basis e, with c 0 = 1 in positive rank, and d : F, such that φ (x i) = (c i)⁻¹ * x i ^ u * c i for every i and, for every q : F, φ carries the conjugate y = q * cusp x * q⁻¹ of the cusp to d'⁻¹ * y ^ u * d' with d' = q * d * (φ q)⁻¹. At q = 1 the conjugator is d.

TauCeti.Peripheral.exists_peripheralAut_conj_cusp.{u_1} {p r : ℕ} [Fact (Nat.Prime p)]
  {F : Type u_1} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F]
  [TotallyDisconnectedSpace F] (hF : TauCeti.IsProP p F) (e : F ≃ₜ* TauCeti.freeProP p (Fin r))
  (u : ℤ_[p]ˣ) :
  ∃ φ c d,
    (∀ (h0 : 0 < r), c ⟨0, h0⟩ = 1) ∧
      (∀ (i : Fin r),
          φ (TauCeti.Peripheral.basis e i) =
            (c i)⁻¹ * hF.padicPow (TauCeti.Peripheral.basis e i) ↑u * c i) ∧
        ∀ (q : F),
          φ (q * TauCeti.Peripheral.cusp (TauCeti.Peripheral.basis e) * q⁻¹) =
            (q * d * (φ q)⁻¹)⁻¹ *
                hF.padicPow (q * TauCeti.Peripheral.cusp (TauCeti.Peripheral.basis e) * q⁻¹) ↑u *
              (q * d * (φ q)⁻¹)
Lean

Formalized in Tau Ceti as TauCeti.Peripheral.exists_peripheralAut_conj_cusp.

Sources
LeanTauCeti.Peripheral.exists_peripheralAut_conj_cusp
Uses 1
Proof usesThe peripheral-power theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.