Documentation

TauCeti.Topology.Algebra.Group.Profinite.Demushkin.Orientation

The standard orientation of D₀ #

The standard dyadic one-relator pro-2 group D₀ = ⟨A, S, Y ∣ A²S⁴(S,Y)⟩ carries a marked continuous character D₀ → ℤ_2ˣ, its standard orientation, with values -1, 1 and (-3)⁻¹ on A, S and Y. It exists because these values kill the relator: (-1)² · 1⁴ · 1 = 1, the commutator dying because ℤ_2ˣ is abelian. In the normal form x₁² x₂^{2^f} (x₂, x₃) of a Demushkin group of odd rank with q = 2, these are the tabulated character values at f = 2, namely χ(x₁) = -1 and χ(x₃) = (1 - 2²)⁻¹, so the orientation is surjective: -1 and -3 topologically generate ℤ_2ˣ = {±1} × (1 + 4ℤ_2). The marked generators topologically generate D₀, so the standard orientation is the only continuous character with these values.

Main declarations #

Main results #

References #

source
theorem TauCeti.isUnit_neg_three :
IsUnit (-3)

-3 is a 2-adic unit: -3 = 1 + (-4) with 2 ∣ -4.

source
@[reducible, inline]
noncomputable abbrev TauCeti.negThreeUnit :
ℤ_[2]ˣ

The 2-adic unit with value -3, whose inverse is the value of the standard orientation of D₀ on Y.

Instances For
    source
    @[simp]
    theorem TauCeti.negThreeUnit_coe :
    ↑negThreeUnit = -3

    The value of negThreeUnit is -3.

    source
    theorem TauCeti.negThreeUnit_neg_coe :
    ↑(-negThreeUnit) = -1 + 2 ^ 2

    The negative of negThreeUnit is 3 = -1 + 2 ^ 2, the generator -1 + 2 ^ k at k = 2 of the twisted closed subgroups U^[k] of ℤ₂ˣ.

    source
    theorem TauCeti.negThreeUnit_inv_mul_one_sub_two_pow_two :
    ↑negThreeUnit⁻¹ * (1 - 2 ^ 2) = 1

    The inverse of negThreeUnit is the value (1 - 2 ^ 2)⁻¹ of the orientation character table: (-3)⁻¹ · (1 - 2²) = 1.

    source
    theorem TauCeti.standardD0Orientation_relator (φ : freeProP 2 (Fin 3) →* ℤ_[2]ˣ) (hA : φ (freeProP.of 0) = -1) (hS : φ (freeProP.of 1) = 1) :
    φ d0Relator = 1

    Any character of the free pro-2 group on A, S, Y with values -1 on A and 1 on S kills the relator A²S⁴(S,Y), regardless of its value on Y: (-1)² · 1⁴ · 1 = 1.

    source
    noncomputable def TauCeti.standardD0Orientation :
    demushkinD0 →ₜ* ℤ_[2]ˣ

    The standard orientation of D₀: the continuous character D₀ →ₜ* ℤ_2ˣ with values -1, 1, (-3)⁻¹ on the marked generators A, S, Y.

    Instances For
      source
      @[simp]
      theorem TauCeti.standardD0Orientation_d0A :
      standardD0Orientation d0A = -1

      The standard orientation sends A to -1.

      source
      @[simp]
      theorem TauCeti.standardD0Orientation_d0S :
      standardD0Orientation d0S = 1

      The standard orientation sends S to 1.

      source
      @[simp]
      theorem TauCeti.standardD0Orientation_d0Y :
      standardD0Orientation d0Y = negThreeUnit⁻¹

      The standard orientation sends Y to (-3)⁻¹.

      source
      theorem TauCeti.standardD0Orientation_surjective :
      Function.Surjective ⇑standardD0Orientation

      The standard orientation of D₀ is surjective: its range is closed, being the continuous image of a compact group, and contains -1 and (-3)⁻¹, which topologically generate ℤ_2ˣ = {±1} × (1 + 4ℤ_2).

      source
      @[simp]
      theorem TauCeti.range_standardD0Orientation :
      (↑standardD0Orientation).range = ⊤

      The image of the standard orientation is ℤ₂ˣ: TauCeti.standardD0Orientation_surjective as an equation of subgroups, stated on the underlying monoid homomorphism.

      source
      theorem TauCeti.standardD0Orientation_unique (ψ : demushkinD0 →ₜ* ℤ_[2]ˣ) (hA : ψ d0A = -1) (hS : ψ d0S = 1) (hY : ψ d0Y = negThreeUnit⁻¹) :
      ψ = standardD0Orientation

      The standard orientation is the only continuous character of D₀ with values -1, 1, (-3)⁻¹ on A, S, Y, because the marked generators topologically generate D₀.